src/Test/tablefuncencodetest.cc

   1 #include "csolver.h"
   2 /**
   3  * e1 = {1, 2}
   4  * e2={3, 5, 7}
   5  * e3= f(e1, e2)
   6  *      1 5 => 7
   7  *      2 3 => 5
   8  *      1 7 => 3
   9  *      2 7 => 5
  10  *      2 5 => 3
  11  *      1 3 => 5
  12  * e4 = {6, 10, 19}
  13  * e4 <= e3
  14  * Result: e1=1, e2=5, e3=7, e4=6, overflow=0
  15  */
  16 int main(int numargs, char **argv) {
  17         CSolver *solver = new CSolver();
  18         uint64_t set1[] = {1, 2};
  19         uint64_t set2[] = {3, 5, 7};
  20         uint64_t set3[] = {6, 10, 19};
  21         Set *s1 = solver->createSet(0, set1, 2);
  22         Set *s2 = solver->createSet(0, set2, 3);
  23         Set *s3 = solver->createSet(0, set3, 3);
  24         Element *e1 = solver->getElementVar(s1);
  25         Element *e2 = solver->getElementVar(s2);
  26         Element *e4 = solver->getElementVar(s3);
  27         BooleanEdge overflow = solver->getBooleanVar(2);
  28         Set *d1[] = {s1, s2};
  29         //change the overflow flag
  30         Table *t1 = solver->createTable(d1, 2, s2);
  31         uint64_t row1[] = {1, 5};
  32         uint64_t row2[] = {2, 3};
  33         uint64_t row3[] = {1, 7};
  34         uint64_t row4[] = {2, 7};
  35         uint64_t row5[] = {2, 5};
  36         uint64_t row6[] = {1, 3};
  37         solver->addTableEntry(t1, row1, 2, 7);
  38         solver->addTableEntry(t1, row2, 2, 5);
  39         solver->addTableEntry(t1, row3, 2, 3);
  40         solver->addTableEntry(t1, row4, 2, 5);
  41         solver->addTableEntry(t1, row5, 2, 3);
  42         solver->addTableEntry(t1, row6, 2, 5);
  43         Function *f1 = solver->completeTable(t1, SATC_FLAGIFFUNDEFINED);
  44         Element *tmparray[] = {e1, e2};
  45         Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
  46
  47         Set *deq[] = {s3,s2};
  48         Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2);
  49         Element *inputs2 [] = {e4, e3};
  50         BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2);
  51         solver->addConstraint(pred);
  52         solver->serialize();
  53
  54         if (solver->solve() == 1)
  55                 printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n",
  56                                          solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3),
  57                                          solver->getElementValue(e4), solver->getBooleanValue(overflow));
  58         else
  59                 printf("UNSAT\n");
  60         delete solver;
  61 }