| /dports/math/vampire/vampire-4.5.1/ |
| H A D | vsat.cpp | 114 SATSolver::Status solverStatus = SATSolver::SATISFIABLE; in runSolverIncrementally()
137 if(solverStatus!=SATSolver::SATISFIABLE) { in runSolverIncrementally()
157 if(solverStatus!=SATSolver::SATISFIABLE) { return solverStatus; } in runSolverIncrementally()
166 ASS_EQ(solver.getStatus(), SATSolver::SATISFIABLE); in runSolverIncrementally()
170 ASS_EQ(solverStatus, SATSolver::SATISFIABLE); in runSolverIncrementally()
171 return SATSolver::SATISFIABLE; in runSolverIncrementally()
231 case SATSolver::SATISFIABLE: in satSolverMode()
233 env.statistics->terminationReason = Statistics::SATISFIABLE; in satSolverMode()
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | xchaff.cpp | 49 case SATISFIABLE: return SatSolver::SATISFIABLE; in Satisfiable()
63 case SATISFIABLE: return SatSolver::SATISFIABLE; in Continue()
|
| H A D | dpllt_basic.cpp | 174 case SatSolver::SATISFIABLE: in handle_result()
434 if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources()) in checkSat()
439 if (result == SatSolver::SATISFIABLE) { in checkSat()
467 result == SatSolver::SATISFIABLE ? SATISFIABLE : in checkSat()
490 if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources()) in continueCheck()
495 if (result == SatSolver::SATISFIABLE) in continueCheck()
518 result == SatSolver::SATISFIABLE ? SATISFIABLE : in continueCheck()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/tests/cnf-files/ |
| H A D | indep_vars_2.cnf | 8 c CHECK: ^s SATISFIABLE$
9 c CHECK: ^s SATISFIABLE$
10 c CHECK-NOT: ^s SATISFIABLE$
|
| H A D | indep_vars.cnf | 8 c CHECK: ^s SATISFIABLE$
9 c CHECK-NOT: ^s SATISFIABLE$
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/tests/cnf-files/ |
| H A D | indep_vars_2.cnf | 8 c CHECK: ^s SATISFIABLE$
9 c CHECK: ^s SATISFIABLE$
10 c CHECK-NOT: ^s SATISFIABLE$
|
| H A D | indep_vars.cnf | 8 c CHECK: ^s SATISFIABLE$
9 c CHECK-NOT: ^s SATISFIABLE$
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | BFNTMainLoop.cpp | 111 …if(innerRes.terminationReason==Statistics::SATISFIABLE || innerRes.terminationReason==Statistics::… in runChild()
118 …nv.options->mode()!=Options::Mode::SPIDER && innerRes.terminationReason==Statistics::SATISFIABLE) { in runChild()
126 case Statistics::SATISFIABLE: in runChild()
181 return MainLoopResult(Statistics::SATISFIABLE); in spawnChild()
218 if(childResult.terminationReason == Statistics::SATISFIABLE) { in runImpl()
|
| /dports/math/cvc3/cvc3-2.4.1/java/src/cvc3/ |
| H A D | SatResult.java | 21 public static final SatResult SATISFIABLE = new SatResult("SATISFIABLE"); field in SatResult
28 if (value.equals(SATISFIABLE.toString())) { in get()
29 return SATISFIABLE; in get()
|
| /dports/math/vampire/vampire-4.5.1/SAT/ |
| H A D | BufferedSolver.cpp | 34 : _inner(inner), _checkedIdx(0), _lastStatus(SATISFIABLE), _varCnt(0), _varCntInnerOld(0) in BufferedSolver()
141 ASS_EQ(_lastStatus,SATISFIABLE); in solve()
155 return SATSolver::SATISFIABLE; in solve()
|
| H A D | MinisatInterfacingNewSimp.cpp | 48 _status(SATISFIABLE) in MinisatInterfacingNewSimp()
144 _status = SATISFIABLE; in solveModuloAssumptionsAndSetStatus()
203 ASS_EQ(_status, SATISFIABLE); in getAssignment()
|
| H A D | Z3MainLoop.cpp | 89 if(status == SATSolver::Status::SATISFIABLE){ reason = Statistics::SATISFIABLE; } in runImpl()
|
| /dports/math/vampire/vampire-4.5.1/UnitTests/ |
| H A D | tSATSolver.cpp | 156 ASS_EQ(s.solve(),SATSolver::SATISFIABLE); in testInterface()
186 ASS_EQ(s.solve(),SATSolver::SATISFIABLE); in testInterface()
214 ASS_EQ(s.solve(),SATSolver::SATISFIABLE); in testInterface()
229 ASS_EQ(s.solve(),SATSolver::SATISFIABLE); in testInterface()
234 ASS_EQ(s.solve(),SATSolver::SATISFIABLE); in testInterface()
|
| /dports/math/clingo/clingo-5.5.1/examples/clingo/blocksworld/ |
| H A D | control_01.out | 13 SATISFIABLE
43 SATISFIABLE
69 SATISFIABLE
99 SATISFIABLE
166 SATISFIABLE
228 SATISFIABLE
230 SATISFIABLE
|
| /dports/math/clingo/clingo-5.5.1/examples/reify/gac/examples/preferences/ |
| H A D | README.md | 11 SATISFIABLE
28 SATISFIABLE
|
| /dports/math/clingo/clingo-5.5.1/examples/clingo/extending/ |
| H A D | README.md | 14 SATISFIABLE
34 SATISFIABLE
|
| /dports/math/vampire/vampire-4.5.1/VUtils/ |
| H A D | SimpleSMT.cpp | 155 if (status == DP::DecisionProcedure::SATISFIABLE || status == DP::DecisionProcedure::UNKNOWN) { in addTheoryConflicts()
249 while(satStatus==SATSolver::SATISFIABLE) { in compute()
295 case DecisionProcedure::SATISFIABLE: in perform()
|
| /dports/math/cvc3/cvc3-2.4.1/src/search/ |
| H A D | search_simple.cpp | 78 return SATISFIABLE; in checkValidRec()
132 if (qres == SATISFIABLE && d_core->incomplete()) qres = UNKNOWN; in checkValidMain()
134 if (qres == SATISFIABLE) { in checkValidMain()
|
| /dports/math/z3/z3-z3-4.8.13/examples/dotnet/ |
| H A D | Program.cs | 203 if (sat == Status.SATISFIABLE) in Check()
239 case Status.SATISFIABLE: in ApplyTactic()
267 case Status.SATISFIABLE: in Prove()
292 case Status.SATISFIABLE: in Disprove()
325 if (q != Status.SATISFIABLE) in ModelConverterTest()
361 if (q != Status.SATISFIABLE) in ArrayExample1()
541 if (s.Check() == Status.SATISFIABLE) in SudokuExample()
757 if (solver.Check() != Status.SATISFIABLE) in BasicTests()
1403 Check(ctx, f, Status.SATISFIABLE); in ParserExample2()
2061 if (slvr.Check() != Status.SATISFIABLE) in FloatingPointExample1()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/dotnet/ |
| H A D | Program.cs | 203 if (sat == Status.SATISFIABLE) in Check()
239 case Status.SATISFIABLE: in ApplyTactic()
267 case Status.SATISFIABLE: in Prove()
292 case Status.SATISFIABLE: in Disprove()
325 if (q != Status.SATISFIABLE) in ModelConverterTest()
361 if (q != Status.SATISFIABLE) in ArrayExample1()
541 if (s.Check() == Status.SATISFIABLE) in SudokuExample()
757 if (solver.Check() != Status.SATISFIABLE) in BasicTests()
1403 Check(ctx, f, Status.SATISFIABLE); in ParserExample2()
2061 if (slvr.Check() != Status.SATISFIABLE) in FloatingPointExample1()
[all …]
|
| /dports/math/eprover/eprover-E-2.0/CONTROL/ |
| H A D | cco_scheduling.c | 163 if((status == SATISFIABLE) || (status == PROOF_FOUND)) in ExecuteSchedule()
198 case SATISFIABLE: in ExecuteSchedule()
|
| /dports/math/z3/z3-z3-4.8.13/examples/java/ |
| H A D | JavaExample.java | 200 if (sat == Status.SATISFIABLE) in check()
230 q = Status.SATISFIABLE; in applyTactic()
239 case SATISFIABLE: in applyTactic()
274 case SATISFIABLE: in prove()
307 case SATISFIABLE: in disprove()
347 if (q != Status.SATISFIABLE) in modelConverterTest()
383 if (q != Status.SATISFIABLE) in arrayExample1()
574 if (s.check() == Status.SATISFIABLE) in sudokuExample()
1471 check(ctx, f, Status.SATISFIABLE); in parserExample2()
2169 if (slvr.check() != Status.SATISFIABLE) in floatingPointExample1()
[all …]
|
| H A D | JavaGenericExample.java | 187 if (sat == Status.SATISFIABLE) in check()
216 q = Status.SATISFIABLE; in applyTactic()
225 case SATISFIABLE: in applyTactic()
260 case SATISFIABLE: in prove()
293 case SATISFIABLE: in disprove()
332 if (q != Status.SATISFIABLE) in modelConverterTest()
369 if (q != Status.SATISFIABLE) in arrayExample1()
541 if (s.check() == Status.SATISFIABLE) in sudokuExample()
1256 check(ctx, f, Status.SATISFIABLE); in parserExample2()
1973 if (slvr.check() != Status.SATISFIABLE) in floatingPointExample1()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
| H A D | JavaExample.java | 200 if (sat == Status.SATISFIABLE) in check()
230 q = Status.SATISFIABLE; in applyTactic()
239 case SATISFIABLE: in applyTactic()
274 case SATISFIABLE: in prove()
307 case SATISFIABLE: in disprove()
347 if (q != Status.SATISFIABLE) in modelConverterTest()
383 if (q != Status.SATISFIABLE) in arrayExample1()
574 if (s.check() == Status.SATISFIABLE) in sudokuExample()
1471 check(ctx, f, Status.SATISFIABLE); in parserExample2()
2169 if (slvr.check() != Status.SATISFIABLE) in floatingPointExample1()
[all …]
|
| /dports/math/jacop/jacop-4.8.0/src/main/java/org/jacop/jasat/core/ |
| H A D | Core.java | 601 currentState = SolverState.SATISFIABLE;
697 return currentState == SolverState.SATISFIABLE || currentState == SolverState.UNSATISFIABLE;
710 if (currentState == SolverState.SATISFIABLE) {
741 case SolverState.SATISFIABLE:
|