From 242f9854b727383788bc85b5fda5803e11f1bb1c Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 28 Jun 2017 23:36:53 -0700
Subject: [PATCH] Fix encoding bug and fix misconception of how memory
 management of Constraints works

---
 src/AST/element.c              | 11 -----------
 src/AST/element.h              |  1 -
 src/Backend/satencoder.c       |  6 +-----
 src/Backend/satencoder.h       |  9 ---------
 src/Encoders/elementencoding.c |  3 +--
 5 files changed, 2 insertions(+), 28 deletions(-)

diff --git a/src/AST/element.c b/src/AST/element.c
index 57f7b6a..f5cd301 100644
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -50,17 +50,6 @@ Set* getElementSet(Element* This){
 	return NULL;
 }
 
-uint getElemEncodingInUseVarsSize(ElementEncoding* This){
-	uint size=0;
-	for(uint i=0; i<This->encArraySize; i++){
-		if(isinUseElement(This, i)){
-			size++;
-		}
-	}
-	return size;
-}
-
-
 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
 	ASTNodeType type = GETELEMENTTYPE(This);
 	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
diff --git a/src/AST/element.h b/src/AST/element.h
index 8fab12c..7e4db28 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -51,6 +51,5 @@ static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func
 	return &func->functionencoding;
 }
 
-uint getElemEncodingInUseVarsSize(ElementEncoding* This);
 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 #endif
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 6b3b0d5..94d19c8 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -13,8 +13,6 @@
 
 SATEncoder * allocSATEncoder() {
 	SATEncoder *This=ourmalloc(sizeof (SATEncoder));
-	allocInlineDefVectorConstraint(getSATEncoderAllConstraints(This));
-	allocInlineDefVectorConstraint(getSATEncoderVars(This));
 	This->varcount=1;
 	return This;
 }
@@ -80,7 +78,6 @@ Constraint * getNewVarSATEncoder(SATEncoder *This) {
 	Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
 	setNegConstraint(var, varneg);
 	setNegConstraint(varneg, var);
-	pushVectorConstraint(getSATEncoderVars(This), var);
 	return var;
 }
 
@@ -184,6 +181,5 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
 		constraints[i]=row;
 	}
 	Constraint* result = allocArrayConstraint(OR, size, constraints);
-	pushVectorConstraint( getSATEncoderAllConstraints(encoder), result);
 	return result;
-}
\ No newline at end of file
+}
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 937db2b..b711457 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -6,17 +6,8 @@
 
 struct SATEncoder {
 	uint varcount;
-	//regarding managing memory 
-	VectorConstraint vars;
-	VectorConstraint allConstraints;
 };
 
-static inline VectorConstraint* getSATEncoderVars(SATEncoder* ne){
-	return &ne->vars;
-}
-static inline VectorConstraint* getSATEncoderAllConstraints(SATEncoder* ne){
-	return &ne->allConstraints;
-}
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void initializeConstraintVars(CSolver* csolver, SATEncoder* This);
diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index f0510d6..08eb2e8 100644
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -43,8 +43,7 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
 
 void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){
 	ASSERT(This->type==BINARYINDEX);
-	uint size = getElemEncodingInUseVarsSize(This);
-	allocElementConstraintVariables(This, NUMBITS(size-1));
+	allocElementConstraintVariables(This, NUMBITS(This->encArraySize-1));
 	getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables);
 }
 
-- 
2.34.1