Encoding Bug Fix

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index e8ef1db7d8278ed20eb31ace02721ba4f4ad2166..4859a936cf5633ac7f1c799d0edc09e4dda324ac 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -711,8 +711,22 @@ void printCNF(Edge e) {
                return;
        }
        Node *n=getNodePtrFromEdge(e);
-       if (isNeg)
+       if (isNeg) {
+               //Pretty print things that are equivalent to OR's
+               if (getNodeType(e)==NodeType_AND) {
+                       printf("or(");
+                       for(uint i=0;i<n->numEdges;i++) {
+                               Edge e=n->edges[i];
+                               if (i!=0)
+                                       printf(" ");
+                               printCNF(constraintNegate(e));
+                       }
+                       printf(")");
+                       return;
+               }
+
                printf("!");
+       }
        switch(getNodeType(e)) {
        case NodeType_AND:
                printf("and");

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index af7c8b3401f8809926d81d20c9623f90c0a927f0..4e1ba3ef36be39ea2ebe4e5f69255c89e282c22f 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -171,7 +171,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
        
        bool notfinished=true;
        while(notfinished) {
-               Edge carray[numDomains+2];
+               Edge carray[numDomains+1];
 
                uint64_t result=applyFunctionOperator(function, numDomains, vals);
                bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
@@ -195,30 +195,26 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
                        case IGNORE:
                        case NOOVERFLOW:
                        case WRAPAROUND: {
-                               clause=constraintAND(This->cnf, numDomains+1, carray);
+                               clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
                                break;
                        }
                        case FLAGFORCESOVERFLOW: {
-                               carray[numDomains+1]=constraintNegate(overFlowConstraint);
-                               clause=constraintAND(This->cnf, numDomains+2, carray);
+                               clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                break;
                        }
                        case OVERFLOWSETSFLAG: {
                                if (isInRange) {
-                                       clause=constraintAND(This->cnf, numDomains+1, carray);
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
                                } else {
-                                       carray[numDomains+1]=overFlowConstraint;
-                                       clause=constraintAND(This->cnf, numDomains+1, carray);
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
                        case FLAGIFFOVERFLOW: {
                                if (isInRange) {
-                               carray[numDomains+1]=constraintNegate(overFlowConstraint);
-                                       clause=constraintAND(This->cnf, numDomains+2, carray);
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                } else {
-                                       carray[numDomains+1]=overFlowConstraint;
-                                       clause=constraintAND(This->cnf, numDomains+1, carray);
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
@@ -244,7 +240,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
                }
        }
 
-       Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        addConstraintCNF(This->cnf, cor);
        deleteVectorEdge(clauses);
 }
@@ -271,5 +267,5 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* fu
                Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
                constraints[i]=row;
        }
-       addConstraintCNF(This->cnf, constraintOR(This->cnf, size, constraints));
+       addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 }

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index e47c7806112dd7e10512c4e47cc9795e08e25105..f30ebd025371ad0aba37c0fe212eee407c3f71e2 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -3,7 +3,10 @@
 int main(int numargs, char ** argv) {
        CSolver * solver=allocCSolver();
        uint64_t set1[]={0, 1, 2};
+       uint64_t setbigarray[]={0, 1, 2, 3, 4};
+       
        Set * s=createSet(solver, 0, set1, 3);
+       Set * setbig=createSet(solver, 0, setbigarray, 5);
        Element * e1=getElementVar(solver, s);
        Element * e2=getElementVar(solver, s);
        Set * domain[]={s, s};
@@ -14,13 +17,13 @@ int main(int numargs, char ** argv) {
 
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
-       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
+       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE);
        
        Table* table = createTable(solver, domain, 2, s);
        uint64_t row1[] = {0, 1};
        uint64_t row2[] = {1, 1};
        uint64_t row3[] = {2, 1};
-       uint64_t row4[] = {1, 2};
+       uint64_t row4[] = {2, 2};
        addTableEntry(solver, table, row1, 2, 0);
        addTableEntry(solver, table, row2, 2, 0);
        addTableEntry(solver, table, row3, 2, 2);