src/Test/bug1.cc

   1
   2 #include "csolver.h"
   3 /**
   4  * TotalOrder(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
   5  * 0=>1
   6  * 1=>2
   7  * 2=>3
   8  * 1=>4
   9  * 4=>5
  10  * 5=>6
  11  * 1=>7
  12  * 7=>8
  13  * 8=>9
  14  * 9=>2
  15  * 6=>2
  16  *
  17  *
  18  */
  19 int main(int numargs, char **argv) {
  20         CSolver *solver = new CSolver();
  21         uint64_t set1[] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
  22         Set *s = solver->createSet(0, set1, 10);
  23         Order *order = solver->createOrder(SATC_TOTAL, s);
  24         BooleanEdge b01 =  solver->orderConstraint(order, 0, 1);
  25         solver->addConstraint(b01);
  26         BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
  27         solver->addConstraint(b12);
  28         BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
  29         solver->addConstraint(b23);
  30         BooleanEdge b14 =  solver->orderConstraint(order, 1, 4);
  31         solver->addConstraint(b14);
  32         BooleanEdge b45 =  solver->orderConstraint(order, 4, 5);
  33         solver->addConstraint(b45);
  34         BooleanEdge b56 =  solver->orderConstraint(order, 5, 6);
  35         solver->addConstraint(b56);
  36         BooleanEdge b17 =  solver->orderConstraint(order, 1, 7);
  37         solver->addConstraint(b17);
  38         BooleanEdge b78 =  solver->orderConstraint(order, 7, 8);
  39         solver->addConstraint(b78);
  40         BooleanEdge b89 =  solver->orderConstraint(order, 8, 9);
  41         solver->addConstraint(b89);
  42         BooleanEdge b92 =  solver->orderConstraint(order, 9, 2);
  43         solver->addConstraint(b92);
  44         BooleanEdge b62 =  solver->orderConstraint(order, 6, 2);
  45         solver->addConstraint(b62);
  46
  47         BooleanEdge v1 = solver->getBooleanVar(0);
  48         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
  49         BooleanEdge v2 = solver->getBooleanVar(0);
  50         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
  51         BooleanEdge v3 = solver->getBooleanVar(0);
  52         BooleanEdge v4 = solver->getBooleanVar(0);
  53         BooleanEdge v5 = solver->getBooleanVar(0);
  54         BooleanEdge be = solver->applyLogicalOperation(SATC_IFF, v3, v4);
  55         BooleanEdge sor = solver->applyLogicalOperation(SATC_OR, be, v5);
  56         solver->addConstraint(sor);
  57         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
  58         BooleanEdge v6 = solver->getBooleanVar(0);
  59         BooleanEdge v7 = solver->getBooleanVar(0);
  60         BooleanEdge v8 = solver->getBooleanVar(0);
  61         solver->addConstraint(
  62                 solver->applyLogicalOperation(SATC_OR,
  63                                                                                                                                         solver->applyLogicalOperation(SATC_IFF, v7, v8),
  64                                                                                                                                         v6));
  65         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
  66         BooleanEdge v9 = solver->getBooleanVar(0);
  67         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
  68         BooleanEdge v10 = solver->getBooleanVar(0);
  69         BooleanEdge v11 = solver->getBooleanVar(0);
  70         BooleanEdge v12 = solver->getBooleanVar(0);
  71         solver->addConstraint(
  72                 solver->applyLogicalOperation(SATC_OR,
  73                                                                                                                                         solver->applyLogicalOperation(SATC_OR, v10, v11),
  74                                                                                                                                         solver->applyLogicalOperation(SATC_IFF, v1, v12)));
  75         BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
  76         BooleanEdge be1 = solver->applyLogicalOperation(SATC_OR, v10, v11);
  77         BooleanEdge be2 = solver->applyLogicalOperation(SATC_OR, be1, b48);
  78         solver->addConstraint(be2);
  79         BooleanEdge v13 = solver->getBooleanVar(0);
  80         BooleanEdge v14 = solver->getBooleanVar(0);
  81         solver->addConstraint(
  82                 solver->applyLogicalOperation(SATC_OR,
  83                                                                                                                                         solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
  84                                                                                                                                         solver->applyLogicalOperation(SATC_AND,
  85                                                                                                                                                                                                                                                                 solver->applyLogicalOperation(SATC_IFF, v12, v13),
  86                                                                                                                                                                                                                                                                 solver->applyLogicalOperation(SATC_NOT,b48))
  87                                                                                                                                         ));
  88         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
  89         solver->addConstraint(v14);
  90         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
  91         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
  92         BooleanEdge v15 = solver->getBooleanVar(0);
  93         BooleanEdge v16 = solver->getBooleanVar(0);
  94         BooleanEdge v17 = solver->getBooleanVar(0);
  95         BooleanEdge v18 = solver->getBooleanVar(0);
  96         solver->addConstraint(
  97                 solver->applyLogicalOperation(SATC_OR,
  98                                                                                                                                         solver->applyLogicalOperation(SATC_OR, v15, v16),
  99                                                                                                                                         solver->applyLogicalOperation(SATC_IFF, v17, v2)
 100                                                                                                                                         ));
 101         BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
 102         solver->addConstraint(
 103                 solver->applyLogicalOperation(SATC_IMPLIES,
 104                                                                                                                                         b57,
 105                                                                                                                                         solver->applyLogicalOperation(SATC_OR, v15, v16)
 106                                                                                                                                         ));
 107         solver->addConstraint(
 108                 solver->applyLogicalOperation(SATC_IMPLIES,
 109                                                                                                                                         solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
 110                                                                                                                                         solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
 111                                                                                                                                         ));
 112         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
 113         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
 114         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
 115         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
 116         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
 117         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
 118         solver->addConstraint(v18);
 119
 120         if (solver->solve() == 1) {
 121                 printf("SAT\n");
 122                 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
 123                                          solver->getOrderConstraintValue(order, 5, 1),
 124                                          solver->getOrderConstraintValue(order, 1, 4),
 125                                          solver->getOrderConstraintValue(order, 5, 4),
 126                                          solver->getOrderConstraintValue(order, 1, 5));
 127         } else {
 128                 printf("UNSAT\n");
 129         }
 130         delete solver;
 131 }