mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
739 lines
23 KiB
C++
739 lines
23 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
asserted_formulas.cpp
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2008-06-11.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "util/warning.h"
|
|
#include "ast/ast_ll_pp.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "ast/for_each_expr.h"
|
|
#include "ast/well_sorted.h"
|
|
#include "ast/rewriter/rewriter_def.h"
|
|
#include "ast/normal_forms/nnf.h"
|
|
#include "ast/pattern/pattern_inference.h"
|
|
#include "ast/macros/quasi_macros.h"
|
|
#include "ast/occurs.h"
|
|
#include "ast/bv_decl_plugin.h"
|
|
#include "solver/assertions/asserted_formulas.h"
|
|
|
|
|
|
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),
|
|
m_scoped_substitution(m_substitution),
|
|
m_defined_names(m),
|
|
m_static_features(m),
|
|
m_qhead(0),
|
|
m_macro_manager(m),
|
|
m_bv_sharing(m),
|
|
m_inconsistent(false),
|
|
m_has_quantifiers(false),
|
|
m_reduce_asserted_formulas(*this),
|
|
m_distribute_forall(*this),
|
|
m_pattern_inference(*this),
|
|
m_refine_inj_axiom(*this),
|
|
m_max_bv_sharing_fn(*this),
|
|
m_elim_term_ite(*this),
|
|
m_qe_lite(*this),
|
|
m_pull_nested_quantifiers(*this),
|
|
m_elim_bvs_from_quantifiers(*this),
|
|
m_cheap_quant_fourier_motzkin(*this),
|
|
m_apply_bit2int(*this),
|
|
m_bv_size_reduce(*this),
|
|
m_lift_ite(*this),
|
|
m_ng_lift_ite(*this),
|
|
m_find_macros(*this),
|
|
m_propagate_values(*this),
|
|
m_nnf_cnf(*this),
|
|
m_apply_quasi_macros(*this),
|
|
m_flatten_clauses(*this),
|
|
m_lazy_scopes(0) {
|
|
|
|
m_macro_finder = alloc(macro_finder, m, m_macro_manager);
|
|
|
|
m_elim_and = true;
|
|
set_eliminate_and(false);
|
|
|
|
}
|
|
|
|
void asserted_formulas::setup() {
|
|
switch (m_smt_params.m_lift_ite) {
|
|
case lift_ite_kind::LI_FULL:
|
|
m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
|
|
break;
|
|
case lift_ite_kind::LI_CONSERVATIVE:
|
|
if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)
|
|
m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
|
|
if (m_smt_params.m_relevancy_lvl == 0)
|
|
m_smt_params.m_relevancy_lemma = false;
|
|
}
|
|
|
|
void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
|
|
if (inconsistent()) {
|
|
return;
|
|
}
|
|
expr* e1 = nullptr;
|
|
if (m.is_false(e)) {
|
|
result.push_back(justified_expr(m, e, pr));
|
|
m_inconsistent = true;
|
|
}
|
|
else if (m.is_true(e)) {
|
|
// skip
|
|
}
|
|
else if (m.is_and(e)) {
|
|
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
|
|
expr* arg = to_app(e)->get_arg(i);
|
|
proof_ref _pr(m.proofs_enabled() ? m.mk_and_elim(pr, i) : nullptr, m);
|
|
push_assertion(arg, _pr, result);
|
|
}
|
|
}
|
|
else if (m.is_not(e, e1) && m.is_or(e1)) {
|
|
for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
|
|
expr* arg = to_app(e1)->get_arg(i);
|
|
proof_ref _pr(m.proofs_enabled() ? m.mk_not_or_elim(pr, i) : nullptr, m);
|
|
expr_ref narg(mk_not(m, arg), m);
|
|
push_assertion(narg, _pr, result);
|
|
}
|
|
}
|
|
else {
|
|
result.push_back(justified_expr(m, e, pr));
|
|
}
|
|
}
|
|
|
|
void asserted_formulas::updt_params(params_ref const& p) {
|
|
m_params.append(p);
|
|
}
|
|
|
|
void asserted_formulas::set_eliminate_and(bool flag) {
|
|
if (flag == m_elim_and) return;
|
|
m_elim_and = flag;
|
|
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("expand_nested_stores", true);
|
|
m_params.set_bool("bv_sort_ac", true);
|
|
// seq theory solver keeps terms in normal form and has to interact with side-effect of rewriting
|
|
m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
|
|
m_params.set_bool("som", true);
|
|
if (m_smt_params.m_arith_mode == arith_solver_id::AS_OLD_ARITH)
|
|
m_params.set_bool("flat", true);
|
|
m_rewriter.updt_params(m_params);
|
|
flush_cache();
|
|
}
|
|
|
|
|
|
void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
|
|
force_push();
|
|
proof_ref in_pr(_in_pr, m), pr(_in_pr, m);
|
|
expr_ref r(e, m);
|
|
SASSERT(m.is_bool(e));
|
|
|
|
if (inconsistent())
|
|
return;
|
|
|
|
if (m.is_true(e))
|
|
return;
|
|
|
|
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);
|
|
if (m.proofs_enabled()) {
|
|
if (e == r)
|
|
pr = in_pr;
|
|
else
|
|
pr = m.mk_modus_ponens(in_pr, pr);
|
|
}
|
|
TRACE("assert_expr_bug", tout << "after...\n" << r << "\n" << pr << "\n";);
|
|
}
|
|
|
|
m_has_quantifiers |= ::has_quantifiers(e);
|
|
|
|
push_assertion(r, pr, m_formulas);
|
|
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
|
|
}
|
|
|
|
void asserted_formulas::assert_expr(expr * e) {
|
|
assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr);
|
|
}
|
|
|
|
void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
|
|
for (justified_expr const& je : m_formulas) result.push_back(je.fml());
|
|
}
|
|
|
|
void asserted_formulas::push_scope() {
|
|
++m_lazy_scopes;
|
|
}
|
|
|
|
void asserted_formulas::push_scope_core() {
|
|
reduce();
|
|
commit();
|
|
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
|
|
TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n");
|
|
m_scoped_substitution.push();
|
|
m_scopes.push_back(scope());
|
|
scope & s = m_scopes.back();
|
|
s.m_formulas_lim = m_formulas.size();
|
|
SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
|
|
s.m_inconsistent_old = m_inconsistent;
|
|
m_defined_names.push();
|
|
m_elim_term_ite.push();
|
|
m_bv_sharing.push_scope();
|
|
m_macro_manager.push_scope();
|
|
m_bv_size_reduce.push_scope();
|
|
commit();
|
|
TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n");
|
|
}
|
|
|
|
void asserted_formulas::force_push() {
|
|
for (; m_lazy_scopes > 0; --m_lazy_scopes)
|
|
push_scope_core();
|
|
}
|
|
|
|
void asserted_formulas::pop_scope(unsigned num_scopes) {
|
|
if (num_scopes <= m_lazy_scopes) {
|
|
m_lazy_scopes -= num_scopes;
|
|
return;
|
|
}
|
|
num_scopes -= m_lazy_scopes;
|
|
m_lazy_scopes = 0;
|
|
|
|
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
|
|
m_bv_sharing.pop_scope(num_scopes);
|
|
m_macro_manager.pop_scope(num_scopes);
|
|
m_bv_size_reduce.pop_scope(num_scopes);
|
|
unsigned new_lvl = m_scopes.size() - num_scopes;
|
|
scope & s = m_scopes[new_lvl];
|
|
m_inconsistent = s.m_inconsistent_old;
|
|
m_defined_names.pop(num_scopes);
|
|
m_elim_term_ite.pop(num_scopes);
|
|
m_scoped_substitution.pop(num_scopes);
|
|
m_formulas.shrink(s.m_formulas_lim);
|
|
m_qhead = s.m_formulas_lim;
|
|
m_scopes.shrink(new_lvl);
|
|
flush_cache();
|
|
TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";);
|
|
}
|
|
|
|
void asserted_formulas::reset() {
|
|
m_defined_names.reset();
|
|
m_qhead = 0;
|
|
m_formulas.reset();
|
|
m_macro_manager.reset();
|
|
m_bv_sharing.reset();
|
|
m_rewriter.reset();
|
|
m_inconsistent = false;
|
|
}
|
|
|
|
void asserted_formulas::finalize() {
|
|
reset();
|
|
m_substitution.cleanup();
|
|
}
|
|
|
|
bool asserted_formulas::check_well_sorted() const {
|
|
for (justified_expr const& je : m_formulas) {
|
|
if (!is_well_sorted(m, je.fml())) return false;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void asserted_formulas::reduce() {
|
|
if (inconsistent())
|
|
return;
|
|
if (canceled())
|
|
return;
|
|
if (m_qhead == m_formulas.size())
|
|
return;
|
|
if (!m_has_quantifiers && !m_smt_params.m_preprocess)
|
|
return;
|
|
if (m_macro_manager.has_macros())
|
|
invoke(m_find_macros);
|
|
|
|
TRACE("before_reduce", display(tout););
|
|
CASSERT("well_sorted", check_well_sorted());
|
|
|
|
IF_VERBOSE(10, verbose_stream() << "(smt.simplify-begin :num-exprs " << get_total_size() << ")\n";);
|
|
|
|
set_eliminate_and(false); // do not eliminate and before nnf.
|
|
if (!invoke(m_propagate_values)) return;
|
|
if (!invoke(m_find_macros)) return;
|
|
if (!invoke(m_nnf_cnf)) return;
|
|
set_eliminate_and(true);
|
|
if (!invoke(m_reduce_asserted_formulas)) return;
|
|
if (!invoke(m_pull_nested_quantifiers)) return;
|
|
if (!invoke(m_lift_ite)) return;
|
|
m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
|
|
m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
|
|
if (!invoke(m_ng_lift_ite)) return;
|
|
if (!invoke(m_elim_term_ite)) return;
|
|
if (!invoke(m_qe_lite)) return;
|
|
if (!invoke(m_refine_inj_axiom)) return;
|
|
if (!invoke(m_distribute_forall)) return;
|
|
if (!invoke(m_find_macros)) return;
|
|
if (!invoke(m_apply_quasi_macros)) return;
|
|
if (!invoke(m_apply_bit2int)) return;
|
|
if (!invoke(m_bv_size_reduce)) return;
|
|
if (!invoke(m_cheap_quant_fourier_motzkin)) return;
|
|
if (!invoke(m_pattern_inference)) return;
|
|
if (!invoke(m_max_bv_sharing_fn)) return;
|
|
if (!invoke(m_elim_bvs_from_quantifiers)) return;
|
|
if (!invoke(m_reduce_asserted_formulas)) return;
|
|
if (!invoke(m_flatten_clauses)) return;
|
|
// if (!invoke(m_propagate_values)) return;
|
|
|
|
IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done :num-exprs " << get_total_size() << ")\n";);
|
|
TRACE("after_reduce", display(tout););
|
|
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
|
|
TRACE("macros", m_macro_manager.display(tout););
|
|
flush_cache();
|
|
CASSERT("well_sorted",check_well_sorted());
|
|
|
|
}
|
|
|
|
|
|
unsigned asserted_formulas::get_formulas_last_level() const {
|
|
if (m_scopes.empty()) {
|
|
return 0;
|
|
}
|
|
else {
|
|
return m_scopes.back().m_formulas_lim;
|
|
}
|
|
}
|
|
|
|
bool asserted_formulas::invoke(simplify_fmls& s) {
|
|
if (!s.should_apply()) return true;
|
|
s();
|
|
IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << " :num-exprs " << get_total_size() << ")\n";);
|
|
IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
|
|
TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
|
|
CASSERT("well_sorted",check_well_sorted());
|
|
TRACE("after_reduce", display(tout << s.id() << "\n"););
|
|
if (inconsistent() || canceled()) {
|
|
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
|
|
return false;
|
|
}
|
|
else {
|
|
return true;
|
|
}
|
|
}
|
|
|
|
void asserted_formulas::display(std::ostream & out) const {
|
|
out << "asserted formulas:\n";
|
|
for (unsigned i = 0; i < m_formulas.size(); i++) {
|
|
if (i == m_qhead)
|
|
out << "[HEAD] ==>\n";
|
|
out << mk_pp(m_formulas[i].fml(), m) << "\n";
|
|
}
|
|
out << "inconsistent: " << inconsistent() << "\n";
|
|
}
|
|
|
|
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.fml(), pp_visited, true, false);
|
|
out << "asserted formulas:\n";
|
|
for (justified_expr const& f : m_formulas)
|
|
out << "#" << f.fml()->get_id() << " ";
|
|
out << "\n";
|
|
}
|
|
}
|
|
|
|
void asserted_formulas::collect_statistics(statistics & st) const {
|
|
}
|
|
|
|
|
|
void asserted_formulas::swap_asserted_formulas(vector<justified_expr>& formulas) {
|
|
SASSERT(!inconsistent() || !formulas.empty());
|
|
m_formulas.shrink(m_qhead);
|
|
m_formulas.append(formulas);
|
|
}
|
|
|
|
|
|
void asserted_formulas::find_macros_core() {
|
|
vector<justified_expr> new_fmls;
|
|
unsigned sz = m_formulas.size();
|
|
(*m_macro_finder)(sz - m_qhead, m_formulas.data() + m_qhead, new_fmls);
|
|
swap_asserted_formulas(new_fmls);
|
|
reduce_and_solve();
|
|
}
|
|
|
|
/**
|
|
\brief rewrite (a or (b & c)) to (a or b), (a or c) if the reference count of (b & c) is 1.
|
|
This avoids the literal for (b & c)
|
|
*/
|
|
void asserted_formulas::flatten_clauses() {
|
|
if (m.proofs_enabled()) return;
|
|
bool change = true;
|
|
vector<justified_expr> new_fmls;
|
|
auto mk_not = [this](expr* e) { return m.is_not(e, e) ? e : m.mk_not(e); };
|
|
auto is_literal = [this](expr *e) { m.is_not(e, e); return !is_app(e) || to_app(e)->get_num_args() == 0; };
|
|
expr *a = nullptr, *b = nullptr, *c = nullptr;
|
|
while (change) {
|
|
change = false;
|
|
new_fmls.reset();
|
|
unsigned sz = m_formulas.size();
|
|
for (unsigned i = m_qhead; i < sz; ++i) {
|
|
auto const& j = m_formulas.get(i);
|
|
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;
|
|
}
|
|
else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
|
|
decomposed = true;
|
|
}
|
|
if (decomposed) {
|
|
for (expr* arg : *to_app(b)) {
|
|
justified_expr j1(m, m.mk_or(a, mk_not(arg)), nullptr);
|
|
new_fmls.push_back(j1);
|
|
}
|
|
change = true;
|
|
continue;
|
|
}
|
|
if (m.is_ite(f, a, b, c)) {
|
|
new_fmls.push_back(justified_expr(m, m.mk_or(mk_not(a), b), nullptr));
|
|
new_fmls.push_back(justified_expr(m, m.mk_or(a, c), nullptr));
|
|
change = true;
|
|
continue;
|
|
}
|
|
new_fmls.push_back(j);
|
|
}
|
|
swap_asserted_formulas(new_fmls);
|
|
}
|
|
}
|
|
|
|
|
|
void asserted_formulas::apply_quasi_macros() {
|
|
TRACE("before_quasi_macros", display(tout););
|
|
vector<justified_expr> new_fmls;
|
|
quasi_macros proc(m, m_macro_manager);
|
|
while (m_qhead == 0 &&
|
|
proc(m_formulas.size() - m_qhead,
|
|
m_formulas.data() + m_qhead,
|
|
new_fmls)) {
|
|
swap_asserted_formulas(new_fmls);
|
|
new_fmls.reset();
|
|
}
|
|
TRACE("after_quasi_macros", display(tout););
|
|
reduce_and_solve();
|
|
}
|
|
|
|
void asserted_formulas::nnf_cnf() {
|
|
nnf apply_nnf(m, m_defined_names);
|
|
vector<justified_expr> new_fmls;
|
|
expr_ref_vector push_todo(m);
|
|
proof_ref_vector push_todo_prs(m);
|
|
|
|
unsigned i = m_qhead;
|
|
unsigned sz = m_formulas.size();
|
|
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
|
|
for (; i < sz; i++) {
|
|
expr * n = m_formulas[i].fml();
|
|
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
|
|
proof_ref pr(m_formulas[i].pr(), m);
|
|
expr_ref r1(m);
|
|
proof_ref pr1(m);
|
|
push_todo.reset();
|
|
push_todo_prs.reset();
|
|
CASSERT("well_sorted", is_well_sorted(m, n));
|
|
apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
|
|
CASSERT("well_sorted",is_well_sorted(m, r1));
|
|
pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr;
|
|
push_todo.push_back(r1);
|
|
push_todo_prs.push_back(pr);
|
|
|
|
if (canceled()) {
|
|
return;
|
|
}
|
|
unsigned sz2 = push_todo.size();
|
|
for (unsigned k = 0; k < sz2; k++) {
|
|
expr * n = push_todo.get(k);
|
|
pr = nullptr;
|
|
m_rewriter(n, r1, pr1);
|
|
CASSERT("well_sorted",is_well_sorted(m, r1));
|
|
if (canceled()) {
|
|
return;
|
|
}
|
|
if (m.proofs_enabled())
|
|
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
|
|
push_assertion(r1, pr, new_fmls);
|
|
}
|
|
}
|
|
swap_asserted_formulas(new_fmls);
|
|
}
|
|
|
|
void asserted_formulas::simplify_fmls::operator()() {
|
|
vector<justified_expr> new_fmls;
|
|
unsigned sz = af.m_formulas.size();
|
|
for (unsigned i = af.m_qhead; i < sz; i++) {
|
|
auto& j = af.m_formulas[i];
|
|
expr_ref result(m);
|
|
proof_ref result_pr(m);
|
|
simplify(j, result, result_pr);
|
|
if (m.proofs_enabled()) {
|
|
if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result);
|
|
result_pr = m.mk_modus_ponens(j.pr(), result_pr);
|
|
}
|
|
if (j.fml() == result) {
|
|
new_fmls.push_back(j);
|
|
}
|
|
else {
|
|
af.push_assertion(result, result_pr, new_fmls);
|
|
}
|
|
if (af.canceled())
|
|
return;
|
|
}
|
|
af.swap_asserted_formulas(new_fmls);
|
|
TRACE("asserted_formulas", af.display(tout););
|
|
post_op();
|
|
}
|
|
|
|
|
|
void asserted_formulas::reduce_and_solve() {
|
|
flush_cache(); // collect garbage
|
|
m_reduce_asserted_formulas();
|
|
IF_VERBOSE(10, verbose_stream() << "(smt.reduced " << get_total_size() << ")\n";);
|
|
}
|
|
|
|
|
|
void asserted_formulas::commit() {
|
|
commit(m_formulas.size());
|
|
}
|
|
|
|
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.fml(), j.pr());
|
|
}
|
|
m_qhead = new_qhead;
|
|
}
|
|
|
|
void asserted_formulas::propagate_values() {
|
|
if (m.proofs_enabled())
|
|
return;
|
|
flush_cache();
|
|
|
|
unsigned num_prop = 0;
|
|
unsigned sz = m_formulas.size();
|
|
unsigned delta_prop = sz;
|
|
while (!inconsistent() && sz/20 < delta_prop) {
|
|
m_scoped_substitution.push();
|
|
unsigned prop = num_prop;
|
|
TRACE("propagate_values", display(tout << "before:\n"););
|
|
unsigned i = m_qhead;
|
|
for (; i < sz; i++) {
|
|
prop += propagate_values(i);
|
|
}
|
|
flush_cache();
|
|
m_scoped_substitution.pop(1);
|
|
m_scoped_substitution.push();
|
|
TRACE("propagate_values", tout << "middle:\n"; display(tout););
|
|
i = sz;
|
|
while (i > m_qhead) {
|
|
--i;
|
|
prop += propagate_values(i);
|
|
}
|
|
m_scoped_substitution.pop(1);
|
|
flush_cache();
|
|
TRACE("propagate_values", tout << "after:\n"; display(tout););
|
|
delta_prop = prop - num_prop;
|
|
num_prop = prop;
|
|
if (sz <= m_formulas.size())
|
|
break;
|
|
sz = m_formulas.size();
|
|
}
|
|
TRACE("asserted_formulas", tout << num_prop << "\n";);
|
|
if (num_prop > 0)
|
|
m_reduce_asserted_formulas();
|
|
}
|
|
|
|
unsigned asserted_formulas::propagate_values(unsigned i) {
|
|
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].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.fml())) {
|
|
m_inconsistent = true;
|
|
}
|
|
update_substitution(new_n, new_pr);
|
|
return (n != new_n) ? 1 : 0;
|
|
}
|
|
|
|
bool asserted_formulas::update_substitution(expr* n, proof* pr) {
|
|
expr* lhs, *rhs, *n1;
|
|
proof_ref pr1(m);
|
|
if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
|
|
if (is_gt(lhs, rhs)) {
|
|
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
|
|
m_scoped_substitution.insert(lhs, rhs, pr);
|
|
return true;
|
|
}
|
|
if (is_gt(rhs, lhs)) {
|
|
TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
|
|
pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr;
|
|
m_scoped_substitution.insert(rhs, lhs, pr1);
|
|
return true;
|
|
}
|
|
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
|
|
}
|
|
if (m.is_not(n, n1)) {
|
|
pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr;
|
|
m_scoped_substitution.insert(n1, m.mk_false(), pr1);
|
|
}
|
|
else {
|
|
pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr;
|
|
m_scoped_substitution.insert(n, m.mk_true(), pr1);
|
|
}
|
|
return false;
|
|
}
|
|
|
|
|
|
/**
|
|
\brief implement a Knuth-Bendix ordering on expressions.
|
|
*/
|
|
|
|
bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
|
|
if (lhs == rhs) {
|
|
return false;
|
|
}
|
|
// values are always less in ordering than non-values.
|
|
bool v1 = m.is_value(lhs);
|
|
bool v2 = m.is_value(rhs);
|
|
if (!v1 && v2) {
|
|
return true;
|
|
}
|
|
if (v1 && !v2) {
|
|
return false;
|
|
}
|
|
SASSERT(is_ground(lhs) && is_ground(rhs));
|
|
if (depth(lhs) > depth(rhs)) {
|
|
return true;
|
|
}
|
|
if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) {
|
|
app* l = to_app(lhs);
|
|
app* r = to_app(rhs);
|
|
if (l->get_decl()->get_id() != r->get_decl()->get_id()) {
|
|
return l->get_decl()->get_id() > r->get_decl()->get_id();
|
|
}
|
|
if (l->get_num_args() != r->get_num_args()) {
|
|
return l->get_num_args() > r->get_num_args();
|
|
}
|
|
for (unsigned i = 0; i < l->get_num_args(); ++i) {
|
|
if (l->get_arg(i) != r->get_arg(i)) {
|
|
return is_gt(l->get_arg(i), r->get_arg(i));
|
|
}
|
|
}
|
|
UNREACHABLE();
|
|
}
|
|
|
|
return false;
|
|
}
|
|
|
|
proof * asserted_formulas::get_inconsistency_proof() const {
|
|
if (!inconsistent())
|
|
return nullptr;
|
|
if (!m.proofs_enabled())
|
|
return nullptr;
|
|
if (!m.inc())
|
|
return nullptr;
|
|
for (justified_expr const& j : m_formulas) {
|
|
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.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.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.fml();
|
|
expr* a, *b, *x;
|
|
unsigned lo, hi;
|
|
rational r;
|
|
expr_ref new_term(m);
|
|
auto check_reduce = [&](expr* a, expr* b) {
|
|
if (bv.is_extract(a, lo, hi, x) && lo > 0 && hi + 1 == bv.get_bv_size(x) && bv.is_numeral(b, r) && r == 0) {
|
|
// 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.fml();
|
|
return true;
|
|
}
|
|
return false;
|
|
};
|
|
if (m.is_eq(f, a, b) && (check_reduce(a, b) || check_reduce(b, a))) {
|
|
// done
|
|
}
|
|
else {
|
|
n = j.fml();
|
|
m_sub(n);
|
|
}
|
|
}
|
|
|
|
void asserted_formulas::bv_size_reduce_fn::push_scope() {
|
|
m_sub.push_scope();
|
|
}
|
|
|
|
void asserted_formulas::bv_size_reduce_fn::pop_scope(unsigned n) {
|
|
m_sub.pop_scope(n);
|
|
}
|
|
|
|
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.fml(), visited);
|
|
return r;
|
|
}
|
|
|
|
|
|
#ifdef Z3DEBUG
|
|
#include <iostream>
|
|
void pp(asserted_formulas & f) {
|
|
f.display(std::cout);
|
|
}
|
|
#endif
|