mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Rename itp_solver into iuc_solver

Browse source 
IUC stands for Interpolanted UNSAT Core
This commit is contained in:
Arie Gurfinkel 2018-05-15 12:44:07 -07:00
parent 5d3b515a50
commit 649bab2f58
5 changed files with 57 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/CMakeLists.txt
View file

@ -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

60
src/muz/spacer/spacer_itp_solver.cpp → src/muz/spacer/spacer_iuc_solver.cpp
View file

@ -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<expr> &core)
void iuc_solver::get_unsat_core (ptr_vector<expr> &core)
{
m_solver.get_unsat_core (core);
undo_proxies_in_core (core);
}
void itp_solver::undo_proxies_in_core (ptr_vector<expr> &r)
void iuc_solver::undo_proxies_in_core (ptr_vector<expr> &r)
{
app_ref e(m);
expr_fast_mark1 bg;
@ -222,7 +222,7 @@ void itp_solver::undo_proxies_in_core (ptr_vector<expr> &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<expr> 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<expr_replacer> 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> 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);

34
src/muz/spacer/spacer_itp_solver.h → src/muz/spacer/spacer_iuc_solver.h
View file

@ -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<expr, app*> m_expr2proxy;
obj_map<app, app*> 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); }}
};
};
}

10
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -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]); }

6
src/muz/spacer/spacer_prop_solver.h
View file

@ -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<itp_solver> m_contexts[2];
itp_solver * m_ctx;
scoped_ptr<iuc_solver> 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