mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-10-09 19:17:44 +01:00
parent 3edf147213
commit 5819e38606
1 changed files with 45 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

90
src/smt/asserted_formulas.cpp
View file

@ -38,7 +38,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_qhead(0),
m_macro_manager(m),
m_bv_sharing(m),
m_inconsistent(false),
m_inconsistent(false),
m_has_quantifiers(false),
m_reduce_asserted_formulas(*this),
m_distribute_forall(*this),
@ -54,8 +54,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_lift_ite(*this),
m_ng_lift_ite(*this),
m_find_macros(*this),
m_propagate_values(*this),
m_nnf_cnf(*this),
m_propagate_values(*this),
m_nnf_cnf(*this),
m_apply_quasi_macros(*this) {
m_macro_finder = alloc(macro_finder, m, m_macro_manager);
@ -68,7 +68,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
void asserted_formulas::setup() {
switch (m_params.m_lift_ite) {
case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE;
m_params.m_ng_lift_ite = LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
@ -77,7 +77,7 @@ void asserted_formulas::setup() {
default:
break;
}
if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false;
}
@ -93,7 +93,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* e1 = 0;
if (m.is_false(e)) {
result.push_back(justified_expr(m, e, pr));
m_inconsistent = true;
m_inconsistent = true;
}
else if (m.is_true(e)) {
// skip
@ -110,8 +110,8 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* arg = to_app(e1)->get_arg(i);
proof_ref _pr(m.mk_not_or_elim(pr, i), m);
expr_ref narg(mk_not(m, arg), m);
push_assertion(narg, _pr, result);
}
push_assertion(narg, _pr, result);
}
}
else {
result.push_back(justified_expr(m, e, pr));
@ -139,7 +139,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
proof_ref in_pr(_in_pr, m), pr(_in_pr, m);
expr_ref r(e, m);
if (inconsistent())
if (inconsistent())
return;
m_has_quantifiers |= ::has_quantifiers(e);
@ -183,7 +183,7 @@ void asserted_formulas::push_scope() {
commit();
TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
}
void asserted_formulas::pop_scope(unsigned num_scopes) {
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
m_bv_sharing.pop_scope(num_scopes);
@ -212,7 +212,7 @@ void asserted_formulas::reset() {
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.get_fml())) return false;
}
return true;
}
@ -224,20 +224,20 @@ void asserted_formulas::reduce() {
return;
if (m_qhead == m_formulas.size())
return;
if (!m_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
if (!m_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());
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_reduce_asserted_formulas)) return;
if (!invoke(m_pull_cheap_ite_trees)) return;
if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) return;
@ -276,14 +276,14 @@ bool asserted_formulas::invoke(simplify_fmls& s) {
if (!s.should_apply()) return true;
IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
s();
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());
if (inconsistent() || canceled()) {
TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
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());
if (inconsistent() || canceled()) {
TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
return false;
}
}
else {
return true;
}
@ -301,10 +301,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)
for (justified_expr const& f : m_formulas)
ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
out << "asserted formulas:\n";
for (justified_expr const& f : m_formulas)
for (justified_expr const& f : m_formulas)
out << "#" << f.get_fml()->get_id() << " ";
out << "\n";
}
@ -332,9 +332,9 @@ void asserted_formulas::find_macros_core() {
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 (proc(m_formulas.size() - m_qhead,
m_formulas.c_ptr() + m_qhead,
quasi_macros proc(m, m_macro_manager);
while (proc(m_formulas.size() - m_qhead,
m_formulas.c_ptr() + m_qhead,
new_fmls)) {
swap_asserted_formulas(new_fmls);
new_fmls.reset();
@ -348,7 +348,7 @@ void asserted_formulas::nnf_cnf() {
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";);
@ -378,7 +378,7 @@ void asserted_formulas::nnf_cnf() {
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);
@ -389,8 +389,8 @@ void asserted_formulas::nnf_cnf() {
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++) {
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);
@ -406,8 +406,8 @@ void asserted_formulas::simplify_fmls::operator()() {
af.push_assertion(result, result_pr, new_fmls);
}
if (af.canceled()) return;
}
af.swap_asserted_formulas(new_fmls);
}
af.swap_asserted_formulas(new_fmls);
TRACE("asserted_formulas", af.display(tout););
post_op();
}
@ -473,12 +473,12 @@ void asserted_formulas::propagate_values() {
unsigned asserted_formulas::propagate_values(unsigned i) {
expr_ref n(m_formulas[i].get_fml(), m);
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
if (m.proofs_enabled()) {
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();
new_pr = m.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
@ -510,10 +510,10 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
}
else {
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
}
}
@ -554,13 +554,13 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
}
UNREACHABLE();
}
return false;
}
void asserted_formulas::compute_depth(expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
unsigned d = 0;
@ -603,7 +603,7 @@ proof * asserted_formulas::get_inconsistency_proof() const {
return 0;
}
void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
expr* f = j.get_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";);