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 }