src/Test/logicopstest.cc

   1 #include "csolver.h"
   2
   3 /**
   4  * b1 AND b2=>b3
   5  * !b3 OR b4
   6  * b1 XOR b4
   7  * Result: b1=1 b2=0 b3=0 b4=0
   8  */
   9 int main(int numargs, char **argv) {
  10         CSolver *solver = new CSolver();
  11         BooleanEdge b1 = solver->getBooleanVar(0);
  12         BooleanEdge b2 = solver->getBooleanVar(0);
  13         BooleanEdge b3 = solver->getBooleanVar(0);
  14         BooleanEdge b4 = solver->getBooleanVar(0);
  15         //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
  16         BooleanEdge barray1[] = {b1,b2};
  17         BooleanEdge andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
  18         BooleanEdge barray2[] = {andb1b2, b3};
  19         BooleanEdge imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);
  20         solver->addConstraint(imply);
  21         BooleanEdge barray3[] = {b3};
  22         BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
  23         BooleanEdge barray4[] = {notb3, b4};
  24         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
  25         BooleanEdge barray5[] = {b1, b4};
  26         solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
  27         if (solver->solve() == 1)
  28                 printf("b1=%d b2=%d b3=%d b4=%d\n",
  29                                          solver->getBooleanValue(b1), solver->getBooleanValue(b2),
  30                                          solver->getBooleanValue(b3), solver->getBooleanValue(b4));
  31         else
  32                 printf("UNSAT\n");
  33         delete solver;
  34 }