diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 6399552e8..5d9a5ae69 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -53,7 +53,7 @@ def init_project_def():
add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
- add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions')
+ add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite', 'simplifiers', 'solver'], 'solver/assertions')
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
index a599ff5a1..2d2adf1b9 100644
--- a/src/ast/justified_expr.h
+++ b/src/ast/justified_expr.h
@@ -20,12 +20,12 @@ public:
justified_expr& operator=(justified_expr const& other) {
SASSERT(&m == &other.m);
if (this != &other) {
- m.inc_ref(other.get_fml());
- m.inc_ref(other.get_proof());
+ m.inc_ref(other.fml());
+ m.inc_ref(other.pr());
m.dec_ref(m_fml);
m.dec_ref(m_proof);
- m_fml = other.get_fml();
- m_proof = other.get_proof();
+ m_fml = other.fml();
+ m_proof = other.pr();
}
return *this;
}
@@ -53,7 +53,7 @@ public:
m_proof = nullptr;
}
- expr* get_fml() const { return m_fml; }
+ expr* fml() const { return m_fml; }
- proof* get_proof() const { return m_proof; }
+ proof* pr() const { return m_proof; }
};
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 824573d46..d47072ebb 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -177,7 +177,7 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
expr_mark visited;
macro_manager_ns::proc p(m_forbidden_set, m_forbidden);
for (unsigned i = 0; i < n; i++)
- for_each_expr(p, visited, exprs[i].get_fml());
+ for_each_expr(p, visited, exprs[i].fml());
}
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index b65daf063..254baa8b8 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -313,14 +313,14 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
for (unsigned i = 0; i < n; i++)
- tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; );
+ tout << i << ": " << mk_pp(exprs[i].fml(), m) << std::endl; );
bool res = false;
m_occurrences.reset();
// Find out how many non-ground appearances for each uninterpreted function there are
for (unsigned i = 0 ; i < n ; i++)
- find_occurrences(exprs[i].get_fml());
+ find_occurrences(exprs[i].fml());
TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
for (auto kv : m_occurrences)
@@ -331,9 +331,9 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
app_ref a(m);
expr_ref t(m);
quantifier_ref macro(m);
- if (is_quasi_macro(exprs[i].get_fml(), a, t) &&
- quasi_macro_to_macro(to_quantifier(exprs[i].get_fml()), a, t, macro)) {
- TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].get_fml(), m) << std::endl;
+ if (is_quasi_macro(exprs[i].fml(), a, t) &&
+ quasi_macro_to_macro(to_quantifier(exprs[i].fml()), a, t, macro)) {
+ TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].fml(), m) << std::endl;
tout << "Macro: " << mk_pp(macro, m) << std::endl; );
proof * pr = nullptr;
if (m.proofs_enabled())
@@ -377,9 +377,9 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<j
for (unsigned i = 0 ; i < n ; i++) {
expr_ref r(m), rr(m);
proof_ref pr(m), prr(m);
- proof * p = m.proofs_enabled() ? fmls[i].get_proof() : nullptr;
+ proof * p = m.proofs_enabled() ? fmls[i].pr() : nullptr;
expr_dependency_ref dep(m);
- m_macro_manager.expand_macros(fmls[i].get_fml(), p, nullptr, r, pr, dep);
+ m_macro_manager.expand_macros(fmls[i].fml(), p, nullptr, r, pr, dep);
m_rewriter(r, rr, prr);
if (pr) pr = m.mk_modus_ponens(pr, prr);
new_fmls.push_back(justified_expr(m, rr, pr));
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index d8bf025e2..3de62df1b 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -133,8 +133,8 @@ namespace sls {
m_sls_model = mdl;
}
- sat::bool_var bool_flip() override {
- return m_ddfw->bool_flip();
+ sat::bool_var external_flip() override {
+ return m_ddfw->external_flip();
}
bool is_external(sat::bool_var v) override {
@@ -158,7 +158,7 @@ namespace sls {
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw->get_clause_info(idx); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
void flip(sat::bool_var v) override {
- m_ddfw->flip(v);
+ m_ddfw->external_flip(v);
}
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override {
return m_ddfw->try_rotate(v, rotated, budget);
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 5a11e4dbb..cb2c895c4 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -88,8 +88,8 @@ namespace sls {
vector<sat::clause_info> const& clauses() const override { return m_ddfw.clauses(); }
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
- void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.flip(v); }
- sat::bool_var bool_flip() override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.bool_flip(); }
+ void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.external_flip(v); }
+ sat::bool_var external_flip() override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.external_flip(); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) override { return m_ddfw.reward(v); }
double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }
diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt
index 6deffd3a5..a1348fca2 100644
--- a/src/solver/assertions/CMakeLists.txt
+++ b/src/solver/assertions/CMakeLists.txt
@@ -5,4 +5,5 @@ z3_add_component(solver_assertions
smt2parser
smt_params
qe_lite
+ solver
)
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index 422adbf82..62f4c1970 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -184,7 +184,7 @@ void asserted_formulas::assert_expr(expr * e) {
}
void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
- for (justified_expr const& je : m_formulas) result.push_back(je.get_fml());
+ for (justified_expr const& je : m_formulas) result.push_back(je.fml());
}
void asserted_formulas::push_scope() {
@@ -258,7 +258,7 @@ void asserted_formulas::finalize() {
bool asserted_formulas::check_well_sorted() const {
for (justified_expr const& je : m_formulas) {
- if (!is_well_sorted(m, je.get_fml())) return false;
+ if (!is_well_sorted(m, je.fml())) return false;
}
return true;
}
@@ -348,7 +348,7 @@ void asserted_formulas::display(std::ostream & out) const {
for (unsigned i = 0; i < m_formulas.size(); i++) {
if (i == m_qhead)
out << "[HEAD] ==>\n";
- out << mk_pp(m_formulas[i].get_fml(), m) << "\n";
+ out << mk_pp(m_formulas[i].fml(), m) << "\n";
}
out << "inconsistent: " << inconsistent() << "\n";
}
@@ -356,10 +356,10 @@ void asserted_formulas::display(std::ostream & out) const {
void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
if (!m_formulas.empty()) {
for (justified_expr const& f : m_formulas)
- ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
+ ast_def_ll_pp(out, m, f.fml(), pp_visited, true, false);
out << "asserted formulas:\n";
for (justified_expr const& f : m_formulas)
- out << "#" << f.get_fml()->get_id() << " ";
+ out << "#" << f.fml()->get_id() << " ";
out << "\n";
}
}
@@ -400,7 +400,7 @@ void asserted_formulas::flatten_clauses() {
unsigned sz = m_formulas.size();
for (unsigned i = m_qhead; i < sz; ++i) {
auto const& j = m_formulas.get(i);
- expr* f = j.get_fml();
+ expr* f = j.fml();
bool decomposed = false;
if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
decomposed = true;
@@ -454,9 +454,9 @@ void asserted_formulas::nnf_cnf() {
unsigned sz = m_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
for (; i < sz; i++) {
- expr * n = m_formulas[i].get_fml();
+ expr * n = m_formulas[i].fml();
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
- proof_ref pr(m_formulas[i].get_proof(), m);
+ proof_ref pr(m_formulas[i].pr(), m);
expr_ref r1(m);
proof_ref pr1(m);
push_todo.reset();
@@ -497,10 +497,10 @@ void asserted_formulas::simplify_fmls::operator()() {
proof_ref result_pr(m);
simplify(j, result, result_pr);
if (m.proofs_enabled()) {
- if (!result_pr) result_pr = m.mk_rewrite(j.get_fml(), result);
- result_pr = m.mk_modus_ponens(j.get_proof(), result_pr);
+ if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result);
+ result_pr = m.mk_modus_ponens(j.pr(), result_pr);
}
- if (j.get_fml() == result) {
+ if (j.fml() == result) {
new_fmls.push_back(j);
}
else {
@@ -530,7 +530,7 @@ void asserted_formulas::commit(unsigned new_qhead) {
m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead);
for (unsigned i = m_qhead; i < new_qhead; ++i) {
justified_expr const& j = m_formulas[i];
- update_substitution(j.get_fml(), j.get_proof());
+ update_substitution(j.fml(), j.pr());
}
m_qhead = new_qhead;
}
@@ -575,17 +575,17 @@ void asserted_formulas::propagate_values() {
}
unsigned asserted_formulas::propagate_values(unsigned i) {
- expr_ref n(m_formulas[i].get_fml(), m);
+ expr_ref n(m_formulas[i].fml(), m);
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
if (m.proofs_enabled()) {
- proof * pr = m_formulas[i].get_proof();
+ proof * pr = m_formulas[i].pr();
new_pr = m.mk_modus_ponens(pr, new_pr);
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
- if (m.is_false(j.get_fml())) {
+ if (m.is_false(j.fml())) {
m_inconsistent = true;
}
update_substitution(new_n, new_pr);
@@ -670,26 +670,26 @@ proof * asserted_formulas::get_inconsistency_proof() const {
if (!m.inc())
return nullptr;
for (justified_expr const& j : m_formulas) {
- if (m.is_false(j.get_fml()))
- return j.get_proof();
+ if (m.is_false(j.fml()))
+ return j.pr();
}
return nullptr;
}
void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
- expr* f = j.get_fml();
+ expr* f = j.fml();
if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);
}
else {
- n = j.get_fml();
+ n = j.fml();
}
}
void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
bv_util bv(m);
- expr* f = j.get_fml();
+ expr* f = j.fml();
expr* a, *b, *x;
unsigned lo, hi;
rational r;
@@ -699,7 +699,7 @@ void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, exp
// insert x -> x[0,lo-1] ++ n into sub
new_term = bv.mk_concat(b, bv.mk_extract(lo - 1, 0, x));
m_sub.insert(x, new_term);
- n = j.get_fml();
+ n = j.fml();
return true;
}
return false;
@@ -708,7 +708,7 @@ void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, exp
// done
}
else {
- n = j.get_fml();
+ n = j.fml();
m_sub(n);
}
}
@@ -725,7 +725,7 @@ unsigned asserted_formulas::get_total_size() const {
expr_mark visited;
unsigned r = 0;
for (justified_expr const& j : m_formulas)
- r += get_num_exprs(j.get_fml(), visited);
+ r += get_num_exprs(j.fml(), visited);
return r;
}
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 7af53e580..d0a748975 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -83,7 +83,7 @@ class asserted_formulas {
class reduce_asserted_formulas_fn : public simplify_fmls {
public:
reduce_asserted_formulas_fn(asserted_formulas& af): simplify_fmls(af, "reduce-asserted") {}
- void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_rewriter(j.get_fml(), n, p); }
+ void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_rewriter(j.fml(), n, p); }
};
class find_macros_fn : public simplify_fmls {
@@ -122,7 +122,7 @@ class asserted_formulas {
distribute_forall m_functor;
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); }
+ void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.fml(), n); }
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);); }
};
@@ -131,7 +131,7 @@ class asserted_formulas {
pattern_inference_rw m_infer;
public:
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); }
+ void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.fml(), n, p); }
bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); }
};
@@ -145,7 +145,7 @@ class asserted_formulas {
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); }
+ void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.fml(), n, p); }
bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; }
void post_op() override { af.m_reduce_asserted_formulas(); }
};
@@ -164,7 +164,7 @@ class asserted_formulas {
elim_term_ite_rw m_elim;
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); }
+ void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.fml(), n, p); }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
void push() { m_elim.push(); }
@@ -186,7 +186,7 @@ class asserted_formulas {
FUNCTOR m_functor; \
NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
- m_functor(j.get_fml(), n, p); \
+ m_functor(j.fml(), n, p); \
} \
virtual void post_op() { if (REDUCE) af.reduce_and_solve(); } \
virtual bool should_apply() const { return APP; } \
@@ -270,8 +270,8 @@ public:
unsigned get_qhead() const { return m_qhead; }
void commit();
void commit(unsigned new_qhead);
- expr * get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); }
- proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); }
+ expr * get_formula(unsigned idx) const { return m_formulas[idx].fml(); }
+ proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].pr(); }
params_ref const& get_params() const { return m_params; }
void get_assertions(ptr_vector<expr> & result) const;