src/Test/tablefuncencodetest.c

   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  * e4 = {6, 10, 19}
   9  * e4 <= e3
  10  * Result: e1=1, e2=5, e4=6, overflow=0
  11  */
  12 int main(int numargs, char ** argv) {
  13         CSolver * solver=allocCSolver();
  14         uint64_t set1[]={1, 2};
  15         uint64_t set2[]={3, 5, 7};
  16         uint64_t set3[]={6, 10, 19};
  17         Set * s1=createSet(solver, 0, set1, 2);
  18         Set * s2=createSet(solver, 0, set2, 3);
  19         Set * s3=createSet(solver, 0, set3, 3);
  20         Element * e1=getElementVar(solver, s1);
  21         Element * e2=getElementVar(solver, s2);
  22         Element * e4=getElementVar(solver, s3);
  23         Boolean* overflow = getBooleanVar(solver , 2);
  24         Set * d1[]={s1, s2};
  25         //change the overflow flag
  26         Table* t1 = createTable(solver, d1, 2, s2);
  27         uint64_t row1[] = {1, 5};
  28         uint64_t row2[] = {2, 3};
  29         addTableEntry(solver, t1, row1, 2, 7);
  30         addTableEntry(solver, t1, row2, 2, 5);
  31         Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);
  32         Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow);
  33
  34         Set* deq[] = {s3,s2};
  35         Predicate* lte = createPredicateOperator(solver, LTE, deq, 2);
  36         Element* inputs2 [] = {e4, e3};
  37         Boolean* pred = applyPredicate(solver, lte, inputs2, 2);
  38         addConstraint(solver, pred);
  39
  40         if (startEncoding(solver)==1)
  41                 printf("e1=%llu e2=%llu e4=%llu overFlow:%d\n",
  42                         getElementValue(solver,e1), getElementValue(solver, e2),
  43                         getElementValue(solver, e4), getBooleanValue(solver, overflow));
  44         else
  45                 printf("UNSAT\n");
  46         deleteSolver(solver);
  47 }