Don't use strings to identify vars, use numbers

1 files changed, 62 insertions, 5 deletions

diff --git a/misc.c b/misc.c
index f25c583..bf7010f 100644
--- a/misc.c
+++ b/misc.c
@@ -5,6 +5,8 @@
 #include "dat.h"
 #include "fns.h"
 
+static uvlong varnr = 0;
+
 Term *
 copyterm(Term *orig, uvlong *clausenr)
 {
@@ -18,17 +20,71 @@ copyterm(Term *orig, uvlong *clausenr)
 	else
 		new->clausenr = orig->clausenr;
 
-	Term *child;
-	for(child = orig->children; child != nil; child = child->next)
-		new->children = appendterm(new->children, copyterm(child, clausenr));
+	if(orig->tag == CompoundTerm){
+		Term *child;
+		for(child = orig->children; child != nil; child = child->next)
+			new->children = appendterm(new->children, copyterm(child, clausenr));
+	}
 	return new;
 }
 
+uvlong
+smallestvar(Term *t)
+{
+	if(t == nil)
+		return varnr;
+
+	if(t->tag == VariableTerm)
+		return t->varnr;
+	if(t->tag == CompoundTerm){
+		Term *child;
+		uvlong min = varnr;
+		for(child = t->children; child != nil; child = child->next){
+			uvlong v = smallestvar(child);
+			if(v < min)
+				min = v;
+		}
+		return min;
+	}else
+		return varnr;
+}
+
+void
+addvarnr(Term *t, uvlong offset)
+{
+	if(t == nil)
+		return;
+
+	if(t->tag == VariableTerm){
+		t->varnr += offset;
+		if(t->varnr >= varnr)
+			varnr = t->varnr+1;
+	}
+	if(t->tag == CompoundTerm){
+		Term *child;
+		for(child = t->children; child != nil; child = child->next)
+			addvarnr(child, offset);
+	}
+}
+
+void
+renameclausevars(Clause *c)
+{
+	uvlong minhead = smallestvar(c->head);
+	uvlong minbody = smallestvar(c->body);
+	uvlong minvar = minhead < minbody ? minhead : minbody;
+	uvlong offset = varnr - minvar;
+	addvarnr(c->head, offset);
+	addvarnr(c->body, offset);
+}
+
 Term *
 appendterm(Term *a, Term *b)
 {
 	if(a == nil)
 		return b;
+	if(b == nil)
+		return a;
 
 	Term *tmp;
 	for(tmp = a; tmp->next != nil; tmp = tmp->next);
@@ -54,6 +110,7 @@ mkterm(int tag)
 	t->text = nil;
 	t->clausenr = 0;
 	t->inparens = 0;
+	t->varnr = 0;
 	return t;
 }
 
@@ -66,10 +123,10 @@ mkatom(Rune *name)
 }
 
 Term *
-mkvariable(Rune *name)
+mkvariable(void)
 {
 	Term *t = mkterm(VariableTerm);
-	t->text = name;
+	t->varnr = varnr++;
 	return t;
 }