From d013ea099b3662cab5ea848429e8d725af25a178 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 19 Jun 2017 23:29:50 -0700
Subject: [PATCH] More SAT Encoder

---
 src/AST/boolean.c        |  1 +
 src/AST/boolean.h        |  1 +
 src/Backend/satencoder.c | 14 +++++++++++++-
 src/Backend/satencoder.h |  3 ++-
 4 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 7d9aec3..1a46ccd 100644
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -4,6 +4,7 @@ Boolean* allocBoolean(VarType t) {
 	BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
 	GETBOOLEANTYPE(tmp)=BOOLEANVAR;
 	tmp->vtype=t;
+	tmp->var=NULL;
 	return & tmp->base;
 }
 
diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index d00a82c..860365f 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -24,6 +24,7 @@ struct BooleanOrder {
 struct BooleanVar {
 	Boolean base;
 	VarType vtype;
+	Constraint * var;
 };
 
 struct BooleanLogic {
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 3b34c3a..2918771 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -6,6 +6,7 @@
 
 SATEncoder * allocSATEncoder() {
 	SATEncoder *This=ourmalloc(sizeof (SATEncoder));
+	This->varcount=1;
 	return This;
 }
 
@@ -39,8 +40,19 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
 	return NULL;
 }
 
+Constraint * getNewVarSATEncoder(SATEncoder *This) {
+	Constraint * var=allocVarConstraint(VAR, This->varcount);
+	Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
+	setNegConstraint(var, varneg);
+	setNegConstraint(varneg, var);
+	return var;
+}
+
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
-	return NULL;
+	if (constraint->var == NULL) {
+		constraint->var=getNewVarSATEncoder(This);
+	}
+	return constraint->var;
 }
 
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index a612930..5d8722c 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -4,13 +4,14 @@
 #include "classlist.h"
 
 struct SATEncoder {
-
+	uint varcount;
 };
 
 
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
+Constraint * getNewVarSATEncoder(SATEncoder *This);
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
-- 
2.34.1