src/Test/funcencodingtest.cc

   1 #include "csolver.h"
   2 /**
   3  * e1 = {6}
   4  * e2={4, 2}
   5  * e3=Fsub(e1,e2) {4, 2}
   6  * e4= f(e1, e2)
   7  *      6 2 => 3
   8  *      6 4 => 1
   9  * e5 = f(e1)=>e1 {6}
  10  * e6 = (e3, e4, e5) {2, 3, 1}
  11  *      4 3 6 => 3
  12  *      2 1 6 => 1
  13  *      2 3 6 => 2
  14  *      4 1 6 => 1
  15  * e7 = {2, 1, 0}
  16  * e7 > e6
  17  * Result: e1=6, e2=4, e7=2
  18  */
  19 int main(int numargs, char **argv) {
  20         CSolver *solver = new CSolver();
  21         uint64_t set1[] = {6};
  22         uint64_t set2[] = {4, 2};
  23         uint64_t set3[] = {3, 1};
  24         uint64_t set4[] = {2, 3, 1};
  25         uint64_t set5[] = {2, 1, 0};
  26         Set *s1 = solver->createSet(0, set1, 1);
  27         Set *s2 = solver->createSet(0, set2, 2);
  28         Set *s3 = solver->createSet(0, set3, 2);
  29         Set *s4 = solver->createSet(0, set4, 3);
  30         Set *s5 = solver->createSet(0, set5, 3);
  31         Element *e1 = solver->getElementVar(s1);
  32         Element *e2 = solver->getElementVar(s2);
  33         Element *e7 = solver->getElementVar(s5);
  34         BooleanEdge overflow = solver->getBooleanVar(2);
  35         //change the overflow flag
  36         Function *f1 = solver->createFunctionOperator(SATC_SUB, s2, SATC_IGNORE);
  37         Element *in1[] = {e1, e2};
  38         Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
  39         Table *t1 = solver->createTable(s3);
  40         uint64_t row1[] = {6, 2};
  41         uint64_t row2[] = {6, 4};
  42         solver->addTableEntry(t1, row1, 2, 3);
  43         solver->addTableEntry(t1, row2, 2, 1);
  44         Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR);
  45         Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
  46
  47         Element *in2[] = {e1};
  48         Table *t2 = solver->createTable(s1);
  49         uint64_t row3[] = {6};
  50         solver->addTableEntry(t2, row3, 1, 6);
  51         Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR);
  52         Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
  53
  54         Element *in3[] = {e3, e4, e5};
  55         Table *t3 = solver->createTable(s4);
  56         uint64_t row4[] = {4, 3, 6};
  57         uint64_t row5[] = {2, 1, 6};
  58         uint64_t row6[] = {2, 3, 6};
  59         uint64_t row7[] = {4, 1, 6};
  60         solver->addTableEntry(t3, row4, 3, 3);
  61         solver->addTableEntry(t3, row5, 3, 1);
  62         solver->addTableEntry(t3, row6, 3, 2);
  63         solver->addTableEntry(t3, row7, 3, 1);
  64         Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR);
  65         Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
  66
  67         Predicate *gt = solver->createPredicateOperator(SATC_GT);
  68         Element *inputs2 [] = {e7, e6};
  69         BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
  70         solver->addConstraint(pred);
  71         solver->serialize();
  72
  73         if (solver->solve() == 1)
  74                 printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
  75                                          solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));
  76         else
  77                 printf("UNSAT\n");
  78         delete solver;
  79 }