| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/test/smtlib/ |
| H A D | parser_utils.py | 75 UNSAT = False variable
83 (QF_LIA, "small_set/QF_LIA/prp-23-47.smt2.bz2", UNSAT),
84 (QF_LIA, "small_set/QF_LIA/prp-20-46.smt2.bz2", UNSAT),
85 (QF_LIA, "small_set/QF_LIA/prp-24-47.smt2.bz2", UNSAT),
86 (QF_LIA, "small_set/QF_LIA/prp-24-46.smt2.bz2", UNSAT),
87 (QF_LIA, "small_set/QF_LIA/prp-22-46.smt2.bz2", UNSAT),
88 (QF_LIA, "small_set/QF_LIA/prp-25-49.smt2.bz2", UNSAT),
89 (QF_LIA, "small_set/QF_LIA/prp-21-46.smt2.bz2", UNSAT),
90 (QF_LIA, "small_set/QF_LIA/prp-23-46.smt2.bz2", UNSAT),
91 (QF_LIA, "small_set/QF_LIA/prp-25-48.smt2.bz2", UNSAT),
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | dual_simplex.cpp | 82 return Result::UNSAT; in dualFindModel()
106 result = Result::UNSAT; in dualFindModel()
111 if(result == Result::UNSAT){ in dualFindModel()
122 if(!d_errorSet.errorEmpty() && result != Result::UNSAT){ in dualFindModel()
125 while(!d_errorSet.errorEmpty() && result != Result::UNSAT){ in dualFindModel()
128 result = Result::UNSAT; in dualFindModel()
134 result = Result::UNSAT; in dualFindModel()
137 if(result == Result::UNSAT){ in dualFindModel()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_unsat_core.c.old | 112 printf("---> UNSAT\n");
124 printf("---> UNSAT\n");
140 printf("---> UNSAT\n");
156 printf("---> UNSAT\n");
175 printf("---> UNSAT\n");
193 printf("---> UNSAT\n");
|
| /dports/math/cvc4/CVC4-1.7/src/util/ |
| H A D | result.cpp | 92 d_sat = UNSAT; in Result()
170 return Result(UNSAT, d_inputName); in asSatisfiabilityResult()
194 case UNSAT: in asValidityResult()
217 case Result::UNSAT: in operator <<()
295 case Result::UNSAT: in toStreamDefault()
338 } else if (isSat() == Result::UNSAT) { in toStreamTptp()
|
| /dports/math/rumur/rumur-2021.09.29/rumur/src/smt/ |
| H A D | solver.cc | 87 return UNSAT; in solve()
96 return solve(claim, true) == UNSAT; in is_true()
100 return solve(claim, false) == UNSAT; in is_false()
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/sets/ |
| H A D | sets-sample.smt2 | 27 ; UF can tell that this is UNSAT (union)
37 ; UF can tell that this is UNSAT (containment)
50 ; UF can tell that this is UNSAT (merge union + containment examples)
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | bv_bounds.cpp | 39 if (lo_min && hi_max) return UNSAT; in record()
58 if (lo > hi) return negated ? CONVERTED : UNSAT; in record()
59 if (lo_min && hi_max) return negated ? UNSAT : CONVERTED; in record()
158 if (val.is_zero()) return negated ? UNSAT : CONVERTED; in convert()
170 if (val1.is_zero()) return negated ? UNSAT : CONVERTED; in convert()
174 … return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); in convert()
179 … return l <= h ? record(to_app(t2), l, h, negated, nis) : (negated ? CONVERTED : UNSAT); in convert()
193 … return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); in convert()
208 if (val1 == val2) return negated ? UNSAT : CONVERTED; in convert()
261 case UNSAT: m_okay = false; break; in rewrite()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | bv_bounds.cpp | 39 if (lo_min && hi_max) return UNSAT; in record()
58 if (lo > hi) return negated ? CONVERTED : UNSAT; in record()
59 if (lo_min && hi_max) return negated ? UNSAT : CONVERTED; in record()
158 if (val.is_zero()) return negated ? UNSAT : CONVERTED; in convert()
170 if (val1.is_zero()) return negated ? UNSAT : CONVERTED; in convert()
174 … return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); in convert()
179 … return l <= h ? record(to_app(t2), l, h, negated, nis) : (negated ? CONVERTED : UNSAT); in convert()
193 … return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); in convert()
208 if (val1 == val2) return negated ? UNSAT : CONVERTED; in convert()
261 case UNSAT: m_okay = false; break; in rewrite()
[all …]
|
| /dports/math/glucose/glucose-syrup-4.1/ |
| H A D | Changelog | 14 - Add certified UNSAT proof.
18 See CP12 paper: Refining Restarts Strategies For SAT and UNSAT
|
| /dports/math/cvc4/CVC4-1.7/src/main/ |
| H A D | command_executor.cpp | 157 res.asSatisfiabilityResult() == Result::UNSAT) { in doCommandSingleton()
165 res.asSatisfiabilityResult() == Result::UNSAT)) { in doCommandSingleton()
170 res.asSatisfiabilityResult() == Result::UNSAT) { in doCommandSingleton()
175 res.asSatisfiabilityResult() == Result::UNSAT) { in doCommandSingleton()
|
| H A D | command_executor_portfolio.cpp | 383 d_result.asSatisfiabilityResult() == Result::UNSAT ) { in doCommandSingleton()
391 d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { in doCommandSingleton()
395 d_result.asSatisfiabilityResult() == Result::UNSAT ){ in doCommandSingleton()
399 d_result.asSatisfiabilityResult() == Result::UNSAT ) { in doCommandSingleton()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | solution_filter.cpp | 65 if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) in addTerm()
84 if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) in addTerm()
|
| /dports/math/clingo/clingo-5.5.1/app/clingo/tests/lua/ |
| H A D | test.sol | 4 UNSAT
6 UNSAT
8 UNSAT
10 UNSAT
|
| H A D | core1.sol | 3 UNSAT
|
| H A D | core2.sol | 3 UNSAT
|
| H A D | unsat-sync.sol | 3 UNSAT
|
| /dports/math/clingo/clingo-5.5.1/app/clingo/tests/python/ |
| H A D | test.sol | 4 UNSAT
7 UNSAT
10 UNSAT
13 UNSAT
|
| H A D | core1.sol | 3 UNSAT
|
| H A D | core2.sol | 3 UNSAT
|
| H A D | add-clause-py.sol | 7 UNSAT
|
| /dports/math/cadical/cadical-1.0.3-cb89cbf/test/cnf/ |
| H A D | drat-trim.c | 34 #define UNSAT 0 macro
238 if (propagate (S, init, 1) == UNSAT) { return UNSAT; } in propagateUnits()
877 return UNSAT; } in init()
895 return UNSAT; } in init()
902 if (propagateUnits (S, 1) == UNSAT) { in init()
905 postprocess (S); return UNSAT; } in init()
910 if (init (S) == UNSAT) return UNSAT; in verify()
987 postprocess (S); return UNSAT; } in verify()
1011 postprocess (S); return UNSAT; } in verify()
1109 return UNSAT; } in verify()
[all …]
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorslvprop.c | 258 goto UNSAT; in sat_prop_solver_aux()
261 goto UNSAT; in sat_prop_solver_aux()
263 goto UNSAT; in sat_prop_solver_aux()
282 goto UNSAT; /* contains false constraint -> unsat */ in sat_prop_solver_aux()
323 if (!(move (btor, nmoves))) goto UNSAT; in sat_prop_solver_aux()
346 UNSAT: in sat_prop_solver_aux()
|
| /dports/math/clingo/clingo-5.5.1/app/clingo/tests/lp/ |
| H A D | istop.sol | 2 UNSAT
|
| H A D | aggregates.sol | 2 UNSAT
|
| H A D | istop.lp | 3 #const istop="UNSAT".
|