Home
last modified time | relevance | path

Searched defs:set_conflict (Results 1 – 25 of 42) sorted by relevance

12

/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/grobner/
H A Dpdd_solver.h170 void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); } in set_conflict() function
171 void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); } in set_conflict() function
/dports/math/z3/z3-z3-4.8.13/src/math/grobner/
H A Dpdd_solver.h170 void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); } in set_conflict() function
171 void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); } in set_conflict() function
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Dpb_solver.h280 inline void set_conflict(sat::justification j, literal l) override { in set_conflict() function
H A Deuf_solver.h293 void set_conflict(th_explain* p) { set_conflict(p->to_index()); } in set_conflict() function
H A Deuf_solver.cpp181 void solver::set_conflict(ext_constraint_idx idx) { in set_conflict() function in euf::solver
H A Darith_solver.cpp1206 void solver::set_conflict() { in set_conflict() function in arith::solver
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Dba_solver.h302 inline void set_conflict(justification j, literal l) override { in set_conflict() function
H A Deuf_solver.h274 void set_conflict(th_propagation* p) { set_conflict(p->to_index()); } in set_conflict() function
H A Deuf_solver.cpp171 void solver::set_conflict(ext_constraint_idx idx) { in set_conflict() function in euf::solver
H A Darith_solver.cpp1155 void solver::set_conflict() { in set_conflict() function in arith::solver
/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_solver.h402 void set_conflict(justification c) { set_conflict(c, null_literal); } in set_conflict() function
403 void set_conflict() { set_conflict(justification(0)); } in set_conflict() function
H A Dsat_lookahead.h535 void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } in set_conflict() function
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_solver.h386 void set_conflict(justification c) { set_conflict(c, null_literal); } in set_conflict() function
387 void set_conflict() { set_conflict(justification(0)); } in set_conflict() function
H A Dsat_lookahead.h531 void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } in set_conflict() function
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dtheory_utvpi_def.h203 void theory_utvpi<Ext>::set_conflict() { in set_conflict() function
H A Dtheory_arith_core.h3051 …void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* pro… in set_conflict() function
3057 …void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* p… in set_conflict() function
3063 …void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs… in set_conflict() function
H A Dsmt_context.h1105 void set_conflict(const b_justification & js) { in set_conflict() function
1110 void set_conflict(justification * js) { in set_conflict() function
H A Dtheory_special_relations.cpp465 void theory_special_relations::set_conflict(relation& r) { in set_conflict() function in smt::theory_special_relations
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/euf/
H A Deuf_egraph.cpp485 void egraph::set_conflict(enode* n1, enode* n2, justification j) { in set_conflict() function in euf::egraph
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dtheory_arith_core.h3051 …void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* pro… in set_conflict() function
3057 …void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* p… in set_conflict() function
3063 …void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs… in set_conflict() function
H A Dsmt_context.h1098 void set_conflict(const b_justification & js) { in set_conflict() function
1103 void set_conflict(justification * js) { in set_conflict() function
/dports/math/z3/z3-z3-4.8.13/src/ast/euf/
H A Deuf_egraph.cpp552 void egraph::set_conflict(enode* n1, enode* n2, justification j) { in set_conflict() function in euf::egraph
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/
H A Dseq_eq_solver.cpp66 void eq_solver::set_conflict() { in set_conflict() function in seq::eq_solver
/dports/math/z3/z3-z3-4.8.13/src/math/subpaving/
H A Dsubpaving_t.h210 void set_conflict(var x) { SASSERT(!inconsistent()); m_conflict = x; } in set_conflict() function
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/subpaving/
H A Dsubpaving_t.h210 void set_conflict(var x) { SASSERT(!inconsistent()); m_conflict = x; } in set_conflict() function

12