Searched refs:resolve_clause (Results 1 – 2 of 2) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1787 void resolve_clause(bool_var b, unsigned sz, literal const * c) { in resolve_clause() function
1797 void resolve_clause(bool_var b, clause const & c) { in resolve_clause() function
1799 resolve_clause(b, c.size(), c.data()); in resolve_clause()
1849 resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.data()); in resolve_lazy_justification()
1990 resolve_clause(null_bool_var, *conflict_clause); in resolve()
2010 resolve_clause(b, *(jst.get_clause())); in resolve()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1787 void resolve_clause(bool_var b, unsigned sz, literal const * c) { in resolve_clause() function
1797 void resolve_clause(bool_var b, clause const & c) { in resolve_clause() function
1799 resolve_clause(b, c.size(), c.c_ptr()); in resolve_clause()
1849 resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.c_ptr()); in resolve_lazy_justification()
1990 resolve_clause(null_bool_var, *conflict_clause); in resolve()
2010 resolve_clause(b, *(jst.get_clause())); in resolve()
|