Check in bug fix

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 6d43ce1b2a8f25a10c4aa2f3ad77d2edf0c81862..d28d43d64d52efd5e835769413e143a721a04293 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -40,7 +40,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
        }
        Edge result=constraintOR(This->cnf, size, constraints);
 
-       return generateNegation ? result: constraintNegate(result);
+       return generateNegation ? constraintNegate(result) : result;
 }
 
 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
@@ -117,7 +117,8 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
                                Element * elem = getArrayElement(&constraint->inputs, i);
                                carray[i] = getElementValueConstraint(This, elem, vals[i]);
                        }
-                       pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray));
+                       Edge term=constraintAND(This->cnf, numDomains, carray);
+                       pushVectorEdge(clauses, term);
                }
                
                notfinished=false;
@@ -138,7 +139,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 
        Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        deleteVectorEdge(clauses);
-       return generateNegation ? cor : constraintNegate(cor);
+       return generateNegation ? constraintNegate(cor) : cor;
 }
 
 

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index c4440a7aade9bf54036b1c1dd8392e6cf687f45b..e47c7806112dd7e10512c4e47cc9795e08e25105 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -11,10 +11,7 @@ int main(int numargs, char ** argv) {
        Element * inputs[]={e1, e2};
        Boolean * b=applyPredicate(solver, equals, inputs, 2);
        addConstraint(solver, b);
-       Order * o=createOrder(solver, TOTAL, s);
-       Boolean * oc=orderConstraint(solver, o, 1, 2);
-       addConstraint(solver, oc);
-               
+
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
        Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
@@ -25,7 +22,7 @@ int main(int numargs, char ** argv) {
        uint64_t row3[] = {2, 1};
        uint64_t row4[] = {1, 2};
        addTableEntry(solver, table, row1, 2, 0);
-       addTableEntry(solver, table, row2, 2, 1);
+       addTableEntry(solver, table, row2, 2, 0);
        addTableEntry(solver, table, row3, 2, 2);
        addTableEntry(solver, table, row4, 2, 2);
        Function * f2 = completeTable(solver, table); //its range would be as same as s
@@ -39,6 +36,7 @@ int main(int numargs, char ** argv) {
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addConstraint(solver, pred);
        
-       startEncoding(solver);
+       if (startEncoding(solver)==1)
+               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
        deleteSolver(solver);
 }

diff --git a/src/csolver.c b/src/csolver.c
index f9f1e1bd534e662975a9f1eae625a74a88228ace..3d062e4733af1df10eb3285848d7b34da39926ef 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,7 +174,7 @@ Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t
        return constraint;
 }
 
-void startEncoding(CSolver* This){
+int startEncoding(CSolver* This){
        naiveEncodingDecision(This);
        SATEncoder* satEncoder = This->satEncoder;
        encodeAllSATEncoder(This, satEncoder);
@@ -184,6 +184,7 @@ void startEncoding(CSolver* This){
                model_print("%d, ", satEncoder->cnf->solver->solution[i]);
        }
        model_print("\n");
+       return result;
 }
 
 uint64_t getElementValue(CSolver* This, Element* element){

diff --git a/src/csolver.h b/src/csolver.h
index 9628f11b2e8d17c059acbf239d006c12c3b2f500..1adb67932e71d60b8986a21b08b806a6dda21e8d 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -114,7 +114,7 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
 
 /** When everything is done, the client calls this function and then csolver starts to encode*/
-void startEncoding(CSolver*);
+int startEncoding(CSolver*);
 
 /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
 uint64_t getElementValue(CSolver*, Element* element);