Searched refs:simplify_clause (Results 1 – 13 of 13) sorted by relevance
/dports/math/cvc4/CVC4-1.7/proofs/signatures/ |
H A D | sat.plf | 42 (program simplify_clause ((c clause)) clause 53 (let c' (simplify_clause c1) 60 (let c' (simplify_clause c1) 64 ((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2))) 73 (let c' (simplify_clause c1) 81 (let c' (simplify_clause c1) 111 (! r (^ (simplify_clause c1) c2) 156 ; A little example to demonstrate simplify_clause.
|
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | sat_solver.c | 1654 static void simplify_clause(sat_solver_t *solver, clause_t *cl) { in simplify_clause() function 1698 for (i=0; i<n; i++) simplify_clause(solver, v[i]); in simplify_clause_set() 1705 for (i=0; i<n; i++) simplify_clause(solver, v[i]); in simplify_clause_set()
|
H A D | smt_core.c | 4762 static void simplify_clause(smt_core_t *s, clause_t *cl) { in simplify_clause() function 4843 simplify_clause(s, v[i]); in simplify_clause_set() 4857 simplify_clause(s, v[i]); in simplify_clause_set()
|
H A D | new_sat_solver2.c | 4223 static bool simplify_clause(sat_solver_t *solver, cidx_t cidx) { in simplify_clause() function 4317 d += simplify_clause(solver, cidx); in simplify_clause_database()
|
H A D | new_sat_solver.c | 4590 static bool simplify_clause(sat_solver_t *solver, cidx_t cidx) { in simplify_clause() function 4684 d += simplify_clause(solver, cidx); in simplify_clause_database()
|
/dports/math/z3/z3-z3-4.8.13/src/sat/ |
H A D | sat_solver.h | 331 bool simplify_clause(unsigned & num_lits, literal * lits) const;
|
H A D | sat_solver.cpp | 418 bool keep = simplify_clause(num_lits, lits); in mk_clause_core() 898 bool solver::simplify_clause(unsigned & num_lits, literal * lits) const { in simplify_clause() function in sat::solver
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
H A D | sat_solver.h | 320 bool simplify_clause(unsigned & num_lits, literal * lits) const;
|
H A D | sat_solver.cpp | 412 bool keep = simplify_clause(num_lits, lits); 892 bool solver::simplify_clause(unsigned & num_lits, literal * lits) const {
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_context.h | 1162 bool simplify_clause(clause& cls);
|
H A D | smt_context.cpp | 2501 bool context::simplify_clause(clause& cls) { in simplify_clause() function in smt::context 2580 else if (simplify_clause(*cls)) { in simplify_clauses()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_context.h | 1155 bool simplify_clause(clause& cls);
|
H A D | smt_context.cpp | 2513 bool context::simplify_clause(clause& cls) { in simplify_clause() function in smt::context 2592 else if (simplify_clause(*cls)) { in simplify_clauses()
|