Add backtracking to the evaluator. This means we have to keep track of choicepoints which is implemented the easy but wasteful way for now.

I have also added a number which is used to differentiate variables from different application of the clauses.

1 files changed, 8 insertions, 2 deletions

diff --git a/misc.c b/misc.c
index 28ba45c..c047159 100644
--- a/misc.c
+++ b/misc.c
@@ -5,16 +5,21 @@
 #include "fns.h"
 
 Term *
-copyterm(Term *orig)
+copyterm(Term *orig, uvlong *clausenr)
 {
 	Term *new = malloc(sizeof(Term));
 	memcpy(new, orig, sizeof(Term));
 	new->next = nil;
 	new->children = nil;
 
+	if(clausenr)
+		new->clausenr = *clausenr;
+	else
+		new->clausenr = orig->clausenr;
+
 	Term *child;
 	for(child = orig->children; child != nil; child = child->next)
-		new->children = appendterm(new->children, copyterm(child));
+		new->children = appendterm(new->children, copyterm(child, clausenr));
 	return new;
 }
 
@@ -46,6 +51,7 @@ mkterm(int tag)
 	t->next = nil;
 	t->children = nil;
 	t->text = nil;
+	t->clausenr = 0;
 	return t;
 }