src/Test/tablepredicencodetest.c

   1 #include "csolver.h"
   2 /**
   3  * e1 = {1, 2}
   4  * e2={1, 3, 5, 7}
   5  * e3 = {6, 10, 19}
   6  * e4= p(e1, e2, e3)
   7  *      1 5 6 => T
   8  *      2 3 19 => T
   9  *      1 3 19 => F
  10  *      2 7 10 => F
  11  *      1 7 6 => F
  12  *      2 5 6 => T
  13  * e1 == e2
  14  * e3 >= e2
  15  * Result: e1=1, e2=1, e3=6 OR 10 OR 19, overflow=1
  16  */
  17 int main(int numargs, char **argv) {
  18         CSolver *solver = allocCSolver();
  19         uint64_t set1[] = {1, 2};
  20         uint64_t set2[] = {1, 3, 5, 7};
  21         uint64_t set3[] = {6, 10, 19};
  22         Set *s1 = createSet(solver, 0, set1, 2);
  23         Set *s2 = createSet(solver, 0, set2, 4);
  24         Set *s3 = createSet(solver, 0, set3, 3);
  25         Element *e1 = getElementVar(solver, s1);
  26         Element *e2 = getElementVar(solver, s2);
  27         Element *e3 = getElementVar(solver, s3);
  28         Set *d2[] = {s1, s2, s3};
  29         //change the overflow flag
  30         Table *t1 = createTableForPredicate(solver, d2, 3);
  31         uint64_t row1[] = {1, 5, 6};
  32         uint64_t row2[] = {2, 3, 19};
  33         uint64_t row3[] = {1, 3, 19};
  34         uint64_t row4[] = {2, 7, 10};
  35         uint64_t row5[] = {1, 7, 6};
  36         uint64_t row6[] = {2, 5, 6};
  37         addTableEntry(solver, t1, row1, 3, true);
  38         addTableEntry(solver, t1, row2, 3, true);
  39         addTableEntry(solver, t1, row3, 3, false);
  40         addTableEntry(solver, t1, row4, 3, false);
  41         addTableEntry(solver, t1, row5, 3, false);
  42         addTableEntry(solver, t1, row6, 3, true);
  43         Predicate *p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED);
  44         Boolean *undef = getBooleanVar(solver, 2);
  45         Boolean *b1 = applyPredicateTable(solver, p1, (Element * []) {e1, e2, e3}, 3, undef);
  46         addConstraint(solver, b1);
  47
  48         Set *deq[] = {s3,s2};
  49         Predicate *gte = createPredicateOperator(solver, GTE, deq, 2);
  50         Element *inputs2 [] = {e3, e2};
  51         Boolean *pred = applyPredicate(solver, gte, inputs2, 2);
  52         addConstraint(solver, pred);
  53
  54         Set *d1[] = {s1, s2};
  55         Predicate *eq = createPredicateOperator(solver, EQUALS, d1, 2);
  56         Boolean *pred2 = applyPredicate(solver, eq,(Element *[]) {e1, e2}, 2);
  57         addConstraint(solver, pred2);
  58
  59         if (startEncoding(solver) == 1)
  60                 printf("e1=%llu e2=%llu e3=%llu undefFlag:%d\n",
  61                                          getElementValue(solver,e1), getElementValue(solver, e2),
  62                                          getElementValue(solver, e3), getBooleanValue(solver, undef));
  63         else
  64                 printf("UNSAT\n");
  65         deleteSolver(solver);
  66 }