diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index f684879ae..66b56d8d4 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -1054,7 +1054,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { ptr_vector ql; - decl_collector decls(m_manager); + ast_manager& m = m_manager; + decl_collector decls(m); smt_renaming rn; for (unsigned i = 0; i < m_assumptions.size(); ++i) { @@ -1065,7 +1066,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { } decls.visit(n); - if (m_manager.is_proof(n)) { + if (m.is_proof(n)) { strm << "("; } if (m_benchmark_name != symbol::null) { @@ -1074,7 +1075,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { if (m_source_info != symbol::null && m_source_info != symbol("")) { strm << "; :source { " << m_source_info << " }\n"; } - if (m_manager.is_bool(n)) { + if (m.is_bool(n)) { strm << "(set-info :status " << m_status << ")\n"; } if (m_category != symbol::null && m_category != symbol("")) { @@ -1091,7 +1092,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { sort* s = decls.get_sorts()[i]; if (!(*m_is_declared)(s)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p.pp_sort_decl(sort_mark, s); } } @@ -1099,7 +1100,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_decls(); ++i) { func_decl* d = decls.get_func_decls()[i]; if (!(*m_is_declared)(d)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); strm << "\n"; } @@ -1108,34 +1109,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_preds(); ++i) { func_decl* d = decls.get_pred_decls()[i]; if (!(*m_is_declared)(d)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); strm << "\n"; } } for (unsigned i = 0; i < m_assumptions.size(); ++i) { - strm << "(assert\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - p(m_assumptions[i].get()); - strm << ")\n"; + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); + strm << "(assert\n "; + p(m_assumptions[i].get()); + strm << ")\n"; } for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - strm << "(assert\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - p(m_assumptions_star[i].get()); + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); + strm << "(assert\n "; + p(m_assumptions_star[i].get()); strm << ")\n"; } - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - if (m_manager.is_bool(n)) { - strm << "(assert\n"; - p(n); - strm << ")\n"; + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0); + if (m.is_bool(n)) { + if (!m.is_true(n)) { + strm << "(assert\n "; + p(n); + strm << ")\n"; + } strm << "(check-sat)\n"; } - else if (m_manager.is_proof(n)) { + else if (m.is_proof(n)) { strm << "(proof\n"; p(n); strm << "))\n"; diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 42f410761..77eb108a9 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -48,6 +48,7 @@ namespace opt { expr_ref_vector m_aux; expr_ref_vector m_assignment; unsigned m_upper_size; + solver & m_original_solver; bool m_use_new_bv_solver; diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index 3aa72baef..5b3a95e46 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -172,7 +172,7 @@ namespace smt { if (!args.empty()) { unsigned g = abs(args[0].second); for (unsigned i = 1; g > 1 && i < args.size(); ++i) { - g = gcd(g, args[i].second); + g = gcd(g, abs(args[i].second)); } if (g > 1) { int k = c->m_k; @@ -184,7 +184,7 @@ namespace smt { k = abs(k); k += (k % g); k /= g; - k = -k; + c->m_k = -k; } for (unsigned i = 0; i < args.size(); ++i) { args[i].second /= g; @@ -214,6 +214,7 @@ namespace smt { void theory_card::collect_statistics(::statistics& st) const { st.update("pb axioms", m_stats.m_num_axioms); + st.update("pb propagations", m_stats.m_num_propagations); st.update("pb predicates", m_stats.m_num_predicates); st.update("pb compilations", m_stats.m_num_compiles); } @@ -317,6 +318,21 @@ namespace smt { return curr_min; } + int theory_card::get_max_delta(card& c) { + if (m_util.is_at_most_k(c.m_app)) { + return 1; + } + int max = 0; + context& ctx = get_context(); + for (unsigned i = 0; i < c.m_args.size(); ++i) { + if (c.m_args[i].second > max && ctx.get_assignment(c.m_args[i].first) == l_undef) { + max = c.m_args[i].second; + } + } + return max; + } + + int theory_card::accumulate_max(literal_vector& lits, card& c) { context& ctx = get_context(); arg_t const& args = c.m_args; @@ -365,19 +381,17 @@ namespace smt { lbool aval = ctx.get_assignment(abv); if (min > k && aval != l_false) { literal_vector& lits = get_lits(); - lits.push_back(~literal(abv)); int curr_min = accumulate_min(lits, c); SASSERT(curr_min > k); - add_clause(c, lits); + add_assign(c, lits, ~literal(abv)); } else if (max <= k && aval != l_true) { literal_vector& lits = get_lits(); - lits.push_back(literal(abv)); int curr_max = accumulate_max(lits, c); SASSERT(curr_max <= k); - add_clause(c, lits); + add_assign(c, lits, literal(abv)); } - else if (min == k && aval == l_true) { + else if (min <= k && k < min + get_max_delta(c) && aval == l_true) { literal_vector& lits = get_lits(); lits.push_back(~literal(abv)); int curr_min = accumulate_min(lits, c); @@ -385,37 +399,70 @@ namespace smt { add_clause(c, lits); } else { - SASSERT(curr_min == k); for (unsigned i = 0; i < args.size(); ++i) { bool_var bv = args[i].first; int inc = args[i].second; - if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { - literal_vector lits_save(lits); // add_clause has a side-effect on literals. - lits_save.push_back(literal(bv, inc > 0)); // avoid incrementing min. - add_clause(c, lits_save); + if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc > 0)); } } } } - else if (max == k + 1 && aval == l_false) { + else if (max - get_max_delta(c) <= k && k < max && aval == l_false) { literal_vector& lits = get_lits(); lits.push_back(literal(abv)); int curr_max = accumulate_max(lits, c); if (curr_max <= k) { add_clause(c, lits); } - else if (curr_max == k + 1) { + else { for (unsigned i = 0; i < args.size(); ++i) { bool_var bv = args[i].first; int inc = args[i].second; - if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { - literal_vector lits_save(lits); // add_clause has a side-effect on literals. - lits_save.push_back(literal(bv, inc < 0)); // avoid decrementing max. - add_clause(c, lits_save); + if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc < 0)); } } } } +#if 0 + else if (aval == l_true) { + SASSERT(min < k); + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + bool all_inc = curr_min == k; + unsigned num_incs = 0; + for (unsigned i = 0; all_inc && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + all_inc = inc + min > k; + num_incs++; + } + } + if (num_incs > 0) { + std::cout << "missed T propgations " << num_incs << "\n"; + } + } + else if (aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + bool all_dec = curr_max > k; + unsigned num_decs = 0; + for (unsigned i = 0; all_dec && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + all_dec = inc + max <= k; + num_decs++; + } + } + if (num_decs > 0) { + std::cout << "missed F propgations " << num_decs << "\n"; + } + } +#endif } void theory_card::assign_eh(bool_var v, bool is_true) { @@ -609,10 +656,14 @@ namespace smt { } bool theory_card::should_compile(card& c) { +#if 1 + return false; +#else if (!m_util.is_at_most_k(c.m_app)) { return false; } return c.m_num_propagations >= c.m_compilation_threshold; +#endif } void theory_card::compile_at_most(card& c) { @@ -687,6 +738,19 @@ namespace smt { return m_literals; } + void theory_card::add_assign(card& c, literal_vector const& lits, literal l) { + literal_vector ls; + ++c.m_num_propagations; + m_stats.m_num_propagations++; + context& ctx = get_context(); + for (unsigned i = 0; i < lits.size(); ++i) { + ls.push_back(~lits[i]); + } + ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l))); + } + + + void theory_card::add_clause(card& c, literal_vector const& lits) { ++c.m_num_propagations; m_stats.m_num_axioms++; @@ -694,7 +758,8 @@ namespace smt { TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); - IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr()); + IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), + lits.size(), lits.c_ptr()); verbose_stream() << "\n";); // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } diff --git a/src/smt/theory_card.h b/src/smt/theory_card.h index e8eae9232..a432ea5a3 100644 --- a/src/smt/theory_card.h +++ b/src/smt/theory_card.h @@ -32,6 +32,7 @@ namespace smt { struct stats { unsigned m_num_axioms; + unsigned m_num_propagations; unsigned m_num_predicates; unsigned m_num_compiles; void reset() { memset(this, 0, sizeof(*this)); } @@ -75,10 +76,12 @@ namespace smt { void add_card(card* c); void add_clause(card& c, literal_vector const& lits); + void add_assign(card& c, literal_vector const& lits, literal l); literal_vector& get_lits(); int find_inc(bool_var bv, svector >const& vars); void propagate_assignment(card& c); + int get_max_delta(card& c); int accumulate_max(literal_vector& lits, card& c); int accumulate_min(literal_vector& lits, card& c); lbool dec_max(int inc, lbool val); diff --git a/src/util/region.h b/src/util/region.h index 7f6bc787e..5be2ae4d3 100644 --- a/src/util/region.h +++ b/src/util/region.h @@ -53,6 +53,7 @@ public: m_scopes.push_back(m_chuncks.size()); } + void pop_scope() { unsigned old_size = m_scopes.back(); m_scopes.pop_back();