From c0c4f17e45f0e5b7881a9f041a4cd5e09f3276ba Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 18 Jul 2018 16:21:45 -0700 Subject: [PATCH] edit --- .gitignore | 3 +++ src/Backend/satfuncopencoder.cc | 4 +-- src/Test/buildsimple.cc | 47 +++++++++++++++++++++++++++++++++ src/pycsolver.py | 13 +++++++++ 4 files changed, 65 insertions(+), 2 deletions(-) create mode 100644 src/Test/buildsimple.cc diff --git a/.gitignore b/.gitignore index 2d1b9f1..bbff0e1 100644 --- 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 79b1303..1fea1a5 100644 --- 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 index 0000000..f7ab9d3 --- /dev/null +++ b/src/Test/buildsimple.cc @@ -0,0 +1,47 @@ +#include "csolver.h" +#include + +/** + * 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 d78836e..3dd296b 100644 --- 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 -- 2.34.1