src/Test/funcencodingtest.c

   1 #include "csolver.h"
   2
   3 int main(int numargs, char ** argv) {
   4         CSolver * solver=allocCSolver();
   5         uint64_t set1[]={6};
   6         uint64_t set2[]={4, 2};
   7         uint64_t set3[]={3, 1};
   8         uint64_t set4[]={2, 3, 1};
   9         uint64_t set5[]={2, 1, 0};
  10         Set * s1=createSet(solver, 0, set1, 1);
  11         Set * s2=createSet(solver, 0, set2, 2);
  12         Set * s3=createSet(solver, 0, set3, 2);
  13         Set * s4=createSet(solver, 0, set4, 3);
  14         Set * s5=createSet(solver, 0, set5, 3);
  15         Element * e1=getElementVar(solver, s1);
  16         Element * e2=getElementVar(solver, s2);
  17         Element * e7=getElementVar(solver, s5);
  18         Boolean* overflow = getBooleanVar(solver , 2);
  19         Set * d1[]={s1, s2};
  20         //change the overflow flag
  21         Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
  22         Element * in1[]={e1, e2};
  23         Element * e3 = applyFunction(solver, f1, in1, 2, overflow);
  24         Table* t1 = createTable(solver, d1, 2, s3);
  25         uint64_t row1[] = {6, 2};
  26         uint64_t row2[] = {6, 4};
  27         addTableEntry(solver, t1, row1, 2, 3);
  28         addTableEntry(solver, t1, row2, 2, 1);
  29         Function * f2 = completeTable(solver, t1, IGNOREBEHAVIOR);
  30         Element * e4 = applyFunction(solver, f2, in1, 2, overflow);
  31
  32         Set *d2[] = {s1};
  33         Element *in2[]={e1};
  34         Table* t2 = createTable(solver, d2, 1, s1);
  35         uint64_t row3[] = {6};
  36         addTableEntry(solver, t2, row3, 1, 6);
  37         Function * f3 = completeTable(solver, t2, IGNOREBEHAVIOR);
  38         Element * e5 = applyFunction(solver, f3, in2, 1, overflow);
  39
  40         Set *d3[] = {s2, s3, s1};
  41         Element *in3[]={e3, e4, e5};
  42         Table* t3 = createTable(solver, d3, 3, s4);
  43         uint64_t row4[] = {4, 3, 6};
  44         uint64_t row5[] = {2, 1, 6};
  45         uint64_t row6[] = {2, 3, 6};
  46         uint64_t row7[] = {4, 1, 6};
  47         addTableEntry(solver, t3, row4, 3, 3);
  48         addTableEntry(solver, t3, row5, 3, 1);
  49         addTableEntry(solver, t3, row6, 3, 2);
  50         addTableEntry(solver, t3, row7, 3, 1);
  51         Function * f4 = completeTable(solver, t3, IGNOREBEHAVIOR);
  52         Element * e6 = applyFunction(solver, f4, in3, 3, overflow);
  53
  54         Set* deq[] = {s5,s4};
  55         Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
  56         Element* inputs2 [] = {e7, e6};
  57         Boolean* pred = applyPredicate(solver, gt, inputs2, 2, overflow);
  58         addConstraint(solver, pred);
  59
  60         if (startEncoding(solver)==1)
  61                 printf("e1=%llu e2=%llu e7=%llu\n",
  62                          getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));
  63         else
  64                 printf("UNSAT\n");
  65         deleteSolver(solver);
  66 }