From 7b8101c502e41930ec0e4d0217311eb2a2790c57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jan 2018 12:25:24 -0800 Subject: [PATCH] fix bugs related to model-converter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 12 ++ src/cmd_context/basic_cmds.cpp | 12 +- src/cmd_context/cmd_context.cpp | 11 +- src/cmd_context/cmd_context.h | 2 +- src/cmd_context/eval_cmd.cpp | 8 +- src/parsers/smt2/smt2parser.cpp | 10 +- src/sat/ba_solver.cpp | 11 +- src/sat/ba_solver.h | 1 + src/sat/sat_model_converter.cpp | 1 + src/sat/sat_scc.cpp | 2 +- src/sat/sat_simplifier.cpp | 13 +- src/sat/sat_solver.cpp | 13 +- src/sat/sat_solver.h | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 51 +++++--- src/sat/tactic/goal2sat.cpp | 20 ++- src/tactic/generic_model_converter.cpp | 115 ++++++++++++------ src/tactic/generic_model_converter.h | 12 +- .../portfolio/bounded_int2bv_solver.cpp | 5 +- src/tactic/portfolio/enum2bv_solver.cpp | 5 +- src/tactic/portfolio/pb2bv_solver.cpp | 17 ++- 20 files changed, 211 insertions(+), 112 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 0a0fed292..d4aa5ad3e 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -39,6 +39,8 @@ struct pb2bv_rewriter::imp { func_decl_ref_vector m_fresh; // all fresh variables unsigned_vector m_fresh_lim; unsigned m_num_translated; + unsigned m_compile_bv; + unsigned m_compile_card; struct card2bv_rewriter { typedef expr* literal; @@ -526,6 +528,7 @@ struct pb2bv_rewriter::imp { } expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) { + ++m_imp.m_compile_bv; decl_kind kind = f->get_decl_kind(); rational k = pb.get_k(f); m_coeffs.reset(); @@ -735,22 +738,27 @@ struct pb2bv_rewriter::imp { else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) { if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false; result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args); + ++m_imp.m_compile_card; } else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) { if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false; result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args); + ++m_imp.m_compile_card; } else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false; result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args); + ++m_imp.m_compile_card; } else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false; result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args); + ++m_imp.m_compile_card; } else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false; result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args); + ++m_imp.m_compile_card; } else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) { return false; @@ -909,6 +917,8 @@ struct pb2bv_rewriter::imp { m_num_translated(0), m_rw(*this, m) { updt_params(p); + m_compile_bv = 0; + m_compile_card = 0; } void updt_params(params_ref const & p) { @@ -953,6 +963,8 @@ struct pb2bv_rewriter::imp { } void collect_statistics(statistics & st) const { + st.update("pb-compile-bv", m_compile_bv); + st.update("pb-compile-card", m_compile_card); st.update("pb-aux-variables", m_fresh.size()); st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses); } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 65c8860b1..88c5cb257 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -109,15 +109,12 @@ public: virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } virtual void execute(cmd_context & ctx) { - if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); model_ref m; + if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0) + throw cmd_exception("model is not available"); if (m_index > 0 && ctx.get_opt()) { ctx.get_opt()->get_box_model(m, m_index); } - else { - ctx.get_check_sat_result()->get_model(m); - } ctx.display_model(m); } virtual void reset(cmd_context& ctx) { @@ -127,10 +124,9 @@ public: ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { - if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); model_ref m; - ctx.get_check_sat_result()->get_model(m); + if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0) + throw cmd_exception("model is not available"); ctx.regular_stream() << "("; dictionary const & macros = ctx.get_macros(); bool first = true; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8d23c5ef4..93d83d2a4 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1696,11 +1696,11 @@ struct contains_underspecified_op_proc { \brief Complete the model if necessary. */ void cmd_context::complete_model() { - if (!is_model_available() || + model_ref md; + if (!is_model_available(md) || gparams::get_value("model.completion") != "true") return; - model_ref md; get_check_sat_result()->get_model(md); SASSERT(md.get() != 0); params_ref p; @@ -1765,11 +1765,11 @@ void cmd_context::complete_model() { \brief Check if the current model satisfies the quantifier free formulas. */ void cmd_context::validate_model() { + model_ref md; if (!validate_model_enabled()) return; - if (!is_model_available()) + if (!is_model_available(md)) return; - model_ref md; get_check_sat_result()->get_model(md); SASSERT(md.get() != 0); params_ref p; @@ -1897,11 +1897,10 @@ void cmd_context::display_assertions() { regular_stream() << ")" << std::endl; } -bool cmd_context::is_model_available() const { +bool cmd_context::is_model_available(model_ref& md) const { if (produce_models() && has_manager() && (cs_state() == css_sat || cs_state() == css_unknown)) { - model_ref md; get_check_sat_result()->get_model(md); return md.get() != 0; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 440c17285..dc85ad2e0 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -445,7 +445,7 @@ public: model_converter* get_model_converter() { return m_mc0.get(); } - bool is_model_available() const; + bool is_model_available(model_ref& md) const; double get_seconds() const { return m_watch.get_seconds(); } diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index 9d3c1ced3..00aabfff3 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -56,16 +56,14 @@ public: } virtual void execute(cmd_context & ctx) { - if (!ctx.is_model_available()) + model_ref md; + if (!ctx.is_model_available(md)) throw cmd_exception("model is not available"); if (!m_target) throw cmd_exception("no arguments passed to eval"); - model_ref md; unsigned index = m_params.get_uint("model_index", 0); - check_sat_result * last_result = ctx.get_check_sat_result(); - SASSERT(last_result); if (index == 0 || !ctx.get_opt()) { - last_result->get_model(md); + // already have model. } else { ctx.get_opt()->get_box_model(md, index); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 4facbc41c..b2fc7d0c7 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2593,15 +2593,11 @@ namespace smt2 { } check_rparen("invalid get-value command, ')' expected"); - if (!m_ctx.is_model_available() || m_ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); model_ref md; - if (index == 0) { - m_ctx.get_check_sat_result()->get_model(md); - } - else { + if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == 0) + throw cmd_exception("model is not available"); + if (index != 0) { m_ctx.get_opt()->get_box_model(md, index); - } m_ctx.regular_stream() << "("; expr ** expr_it = expr_stack().c_ptr() + spos; diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 4099693c5..5868c4289 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1139,8 +1139,7 @@ namespace sat { if (m_overflow || offset > (1 << 12)) { IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n"; - active2pb(m_A); - display(verbose_stream(), m_A);); + DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A););); goto bail_out; } @@ -1148,7 +1147,7 @@ namespace sat { goto process_next_resolvent; } - TRACE("sat_verbose", display(tout, m_A);); + DEBUG_CODE(TRACE("sat_verbose", display(tout, m_A););); TRACE("ba", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";); SASSERT(offset > 0); @@ -1248,9 +1247,8 @@ namespace sat { DEBUG_CODE( active2pb(m_C); VERIFY(validate_resolvent()); - m_A = m_C;); - - TRACE("ba", display(tout << "conflict: ", m_A);); + m_A = m_C; + TRACE("ba", display(tout << "conflict: ", m_A););); cut(); @@ -1528,6 +1526,7 @@ namespace sat { ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); + m_num_propagations_since_pop = 0; } ba_solver::~ba_solver() { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index cd2e941ce..6e5c00e38 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -198,6 +198,7 @@ namespace sat { literal_vector m_lits; svector m_coeffs; uint64 m_k; + ineq(): m_k(0) {} void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; } void push(literal l, uint64 c) { m_lits.push_back(l); m_coeffs.push_back(c); } }; diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index cc6614621..ce059a07b 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -325,6 +325,7 @@ namespace sat { } void model_converter::flush(model_converter & src) { + VERIFY(this != &src); m_entries.append(src.m_entries); src.m_entries.reset(); } diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 960174e79..4bd16c5c5 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -275,7 +275,7 @@ namespace sat { } void scc::collect_statistics(statistics & st) const { - st.update("elim bool vars", m_num_elim); + st.update("elim bool vars scc", m_num_elim); st.update("elim binary", m_num_elim_bin); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index c101e3a29..b983a0da3 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -260,7 +260,6 @@ namespace sat { break; } while (!m_sub_todo.empty()); - bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars; if (m_need_cleanup || vars_eliminated) { @@ -981,17 +980,21 @@ namespace sat { void operator()() { integrity_checker si(s.s); si.check_watches(); - if (s.bce_enabled()) + if (s.bce_enabled()) { block_clauses(); + } si.check_watches(); - if (s.abce_enabled()) + if (s.abce_enabled()) { cce(); + } si.check_watches(); - if (s.cce_enabled()) + if (s.cce_enabled()) { cce(); + } si.check_watches(); - if (s.bca_enabled()) + if (s.bca_enabled()) { bca(); + } si.check_watches(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index de75882af..61e05b3ed 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1566,6 +1566,17 @@ namespace sat { #endif } + unsigned solver::get_hash() const { + unsigned result = 0; + for (clause* cp : m_clauses) { + result = combine_hash(cp->size(), combine_hash(result, cp->id())); + } + for (clause* cp : m_learned) { + result = combine_hash(cp->size(), combine_hash(result, cp->id())); + } + return result; + } + bool solver::set_root(literal l, literal r) { return !m_ext || m_ext->set_root(l, r); } @@ -4032,7 +4043,7 @@ namespace sat { st.update("dyn subsumption resolution", m_dyn_sub_res); st.update("blocked correction sets", m_blocked_corr_sets); st.update("units", m_units); - st.update("elim bool vars", m_elim_var_res); + st.update("elim bool vars res", m_elim_var_res); st.update("elim bool vars bdd", m_elim_var_bdd); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 651eedee8..e37fa3cca 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -538,6 +538,8 @@ namespace sat { private: + unsigned get_hash() const; + typedef hashtable index_set; u_map m_antecedents; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ef85ad921..e0cc8e581 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -18,30 +18,31 @@ Notes: --*/ +#include "ast/ast_pp.h" +#include "ast/ast_translation.h" +#include "ast/ast_util.h" #include "solver/solver.h" -#include "tactic/tactical.h" -#include "sat/sat_solver.h" #include "solver/tactic2solver.h" +#include "tactic/tactical.h" #include "tactic/aig/aig_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/bv/max_bv_sharing_tactic.h" #include "tactic/arith/card2bv_tactic.h" #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/core/simplify_tactic.h" -#include "sat/tactic/goal2sat.h" -#include "ast/ast_pp.h" #include "model/model_smt2_pp.h" +#include "model/model_v2_pp.h" #include "tactic/bv/bit_blaster_model_converter.h" -#include "ast/ast_translation.h" -#include "ast/ast_util.h" #include "tactic/core/propagate_values_tactic.h" +#include "sat/sat_solver.h" #include "sat/sat_params.hpp" +#include "sat/tactic/goal2sat.h" #include "sat/sat_simplifier_params.hpp" // incremental SAT solver. class inc_sat_solver : public solver { ast_manager& m; - sat::solver m_solver; + mutable sat::solver m_solver; goal2sat m_goal2sat; params_ref m_params; expr_ref_vector m_fmls; @@ -62,7 +63,7 @@ class inc_sat_solver : public solver { model_converter_ref m_mc; mutable model_converter_ref m_mc0; mutable obj_hashtable m_inserted_const2bits; - ref m_sat_mc; + mutable ref m_sat_mc; mutable model_converter_ref m_cached_mc; svector m_weights; std::string m_unknown; @@ -382,7 +383,7 @@ public: return r; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { sat::literal_vector ls; u_map lit2var; for (unsigned i = 0; i < vars.size(); ++i) { @@ -410,15 +411,19 @@ public: void init_reason_unknown() { m_unknown = "no reason given"; } - virtual std::string reason_unknown() const { + + std::string reason_unknown() const override { return m_unknown; } - virtual void set_reason_unknown(char const* msg) { + + void set_reason_unknown(char const* msg) override { m_unknown = msg; } - virtual void get_labels(svector & r) { + + void get_labels(svector & r) override { } - virtual unsigned get_num_assertions() const { + + unsigned get_num_assertions() const override { const_cast(this)->convert_internalized(); if (is_internalized() && m_internalized_converted) { return m_internalized_fmls.size(); @@ -427,28 +432,33 @@ public: return m_fmls.size(); } } - virtual expr * get_assertion(unsigned idx) const { + + expr * get_assertion(unsigned idx) const override { if (is_internalized() && m_internalized_converted) { return m_internalized_fmls[idx]; } return m_fmls[idx]; } - virtual unsigned get_num_assumptions() const { + + unsigned get_num_assumptions() const override { return m_asmsf.size(); } - virtual expr * get_assumption(unsigned idx) const { + + expr * get_assumption(unsigned idx) const override { return m_asmsf[idx]; } - virtual model_converter_ref get_model_converter() const { + model_converter_ref get_model_converter() const override { const_cast(this)->convert_internalized(); if (m_cached_mc) return m_cached_mc; if (is_internalized() && m_internalized_converted) { insert_const2bits(); + m_sat_mc->flush_smc(m_solver, m_map); m_cached_mc = m_mc0.get(); m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get()); m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get()); + // IF_VERBOSE(0, m_cached_mc->display(verbose_stream() << "get-model-converter\n");); return m_cached_mc; } else { @@ -804,16 +814,22 @@ private: } } m_model = md; + //IF_VERBOSE(0, model_v2_pp(verbose_stream(), *m_model, true);); if (m_sat_mc) { + // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n");); (*m_sat_mc)(m_model); } insert_const2bits(); if (m_mc0) { + // IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n");); (*m_mc0)(m_model); } TRACE("sat", model_smt2_pp(tout, m, *m_model, 0);); + // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "after\n");); + +#if 0 IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";); for (expr * f : m_fmls) { expr_ref tmp(m); @@ -828,6 +844,7 @@ private: VERIFY(m.is_true(tmp)); } } +#endif } }; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 596712a7b..68d15c48f 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -892,14 +892,15 @@ void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { void sat2goal::mc::flush_gmc() { sat::literal_vector updates; - m_smc.expand(updates); + m_smc.expand(updates); m_smc.reset(); if (!m_gmc) m_gmc = alloc(generic_model_converter, m); // now gmc owns the model converter sat::literal_vector clause; expr_ref_vector tail(m); expr_ref def(m); - for (sat::literal l : updates) { + for (unsigned i = 0; i < updates.size(); ++i) { + sat::literal l = updates[i]; if (l == sat::null_literal) { sat::literal lit0 = clause[0]; for (unsigned i = 1; i < clause.size(); ++i) { @@ -914,6 +915,21 @@ void sat2goal::mc::flush_gmc() { clause.reset(); tail.reset(); } + // short circuit for equivalences: + else if (clause.empty() && tail.empty() && + i + 5 < updates.size() && + updates[i] == ~updates[i + 3] && + updates[i + 1] == ~updates[i + 4] && + updates[i + 2] == sat::null_literal && + updates[i + 5] == sat::null_literal) { + sat::literal r = ~updates[i+1]; + if (l.sign()) { + l.neg(); + r.neg(); + } + m_gmc->add(lit2expr(l), lit2expr(r)); + i += 5; + } else { clause.push_back(l); } diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 47a4b4d48..aa1f1cdc4 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -31,8 +31,8 @@ Notes: void generic_model_converter::add(func_decl * d, expr* e) { struct entry et(d, e, m, ADD); VERIFY(d->get_range() == m.get_sort(e)); - m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size()); - m_add_entries.push_back(et); + m_first_idx.insert_if_not_there(et.m_f, m_entries.size()); + m_entries.push_back(et); } void generic_model_converter::operator()(model_ref & md) { @@ -42,54 +42,86 @@ void generic_model_converter::operator()(model_ref & md) { ev.set_expand_array_equalities(false); expr_ref val(m); unsigned arity; - for (unsigned i = m_hide_entries.size(); i-- > 0; ) { - entry const& e = m_hide_entries[i]; - md->unregister_decl(e.m_f); - } - for (unsigned i = m_add_entries.size(); i-- > 0; ) { - entry const& e = m_add_entries[i]; - ev(e.m_def, val); - TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); - arity = e.m_f->get_arity(); - if (arity == 0) { - md->register_decl(e.m_f, val); - } - else { - func_interp * new_fi = alloc(func_interp, m, arity); - new_fi->set_else(val); - md->register_decl(e.m_f, new_fi); + for (unsigned i = m_entries.size(); i-- > 0; ) { + entry const& e = m_entries[i]; + switch (e.m_instruction) { + case instruction::HIDE: + md->unregister_decl(e.m_f); + break; + case instruction::ADD: + ev(e.m_def, val); +#if 0 + if (e.m_f->get_name() == symbol("XX")) { + IF_VERBOSE(0, verbose_stream() << e.m_f->get_name() << " " << e.m_def << " -> " << val << "\n";); + ptr_vector ts; + ts.push_back(e.m_def); + while (!ts.empty()) { + app* t = to_app(ts.back()); + ts.pop_back(); + if (t->get_num_args() > 0) { + ts.append(t->get_num_args(), t->get_args()); + } + expr_ref tmp(m); + ev(t, tmp); + IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " -> " << tmp << "\n";); + } + } +#endif + TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); + arity = e.m_f->get_arity(); + if (arity == 0) { + expr* old_val = md->get_const_interp(e.m_f); + if (old_val && old_val == val) { + // skip + } + else { + if (old_val) ev.reset(); + md->register_decl(e.m_f, val); + } + } + else { + func_interp * old_val = md->get_func_interp(e.m_f); + if (old_val && old_val->get_else() == val) { + // skip + } + else { + if (old_val) ev.reset(); + func_interp * new_fi = alloc(func_interp, m, arity); + new_fi->set_else(val); + md->register_decl(e.m_f, new_fi); + } + } + break; } } TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md);); } void generic_model_converter::display(std::ostream & out) { - for (entry const& e : m_hide_entries) { - display_del(out, e.m_f); - } - for (entry const& e : m_add_entries) { - display_add(out, m, e.m_f, e.m_def); + for (entry const& e : m_entries) { + switch (e.m_instruction) { + case instruction::HIDE: + display_del(out, e.m_f); + break; + case instruction::ADD: + display_add(out, m, e.m_f, e.m_def); + break; + } } } model_converter * generic_model_converter::translate(ast_translation & translator) { ast_manager& to = translator.to(); generic_model_converter * res = alloc(generic_model_converter, to); - for (entry const& e : m_hide_entries) { - res->m_hide_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); - } - for (entry const& e : m_add_entries) { - res->m_add_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); + for (entry const& e : m_entries) { + res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); } return res; } void generic_model_converter::collect(ast_pp_util& visitor) { m_env = &visitor.env(); - for (entry const& e : m_hide_entries) { - visitor.coll.visit_func(e.m_f); - } - for (entry const& e : m_add_entries) { + for (entry const& e : m_entries) { visitor.coll.visit_func(e.m_f); if (e.m_def) visitor.coll.visit(e.m_def); } @@ -116,8 +148,11 @@ void generic_model_converter::operator()(expr_ref& fml) { if (min_idx == UINT_MAX) return; expr_ref_vector fmls(m); fmls.push_back(fml); - for (unsigned i = m_add_entries.size(); i-- > min_idx;) { - entry const& e = m_add_entries[i]; + for (unsigned i = m_entries.size(); i-- > min_idx;) { + entry const& e = m_entries[i]; + if (e.m_instruction != instruction::ADD) { + continue; + } unsigned arity = e.m_f->get_arity(); if (arity == 0) { fmls.push_back(simplify_def(e)); @@ -139,8 +174,18 @@ void generic_model_converter::operator()(expr_ref& fml) { if (m_first_idx[e.m_f] == i) { m_first_idx.remove(e.m_f); } - m_add_entries.pop_back(); } + unsigned j = min_idx; + for (unsigned i = min_idx; i < m_entries.size(); ++i) { + entry const& e = m_entries[i]; + if (e.m_instruction == instruction::HIDE) { + if (i != j) { + m_entries[j] = e; + } + ++j; + } + } + m_entries.shrink(j); fml = mk_and(fmls); } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 34e9d8166..8d40d55b7 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -30,10 +30,16 @@ class generic_model_converter : public model_converter { instruction m_instruction; entry(func_decl* f, expr* d, ast_manager& m, instruction i): m_f(f, m), m_def(d, m), m_instruction(i) {} + + entry& operator=(entry const& other) { + m_f = other.m_f; + m_def = other.m_def; + m_instruction = other.m_instruction; + return *this; + } }; ast_manager& m; - vector m_add_entries; - vector m_hide_entries; + vector m_entries; obj_map m_first_idx; expr_ref simplify_def(entry const& e); @@ -45,7 +51,7 @@ public: void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } - void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); } + void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); } void add(func_decl * d, expr* e); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index c81d413b8..3e1b5d2f4 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -81,10 +81,9 @@ public: for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f)); for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f)); for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m)); - model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get()); - if (mc) { + if (mc0()) { ast_translation tr(m, dst_m); - result->set_model_converter(mc->translate(tr)); + result->set_model_converter(mc0()->translate(tr)); } return result; } diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index bfe057f82..5db907c2c 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -50,10 +50,9 @@ public: virtual solver* translate(ast_manager& dst_m, params_ref const& p) { solver* result = alloc(enum2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); - model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get()); - if (mc) { + if (mc0()) { ast_translation tr(m, dst_m); - result->set_model_converter(mc->translate(tr)); + result->set_model_converter(mc0()->translate(tr)); } return result; } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index eba10cbd1..cee566ec6 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -16,14 +16,14 @@ Notes: --*/ -#include "tactic/portfolio/pb2bv_solver.h" -#include "solver/solver_na2as.h" -#include "tactic/tactic.h" -#include "ast/rewriter/pb2bv_rewriter.h" -#include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" +#include "tactic/portfolio/pb2bv_solver.h" +#include "tactic/tactic.h" +#include "tactic/generic_model_converter.h" +#include "solver/solver_na2as.h" +#include "ast/rewriter/pb2bv_rewriter.h" +#include "ast/rewriter/th_rewriter.h" class pb2bv_solver : public solver_na2as { ast_manager& m; @@ -50,10 +50,9 @@ public: virtual solver* translate(ast_manager& dst_m, params_ref const& p) { flush_assertions(); solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); - model_converter_ref mc = mc0(); - if (mc) { + if (mc0()) { ast_translation tr(m, dst_m); - result->set_model_converter(mc->translate(tr)); + result->set_model_converter(mc0()->translate(tr)); } return result; }