From 80acf8ed79bb18d2cd11e49476dea73c65976b8e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Oct 2018 13:26:32 -0500 Subject: [PATCH] add recfuns to model Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 3 ++- src/ast/ast.h | 2 +- src/ast/recfun_decl_plugin.cpp | 3 ++- src/ast/recfun_decl_plugin.h | 16 ++++++++++++---- src/ast/rewriter/rewriter.h | 5 +++-- src/ast/rewriter/rewriter_def.h | 6 ++---- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_context.cpp | 21 +++++++++++++++++++++ src/smt/theory_recfun.cpp | 2 +- 9 files changed, 45 insertions(+), 15 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index e2ff19776..9a15bc7d3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1360,7 +1360,8 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs): m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode), m_trace_stream(src.m_trace_stream), m_trace_stream_owner(false), - m_rec_fun(":rec-fun") { + m_rec_fun(":rec-fun"), + m_lambda_def(":lambda-def") { SASSERT(!src.is_format_manager()); m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); init(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 37a6126f2..9a0e223de 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1636,7 +1636,7 @@ public: bool are_distinct(expr * a, expr * b) const; bool contains(ast * a) const { return m_ast_table.contains(a); } - + bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; } bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; } func_decl* get_rec_fun_decl(quantifier* q) const; diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 25f545ca4..ca929a9d7 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -56,6 +56,7 @@ namespace recfun { m_domain(m, arity, domain), m_range(range, m), m_vars(m), m_cases(), m_decl(m), + m_rhs(m), m_fid(fid) { SASSERT(arity == get_arity()); @@ -211,7 +212,7 @@ namespace recfun { name.append(m_name.bare_str()); m_vars.append(n_vars, vars); - + m_rhs = rhs; expr_ref_vector conditions(m); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index b516ae2bd..6bd338f54 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -99,6 +99,7 @@ namespace recfun { vars m_vars; //get_rec_funs(); + } + app_ref mk_depth_limit_pred(unsigned d); decl::plugin& get_plugin() { return *m_plugin; } diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 84fef488f..4195e7de6 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -279,8 +279,9 @@ protected: return false; } - bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { - return m_cfg.get_macro(f, def, q, def_pr); + bool get_macro(func_decl * f, expr * & def, proof * & def_pr) { + quantifier* q = nullptr; + return m_cfg.get_macro(f, def, q, def_pr); } void push_frame(expr * t, bool mcache, unsigned max_depth) { diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index ebe52f52a..3ee1e4caf 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -212,6 +212,7 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { return false; } + template template void rewriter_tpl::process_app(app * t, frame & fr) { @@ -338,15 +339,12 @@ void rewriter_tpl::process_app(app * t, frame & fr) { // TODO: add rewrite rules support expr * def = nullptr; proof * def_pr = nullptr; - quantifier * def_q = nullptr; // When get_macro succeeds, then // we know that: // forall X. f(X) = def[X] // and def_pr is a proof for this quantifier. // - // Remark: def_q is only used for proof generation. - // It is the quantifier forall X. f(X) = def[X] - if (get_macro(f, def, def_q, def_pr)) { + if (get_macro(f, def, def_pr)) { SASSERT(!f->is_associative() || !flat_assoc(f)); SASSERT(new_num_args == t->get_num_args()); SASSERT(m().get_sort(def) == m().get_sort(t)); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 2f87f24c0..6b4aee1c3 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -96,6 +96,6 @@ def_module_params(module_name='smt', ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'), ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), - ('recfun.native', BOOL, False, 'use native rec-fun solver'), + ('recfun.native', BOOL, True, 'use native rec-fun solver'), ('recfun.depth', UINT, 2, 'initial depth for maxrec expansion') )) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index a56110bc2..15887920a 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -37,6 +37,7 @@ Revision History: #include "model/model_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_translation.h" +#include "ast/recfun_decl_plugin.h" namespace smt { @@ -4453,6 +4454,26 @@ namespace smt { m_model->register_decl(f, fi); } } + recfun::util u(m); + recfun::decl::plugin& p = u.get_plugin(); + func_decl_ref_vector recfuns = u.get_rec_funs(); + for (func_decl* f : recfuns) { + auto& def = u.get_def(f); + expr* rhs = def.get_rhs(); + if (!rhs) continue; + func_interp* fi = alloc(func_interp, m, f->get_arity()); + // reverse argument order so that variable 0 starts at the beginning. + expr_ref_vector subst(m); + unsigned idx = 0; + for (unsigned i = 0; i < f->get_arity(); ++i) { + subst.push_back(m.mk_var(i, f->get_domain(i))); + } + var_subst sub(m, true); + expr_ref bodyr = sub(rhs, subst.size(), subst.c_ptr()); + + fi->set_else(bodyr); + m_model->register_decl(f, fi); + } } }; diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 1c1ee964d..88354f1eb 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -306,7 +306,7 @@ namespace smt { auto & vars = e.m_def->get_vars(); expr_ref lhs(e.m_lhs, m); unsigned depth = get_depth(e.m_lhs); - expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_macro_rhs()), m); + expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); literal lit = mk_eq_lit(lhs, rhs); ctx().mk_th_axiom(get_id(), 1, &lit); TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<