edit
authorHamed Gorjiara <hgorjiar@uci.edu>
Wed, 18 Jul 2018 23:21:45 +0000 (16:21 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Wed, 18 Jul 2018 23:21:45 +0000 (16:21 -0700)
.gitignore
src/Backend/satfuncopencoder.cc
src/Test/buildsimple.cc [new file with mode: 0644]
src/pycsolver.py

index 2d1b9f1..bbff0e1 100644 (file)
@@ -9,3 +9,6 @@ src/lib_cons_comp.so
 /src/mymemory.cc
 .*
 *.dSYM
 /src/mymemory.cc
 .*
 *.dSYM
+
+#Ignoring Benchmarks
+src/Benchmarks/
index 79b1303..1fea1a5 100644 (file)
@@ -190,8 +190,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                deleteVectorEdge(clauses);
                return;
        }
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(cnf, cor);
+       Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(cnf, cand);
        deleteVectorEdge(clauses);
 }
 
        deleteVectorEdge(clauses);
 }
 
diff --git a/src/Test/buildsimple.cc b/src/Test/buildsimple.cc
new file mode 100644 (file)
index 0000000..f7ab9d3
--- /dev/null
@@ -0,0 +1,47 @@
+#include "csolver.h"
+#include <unistd.h>
+
+/**
+ * e1={0, 1, 2}
+ * e2={0, 1, 2}
+ * e1 == e2
+ * e3= e1+e2 {0, 1, 2, 3, 4}
+ * e4 = f(e1, e2)
+ *     0 1 => 0
+ *     1 1 => 0
+ *     2 1 => 2
+ *     2 2 => 2
+ * e3 == e4
+ * Result: UNSAT!
+ */
+int main(int numargs, char **argv) {
+       CSolver *solver = new CSolver();
+       uint64_t set1[] = {1, 2, 3};
+       Set *s1 = solver->createSet(1, set1, 3);
+       Set *s2 = solver->createSet(1, set1, 3);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
+       solver->mustHaveValue(e1);
+       solver->mustHaveValue(e2);
+       Set *domain[] = {s1, s2};
+       Element *inputs[] = {e1, e2};
+
+       uint64_t set2[] = {3};
+       Set *rangef1 = solver->createSet(1, set2, 1);
+       Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, rangef1, SATC_FLAGIFFOVERFLOW);
+
+       BooleanEdge overflow = solver->getBooleanVar(2);
+       Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
+       Element *e4 = solver->getElementConst(5, 3);
+       Set *domain2[] = {rangef1,rangef1};
+       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
+       Element *inputs2 [] = {e4, e3};
+       BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
+       solver->addConstraint(pred);
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, overflow));
+       if (solver->solve() == 1)
+               printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
+       else
+               printf("UNSAT\n");
+       delete solver;
+}
index d78836e..3dd296b 100644 (file)
@@ -15,6 +15,19 @@ class CompOp:
        SATC_LTE=3
        SATC_GTE=4
 
        SATC_LTE=3
        SATC_GTE=4
 
+class ArithOp:
+    SATC_ADD=0
+    SATC_SUB=1
+
+class OverFlowBehavior:
+    SATC_IGNORE=0
+    SATC_WRAPAROUND=1
+    SATC_FLAGFORCESOVERFLOW=2
+    SATC_OVERFLOWSETSFLAG=3
+    SATC_FLAGIFFOVERFLOW=4
+    SATC_NOOVERFLOW=5
+
+
 def loadCSolver():
         csolverlb = cdll.LoadLibrary("lib_cons_comp.so")
         csolverlb.createCCSolver.restype = c_void_p
 def loadCSolver():
         csolverlb = cdll.LoadLibrary("lib_cons_comp.so")
         csolverlb.createCCSolver.restype = c_void_p