mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs related to model-converter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ae728374c8
commit
7b8101c502
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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<macro_decls> const & macros = ctx.get_macros();
|
||||
bool first = true;
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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(); }
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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() {
|
||||
|
|
|
@ -198,6 +198,7 @@ namespace sat {
|
|||
literal_vector m_lits;
|
||||
svector<uint64> 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); }
|
||||
};
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
@ -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<false>();
|
||||
}
|
||||
si.check_watches();
|
||||
if (s.cce_enabled())
|
||||
if (s.cce_enabled()) {
|
||||
cce<true>();
|
||||
}
|
||||
si.check_watches();
|
||||
if (s.bca_enabled())
|
||||
if (s.bca_enabled()) {
|
||||
bca();
|
||||
}
|
||||
si.check_watches();
|
||||
}
|
||||
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
@ -538,6 +538,8 @@ namespace sat {
|
|||
|
||||
private:
|
||||
|
||||
unsigned get_hash() const;
|
||||
|
||||
typedef hashtable<unsigned, u_hash, u_eq> index_set;
|
||||
|
||||
u_map<index_set> m_antecedents;
|
||||
|
|
|
@ -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<func_decl> m_inserted_const2bits;
|
||||
ref<sat2goal::mc> m_sat_mc;
|
||||
mutable ref<sat2goal::mc> m_sat_mc;
|
||||
mutable model_converter_ref m_cached_mc;
|
||||
svector<double> m_weights;
|
||||
std::string m_unknown;
|
||||
|
@ -382,7 +383,7 @@ public:
|
|||
return r;
|
||||
}
|
||||
|
||||
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
|
||||
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {
|
||||
sat::literal_vector ls;
|
||||
u_map<expr*> 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<symbol> & r) {
|
||||
|
||||
void get_labels(svector<symbol> & r) override {
|
||||
}
|
||||
virtual unsigned get_num_assertions() const {
|
||||
|
||||
unsigned get_num_assertions() const override {
|
||||
const_cast<inc_sat_solver*>(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<inc_sat_solver*>(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
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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<expr> 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);
|
||||
}
|
||||
|
||||
|
|
|
@ -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<entry> m_add_entries;
|
||||
vector<entry> m_hide_entries;
|
||||
vector<entry> m_entries;
|
||||
obj_map<func_decl, unsigned> 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);
|
||||
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue