Home
last modified time | relevance | path

Searched refs:enode2literal (Results 1 – 12 of 12) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Deuf_invariant.cpp30 s().value(enode2literal(n)) == s().value(enode2literal(n->get_root()))); in check_eqc_bool_assignment()
36 if (m.is_bool(n->get_expr()) && l_undef == s().value(enode2literal(n))) { in check_missing_bool_enode_propagation()
38 VERIFY(l_undef == s().value(enode2literal(n->get_root()))); in check_missing_bool_enode_propagation()
42 VERIFY(l_undef == s().value(enode2literal(o))); in check_missing_bool_enode_propagation()
H A Deuf_solver.h252 sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); } in expr2literal()
253 sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); } in enode2literal() function
254 lbool value(enode* n) const { return s().value(enode2literal(n)); } in value()
H A Ddt_solver.cpp161 literal l = ctx.enode2literal(r); in sign_recognizer_conflict()
430 m_lits.push_back(~ctx.enode2literal(r)); in propagate_recognizer()
455 consequent = ctx.enode2literal(r); in propagate_recognizer()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Deuf_invariant.cpp30 s().value(enode2literal(n)) == s().value(enode2literal(n->get_root()))); in check_eqc_bool_assignment()
36 if (m.is_bool(n->get_expr()) && l_undef == s().value(enode2literal(n))) { in check_missing_bool_enode_propagation()
38 VERIFY(l_undef == s().value(enode2literal(n->get_root()))); in check_missing_bool_enode_propagation()
42 VERIFY(l_undef == s().value(enode2literal(o))); in check_missing_bool_enode_propagation()
H A Deuf_solver.h237 sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); } in expr2literal()
238 sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); } in enode2literal() function
239 lbool value(enode* n) const { return s().value(enode2literal(n)); } in value()
H A Ddt_solver.cpp164 literal l = ctx.enode2literal(r); in sign_recognizer_conflict()
413 lits.push_back(~ctx.enode2literal(r)); in propagate_recognizer()
439 consequent = ctx.enode2literal(r); in propagate_recognizer()
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dtheory_special_relations.cpp273 literal lit = ctx.enode2literal(n); in final_check_tc()
H A Dsmt_context.h348 literal enode2literal(enode const * n) const { in enode2literal() function
H A Dsmt_context.cpp1129 literal l = enode2literal(r->get_root()); in is_diseq()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dtheory_special_relations.cpp273 literal lit = ctx.enode2literal(n); in final_check_tc()
H A Dsmt_context.h347 literal enode2literal(enode const * n) const { in enode2literal() function
H A Dsmt_context.cpp1140 literal l = enode2literal(r->get_root()); in is_diseq()