mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
add hiding to auxiliary declarations created in mc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
19b1248e5e
commit
f04e805fa4
|
@ -1718,11 +1718,13 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
|
||||
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
|
||||
|
||||
#if 0
|
||||
static unsigned count = 0;
|
||||
if (n->m_id == 404) {
|
||||
if (n->m_id == 1293522) {
|
||||
++count;
|
||||
//if (count == 2) SASSERT(false);
|
||||
}
|
||||
#endif
|
||||
|
||||
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
|
||||
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
|
||||
|
|
|
@ -15,6 +15,9 @@ Author:
|
|||
|
||||
Notes:
|
||||
|
||||
TBD: also keep track of which fresh constants are introduced
|
||||
to instruct model converter to delete them.
|
||||
|
||||
--*/
|
||||
#include "ast/rewriter/bit_blaster/bit_blaster_rewriter.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
|
|
|
@ -870,11 +870,12 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
|
|||
dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
|
||||
func_decls & fs = e->get_data().m_value;
|
||||
fs.insert(m(), fn);
|
||||
VERIFY(fn->get_range() == m().get_sort(t));
|
||||
m_mc0->add(fn, t);
|
||||
}
|
||||
|
||||
void cmd_context::model_del(func_decl* f) {
|
||||
if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "model_del");
|
||||
if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "cmd_context");
|
||||
if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get());
|
||||
m_mc0->hide(f);
|
||||
}
|
||||
|
|
|
@ -245,7 +245,7 @@ namespace sat {
|
|||
m_pos.push_back(l);
|
||||
m_neg.push_back(~l);
|
||||
}
|
||||
#if 0
|
||||
#if 1
|
||||
compare_left cmp(big);
|
||||
std::sort(m_pos.begin(), m_pos.end(), cmp);
|
||||
std::sort(m_neg.begin(), m_neg.end(), cmp);
|
||||
|
|
|
@ -142,7 +142,6 @@ struct goal2sat::imp {
|
|||
sat::bool_var v = m_solver.mk_var(ext);
|
||||
m_map.insert(t, v);
|
||||
l = sat::literal(v, sign);
|
||||
// if (to_app(t)->get_decl()->get_name() == "XX") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(t, m) << ": " << "v" << v << "\n";);
|
||||
TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
|
||||
if (ext && !is_uninterp_const(t)) {
|
||||
m_interpreted_atoms.push_back(t);
|
||||
|
@ -1051,8 +1050,9 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
|
|||
expr_ref sat2goal::mc::lit2expr(sat::literal l) {
|
||||
if (!m_var2expr.get(l.var())) {
|
||||
app* aux = m.mk_fresh_const(0, m.mk_bool_sort());
|
||||
// if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";);
|
||||
m_var2expr.set(l.var(), aux);
|
||||
if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
|
||||
m_gmc->hide(aux->get_decl());
|
||||
}
|
||||
VERIFY(m_var2expr.get(l.var()));
|
||||
expr_ref result(m_var2expr.get(l.var()), m);
|
||||
|
@ -1094,9 +1094,9 @@ struct sat2goal::imp {
|
|||
app* aux = mc ? mc->var2expr(l.var()) : nullptr;
|
||||
if (!aux) {
|
||||
aux = m.mk_fresh_const(0, m.mk_bool_sort());
|
||||
// if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";);
|
||||
if (mc)
|
||||
if (mc) {
|
||||
mc->insert(l.var(), aux, true);
|
||||
}
|
||||
}
|
||||
sat::literal lit(l.var(), false);
|
||||
m_lit2expr.set(lit.index(), aux);
|
||||
|
|
|
@ -28,9 +28,12 @@ Notes:
|
|||
#include "model/model_evaluator.h"
|
||||
|
||||
|
||||
generic_model_converter::~generic_model_converter() {
|
||||
}
|
||||
|
||||
void generic_model_converter::add(func_decl * d, expr* e) {
|
||||
VERIFY(e);
|
||||
struct entry et(d, e, m, ADD);
|
||||
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_entries.size());
|
||||
m_entries.push_back(et);
|
||||
|
@ -169,7 +172,7 @@ void generic_model_converter::operator()(expr_ref& fml) {
|
|||
}
|
||||
unsigned j = min_idx;
|
||||
for (unsigned i = min_idx; i < m_entries.size(); ++i) {
|
||||
entry const& e = m_entries[i];
|
||||
entry& e = m_entries[i];
|
||||
if (e.m_instruction == instruction::HIDE) {
|
||||
if (i != j) {
|
||||
m_entries[j] = e;
|
||||
|
|
|
@ -48,7 +48,7 @@ class generic_model_converter : public model_converter {
|
|||
public:
|
||||
generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
|
||||
|
||||
virtual ~generic_model_converter() { }
|
||||
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()); }
|
||||
|
||||
|
|
|
@ -24,7 +24,7 @@ Notes:
|
|||
* Add or overwrite value in model.
|
||||
*/
|
||||
void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
|
||||
VERIFY(e);
|
||||
VERIFY(e);
|
||||
smt2_pp_environment_dbg env(m);
|
||||
smt2_pp_environment* _env = m_env ? m_env : &env;
|
||||
VERIFY(f->get_range() == m.get_sort(e));
|
||||
|
|
Loading…
Reference in a new issue