Home
last modified time | relevance | path

Searched refs:simplify_clause (Results 1 – 13 of 13) sorted by relevance

/dports/math/cvc4/CVC4-1.7/proofs/signatures/
H A Dsat.plf42 (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 Dsat_solver.c1654 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 Dsmt_core.c4762 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 Dnew_sat_solver2.c4223 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 Dnew_sat_solver.c4590 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 Dsat_solver.h331 bool simplify_clause(unsigned & num_lits, literal * lits) const;
H A Dsat_solver.cpp418 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 Dsat_solver.h320 bool simplify_clause(unsigned & num_lits, literal * lits) const;
H A Dsat_solver.cpp412 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 Dsmt_context.h1162 bool simplify_clause(clause& cls);
H A Dsmt_context.cpp2501 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 Dsmt_context.h1155 bool simplify_clause(clause& cls);
H A Dsmt_context.cpp2513 bool context::simplify_clause(clause& cls) { in simplify_clause() function in smt::context
2592 else if (simplify_clause(*cls)) { in simplify_clauses()