| 107 | BoolVarArray X; |
| 108 | public: |
| 109 | QBFProblem(const QBFOptions& opt) : Script(opt), QSpaceInfo() |
| 110 | { |
| 111 | std::cout << "Loading problem" << std::endl; |
| 112 | if (!opt.printStrategy()) strategyMethod(0); // disable build and print strategy |
| 113 | using namespace Int; |
| 114 | |
| 115 | X = BoolVarArray(*this,4,0,1); |
| 116 | BoolVarArray O(*this,7,0,1); |
| 117 | |
| 118 | switch (opt.n) { |
| 119 | case 0: |
| 120 | // forall{a}(forall{b}(forall{c}(exists{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT ( 6p, 4n, 1f) Q:( 0p, 0n, 1f) |
| 121 | setForAll(*this,X[0]); |
| 122 | setForAll(*this,X[1]); |
| 123 | setForAll(*this,X[2]); |
| 124 | break; |
| 125 | case 1: |
| 126 | // forall{a}(forall{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (27p, 10n, 2f) Q:( 3p, 0n, 1f) |
| 127 | setForAll(*this,X[0]); |
| 128 | setForAll(*this,X[1]); |
| 129 | setForAll(*this,X[3]); |
| 130 | break; |
| 131 | case 2: |
| 132 | // forall[a](exists[b](forall[c](forall[d] ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (18p, 8n, 2f) Q:( 0p, 0n, 1f) |
| 133 | setForAll(*this,X[0]); |
| 134 | setForAll(*this,X[2]); |
| 135 | setForAll(*this,X[3]); |
| 136 | break; |
| 137 | case 3: |
| 138 | // forall{a}(exists{b}(forall{c}(exists{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT (40p, 13n, 2f) Q:(18p, 7n, 1f) |
| 139 | setForAll(*this,X[0]); |
| 140 | setForAll(*this,X[2]); |
| 141 | break; |
| 142 | case 4: |
| 143 | // exists{a}(forall{b}(forall{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (18p, 9n, 2f) Q:( 0p, 0n, 1f) |
| 144 | setForAll(*this,X[1]); |
| 145 | setForAll(*this,X[2]); |
| 146 | setForAll(*this,X[3]); |
| 147 | break; |
| 148 | case 5: |
| 149 | // exists{a}(forall{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (53p, 19n, 4f) Q:( 3p, 0n, 1f) |
| 150 | setForAll(*this,X[1]); |
| 151 | setForAll(*this,X[3]); |
| 152 | break; |
| 153 | case 6: |
| 154 | // exists{a}(exists{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT (16p, 5n, 0f) Q:( 9p, 5n, 0f) |
| 155 | setForAll(*this,X[3]); |
| 156 | break; |
| 157 | case 7: |
| 158 | // exists[a](exists[b](exists[c](exists[d] ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT ( 9p, 4n, 0f) Q:( 9p, 4n, 0f) |
| 159 | break; |
| 160 | default: |
| 161 | GECODE_NEVER; |
| 162 | } |
| 163 | |
| 164 | |
| 165 | if (opt.qConstraint()) { |
| 166 | QBoolVar qa, qb, qc, qd; |
nothing calls this directly
no test coverage detected