mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
re-enable proofs for qe-lite #3153
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
395a304262
commit
d09e6eccf0
|
@ -2331,11 +2331,12 @@ public:
|
|||
}
|
||||
|
||||
void operator()(expr_ref& fml, proof_ref& pr) {
|
||||
if (!m.proofs_enabled()) {
|
||||
expr_ref tmp(m);
|
||||
m_elim_star(fml, tmp, pr);
|
||||
fml = std::move(tmp);
|
||||
expr_ref tmp(m);
|
||||
m_elim_star(fml, tmp, pr);
|
||||
if (m.proofs_enabled()) {
|
||||
pr = m.mk_rewrite(fml, tmp);
|
||||
}
|
||||
fml = std::move(tmp);
|
||||
}
|
||||
|
||||
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
|
||||
|
|
|
@ -3916,7 +3916,8 @@ public:
|
|||
if (!use_bounded_expansion())
|
||||
return;
|
||||
ctx().push_trail(value_trail<context, literal>(m_bounded_range_lit));
|
||||
m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
|
||||
if (!m_bound_predicate || !m_term2bound_info.empty())
|
||||
m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
|
||||
m_bounded_range_lit = mk_literal(m_bound_predicate);
|
||||
// add max-unfolding literal
|
||||
// add variable bounds
|
||||
|
@ -3947,8 +3948,10 @@ public:
|
|||
else if (m_predicate2term.find(e, t)) {
|
||||
found = true;
|
||||
bound_info bi;
|
||||
VERIFY(m_term2bound_info.find(t, bi));
|
||||
if (bi.m_range >= max_range()) {
|
||||
if (!m_term2bound_info.find(t, bi)) {
|
||||
TRACE("arith", tout << "bound information for term " << mk_pp(t, m) << " not found\n";);
|
||||
}
|
||||
else if (bi.m_range >= max_range()) {
|
||||
m_term2bound_info.erase(t);
|
||||
}
|
||||
else {
|
||||
|
@ -3981,6 +3984,15 @@ public:
|
|||
m_term2bound_info.insert(t, bi);
|
||||
}
|
||||
|
||||
void setup() {
|
||||
m_bounded_range_lit = null_literal;
|
||||
m_bound_predicates.reset();
|
||||
m_bound_predicate = nullptr;
|
||||
m_predicate2term.reset();
|
||||
m_term2bound_info.reset();
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
theory_lra::theory_lra(context& ctx):
|
||||
|
@ -4109,6 +4121,9 @@ void theory_lra::add_theory_assumptions(expr_ref_vector& assumptions) {
|
|||
bool theory_lra::should_research(expr_ref_vector& unsat_core) {
|
||||
return m_imp->should_research(unsat_core);
|
||||
}
|
||||
void theory_lra::setup() {
|
||||
m_imp->setup();
|
||||
}
|
||||
|
||||
}
|
||||
template class lp::lp_bound_propagator<smt::theory_lra::imp>;
|
||||
|
|
|
@ -95,6 +95,8 @@ namespace smt {
|
|||
|
||||
void collect_statistics(::statistics & st) const override;
|
||||
|
||||
void setup() override;
|
||||
|
||||
void add_theory_assumptions(expr_ref_vector& assumptions) override;
|
||||
|
||||
bool should_research(expr_ref_vector& unsat_core) override;
|
||||
|
|
Loading…
Reference in a new issue