summaryrefslogtreecommitdiff
path: root/misc.c
diff options
context:
space:
mode:
Diffstat (limited to 'misc.c')
-rw-r--r--misc.c24
1 files changed, 13 insertions, 11 deletions
diff --git a/misc.c b/misc.c
index bf7010f..91396bd 100644
--- a/misc.c
+++ b/misc.c
@@ -8,22 +8,17 @@
static uvlong varnr = 0;
Term *
-copyterm(Term *orig, uvlong *clausenr)
+copyterm(Term *orig)
{
Term *new = gmalloc(sizeof(Term));
memcpy(new, orig, sizeof(Term));
new->next = nil;
new->children = nil;
- if(clausenr)
- new->clausenr = *clausenr;
- else
- new->clausenr = orig->clausenr;
-
if(orig->tag == CompoundTerm){
Term *child;
for(child = orig->children; child != nil; child = child->next)
- new->children = appendterm(new->children, copyterm(child, clausenr));
+ new->children = appendterm(new->children, copyterm(child));
}
return new;
}
@@ -68,6 +63,14 @@ addvarnr(Term *t, uvlong offset)
}
void
+renametermvars(Term *t)
+{
+ uvlong minvar = smallestvar(t);
+ uvlong offset = varnr - minvar;
+ addvarnr(t, offset);
+}
+
+void
renameclausevars(Clause *c)
{
uvlong minhead = smallestvar(c->head);
@@ -108,7 +111,6 @@ mkterm(int tag)
t->next = nil;
t->children = nil;
t->text = nil;
- t->clausenr = 0;
t->inparens = 0;
t->varnr = 0;
return t;
@@ -191,7 +193,7 @@ mklist(Term *elems)
if(elems == nil)
return mkatom(L"[]");
else{
- Term *t = copyterm(elems, nil);
+ Term *t = copyterm(elems);
t->next = mklist(elems->next);
return mkcompound(L".", 2, t);
}
@@ -201,9 +203,9 @@ Clause *
copyclause(Clause *orig, uvlong *clausenr)
{
Clause *new = gmalloc(sizeof(Clause));
- new->head = copyterm(orig->head, clausenr);
+ new->head = copyterm(orig->head);
if(orig->body)
- new->body = copyterm(orig->body, clausenr);
+ new->body = copyterm(orig->body);
else
new->body = nil;
if(clausenr)