/dports/math/py-cryptominisat/cryptominisat-5.8.0/tests/ |
H A D | basic_test.cpp | 39 EXPECT_EQ( ret, l_True); in TEST() 49 EXPECT_EQ( ret, l_True); in TEST() 104 EXPECT_EQ( ret, l_True); in TEST() 108 EXPECT_EQ( ret, l_True); in TEST() 120 EXPECT_EQ( ret, l_True); in TEST() 203 EXPECT_EQ(ret, l_True); in TEST() 230 EXPECT_EQ( ret, l_True); in TEST() 246 EXPECT_EQ( ret, l_True); in TEST() 263 EXPECT_EQ( ret, l_True); in TEST() 290 EXPECT_EQ( ret, l_True); in TEST() [all …]
|
H A D | stp_test.cpp | 80 EXPECT_EQ(ret, l_True); in TEST() 81 EXPECT_EQ(s.get_model()[0], l_True); in TEST() 106 EXPECT_EQ(ret, l_True); in TEST() 120 EXPECT_EQ(ret, l_True); in TEST() 122 EXPECT_EQ(s.get_model()[0], l_True); in TEST()
|
H A D | multisol_test.cpp | 57 lbool ret = l_True; in main() 58 while(ret == l_True) { in main() 60 if (ret == l_True) { in main() 71 clause.push_back(Lit(i, solver.get_model()[i] == l_True)); in main()
|
H A D | assump_test.cpp | 50 EXPECT_EQ( ret, l_True); in TEST_F() 60 EXPECT_EQ( ret, l_True); in TEST_F() 86 EXPECT_EQ( ret, l_True); in TEST_F() 98 EXPECT_EQ( ret, l_True ); in TEST_F() 100 EXPECT_EQ( s->get_model()[1], l_True ); in TEST_F() 129 EXPECT_EQ( ret, l_True); in TEST_F() 204 EXPECT_EQ( ret, l_True ); in TEST_F()
|
H A D | readme_test.cpp | 64 assert(ret == l_True); in main() 65 assert(solver.get_model()[0] == l_True); in main() 67 assert(solver.get_model()[2] == l_True); in main()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/tests/ |
H A D | basic_test.cpp | 39 EXPECT_EQ( ret, l_True); in TEST() 49 EXPECT_EQ( ret, l_True); in TEST() 104 EXPECT_EQ( ret, l_True); in TEST() 108 EXPECT_EQ( ret, l_True); in TEST() 120 EXPECT_EQ( ret, l_True); in TEST() 203 EXPECT_EQ(ret, l_True); in TEST() 230 EXPECT_EQ( ret, l_True); in TEST() 246 EXPECT_EQ( ret, l_True); in TEST() 263 EXPECT_EQ( ret, l_True); in TEST() 290 EXPECT_EQ( ret, l_True); in TEST() [all …]
|
H A D | stp_test.cpp | 80 EXPECT_EQ(ret, l_True); in TEST() 81 EXPECT_EQ(s.get_model()[0], l_True); in TEST() 106 EXPECT_EQ(ret, l_True); in TEST() 120 EXPECT_EQ(ret, l_True); in TEST() 122 EXPECT_EQ(s.get_model()[0], l_True); in TEST()
|
H A D | multisol_test.cpp | 57 lbool ret = l_True; in main() 58 while(ret == l_True) { in main() 60 if (ret == l_True) { in main() 71 clause.push_back(Lit(i, solver.get_model()[i] == l_True)); in main()
|
H A D | assump_test.cpp | 50 EXPECT_EQ( ret, l_True); in TEST_F() 60 EXPECT_EQ( ret, l_True); in TEST_F() 86 EXPECT_EQ( ret, l_True); in TEST_F() 98 EXPECT_EQ( ret, l_True ); in TEST_F() 100 EXPECT_EQ( s->get_model()[1], l_True ); in TEST_F() 129 EXPECT_EQ( ret, l_True); in TEST_F() 204 EXPECT_EQ( ret, l_True ); in TEST_F()
|
H A D | readme_test.cpp | 64 assert(ret == l_True); in main() 65 assert(solver.get_model()[0] == l_True); in main() 67 assert(solver.get_model()[2] == l_True); in main()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | lucky.cpp | 107 if (solver->value(lit) == l_True) { in check_all() 114 if (w.isBin() && solver->value(w.lit2()) == l_True) in check_all() 127 if (solver->value(l) == l_True) { in check_all() 156 solver->varData[i].polarity = solver->value(i) == l_True; in set_polarities_to_enq_val() 200 if (solver->value(p) == l_True) { in enqueue_and_prop_assumptions() 269 if (solver->value(l) == l_True) { in horn_sat() 296 if (solver->value(lit) == l_True) { in horn_sat() 303 solver->value(w.lit2()) != l_True) in horn_sat() 323 solver->value(w.lit2()) != l_True) in horn_sat() 342 if (solver->value(x) == l_True) { in horn_sat()
|
H A D | main_emscripten.cpp | 71 if (ret == l_True) { in start_solve() 79 if (ret == l_True) { in start_solve() 93 if (ret == l_True) { in continue_solve() 101 if (ret == l_True) { in continue_solve() 105 if (ret == l_True) { in continue_solve()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | lucky.cpp | 107 if (solver->value(lit) == l_True) { in check_all() 114 if (w.isBin() && solver->value(w.lit2()) == l_True) in check_all() 127 if (solver->value(l) == l_True) { in check_all() 156 solver->varData[i].polarity = solver->value(i) == l_True; in set_polarities_to_enq_val() 200 if (solver->value(p) == l_True) { in enqueue_and_prop_assumptions() 269 if (solver->value(l) == l_True) { in horn_sat() 296 if (solver->value(lit) == l_True) { in horn_sat() 303 solver->value(w.lit2()) != l_True) in horn_sat() 323 solver->value(w.lit2()) != l_True) in horn_sat() 342 if (solver->value(x) == l_True) { in horn_sat()
|
H A D | main_emscripten.cpp | 71 if (ret == l_True) { in start_solve() 79 if (ret == l_True) { in start_solve() 93 if (ret == l_True) { in continue_solve() 101 if (ret == l_True) { in continue_solve() 105 if (ret == l_True) { in continue_solve()
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Main.cc | 128 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 130 if (ret == l_True){ in main() 134 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 144 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 146 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/minisat/minisat-2.2.1/minisat/simp/ |
H A D | Main.cc | 146 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 148 if (ret == l_True){ in main() 152 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 162 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 164 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/glucose/glucose-syrup-4.1/simp/ |
H A D | Main.cc | 267 …printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE… in main() 270 if (ret == l_True){ in main() 274 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 283 if(S.showModel && ret==l_True) { in main() 287 printf("%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 296 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 298 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/glucose/glucose-syrup-4.1/parallel/ |
H A D | Main.cc | 237 …printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE… in main() 239 if(msolver.getShowModel() && ret==l_True) { in main() 244 printf("%s%s%d", (i==0)?"":" ", (msolver.model[i]==l_True)?"":"-", i+1); in main() 252 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 254 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | Main.cc | 173 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 175 if (ret == l_True){ in main() 179 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 189 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 191 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
H A D | Main.cc | 172 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 174 if (ret == l_True){ in main() 178 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 188 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 190 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | MainSimp.cpp | 181 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in MainSimp() 183 if (ret == l_True){ in MainSimp() 187 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in MainSimp() 199 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in MainSimp()
|
H A D | MainSat.cpp | 172 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in MainSat() 174 if (ret == l_True){ in MainSat() 178 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in MainSat() 190 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in MainSat()
|
H A D | SimpSolver.h | 184 …n_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } in solve() 185 …Off(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } in solve() 186 …ear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } in solve() 187 …sh(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } in solve() 189 budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; } in solve()
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/ |
H A D | Main.cc | 192 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 194 if (ret == l_True){ in main() 198 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 208 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 210 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/simp/ |
H A D | Main.cc | 193 … printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); in main() 195 if (ret == l_True){ in main() 199 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); in main() 209 …exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invok… in main() 211 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in main()
|