Fix encoding bug and fix misconception of how memory management of Constraints works

diff --git a/src/AST/element.c b/src/AST/element.c
index 57f7b6a5b27abf9ec8cb661295451c272bad6663..f5cd301fd7df13fc493cd6ec34a12edcaaf6a392 100644 (file)
--- 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 8fab12cc9f573666fb94824df962748d3479836f..7e4db2880de743381ad9aab76925064f4d72af32 100644 (file)
--- 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 6b3b0d5e4f6c9f7ff7f462fbd137b5bd2aa68626..94d19c811e946c9fe69eabf2a585c29009c83eac 100644 (file)
--- 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 937db2bce7533d240a85d03a08a00e01aff65f3f..b711457687abca5dc0ac9738cb2ad5458bfdb543 100644 (file)
--- 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 f0510d6e50d39fc9eb0cddc297300003af6835f2..08eb2e8dd6200fa403a6b910616597232508e406 100644 (file)
--- 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);
 }