src/Test/logicopstest.c

   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 = allocCSolver();
  11         Boolean *b1 = getBooleanVar(solver, 0);
  12         Boolean *b2 = getBooleanVar(solver, 0);
  13         Boolean *b3 = getBooleanVar(solver, 0);
  14         Boolean *b4 = getBooleanVar(solver, 0);
  15         //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
  16         Boolean *andb1b2 = applyLogicalOperation(solver, L_AND,(Boolean *[]) {b1, b2}, 2);
  17         Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, (Boolean *[]) {andb1b2, b3}, 2);
  18         addConstraint(solver, imply);
  19         Boolean *notb3 = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {b3}, 1);
  20         addConstraint(solver, applyLogicalOperation(solver, L_OR, (Boolean *[]) {notb3, b4}, 2));
  21         addConstraint(solver, applyLogicalOperation(solver, L_XOR, (Boolean * []) {b1, b4}, 2));
  22         if (startEncoding(solver) == 1)
  23                 printf("b1=%d b2=%d b3=%d b4=%d\n",
  24                                          getBooleanValue(solver,b1), getBooleanValue(solver, b2),
  25                                          getBooleanValue(solver, b3), getBooleanValue(solver, b4));
  26         else
  27                 printf("UNSAT\n");
  28         deleteSolver(solver);
  29 }