From 7c9e3c3b70296ef416e1bdb81fd8ef39e0b95f2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Aug 2013 14:44:34 -0700 Subject: [PATCH] debug scale transformer, add model converter Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 2 + src/muz_qe/dl_mk_scale.cpp | 109 ++++++++++++++++++++++++++--- src/muz_qe/dl_mk_scale.h | 13 ++-- src/muz_qe/dl_rule_transformer.cpp | 2 +- 4 files changed, 113 insertions(+), 13 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index d8a50668b..9f250742c 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -48,6 +48,7 @@ Revision History: #include"dl_mk_magic_symbolic.h" #include"dl_mk_quantifier_abstraction.h" #include"dl_mk_quantifier_instantiation.h" +#include"dl_mk_scale.h" #include"datatype_decl_plugin.h" @@ -869,6 +870,7 @@ namespace datalog { if (get_params().magic()) { m_transf.register_plugin(alloc(datalog::mk_magic_symbolic, *this, 36020)); } + m_transf.register_plugin(alloc(datalog::mk_scale, *this, 36030)); transform_rules(m_transf); } diff --git a/src/muz_qe/dl_mk_scale.cpp b/src/muz_qe/dl_mk_scale.cpp index bcd19d0a4..90cbedb6c 100644 --- a/src/muz_qe/dl_mk_scale.cpp +++ b/src/muz_qe/dl_mk_scale.cpp @@ -21,6 +21,85 @@ Revision History: namespace datalog { + class mk_scale::scale_model_converter : public model_converter { + ast_manager& m; + func_decl_ref_vector m_trail; + arith_util a; + obj_map m_new2old; + public: + scale_model_converter(ast_manager& m): m(m), m_trail(m), a(m) {} + + virtual ~scale_model_converter() {} + + void add_new2old(func_decl* new_f, func_decl* old_f) { + m_trail.push_back(old_f); + m_trail.push_back(new_f); + m_new2old.insert(new_f, old_f); + } + + virtual void operator()(model_ref& md) { + model_ref old_model = alloc(model, m); + obj_map::iterator it = m_new2old.begin(); + obj_map::iterator end = m_new2old.end(); + for (; it != end; ++it) { + func_decl* old_p = it->m_value; + func_decl* new_p = it->m_key; + func_interp* old_fi = alloc(func_interp, m, old_p->get_arity()); + + if (new_p->get_arity() == 0) { + old_fi->set_else(md->get_const_interp(new_p)); + } + else { + func_interp* new_fi = md->get_func_interp(new_p); + expr_ref_vector subst(m); + var_subst vs(m, false); + expr_ref tmp(m); + + if (!new_fi) { + TRACE("dl", tout << new_p->get_name() << " has no value in the current model\n";); + dealloc(old_fi); + continue; + } + for (unsigned i = 0; i < old_p->get_arity(); ++i) { + subst.push_back(m.mk_var(i, old_p->get_domain(i))); + } + subst.push_back(a.mk_numeral(rational(1), a.mk_real())); + + // Hedge that we don't have to handle the general case for models produced + // by Horn clause solvers. + SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0); + vs(new_fi->get_else(), subst.size(), subst.c_ptr(), tmp); + old_fi->set_else(tmp); + old_model->register_decl(old_p, old_fi); + } + } + + // register values that have not been scaled. + unsigned sz = md->get_num_constants(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* c = md->get_constant(i); + if (!m_new2old.contains(c)) { + old_model->register_decl(c, md->get_const_interp(c)); + } + } + sz = md->get_num_functions(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* f = md->get_function(i); + if (!m_new2old.contains(f)) { + func_interp* fi = md->get_func_interp(f); + old_model->register_decl(f, fi->copy()); + } + } + md = old_model; + //TRACE("dl", model_smt2_pp(tout, m, *md, 0); ); + } + + virtual model_converter * translate(ast_translation & translator) { + UNREACHABLE(); + return 0; + } + }; + mk_scale::mk_scale(context & ctx, unsigned priority): plugin(priority), @@ -30,21 +109,27 @@ namespace datalog { m_trail(m) { } - mk_scale::~mk_scale() { } + mk_scale::~mk_scale() { + } rule_set * mk_scale::operator()(rule_set const & source) { if (!m_ctx.get_params().scale()) { return 0; } - context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + rule_set * result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); svector neg; ptr_vector vars; + ref smc; + if (m_ctx.get_model_converter()) { + smc = alloc(scale_model_converter, m); + } + m_mc = smc.get(); + for (unsigned i = 0; i < sz; ++i) { rule & r = *source.get_rule(i); unsigned utsz = r.get_uninterpreted_tail_size(); @@ -52,15 +137,15 @@ namespace datalog { tail.reset(); neg.reset(); vars.reset(); - r.get_vars(vars); m_cache.reset(); m_trail.reset(); + r.get_vars(vars); unsigned num_vars = vars.size(); - for (unsigned j = utsz; j < tsz; ++j) { + for (unsigned j = 0; j < utsz; ++j) { tail.push_back(mk_pred(num_vars, r.get_tail(j))); neg.push_back(false); } - for (unsigned j = 0; j < utsz; ++j) { + for (unsigned j = utsz; j < tsz; ++j) { tail.push_back(mk_constraint(num_vars, r.get_tail(j))); neg.push_back(false); } @@ -73,6 +158,11 @@ namespace datalog { } } TRACE("dl", result->display(tout);); + if (m_mc) { + m_ctx.add_model_converter(m_mc); + } + m_trail.reset(); + m_cache.reset(); return result; } @@ -85,6 +175,9 @@ namespace datalog { ptr_vector args(q->get_num_args(), q->get_args()); args.push_back(m.mk_var(num_vars, a.mk_real())); m_ctx.register_predicate(g, false); + if (m_mc) { + m_mc->add_new2old(g, f); + } return app_ref(m.mk_app(g, q->get_num_args() + 1, args.c_ptr()), m); } @@ -97,10 +190,10 @@ namespace datalog { expr* mk_scale::linearize(unsigned num_vars, expr* e) { expr* r; if (m_cache.find(e, r)) { - return expr_ref(r, m); + return r; } if (!is_app(e)) { - return expr_ref(e, m); + return e; } expr_ref result(m); app* ap = to_app(e); diff --git a/src/muz_qe/dl_mk_scale.h b/src/muz_qe/dl_mk_scale.h index cff226321..387a8868f 100644 --- a/src/muz_qe/dl_mk_scale.h +++ b/src/muz_qe/dl_mk_scale.h @@ -27,17 +27,22 @@ Revision History: namespace datalog { class mk_scale : public rule_transformer::plugin { + + class scale_model_converter; + ast_manager& m; context& m_ctx; arith_util a; expr_ref_vector m_trail; obj_map m_cache; - expr* linearize(unsigned num_vars, expr* e); - app_ref mk_pred(unsigned num_vars, app* q); - app_ref mk_constraint(unsigned num_vars, app* q); + scale_model_converter* m_mc; + + expr* linearize(unsigned num_vars, expr* e); + app_ref mk_pred(unsigned num_vars, app* q); + app_ref mk_constraint(unsigned num_vars, app* q); public: mk_scale(context & ctx, unsigned priority = 33039); - ~mk_scale(); + virtual ~mk_scale(); rule_set * operator()(rule_set const & source); }; diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 0cad08cb4..9055007b9 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -37,7 +37,7 @@ namespace datalog { void rule_transformer::reset() { plugin_vector::iterator it = m_plugins.begin(); plugin_vector::iterator end = m_plugins.end(); - for(; it!=end; ++it) { + for(; it!=end; ++it) { dealloc(*it); } m_plugins.reset();