Searched refs:m_assumption (Results 1 – 14 of 14) sorted by relevance
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_bool_var_data.h | 31 unsigned m_assumption:1; member 122 m_assumption = false; in init()
|
H A D | smt_context.cpp | 3297 get_bdata(l.var()).m_assumption = true; in init_assumptions() 3311 get_bdata(lit.var()).m_assumption = false; in reset_assumptions() 3340 SASSERT(get_bdata(l.var()).m_assumption); in mk_unsat_core()
|
H A D | smt_context.h | 427 return get_bdata(v).m_assumption; in is_assumption()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_bool_var_data.h | 31 unsigned m_assumption:1; member 122 m_assumption = false; in init()
|
H A D | smt_context.cpp | 3307 get_bdata(l.var()).m_assumption = true; in init_assumptions() 3321 get_bdata(lit.var()).m_assumption = false; in reset_assumptions() 3350 SASSERT(get_bdata(l.var()).m_assumption); in mk_unsat_core()
|
H A D | smt_context.h | 426 return get_bdata(v).m_assumption; in is_assumption()
|
/dports/math/z3/z3-z3-4.8.13/src/qe/ |
H A D | qe.cpp | 2016 expr_ref m_assumption; member in qe::quant_elim_new 2025 m_assumption(m), in quant_elim_new() 2087 m_assumption = fml; in set_assumption() 2147 th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs); in eliminate_block() 2214 m_assumption(m.mk_true()) in expr_quant_elim() 2228 m_assumption = assumption; in operator ()() 2338 m_qe->set_assumption(m_assumption); in elim() 2417 m_quant_elim(m_assumption, new_q, r); 2430 simplifier(m), m_quant_elim(m, p), m_assumption(m.mk_true())
|
H A D | qe.h | 285 expr* m_assumption; variable
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
H A D | qe.cpp | 2020 expr_ref m_assumption; member in qe::quant_elim_new 2029 m_assumption(m), in quant_elim_new() 2091 m_assumption = fml; in set_assumption() 2151 th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs); in eliminate_block() 2218 m_assumption(m.mk_true()) in expr_quant_elim() 2232 m_assumption = assumption; in operator ()() 2342 m_qe->set_assumption(m_assumption); in elim() 2421 m_quant_elim(m_assumption, new_q, r); 2434 simplifier(m), m_quant_elim(m, p), m_assumption(m.mk_true())
|
H A D | qe.h | 284 expr* m_assumption;
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
H A D | bound_propagator.cpp | 67 m_assumption = a; in bound() 797 ex.push_back(b->m_assumption); in explain() 812 ex.push_back(b->m_assumption); in explain()
|
H A D | bound_propagator.h | 86 assumption m_assumption; member
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
H A D | bound_propagator.cpp | 67 m_assumption = a; in bound() 797 ex.push_back(b->m_assumption); in explain() 812 ex.push_back(b->m_assumption); in explain()
|
H A D | bound_propagator.h | 86 assumption m_assumption; member
|