mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-04 21:57:08 -08:00
parent 534a31f74e
commit eb1122c5cb
8 changed files with 47 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -8266,7 +8266,7 @@ def tree_interpolant(pat,p=None,ctx=None):
solver that determines satisfiability.
>>> x = Int('x')
>>> y = Int('y')
>>> y = Int('y')
>>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)))
[Not(x >= 0), Not(y <= 2)]

44
src/smt/asserted_formulas.cpp
View file

@ -27,8 +27,9 @@ Revision History:
#include "ast/macros/quasi_macros.h"
#include "smt/asserted_formulas.h"
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
m(m),
m_smt_params(sp),
m_params(p),
m_rewriter(m),
m_substitution(m),
@ -65,20 +66,20 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
}
void asserted_formulas::setup() {
switch (m_params.m_lift_ite) {
switch (m_smt_params.m_lift_ite) {
case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE;
m_smt_params.m_ng_lift_ite = LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
m_params.m_ng_lift_ite = LI_NONE;
if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
m_smt_params.m_ng_lift_ite = LI_NONE;
break;
default:
break;
}
if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false;
if (m_smt_params.m_relevancy_lvl == 0)
m_smt_params.m_relevancy_lemma = false;
}
@ -118,24 +119,23 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
}
void asserted_formulas::updt_params(params_ref const& p) {
m_rewriter.updt_params(p);
m_params.append(p);
}
void asserted_formulas::set_eliminate_and(bool flag) {
if (flag == m_elim_and) return;
m_elim_and = flag;
params_ref p;
if (m_params.m_pull_cheap_ite) p.set_bool("pull_cheap_ite", true);
p.set_bool("elim_and", flag);
p.set_bool("arith_ineq_lhs", true);
p.set_bool("sort_sums", true);
p.set_bool("rewrite_patterns", true);
p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
p.set_bool("gcd_rounding", true);
p.set_bool("expand_select_store", true);
p.set_bool("bv_sort_ac", true);
p.set_bool("som", true);
m_rewriter.updt_params(p);
if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
m_params.set_bool("elim_and", flag);
m_params.set_bool("arith_ineq_lhs", true);
m_params.set_bool("sort_sums", true);
m_params.set_bool("rewrite_patterns", true);
m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
m_params.set_bool("gcd_rounding", true);
m_params.set_bool("expand_select_store", true);
m_params.set_bool("bv_sort_ac", true);
m_params.set_bool("som", true);
m_rewriter.updt_params(m_params);
flush_cache();
}
@ -147,7 +147,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
if (inconsistent())
return;
if (m_params.m_preprocess) {
if (m_smt_params.m_preprocess) {
TRACE("assert_expr_bug", tout << r << "\n";);
set_eliminate_and(false); // do not eliminate and before nnf.
m_rewriter(e, r, pr);
@ -230,7 +230,7 @@ void asserted_formulas::reduce() {
return;
if (m_qhead == m_formulas.size())
return;
if (!m_params.m_preprocess)
if (!m_smt_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
invoke(m_find_macros);

37
src/smt/asserted_formulas.h
View file

@ -43,7 +43,8 @@ Revision History:
class asserted_formulas {
ast_manager & m;
smt_params & m_params;
smt_params & m_smt_params;
params_ref m_params;
th_rewriter m_rewriter;
expr_substitution m_substitution;
scoped_expr_substitution m_scoped_substitution;
@ -88,7 +89,7 @@ class asserted_formulas {
public:
find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
void operator()() override { af.find_macros_core(); }
bool should_apply() const override { return af.m_params.m_macro_finder && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -96,7 +97,7 @@ class asserted_formulas {
public:
apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
void operator()() override { af.apply_quasi_macros(); }
bool should_apply() const override { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_quasi_macros && af.has_quantifiers(); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -104,7 +105,7 @@ class asserted_formulas {
public:
nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
void operator()() override { af.nnf_cnf(); }
bool should_apply() const override { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || (af.m_smt_params.m_mbqi && af.has_quantifiers()); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -112,7 +113,7 @@ class asserted_formulas {
public:
propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
void operator()() override { af.propagate_values(); }
bool should_apply() const override { return af.m_params.m_propagate_values; }
bool should_apply() const override { return af.m_smt_params.m_propagate_values; }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -121,30 +122,30 @@ class asserted_formulas {
public:
distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.get_fml(), n); }
bool should_apply() const override { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_distribute_forall && af.has_quantifiers(); }
void post_op() override { af.reduce_and_solve(); TRACE("asserted_formulas", af.display(tout);); }
};
class pattern_inference_fn : public simplify_fmls {
pattern_inference_rw m_infer;
public:
pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_smt_params) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_ematching && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); }
};
class refine_inj_axiom_fn : public simplify_fmls {
public:
refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override;
bool should_apply() const override { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_refine_inj_axiom && af.has_quantifiers(); }
};
class max_bv_sharing_fn : public simplify_fmls {
public:
max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_max_bv_sharing; }
bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; }
void post_op() override { af.m_reduce_asserted_formulas(); }
};
@ -153,7 +154,7 @@ class asserted_formulas {
public:
elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
};
@ -171,12 +172,12 @@ class asserted_formulas {
#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_smt_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas;
@ -220,7 +221,7 @@ class asserted_formulas {
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
public:
asserted_formulas(ast_manager & m, smt_params & p);
asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
~asserted_formulas();
void updt_params(params_ref const& p);

2
src/smt/mam.cpp
View file

@ -3924,7 +3924,7 @@ namespace smt {
}
#ifdef Z3DEBUG
virtual bool check_missing_instances() {
bool check_missing_instances() override {
TRACE("missing_instance", tout << "checking for missing instances...\n";);
flet<bool> l(m_check_missing_instances, true);
rematch(false);

1
src/smt/params/preprocessor_params.cpp
View file

@ -25,7 +25,6 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
m_quasi_macros = p.quasi_macros();
m_restricted_quasi_macros = p.restricted_quasi_macros();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
// m_pull_cheap_ite = _p.get_bool("pull_cheap_ite", m_pull_cheap_ite);
m_refine_inj_axiom = p.refine_inj_axioms();
}

2
src/smt/smt_context.cpp
View file

@ -45,7 +45,7 @@ namespace smt {
m_fparams(p),
m_params(_p),
m_setup(*this, p),
m_asserted_formulas(m, p),
m_asserted_formulas(m, p, _p),
m_qmanager(alloc(quantifier_manager, *this, p, _p)),
m_model_generator(alloc(model_generator, m)),
m_relevancy_propagator(mk_relevancy_propagator(*this)),

6
src/smt/smt_relevancy.cpp
View file

@ -527,7 +527,7 @@ namespace smt {
}
#ifdef Z3DEBUG
bool check_relevancy_app(app * n) const {
bool check_relevancy_app(app * n) const {
SASSERT(is_relevant(n));
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
@ -537,7 +537,7 @@ namespace smt {
return true;
}
virtual bool check_relevancy_or(app * n, bool root) const {
bool check_relevancy_or(app * n, bool root) const override {
lbool val = root ? l_true : m_context.find_assignment(n);
if (val == l_false)
return check_relevancy_app(n);
@ -600,7 +600,7 @@ namespace smt {
return true;
}
bool check_relevancy(expr_ref_vector const & v) const {
bool check_relevancy(expr_ref_vector const & v) const override {
SASSERT(!can_propagate());
ast_manager & m = get_manager();
unsigned sz = v.size();

1
src/smt/theory_seq.cpp
View file

@ -2449,7 +2449,6 @@ expr_ref theory_seq::digit2int(expr* ch) {
}
void theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);