Searched refs:satSolverClause (Results 1 – 5 of 5) sorted by relevance
| /dports/math/stp/stp-2.3.3/lib/Simplifier/constantBitP/ |
| H A D | ConstantBitP_MaxPrecision.cpp | 146 satSolverClause.push(SATSolver::mkLit(v, false)); in concretise()
152 satSolverClause.push(SATSolver::mkLit(v, true)); in concretise()
166 satSolverClause.push(SATSolver::mkLit(v, fixed.getValue(i))); in concretise()
475 SATSolver::vec_literals satSolverClause; in maxPrecision() local
489 assert(satSolverClause.size() > 0); in maxPrecision()
490 newS.addClause(satSolverClause); in maxPrecision()
491 satSolverClause.clear(); in maxPrecision()
513 concretise(variables[i], *(children[i]), satSolverClause, beev, in maxPrecision()
520 concretise(outputNode, output, satSolverClause, beev, in maxPrecision()
538 concretise(outputNode, output, satSolverClause, beev, in maxPrecision()
[all …]
|
| /dports/math/stp/stp-2.3.3/lib/ToSat/AIG/ |
| H A D | ToSATAIG.cpp | 151 SATSolver::vec_literals satSolverClause; in add_cnf_to_solver() local
154 satSolverClause.clear(); in add_cnf_to_solver()
161 satSolverClause.push(l); in add_cnf_to_solver()
164 satSolver.addClause(satSolverClause); in add_cnf_to_solver()
|
| /dports/math/stp/stp-2.3.3/lib/ToSat/ASTNode/ |
| H A D | ToSAT.cpp | 166 SATSolver::vec_literals satSolverClause; in fill_satsolver_with_clauses() local
172 satSolverClause.clear(); in fill_satsolver_with_clauses()
182 satSolverClause.push(l); in fill_satsolver_with_clauses()
185 newSolver.addClause(satSolverClause); in fill_satsolver_with_clauses()
|
| /dports/math/stp/stp-2.3.3/lib/AbsRefineCounterExample/ |
| H A D | AbstractionRefinement.cpp | 227 SATSolver::vec_literals satSolverClause; in applyAxiomToSAT() local
228 satSolverClause.push(SATSolver::mkLit(a, true)); in applyAxiomToSAT()
229 satSolverClause.push(SATSolver::mkLit(b, false)); in applyAxiomToSAT()
230 SatSolver.addClause(satSolverClause); in applyAxiomToSAT()
|
| /dports/math/stp/stp-2.3.3/tools/rewrite_rule_gen/ |
| H A D | rewrite_rule_gen.cpp | 656 SATSolver::vec_literals satSolverClause; in getDifficulty() local
659 satSolverClause.clear(); in getDifficulty()
666 satSolverClause.push(l); in getDifficulty()
669 ss->addClause(satSolverClause); in getDifficulty()
|