diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index 310d9a942..dad8dfa98 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -11,7 +11,7 @@ z3_add_component(spacer spacer_smt_context_manager.cpp spacer_sym_mux.cpp spacer_util.cpp - spacer_itp_solver.cpp + spacer_iuc_solver.cpp spacer_virtual_solver.cpp spacer_legacy_mbp.cpp spacer_unsat_core_learner.cpp diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp similarity index 88% rename from src/muz/spacer/spacer_itp_solver.cpp rename to src/muz/spacer/spacer_iuc_solver.cpp index fabe9a57f..90a28c341 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -3,11 +3,11 @@ Copyright (c) 2017 Arie Gurfinkel Module Name: - spacer_itp_solver.cpp + spacer_iuc_solver.cpp Abstract: - A solver that produces interpolated unsat cores + A solver that produces interpolated unsat cores (IUCs) Author: @@ -16,7 +16,7 @@ Author: Notes: --*/ -#include"muz/spacer/spacer_itp_solver.h" +#include"muz/spacer/spacer_iuc_solver.h" #include"ast/ast.h" #include"muz/spacer/spacer_util.h" #include"muz/base/proof_utils.h" @@ -27,13 +27,13 @@ Notes: #include "muz/spacer/spacer_iuc_proof.h" namespace spacer { -void itp_solver::push () +void iuc_solver::push () { m_defs.push_back (def_manager (*this)); m_solver.push (); } -void itp_solver::pop (unsigned n) +void iuc_solver::pop (unsigned n) { m_solver.pop (n); unsigned lvl = m_defs.size (); @@ -45,7 +45,7 @@ void itp_solver::pop (unsigned n) } } -app* itp_solver::fresh_proxy () +app* iuc_solver::fresh_proxy () { if (m_num_proxies == m_proxies.size()) { std::stringstream name; @@ -64,7 +64,7 @@ app* itp_solver::fresh_proxy () return m_proxies.get (m_num_proxies++); } -app* itp_solver::mk_proxy (expr *v) +app* iuc_solver::mk_proxy (expr *v) { { expr *e = v; @@ -76,7 +76,7 @@ app* itp_solver::mk_proxy (expr *v) return def.mk_proxy (v); } -bool itp_solver::mk_proxies (expr_ref_vector &v, unsigned from) +bool iuc_solver::mk_proxies (expr_ref_vector &v, unsigned from) { bool dirty = false; for (unsigned i = from, sz = v.size(); i < sz; ++i) { @@ -87,7 +87,7 @@ bool itp_solver::mk_proxies (expr_ref_vector &v, unsigned from) return dirty; } -void itp_solver::push_bg (expr *e) +void iuc_solver::push_bg (expr *e) { if (m_assumptions.size () > m_first_assumption) { m_assumptions.shrink(m_first_assumption); } @@ -95,7 +95,7 @@ void itp_solver::push_bg (expr *e) m_first_assumption = m_assumptions.size (); } -void itp_solver::pop_bg (unsigned n) +void iuc_solver::pop_bg (unsigned n) { if (n == 0) { return; } @@ -105,9 +105,9 @@ void itp_solver::pop_bg (unsigned n) m_assumptions.shrink (m_first_assumption); } -unsigned itp_solver::get_num_bg () {return m_first_assumption;} +unsigned iuc_solver::get_num_bg () {return m_first_assumption;} -lbool itp_solver::check_sat (unsigned num_assumptions, expr * const *assumptions) +lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions) { // -- remove any old assumptions if (m_assumptions.size () > m_first_assumption) @@ -128,7 +128,7 @@ lbool itp_solver::check_sat (unsigned num_assumptions, expr * const *assumptions } -app* itp_solver::def_manager::mk_proxy (expr *v) +app* iuc_solver::def_manager::mk_proxy (expr *v) { app* r; if (m_expr2proxy.find(v, r)) { return r; } @@ -146,7 +146,7 @@ app* itp_solver::def_manager::mk_proxy (expr *v) return proxy; } -bool itp_solver::def_manager::is_proxy (app *k, app_ref &def) +bool iuc_solver::def_manager::is_proxy (app *k, app_ref &def) { app *r = nullptr; bool found = m_proxy2def.find (k, r); @@ -154,20 +154,20 @@ bool itp_solver::def_manager::is_proxy (app *k, app_ref &def) return found; } -void itp_solver::def_manager::reset () +void iuc_solver::def_manager::reset () { m_expr2proxy.reset (); m_proxy2def.reset (); m_defs.reset (); } -bool itp_solver::def_manager::is_proxy_def (expr *v) +bool iuc_solver::def_manager::is_proxy_def (expr *v) { // XXX This might not be the most robust way to check return m_defs.contains (v); } -bool itp_solver::is_proxy(expr *e, app_ref &def) +bool iuc_solver::is_proxy(expr *e, app_ref &def) { if (!is_uninterp_const(e)) { return false; } @@ -183,23 +183,23 @@ bool itp_solver::is_proxy(expr *e, app_ref &def) return false; } -void itp_solver::collect_statistics (statistics &st) const +void iuc_solver::collect_statistics (statistics &st) const { m_solver.collect_statistics (st); - st.update ("time.itp_solver.itp_core", m_itp_watch.get_seconds ()); + st.update ("time.iuc_solver.iuc_core", m_iuc_watch.get_seconds ()); } -void itp_solver::reset_statistics () +void iuc_solver::reset_statistics () { - m_itp_watch.reset (); + m_iuc_watch.reset (); } -void itp_solver::get_unsat_core (ptr_vector &core) +void iuc_solver::get_unsat_core (ptr_vector &core) { m_solver.get_unsat_core (core); undo_proxies_in_core (core); } -void itp_solver::undo_proxies_in_core (ptr_vector &r) +void iuc_solver::undo_proxies_in_core (ptr_vector &r) { app_ref e(m); expr_fast_mark1 bg; @@ -222,7 +222,7 @@ void itp_solver::undo_proxies_in_core (ptr_vector &r) r.shrink (j); } -void itp_solver::undo_proxies (expr_ref_vector &r) +void iuc_solver::undo_proxies (expr_ref_vector &r) { app_ref e(m); // expand proxies @@ -233,14 +233,14 @@ void itp_solver::undo_proxies (expr_ref_vector &r) } } -void itp_solver::get_unsat_core (expr_ref_vector &_core) +void iuc_solver::get_unsat_core (expr_ref_vector &_core) { ptr_vector core; get_unsat_core (core); _core.append (core.size (), core.c_ptr ()); } -void itp_solver::elim_proxies (expr_ref_vector &v) +void iuc_solver::elim_proxies (expr_ref_vector &v) { expr_ref f = mk_and (v); scoped_ptr rep = mk_expr_simp_replacer (m); @@ -250,9 +250,9 @@ void itp_solver::elim_proxies (expr_ref_vector &v) flatten_and (f, v); } -void itp_solver::get_itp_core (expr_ref_vector &core) +void iuc_solver::get_iuc(expr_ref_vector &core) { - scoped_watch _t_ (m_itp_watch); + scoped_watch _t_ (m_iuc_watch); typedef obj_hashtable expr_set; expr_set B; @@ -379,12 +379,12 @@ void itp_solver::get_itp_core (expr_ref_vector &core) } IF_VERBOSE(2, - verbose_stream () << "Itp Core:\n" + verbose_stream () << "IUC Core:\n" << mk_pp (mk_and (core), m) << "\n";); } -void itp_solver::refresh () +void iuc_solver::refresh () { // only refresh in non-pushed state SASSERT (m_defs.size () == 0); diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_iuc_solver.h similarity index 85% rename from src/muz/spacer/spacer_itp_solver.h rename to src/muz/spacer/spacer_iuc_solver.h index 0b3527bb3..568124629 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -3,7 +3,7 @@ Copyright (c) 2017 Arie Gurfinkel Module Name: - spacer_itp_solver.h + spacer_iuc_solver.h Abstract: @@ -16,23 +16,23 @@ Author: Notes: --*/ -#ifndef SPACER_ITP_SOLVER_H_ -#define SPACER_ITP_SOLVER_H_ +#ifndef SPACER_IUC_SOLVER_H_ +#define SPACER_IUC_SOLVER_H_ #include"solver/solver.h" #include"ast/expr_substitution.h" #include"util/stopwatch.h" namespace spacer { -class itp_solver : public solver { +class iuc_solver : public solver { private: struct def_manager { - itp_solver &m_parent; + iuc_solver &m_parent; obj_map m_expr2proxy; obj_map m_proxy2def; expr_ref_vector m_defs; - def_manager(itp_solver &parent) : + def_manager(iuc_solver &parent) : m_parent(parent), m_defs(m_parent.m) {} @@ -54,7 +54,7 @@ private: unsigned m_first_assumption; bool m_is_proxied; - stopwatch m_itp_watch; + stopwatch m_iuc_watch; expr_substitution m_elim_proxies_sub; bool m_split_literals; @@ -68,7 +68,9 @@ private: app* fresh_proxy(); void elim_proxies(expr_ref_vector &v); public: - itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool old_hyp_reducer, bool split_literals = false) : + iuc_solver(solver &solver, unsigned iuc, unsigned iuc_arith, + bool print_farkas_stats, bool old_hyp_reducer, + bool split_literals = false) : m(solver.get_manager()), m_solver(solver), m_proxies(m), @@ -85,11 +87,11 @@ public: m_old_hyp_reducer(old_hyp_reducer) {} - ~itp_solver() override {} + ~iuc_solver() override {} - /* itp solver specific */ + /* iuc solver specific */ void get_unsat_core(expr_ref_vector &core) override; - virtual void get_itp_core(expr_ref_vector &core); + virtual void get_iuc(expr_ref_vector &core); void set_split_literals(bool v) {m_split_literals = v;} bool mk_proxies(expr_ref_vector &v, unsigned from = 0); void undo_proxies(expr_ref_vector &v); @@ -149,22 +151,22 @@ public: virtual void refresh(); class scoped_mk_proxy { - itp_solver &m_s; + iuc_solver &m_s; expr_ref_vector &m_v; public: - scoped_mk_proxy(itp_solver &s, expr_ref_vector &v) : m_s(s), m_v(v) + scoped_mk_proxy(iuc_solver &s, expr_ref_vector &v) : m_s(s), m_v(v) {m_s.mk_proxies(m_v);} ~scoped_mk_proxy() {m_s.undo_proxies(m_v);} }; class scoped_bg { - itp_solver &m_s; + iuc_solver &m_s; unsigned m_bg_sz; public: - scoped_bg(itp_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {} + scoped_bg(iuc_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {} ~scoped_bg() - {if (m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }} + {if(m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }} }; }; } diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 9850f9e6e..39db6129c 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -60,11 +60,11 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& m_solvers[1] = pm.mk_fresh2(); m_fparams[1] = &pm.fparams2(); - m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_iuc(), + m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_iuc_old_hyp_reducer(), p.spacer_iuc_split_farkas_literals()); - m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_iuc(), + m_contexts[1] = alloc(spacer::iuc_solver, *(m_solvers[1]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_iuc_old_hyp_reducer(), p.spacer_iuc_split_farkas_literals()); @@ -138,7 +138,7 @@ void prop_solver::assert_expr(expr * form, unsigned level) lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft) { // replace expressions by assumption literals - itp_solver::scoped_mk_proxy _p_(*m_ctx, hard); + iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard); unsigned hard_sz = hard.size(); // assume soft constraints are propositional literals (no need to proxy) hard.append(soft); @@ -234,7 +234,7 @@ lbool prop_solver::internal_check_assumptions( if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) { TRACE("spacer", tout << "theory core\n";); m_core->reset(); - m_ctx->get_itp_core(*m_core); + m_ctx->get_iuc(*m_core); } else if (result == l_false && m_core) { m_core->reset(); m_ctx->get_unsat_core(*m_core); @@ -263,7 +263,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, // can be disabled if use_push_bg == true // solver::scoped_push _s_(*m_ctx); if (!m_use_push_bg) { m_ctx->push(); } - itp_solver::scoped_bg _b_(*m_ctx); + iuc_solver::scoped_bg _b_(*m_ctx); for (unsigned i = 0; i < num_bg; ++i) if (m_use_push_bg) { m_ctx->push_bg(bg [i]); } diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 4aedb9676..295b47982 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -31,7 +31,7 @@ Revision History: #include "util/vector.h" #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_smt_context_manager.h" -#include "muz/spacer/spacer_itp_solver.h" +#include "muz/spacer/spacer_iuc_solver.h" struct fixedpoint_params; @@ -45,8 +45,8 @@ private: symbol m_name; smt_params* m_fparams[2]; solver* m_solvers[2]; - scoped_ptr m_contexts[2]; - itp_solver * m_ctx; + scoped_ptr m_contexts[2]; + iuc_solver * m_ctx; smt_params * m_ctx_fparams; decl_vector m_level_preds; app_ref_vector m_pos_level_atoms; // atoms used to identify level