edit

diff --git a/.gitignore b/.gitignore
index 2d1b9f1b8d7cd96e8299ce2f07102a6b4914e384..bbff0e1594c76c80d5a8b17306af2f00528772bb 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -9,3 +9,6 @@ src/lib_cons_comp.so
 /src/mymemory.cc
 .*
 *.dSYM
+
+#Ignoring Benchmarks
+src/Benchmarks/

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 79b13033ebdc40f4ffd82963ac83885d936f3cdc..1fea1a58f41ebf23391bba824a6744bc84662ae8 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -190,8 +190,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                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);
 }
 

diff --git a/src/Test/buildsimple.cc b/src/Test/buildsimple.cc
new file mode 100644 (file)
index 0000000..f7ab9d3
--- /dev/null
+++ b/src/Test/buildsimple.cc
@@ -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;
+}

diff --git a/src/pycsolver.py b/src/pycsolver.py
index d78836e023e1e6188880d6187ee198d0ec978d09..3dd296b7c6c6ba0cb77a221c2026af2c8ef65fcf 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -15,6 +15,19 @@ class CompOp:
        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