Home
last modified time | relevance | path

Searched refs:m_assumption (Results 1 – 14 of 14) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_bool_var_data.h31 unsigned m_assumption:1; member
122 m_assumption = false; in init()
H A Dsmt_context.cpp3297 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 Dsmt_context.h427 return get_bdata(v).m_assumption; in is_assumption()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_bool_var_data.h31 unsigned m_assumption:1; member
122 m_assumption = false; in init()
H A Dsmt_context.cpp3307 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 Dsmt_context.h426 return get_bdata(v).m_assumption; in is_assumption()
/dports/math/z3/z3-z3-4.8.13/src/qe/
H A Dqe.cpp2016 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 Dqe.h285 expr* m_assumption; variable
/dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/
H A Dqe.cpp2020 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 Dqe.h284 expr* m_assumption;
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Dbound_propagator.cpp67 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 Dbound_propagator.h86 assumption m_assumption; member
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Dbound_propagator.cpp67 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 Dbound_propagator.h86 assumption m_assumption; member