Incremental solver works and the test case passes

[satune.git] / src / Backend / satelemencoder.cc

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3f26b5c3a31700b4b3e36c24d38e8055b86c037b..aa739242d002acb28330e6112a6f702ec7548b41 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -220,6 +220,15 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
+void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
+       ASSERT(encoding->element->frozen);
+       for(uint i=0; i< encoding->numVars; i++){
+               Edge e = encoding->variables[i];
+               ASSERT(edgeIsVarConst(e));
+               freezeVariable(cnf, e);
+       }
+}
+
 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));