mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
fix #3972 regression from changing the way assumptions are initialized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
25252af1fc
commit
1ec977930a
|
@ -81,29 +81,11 @@ void expr_context_simplifier::reduce_rec(expr * m, expr_ref & result) {
|
|||
|
||||
void expr_context_simplifier::reduce_rec(quantifier* q, expr_ref & result) {
|
||||
result = q;
|
||||
|
||||
#if 0
|
||||
//
|
||||
// The context assumes that asserted expressions are in NNF with
|
||||
// respect to the quantifier occurrences.
|
||||
// This can be disabled if the strong context simplifier
|
||||
// is called from the API over the Z3_simplify method.
|
||||
//
|
||||
expr_context_simplifier nested(m_manager);
|
||||
expr_ref body_r(m_manager);
|
||||
nested.reduce(q->get_expr(), body_r);
|
||||
if (body_r.get() != q->get_expr()) {
|
||||
result = m_manager.update_quantifier(q, body_r.get());
|
||||
}
|
||||
else {
|
||||
result = q;
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) {
|
||||
if (m_manager.get_basic_family_id() == a->get_family_id()) {
|
||||
switch(a->get_decl_kind()) {
|
||||
switch (a->get_decl_kind()) {
|
||||
case OP_AND:
|
||||
reduce_and(a->get_num_args(), a->get_args(), result);
|
||||
return;
|
||||
|
@ -168,18 +150,18 @@ void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) {
|
|||
}
|
||||
|
||||
expr_ref_vector args(m_manager);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
for (expr* arg : *a) {
|
||||
expr_ref tmp(m_manager);
|
||||
reduce_rec(a->get_arg(i), tmp);
|
||||
reduce_rec(arg, tmp);
|
||||
args.push_back(tmp.get());
|
||||
}
|
||||
result = m_manager.mk_app(a->get_decl(), args.size(), args.c_ptr());
|
||||
result = m_manager.mk_app(a->get_decl(), args);
|
||||
}
|
||||
|
||||
void expr_context_simplifier::clean_trail(unsigned old_lim) {
|
||||
for (unsigned i = m_trail.size(); i > old_lim; ) {
|
||||
--i;
|
||||
m_context.erase(m_trail[i].get());
|
||||
m_context.erase(m_trail.get(i));
|
||||
}
|
||||
m_trail.resize(old_lim);
|
||||
}
|
||||
|
@ -436,7 +418,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
|
|||
args.push_back(arg);
|
||||
}
|
||||
}
|
||||
r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
|
||||
r = m.mk_app(a->get_decl(), args);
|
||||
trail.push_back(r);
|
||||
if (n2) {
|
||||
m_solver.push();
|
||||
|
@ -712,7 +694,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
|
|||
args.push_back(arg);
|
||||
}
|
||||
}
|
||||
r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
|
||||
r = m.mk_app(a->get_decl(), args);
|
||||
trail.push_back(r);
|
||||
if (n2) {
|
||||
m_solver.push();
|
||||
|
|
|
@ -3025,17 +3025,21 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
static bool is_valid_assumption(ast_manager & m, expr * assumption) {
|
||||
static bool is_valid_assumption(ast_manager & m, expr * a) {
|
||||
expr* arg;
|
||||
if (!m.is_bool(assumption))
|
||||
if (!m.is_bool(a))
|
||||
return false;
|
||||
if (is_uninterp_const(assumption))
|
||||
if (is_uninterp_const(a))
|
||||
return true;
|
||||
if (m.is_not(assumption, arg) && is_uninterp_const(arg))
|
||||
if (m.is_not(a, arg) && is_uninterp_const(arg))
|
||||
return true;
|
||||
if (!is_app(assumption))
|
||||
if (!is_app(a))
|
||||
return false;
|
||||
if (m.is_true(assumption) || m.is_false(assumption))
|
||||
if (m.is_true(a) || m.is_false(a))
|
||||
return true;
|
||||
if (is_app(a) && to_app(a)->get_family_id() == m.get_basic_family_id())
|
||||
return false;
|
||||
if (is_app(a) && to_app(a)->get_num_args() == 0)
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
@ -3192,6 +3196,8 @@ namespace smt {
|
|||
vector<std::pair<expr*,expr_ref>> asm2proxy;
|
||||
internalize_proxies(asms, asm2proxy);
|
||||
for (auto const& p: asm2proxy) {
|
||||
if (inconsistent())
|
||||
break;
|
||||
expr_ref curr_assumption = p.second;
|
||||
expr* orig_assumption = p.first;
|
||||
if (m.is_true(curr_assumption)) continue;
|
||||
|
@ -3199,17 +3205,16 @@ namespace smt {
|
|||
proof * pr = m.mk_asserted(curr_assumption);
|
||||
internalize_assertion(curr_assumption, pr, 0);
|
||||
literal l = get_literal(curr_assumption);
|
||||
if (l == true_literal)
|
||||
SASSERT(get_assignment(l) != l_undef);
|
||||
SASSERT(l != false_literal || inconsistent());
|
||||
if (l == true_literal || l == false_literal) {
|
||||
continue;
|
||||
if (inconsistent())
|
||||
break;
|
||||
SASSERT(get_assignment(l) == l_true);
|
||||
}
|
||||
m_literal2assumption.insert(l.index(), orig_assumption);
|
||||
// internalize_assertion marked l as relevant.
|
||||
SASSERT(is_relevant(l));
|
||||
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";);
|
||||
m_assumptions.push_back(l);
|
||||
get_bdata(l.var()).m_assumption = true;
|
||||
SASSERT(is_relevant(l));
|
||||
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";);
|
||||
}
|
||||
}
|
||||
m_search_lvl = m_scope_lvl;
|
||||
|
|
|
@ -4610,7 +4610,7 @@ expr_ref theory_seq::elim_skolem(expr* e) {
|
|||
}
|
||||
|
||||
todo.pop_back();
|
||||
result = m.mk_app(to_app(a)->get_decl(), args.size(), args.c_ptr());
|
||||
result = m.mk_app(to_app(a)->get_decl(), args);
|
||||
trail.push_back(result);
|
||||
cache.insert(a, result);
|
||||
}
|
||||
|
@ -4618,7 +4618,6 @@ expr_ref theory_seq::elim_skolem(expr* e) {
|
|||
}
|
||||
|
||||
void theory_seq::validate_axiom(literal_vector const& lits) {
|
||||
return;
|
||||
if (get_context().get_fparams().m_seq_validate) {
|
||||
enode_pair_vector eqs;
|
||||
literal_vector _lits;
|
||||
|
@ -4744,7 +4743,7 @@ bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs, bool&
|
|||
return false;
|
||||
}
|
||||
change |= e4 != e3;
|
||||
m_util.str.get_concat_units(e4, es);
|
||||
m_util.str.get_concat(e4, es);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -4793,9 +4792,12 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
|
|||
}
|
||||
bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
|
||||
result = try_expand(e0, eqs);
|
||||
if (result) return true;
|
||||
if (result) {
|
||||
return true;
|
||||
}
|
||||
dependency* deps = nullptr;
|
||||
expr* e = m_rep.find(e0, deps);
|
||||
|
||||
expr* e1, *e2, *e3;
|
||||
expr_ref arg1(m), arg2(m);
|
||||
context& ctx = get_context();
|
||||
|
@ -4870,9 +4872,6 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_itos(e, e1)) {
|
||||
result = e;
|
||||
}
|
||||
else {
|
||||
result = e;
|
||||
}
|
||||
|
@ -5905,7 +5904,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
|
|||
|
||||
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) {
|
||||
expr* es[4] = { e1, e2, e3, e4 };
|
||||
unsigned len = e4?4:(e3?3:(e2?2:1));
|
||||
unsigned len = e4?4:(e3?3:(e2?2:(e1?1:0)));
|
||||
|
||||
if (!range) {
|
||||
range = m.get_sort(e1);
|
||||
|
|
|
@ -696,8 +696,7 @@ namespace smt {
|
|||
bool is_step(expr* e) const;
|
||||
bool is_max_unfolding(expr* e) const { return is_skolem(symbol("seq.max_unfolding_depth"), e); }
|
||||
expr_ref mk_max_unfolding_depth() {
|
||||
return mk_skolem(symbol("seq.max_unfolding_depth"),
|
||||
m_autil.mk_int(m_max_unfolding_depth),
|
||||
return mk_skolem(symbol("seq.max_unfolding_depth"), m_autil.mk_int(m_max_unfolding_depth),
|
||||
nullptr, nullptr, nullptr, m.mk_bool_sort());
|
||||
}
|
||||
void propagate_not_prefix(expr* e);
|
||||
|
|
Loading…
Reference in a new issue