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         solver->addConstraint(
  55                 solver->applyLogicalOperation(SATC_OR,
  56                 solver->applyLogicalOperation(SATC_IFF, v3, v4),
  57                 v5));
  58         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
  59         BooleanEdge v6 = solver->getBooleanVar(0);
  60         BooleanEdge v7 = solver->getBooleanVar(0);
  61         BooleanEdge v8 = solver->getBooleanVar(0);
  62         solver->addConstraint(
  63                 solver->applyLogicalOperation(SATC_OR,
  64                 solver->applyLogicalOperation(SATC_IFF, v7, v8),
  65                 v6));
  66         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
  67         BooleanEdge v9 = solver->getBooleanVar(0);
  68         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
  69         BooleanEdge v10 = solver->getBooleanVar(0);
  70         BooleanEdge v11 = solver->getBooleanVar(0);
  71         BooleanEdge v12 = solver->getBooleanVar(0);
  72         solver->addConstraint(
  73                 solver->applyLogicalOperation(SATC_OR,
  74                 solver->applyLogicalOperation(SATC_OR, v10, v11),
  75                 solver->applyLogicalOperation(SATC_IFF, v1, v12)));
  76         BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
  77         solver->addConstraint(
  78                 solver->applyLogicalOperation(SATC_OR,
  79                 solver->applyLogicalOperation(SATC_OR, v10, v11),
  80                 b48));
  81         BooleanEdge v13 = solver->getBooleanVar(0);
  82         BooleanEdge v14 = solver->getBooleanVar(0);
  83         solver->addConstraint(
  84                 solver->applyLogicalOperation(SATC_OR,
  85                 solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
  86                 solver->applyLogicalOperation(SATC_AND,
  87                         solver->applyLogicalOperation(SATC_IFF, v12, v13),
  88                         solver->applyLogicalOperation(SATC_NOT,b48))
  89         ));
  90         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
  91         solver->addConstraint(v14);
  92         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
  93         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
  94         BooleanEdge v15 = solver->getBooleanVar(0);
  95         BooleanEdge v16 = solver->getBooleanVar(0);
  96         BooleanEdge v17 = solver->getBooleanVar(0);
  97         BooleanEdge v18 = solver->getBooleanVar(0);
  98         solver->addConstraint(
  99                 solver->applyLogicalOperation(SATC_OR,
 100                 solver->applyLogicalOperation(SATC_OR, v15, v16),
 101                 solver->applyLogicalOperation(SATC_IFF, v17, v2)
 102         ));
 103         BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
 104         solver->addConstraint(
 105                 solver->applyLogicalOperation(SATC_IMPLIES,
 106                 b57,
 107                 solver->applyLogicalOperation(SATC_OR, v15, v16)
 108         ));
 109         solver->addConstraint(
 110                 solver->applyLogicalOperation(SATC_IMPLIES,
 111                 solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
 112                 solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
 113         ));
 114         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
 115         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
 116         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
 117         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
 118         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
 119         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
 120         solver->addConstraint(v18);
 121
 122         if (solver->solve() == 1){
 123                 printf("SAT\n");
 124                 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
 125                         solver->getOrderConstraintValue(order, 5, 1),
 126                         solver->getOrderConstraintValue(order, 1, 4),
 127                         solver->getOrderConstraintValue(order, 5, 4),
 128                         solver->getOrderConstraintValue(order, 1, 5));
 129         } else {
 130                 printf("UNSAT\n");
 131         }
 132         delete solver;
 133 }