mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 18:50:26 +00:00
Code Activity

add stubs for converting assertions, consolidate filter_model_converter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-17 14:51:13 -08:00
parent 53e36c9cf9
commit 0d15b6abb7
76 changed files with 244 additions and 356 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/CMakeLists.txt
View file

@ -2,7 +2,6 @@ z3_add_component(tactic
SOURCES
equiv_proof_converter.cpp
extension_model_converter.cpp
filter_model_converter.cpp
generic_model_converter.cpp
goal.cpp
goal_num_occurs.cpp

6
src/tactic/arith/card2bv_tactic.cpp
View file

@ -23,7 +23,7 @@ Notes:
#include "ast/rewriter/pb2bv_rewriter.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
class card2bv_tactic : public tactic {
ast_manager & m;
@ -89,9 +89,9 @@ public:
func_decl_ref_vector const& fns = rw2.fresh_constants();
if (!fns.empty()) {
filter_model_converter* filter = alloc(filter_model_converter, m);
generic_model_converter* filter = alloc(generic_model_converter, m);
for (unsigned i = 0; i < fns.size(); ++i) {
filter->insert(fns[i]);
filter->hide(fns[i]);
}
mc = filter;
}

7
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -20,7 +20,6 @@ Revision History:
--*/
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "util/cooperate.h"
#include "ast/arith_decl_plugin.h"
@ -197,12 +196,10 @@ class degree_shift_tactic : public tactic {
void prepare_substitution(model_converter_ref & mc) {
SASSERT(!m_var2degree.empty());
filter_model_converter * fmc = 0;
generic_model_converter * xmc = 0;
if (m_produce_models) {
fmc = alloc(filter_model_converter, m);
xmc = alloc(generic_model_converter, m);
mc = concat(fmc, xmc);
mc = xmc;
}
for (auto const& kv : m_var2degree) {
SASSERT(kv.m_value.is_int());
@ -211,7 +208,7 @@ class degree_shift_tactic : public tactic {
m_pinned.push_back(fresh);
m_var2var.insert(kv.m_key, fresh);
if (m_produce_models) {
fmc->insert(fresh->get_decl());
xmc->hide(fresh->get_decl());
xmc->add(kv.m_key->get_decl(), mk_power(fresh, rational(1)/kv.m_value));
}
if (m_produce_proofs) {

8
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -21,7 +21,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h"
#include "ast/for_each_expr.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h"
@ -225,10 +225,10 @@ class lia2pb_tactic : public tactic {
throw tactic_exception("lia2pb failed, number of necessary bits exceeds specified threshold (use option :lia2pb-total-bits to increase threshold)");
extension_model_converter * mc1 = 0;
filter_model_converter * mc2 = 0;
generic_model_converter * mc2 = 0;
if (m_produce_models) {
mc1 = alloc(extension_model_converter, m);
mc2 = alloc(filter_model_converter, m);
mc2 = alloc(generic_model_converter, m);
mc = concat(mc2, mc1);
}
@ -259,7 +259,7 @@ class lia2pb_tactic : public tactic {
else
def_args.push_back(m_util.mk_mul(m_util.mk_numeral(a, true), x_prime));
if (m_produce_models)
mc2->insert(x_prime->get_decl());
mc2->hide(x_prime->get_decl());
a *= rational(2);
}
SASSERT(def_args.size() > 1);

14
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -27,7 +27,7 @@ Notes:
#include "tactic/arith/bv2int_rewriter.h"
#include "tactic/arith/bv2real_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/arith/bound_manager.h"
#include "util/obj_pair_hashtable.h"
#include "ast/ast_smt2_pp.h"
@ -60,7 +60,7 @@ class nla2bv_tactic : public tactic {
expr_ref_vector m_trail;
unsigned m_num_bits;
unsigned m_default_bv_size;
filter_model_converter_ref m_fmc;
generic_model_converter_ref m_fmc;
public:
imp(ast_manager & m, params_ref const& p):
@ -86,7 +86,7 @@ class nla2bv_tactic : public tactic {
TRACE("nla2bv", g.display(tout);
tout << "Muls: " << count_mul(g) << "\n";
);
m_fmc = alloc(filter_model_converter, m_manager);
m_fmc = alloc(generic_model_converter, m_manager);
m_bounds(g);
collect_power2(g);
if(!collect_vars(g)) {
@ -104,7 +104,7 @@ class nla2bv_tactic : public tactic {
evc->insert(m_vars[i].get(), m_defs[i].get());
}
for (unsigned i = 0; i < m_bv2real.num_aux_decls(); ++i) {
m_fmc->insert(m_bv2real.get_aux_decl(i));
m_fmc->hide(m_bv2real.get_aux_decl(i));
}
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(nla->bv :sat-preserving " << m_is_sat_preserving << ")\n";);
TRACE("nla2bv_verbose", g.display(tout););
@ -233,7 +233,7 @@ class nla2bv_tactic : public tactic {
bv_sort = m_bv.mk_sort(num_bits);
std::string name = n->get_decl()->get_name().str();
s_bv = m_manager.mk_fresh_const(name.c_str(), bv_sort);
m_fmc->insert(to_app(s_bv)->get_decl());
m_fmc->hide(s_bv);
s_bv = m_bv.mk_bv2int(s_bv);
if (low) {
if (!(*low).is_zero()) {
@ -271,8 +271,8 @@ class nla2bv_tactic : public tactic {
s = m_manager.mk_fresh_const(name.c_str(), bv_sort);
name += "_r";
t = m_manager.mk_fresh_const(name.c_str(), bv_sort);
m_fmc->insert(to_app(s)->get_decl());
m_fmc->insert(to_app(t)->get_decl());
m_fmc->hide(s);
m_fmc->hide(t);
s_bv = m_bv2real.mk_bv2real(s, t);
m_trail.push_back(s_bv);
m_subst.insert(n, s_bv);

8
src/tactic/arith/normalize_bounds_tactic.cpp
View file

@ -22,7 +22,7 @@ Revision History:
#include "tactic/arith/bound_manager.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h"
@ -99,10 +99,10 @@ class normalize_bounds_tactic : public tactic {
}
extension_model_converter * mc1 = 0;
filter_model_converter * mc2 = 0;
generic_model_converter * mc2 = 0;
if (produce_models) {
mc1 = alloc(extension_model_converter, m);
mc2 = alloc(filter_model_converter, m);
mc2 = alloc(generic_model_converter, m);
mc = concat(mc2, mc1);
}
@ -121,7 +121,7 @@ class normalize_bounds_tactic : public tactic {
subst.insert(x, def);
if (produce_models) {
mc1->insert(to_app(x)->get_decl(), def);
mc2->insert(x_prime->get_decl());
mc2->hide(x_prime->get_decl());
}
}
}

12
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -26,7 +26,7 @@ Notes:
#include "util/trace.h"
#include "ast/ast_smt2_pp.h"
#include "ast/expr_substitution.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/arith/pb2bv_model_converter.h"
#include "tactic/arith/pb2bv_tactic.h"
#include "ast/ast_pp.h"
@ -949,15 +949,13 @@ private:
g->update(idx, new_exprs[idx].get(), 0, (m_produce_unsat_cores) ? new_deps[idx].get() : g->dep(idx));
if (m_produce_models) {
filter_model_converter * mc1 = alloc(filter_model_converter, m);
obj_map<func_decl, expr*>::iterator it = m_const2bit.begin();
obj_map<func_decl, expr*>::iterator end = m_const2bit.end();
for (; it != end; ++it)
mc1->insert(to_app(it->m_value)->get_decl());
generic_model_converter * mc1 = alloc(generic_model_converter, m);
for (auto const& kv : m_const2bit)
mc1->hide(kv.m_value);
// store temp int constants in the filter
unsigned num_temps = m_temporary_ints.size();
for (unsigned i = 0; i < num_temps; i++)
mc1->insert(to_app(m_temporary_ints.get(i))->get_decl());
mc1->hide(m_temporary_ints.get(i));
pb2bv_model_converter * mc2 = alloc(pb2bv_model_converter, m, m_const2bit, m_bm);
mc = concat(mc1, mc2);
}

14
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -27,7 +27,7 @@ Revision History:
#include "tactic/core/nnf_tactic.h"
#include "tactic/core/simplify_tactic.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/ast_smt2_pp.h"
#include "ast/rewriter/expr_replacer.h"
@ -764,17 +764,15 @@ struct purify_arith_proc {
m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : 0, 0);
}
// add filter_model_converter to eliminate auxiliary variables from model
// add generic_model_converter to eliminate auxiliary variables from model
if (produce_models) {
filter_model_converter * fmc = alloc(filter_model_converter, m());
generic_model_converter * fmc = alloc(generic_model_converter, m());
mc = fmc;
obj_map<app, expr*> & f2v = r.cfg().m_app2fresh;
obj_map<app, expr*>::iterator it = f2v.begin();
obj_map<app, expr*>::iterator end = f2v.end();
for (; it != end; ++it) {
app * v = to_app(it->m_value);
for (auto const& kv : f2v) {
app * v = to_app(kv.m_value);
SASSERT(is_uninterp_const(v));
fmc->insert(v->get_decl());
fmc->hide(v->get_decl());
}
}
if (produce_models && !m_sin_cos.empty()) {

8
src/tactic/arith/recover_01_tactic.cpp
View file

@ -33,7 +33,7 @@ Revision History:
#include "tactic/tactical.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h"
#include "util/dec_ref_util.h"
@ -113,7 +113,7 @@ class recover_01_tactic : public tactic {
// temporary fields used by operator() and process
extension_model_converter * mc1;
filter_model_converter * mc2;
generic_model_converter * mc2;
expr_substitution * subst;
goal_ref new_goal;
obj_map<expr, expr *> bool2int;
@ -205,7 +205,7 @@ class recover_01_tactic : public tactic {
expr * bool_def = m.mk_eq(var, m_util.mk_numeral(rational(1), true));
subst->insert(atom, bool_def);
if (m_produce_models) {
mc2->insert(to_app(var)->get_decl());
mc2->hide(to_app(var)->get_decl());
mc1->insert(to_app(atom)->get_decl(), bool_def);
}
m.inc_ref(atom);
@ -329,7 +329,7 @@ class recover_01_tactic : public tactic {
if (m_produce_models) {
mc1 = alloc(extension_model_converter, m);
mc2 = alloc(filter_model_converter, m);
mc2 = alloc(generic_model_converter, m);
mc = concat(mc2, mc1);
}

12
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -25,7 +25,7 @@ Notes:
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_replacer.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.h"
class bv_size_reduction_tactic : public tactic {
@ -60,7 +60,7 @@ struct bv_size_reduction_tactic::imp {
obj_map<app, numeral> m_unsigned_lowers;
obj_map<app, numeral> m_unsigned_uppers;
ref<bv_size_reduction_mc> m_mc;
filter_model_converter_ref m_fmc;
generic_model_converter_ref m_fmc;
scoped_ptr<expr_replacer> m_replacer;
bool m_produce_models;
@ -269,9 +269,9 @@ struct bv_size_reduction_tactic::imp {
m_mc = alloc(bv_size_reduction_mc, m);
m_mc->insert(v->get_decl(), new_def);
if (!m_fmc && new_const)
m_fmc = alloc(filter_model_converter, m);
m_fmc = alloc(generic_model_converter, m);
if (new_const)
m_fmc->insert(new_const->get_decl());
m_fmc->hide(new_const);
}
num_reduced++;
}
@ -335,9 +335,9 @@ struct bv_size_reduction_tactic::imp {
m_mc = alloc(bv_size_reduction_mc, m);
m_mc->insert(v->get_decl(), new_def);
if (!m_fmc && new_const)
m_fmc = alloc(filter_model_converter, m);
m_fmc = alloc(generic_model_converter, m);
if (new_const)
m_fmc->insert(new_const->get_decl());
m_fmc->hide(new_const);
}
num_reduced++;
TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);

6
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -120,7 +120,7 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
m_array_util.mk_as_array(bv_f));
}
else if (m_fmc)
m_fmc->insert(bv_f);
m_fmc->hide(bv_f);
m_arrays_fs.insert(e, bv_f);
m_manager.inc_ref(e);
m_manager.inc_ref(bv_f);
@ -193,10 +193,10 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
if (is_uninterp_const(e)) {
if (m_emc)
m_emc->insert(e->get_decl(),
m_array_util.mk_as_array(bv_f));
m_array_util.mk_as_array(bv_f));
}
else if (m_fmc)
m_fmc->insert(bv_f);
m_fmc->hide(bv_f);
m_arrays_fs.insert(e, bv_f);
m_manager.inc_ref(e);
m_manager.inc_ref(bv_f);

8
src/tactic/bv/bvarray2uf_rewriter.h
View file

@ -22,7 +22,7 @@ Notes:
#include "ast/rewriter/rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
class bvarray2uf_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
@ -31,7 +31,7 @@ class bvarray2uf_rewriter_cfg : public default_rewriter_cfg {
bv_util m_bv_util;
array_util m_array_util;
extension_model_converter * m_emc;
filter_model_converter * m_fmc;
generic_model_converter * m_fmc;
obj_map<expr, func_decl*> m_arrays_fs;
@ -59,7 +59,7 @@ public:
expr_ref_vector extra_assertions;
void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; }
void set_mcs(extension_model_converter * emc, generic_model_converter * fmc) { m_emc = emc; m_fmc = fmc; }
protected:
sort * get_index_sort(expr * e);
@ -79,7 +79,7 @@ struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
m_cfg(m, p) {
}
void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); }
void set_mcs(extension_model_converter * emc, generic_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); }
};
#endif

4
src/tactic/bv/bvarray2uf_tactic.cpp
View file

@ -21,7 +21,7 @@ Notes:
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_replacer.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.h"
#include "tactic/bv/bvarray2uf_tactic.h"
@ -69,7 +69,7 @@ class bvarray2uf_tactic : public tactic {
if (m_produce_models) {
extension_model_converter * emc = alloc(extension_model_converter, m_manager);
filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
generic_model_converter * fmc = alloc(generic_model_converter, m_manager);
mc = concat(emc, fmc);
m_rw.set_mcs(emc, fmc);
}

8
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -21,11 +21,11 @@ Revision History:
#include "tactic/bv/dt2bv_tactic.h"
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_util.h"
@ -135,7 +135,7 @@ public:
m_fd_sorts.remove(s);
if (!m_fd_sorts.empty()) {
ref<extension_model_converter> ext = alloc(extension_model_converter, m);
ref<filter_model_converter> filter = alloc(filter_model_converter, m);
ref<generic_model_converter> filter = alloc(generic_model_converter, m);
enum2bv_rewriter rw(m, m_params);
rw.set_is_fd(&m_is_fd);
expr_ref new_curr(m);
@ -153,7 +153,7 @@ public:
for (expr* b : bounds)
g->assert_expr(b);
for (auto const& kv : rw.enum2bv())
filter->insert(kv.m_value);
filter->hide(kv.m_value);
for (auto const& kv : rw.enum2def())
ext->insert(kv.m_key, kv.m_value);

4
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#include "tactic/tactical.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "util/cooperate.h"
#include "ast/bv_decl_plugin.h"
#include "ast/used_vars.h"
@ -35,7 +35,7 @@ class elim_small_bv_tactic : public tactic {
params_ref m_params;
bv_util m_util;
th_rewriter m_simp;
ref<filter_model_converter> m_mc;
ref<generic_model_converter> m_mc;
goal * m_goal;
unsigned m_max_bits;
unsigned long long m_max_steps;

1
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -19,7 +19,6 @@ Notes:
#include "tactic/tactical.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/filter_model_converter.h"
#include "util/cooperate.h"
#include "ast/scoped_proof.h"

8
src/tactic/core/elim_term_ite_tactic.cpp
View file

@ -20,7 +20,7 @@ Notes:
#include "tactic/tactical.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "util/cooperate.h"
class elim_term_ite_tactic : public tactic {
@ -28,7 +28,7 @@ class elim_term_ite_tactic : public tactic {
struct rw_cfg : public default_rewriter_cfg {
ast_manager & m;
defined_names m_defined_names;
ref<filter_model_converter> m_mc;
ref<generic_model_converter> m_mc;
goal * m_goal;
unsigned long long m_max_memory; // in bytes
bool m_produce_models;
@ -55,8 +55,8 @@ class elim_term_ite_tactic : public tactic {
m_num_fresh++;
if (m_produce_models) {
if (!m_mc)
m_mc = alloc(filter_model_converter, m);
m_mc->insert(_result->get_decl());
m_mc = alloc(generic_model_converter, m);
m_mc->hide(_result->get_decl());
}
}
result = _result.get();

9
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -18,7 +18,6 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "tactic/generic_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
@ -873,9 +872,9 @@ class elim_uncnstr_tactic : public tactic {
app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
m_num_elim_apps = fresh_vars.size();
if (produce_models && !fresh_vars.empty()) {
filter_model_converter * fmc = alloc(filter_model_converter, m());
for (unsigned i = 0; i < fresh_vars.size(); i++)
fmc->insert(fresh_vars.get(i)->get_decl());
generic_model_converter * fmc = alloc(generic_model_converter, m());
for (app * f : fresh_vars)
fmc->hide(f);
mc = concat(fmc, m_mc.get());
}
else {
@ -910,7 +909,7 @@ class elim_uncnstr_tactic : public tactic {
imp * m_imp;
params_ref m_params;
public:
elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}

6
src/tactic/core/nnf_tactic.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#include "ast/normal_forms/nnf.h"
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
class nnf_tactic : public tactic {
params_ref m_params;
@ -97,10 +97,10 @@ public:
result.push_back(g.get());
unsigned num_extra_names = dnames.get_num_names();
if (num_extra_names > 0) {
filter_model_converter * fmc = alloc(filter_model_converter, m);
generic_model_converter * fmc = alloc(generic_model_converter, m);
mc = fmc;
for (unsigned i = 0; i < num_extra_names; i++)
fmc->insert(dnames.get_name_decl(i));
fmc->hide(dnames.get_name_decl(i));
}
TRACE("nnf", g->display(tout););
SASSERT(g->is_well_sorted());

8
src/tactic/core/occf_tactic.cpp
View file

@ -23,13 +23,13 @@ Revision History:
--*/
#include "tactic/tactical.h"
#include "tactic/core/occf_tactic.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "util/cooperate.h"
class occf_tactic : public tactic {
struct imp {
ast_manager & m;
filter_model_converter * m_mc;
generic_model_converter * m_mc;
imp(ast_manager & _m):
m(_m) {
@ -115,7 +115,7 @@ class occf_tactic : public tactic {
SASSERT(!c2b.contains(cnstr));
expr * bvar = m.mk_fresh_const(0, m.mk_bool_sort());
if (produce_models)
m_mc->insert(to_app(bvar)->get_decl());
m_mc->hide(to_app(bvar)->get_decl());
c2b.insert(cnstr, bvar_info(bvar, sign));
if (sign) {
g->assert_expr(m.mk_or(bvar, m.mk_not(cnstr)), 0, 0);
@ -157,7 +157,7 @@ class occf_tactic : public tactic {
if (!is_target(cls))
continue;
if (produce_models && !m_mc) {
m_mc = alloc(filter_model_converter, m);
m_mc = alloc(generic_model_converter, m);
mc = m_mc;
}
expr * keep = 0;

6
src/tactic/core/reduce_args_tactic.cpp
View file

@ -23,7 +23,7 @@ Notes:
#include "util/map.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
/**
\brief Reduce the number of arguments in function applications.
@ -395,7 +395,7 @@ struct reduce_args_tactic::imp {
var_ref_vector new_vars(m_manager);
ptr_buffer<expr> new_eqs;
extension_model_converter * e_mc = alloc(extension_model_converter, m_manager);
filter_model_converter * f_mc = alloc(filter_model_converter, m_manager);
generic_model_converter * f_mc = alloc(generic_model_converter, m_manager);
decl2arg2func_map::iterator it = decl2arg2funcs.begin();
decl2arg2func_map::iterator end = decl2arg2funcs.end();
for (; it != end; ++it) {
@ -416,7 +416,7 @@ struct reduce_args_tactic::imp {
for (; it2 != end2; ++it2) {
app * t = it2->m_key;
func_decl * new_def = it2->m_value;
f_mc->insert(new_def);
f_mc->hide(new_def);
SASSERT(new_def->get_arity() == new_args.size());
app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.c_ptr());
if (def == 0) {

8
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -51,7 +51,7 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "tactic/goal_shared_occs.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/rewriter/bool_rewriter.h"
#include "tactic/core/simplify_tactic.h"
#include "util/cooperate.h"
@ -80,7 +80,7 @@ class tseitin_cnf_tactic : public tactic {
frame(app * n):m_t(n), m_first(true) {}
};
typedef filter_model_converter mc;
typedef generic_model_converter mc;
ast_manager & m;
svector<frame> m_frame_stack;
@ -344,7 +344,7 @@ class tseitin_cnf_tactic : public tactic {
app * v = m.mk_fresh_const(0, m.mk_bool_sort());
m_fresh_vars.push_back(v);
if (m_mc)
m_mc->insert(v->get_decl());
m_mc->hide(v->get_decl());
return v;
}
@ -817,7 +817,7 @@ class tseitin_cnf_tactic : public tactic {
m_frame_stack.reset();
m_clauses.reset();
if (m_produce_models)
m_mc = alloc(filter_model_converter, m);
m_mc = alloc(generic_model_converter, m);
else
m_mc = 0;

2
src/tactic/extension_model_converter.h
View file

@ -10,6 +10,8 @@ Abstract:
Model converter that introduces new interpretations into a model.
It used to be called elim_var_model_converter
TBD: special case of generic_model_converter
Author:
Leonardo (leonardo) 2011-10-21

74
src/tactic/filter_model_converter.cpp
View file

@ -1,74 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
filter_model_converter.cpp
Abstract:
Filter decls from a model
Author:
Leonardo (leonardo) 2011-05-06
Notes:
--*/
#include "tactic/filter_model_converter.h"
#include "model/model_v2_pp.h"
filter_model_converter::~filter_model_converter() {
}
void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx) {
TRACE("filter_mc", tout << "before filter_model_converter\n"; model_v2_pp(tout, *old_model); display(tout););
ast_fast_mark1 fs;
unsigned num = m_decls.size();
for (unsigned i = 0; i < num; i++)
fs.mark(m_decls.get(i));
model * new_model = alloc(model, m());
num = old_model->get_num_constants();
for (unsigned i = 0; i < num; i++) {
func_decl * f = old_model->get_constant(i);
if (fs.is_marked(f))
continue;
expr * fi = old_model->get_const_interp(f);
new_model->register_decl(f, fi);
}
num = old_model->get_num_functions();
for (unsigned i = 0; i < num; i++) {
func_decl * f = old_model->get_function(i);
if (fs.is_marked(f))
continue;
func_interp * fi = old_model->get_func_interp(f);
SASSERT(fi);
new_model->register_decl(f, fi->copy());
}
new_model->copy_usort_interps(*old_model);
old_model = new_model;
TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model););
}
void filter_model_converter::operator()(svector<symbol> & labels, unsigned goal_idx) {
}
void filter_model_converter::display(std::ostream & out) {
for (func_decl* f : m_decls) {
display_del(out, f);
}
}
model_converter * filter_model_converter::translate(ast_translation & translator) {
filter_model_converter * res = alloc(filter_model_converter, translator.to());
for (func_decl* f : m_decls)
res->m_decls.push_back(translator(f));
return res;
}
void filter_model_converter::collect(ast_pp_util& visitor) {
m_env = &visitor.env();
for (func_decl* f : m_decls) visitor.coll.visit_func(f);
}

56
src/tactic/filter_model_converter.h
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
filter_model_converter.h
Abstract:
Filter decls from a model
Author:
Leonardo (leonardo) 2011-05-06
Notes:
--*/
#ifndef FILTER_MODEL_CONVERTER_H_
#define FILTER_MODEL_CONVERTER_H_
#include "tactic/model_converter.h"
#include "ast/ast_pp_util.h"
class filter_model_converter : public model_converter {
func_decl_ref_vector m_decls;
public:
filter_model_converter(ast_manager & m): m_decls(m) {}
virtual ~filter_model_converter();
ast_manager & m() const { return m_decls.get_manager(); }
virtual void operator()(model_ref & md, unsigned goal_idx);
virtual void operator()(svector<symbol> & labels, unsigned goal_idx);
virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
virtual void cancel() {}
virtual void display(std::ostream & out);
void insert(func_decl * d) {
m_decls.push_back(d);
}
virtual model_converter * translate(ast_translation & translator);
virtual void collect(ast_pp_util& visitor);
};
typedef ref<filter_model_converter> filter_model_converter_ref;
#endif

4
src/tactic/generic_model_converter.cpp
View file

@ -85,3 +85,7 @@ void generic_model_converter::collect(ast_pp_util& visitor) {
if (e.m_def) visitor.coll.visit(e.m_def);
}
}
void generic_model_converter::operator()(expr_ref& fml) {
NOT_IMPLEMENTED_YET();
}

4
src/tactic/generic_model_converter.h
View file

@ -38,6 +38,8 @@ public:
virtual ~generic_model_converter() { }
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_entries.push_back(entry(f, 0, m, HIDE)); }
void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); }
@ -55,6 +57,8 @@ public:
virtual model_converter * translate(ast_translation & translator);
virtual void collect(ast_pp_util& visitor);
void operator()(expr_ref& fml) override;
};
typedef ref<generic_model_converter> generic_model_converter_ref;

9
src/tactic/model_converter.h
View file

@ -45,12 +45,19 @@ public:
SASSERT(goal_idx == 0);
operator()(m);
}
virtual void operator()(labels_vec & r, unsigned goal_idx) {}
virtual void operator()(labels_vec & r, unsigned goal_idx) {}
virtual model_converter * translate(ast_translation & translator) = 0;
virtual void collect(ast_pp_util& visitor) { m_env = &visitor.env(); }
/**
\brief we are adding a formula to the context of the model converter.
The operator has as side effect of adding definitions as assertions to the
formula and removing these definitions from the model converter.
*/
virtual void operator()(expr_ref& formula) { UNREACHABLE(); }
};
typedef ref<model_converter> model_converter_ref;

12
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -49,7 +49,7 @@ Revision History:
#include "smt/tactic/smt_tactic.h"
#include "ast/rewriter/rewriter.h"
#include "nlsat/tactic/nlsat_tactic.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "util/obj_pair_hashtable.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
@ -73,7 +73,7 @@ class nl_purify_tactic : public tactic {
arith_util m_util;
params_ref m_params;
bool m_produce_proofs;
ref<filter_model_converter> m_fmc;
ref<generic_model_converter> m_fmc;
tactic_ref m_nl_tac; // nlsat tactic
goal_ref m_nl_g; // nlsat goal
ref<solver> m_solver; // SMT solver
@ -133,7 +133,7 @@ public:
}
r = m.mk_fresh_const(0, u().mk_real());
m_new_reals.push_back(to_app(r));
m_owner.m_fmc->insert(to_app(r)->get_decl());
m_owner.m_fmc->hide(r);
m_interface_cache.insert(arg, r);
expr_ref eq(m);
eq = m.mk_eq(r, arg);
@ -159,7 +159,7 @@ public:
result = m.mk_fresh_const(0, m.mk_bool_sort());
m_polarities.insert(result, pol);
m_new_preds.push_back(to_app(result));
m_owner.m_fmc->insert(to_app(result)->get_decl());
m_owner.m_fmc->hide(result);
if (pol != pol_neg) {
m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred));
}
@ -491,7 +491,7 @@ private:
pred = m.mk_fresh_const(0, m.mk_bool_sort());
m_eq_preds.push_back(pred);
m_eq_values.push_back(l_true);
m_fmc->insert(to_app(pred)->get_decl());
m_fmc->hide(pred);
nl_g->assert_expr(m.mk_or(m.mk_not(pred), m.mk_eq(w, v)));
nl_g->assert_expr(m.mk_or(pred, m.mk_not(m.mk_eq(w, v))));
m_solver->assert_expr(m.mk_iff(pred, m.mk_eq(w, v)));
@ -761,7 +761,7 @@ public:
rw r(*this);
expr_ref_vector clauses(m);
m_nl_g = alloc(goal, m, true, false);
m_fmc = alloc(filter_model_converter, m);
m_fmc = alloc(generic_model_converter, m);
// first hoist interface variables,
// then annotate subformulas by polarities,

10
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -21,7 +21,7 @@ Notes:
#include "solver/solver_na2as.h"
#include "tactic/tactic.h"
#include "ast/rewriter/pb2bv_rewriter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/ast_pp.h"
#include "model/model_smt2_pp.h"
@ -86,7 +86,7 @@ public:
return result;
}
virtual void assert_expr(expr * t) {
virtual void assert_expr_core(expr * t) {
unsigned i = m_assertions.size();
m_assertions.push_back(t);
while (i < m_assertions.size()) {
@ -209,10 +209,8 @@ private:
if (m_bv_fns.empty()) {
return;
}
filter_model_converter filter(m);
for (unsigned i = 0; i < m_bv_fns.size(); ++i) {
filter.insert(m_bv_fns[i].get());
}
generic_model_converter filter(m);
for (func_decl* f : m_bv_fns) filter.hide(f);
filter(mdl, 0);
}

8
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -26,7 +26,7 @@ Notes:
#include "model/model_smt2_pp.h"
#include "tactic/tactic.h"
#include "tactic/extension_model_converter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "tactic/portfolio/enum2bv_solver.h"
#include "solver/solver_na2as.h"
#include "ast/rewriter/enum2bv_rewriter.h"
@ -58,7 +58,7 @@ public:
return result;
}
virtual void assert_expr(expr * t) {
virtual void assert_expr_core(expr * t) {
expr_ref tmp(t, m);
expr_ref_vector bounds(m);
proof_ref tmp_proof(m);
@ -164,9 +164,9 @@ public:
}
void filter_model(model_ref& mdl) {
filter_model_converter filter(m);
generic_model_converter filter(m);
for (auto const& kv : m_rewriter.enum2bv()) {
filter.insert(kv.m_value);
filter.hide(kv.m_value);
}
filter(mdl, 0);
}

2
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -549,7 +549,7 @@ public:
expr_ref_vector clauses(m);
ptr_vector<expr> assumptions;
obj_map<expr, expr*> bool2dep;
ref<filter_model_converter> fmc;
ref<generic_model_converter> fmc;
extract_clauses_and_dependencies(g, clauses, assumptions, bool2dep, fmc);
for (expr * clause : clauses) {
s->assert_expr(clause);

14
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -21,7 +21,7 @@ Notes:
#include "tactic/tactic.h"
#include "ast/rewriter/pb2bv_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/ast_pp.h"
#include "model/model_smt2_pp.h"
@ -57,7 +57,7 @@ public:
return result;
}
virtual void assert_expr(expr * t) {
virtual void assert_expr_core(expr * t) {
m_assertions.push_back(t);
}
@ -113,10 +113,10 @@ public:
if (m_rewriter.fresh_constants().empty()) {
return;
}
filter_model_converter filter(m);
generic_model_converter filter(m);
func_decl_ref_vector const& fns = m_rewriter.fresh_constants();
for (unsigned i = 0; i < fns.size(); ++i) {
filter.insert(fns[i]);
for (func_decl* f : fns) {
filter.hide(f);
}
filter(mdl, 0);
}
@ -138,8 +138,8 @@ private:
proof_ref proof(m);
expr_ref fml1(m), fml(m);
expr_ref_vector fmls(m);
for (unsigned i = 0; i < m_assertions.size(); ++i) {
m_th_rewriter(m_assertions[i].get(), fml1, proof);
for (expr* a : m_assertions) {
m_th_rewriter(a, fml1, proof);
m_rewriter(fml1, fml, proof);
m_solver->assert_expr(fml);
}

5
src/tactic/sine_filter.cpp
View file

@ -18,10 +18,9 @@ Revision History:
#include "tactic/sine_filter.h"
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/filter_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_util.h"
@ -69,7 +68,7 @@ public:
result.push_back(g.get());
TRACE("sine", result[0]->display(tout););
SASSERT(g->is_well_sorted());
filter_model_converter * fmc = alloc(filter_model_converter, m);
generic_model_converter * fmc = alloc(generic_model_converter, m);
mc = fmc;
}