src/Test/logicopstest.c

   1 #include "csolver.h"
   2
   3 /**
   4  * b1 AND b2=>b3
   5  * !b3 OR b4
   6  * b1 XOR b4
   7  * @param numargs
   8  * @param argv
   9  * @return
  10  */
  11 int main(int numargs, char** argv){
  12         CSolver * solver=allocCSolver();
  13         Boolean *b1= getBooleanVar(solver, 0);
  14         Boolean *b2= getBooleanVar(solver, 0);
  15         Boolean *b3= getBooleanVar(solver, 0);
  16         Boolean *b4= getBooleanVar(solver, 0);
  17         //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
  18         Boolean *andb1b2= applyLogicalOperation(solver, L_AND,(Boolean*[]) {b1, b2}, 2);
  19         Boolean * imply = applyLogicalOperation(solver, L_IMPLIES, (Boolean*[]) {andb1b2, b3}, 2);
  20         addConstraint(solver, imply);
  21         Boolean* notb3 = applyLogicalOperation(solver, L_NOT, (Boolean*[]) {b3}, 1);
  22         addConstraint(solver, applyLogicalOperation(solver, L_OR, (Boolean*[]){notb3, b4} , 2));
  23         addConstraint(solver, applyLogicalOperation(solver, L_XOR, (Boolean* []) {b1, b4}, 2));
  24         if (startEncoding(solver)==1)
  25                 printf("b1=%d b2=%d b3=%d b4=%d\n",
  26                         getBooleanValue(solver,b1), getBooleanValue(solver, b2),
  27                         getBooleanValue(solver, b3), getBooleanValue(solver, b4));
  28         else
  29                 printf("UNSAT\n");
  30         deleteSolver(solver);
  31 }