diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index ebdf86ca5..bdaf3fcf0 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -316,6 +316,7 @@ namespace recfun { return alloc(def, m(), m_fid, name, n, domain, range); } + void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { d.set_definition(subst, n_vars, vars, rhs); } @@ -384,7 +385,17 @@ namespace recfun { promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) { def* d = u().decl_fun(name, n, params, range); - SASSERT(! m_defs.contains(d->get_decl())); + SASSERT(!m_defs.contains(d->get_decl())); + m_defs.insert(d->get_decl(), d); + return promise_def(&u(), d); + } + + promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range) { + def* d = u().decl_fun(name, n, params, range); + def* d2 = nullptr; + if (m_defs.find(d->get_decl(), d2)) { + dealloc(d2); + } m_defs.insert(d->get_decl(), d); return promise_def(&u(), d); } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index b294cdfce..33b5294f5 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -172,6 +172,8 @@ namespace recfun { unsigned arity, sort * const * domain, sort * range) override; promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range); + + promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range); void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); @@ -223,7 +225,6 @@ namespace recfun { //has_def(f)); return m_plugin->get_def(f); diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index e3530b4b5..e86475252 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -30,6 +30,7 @@ static_features::static_features(ast_manager & m): m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), m_arrfid(m.mk_family_id("array")), + m_srfid(m.mk_family_id("special_relations")), m_label_sym("label"), m_pattern_sym("pattern"), m_expr_list_sym("expr-list") { @@ -78,6 +79,7 @@ void static_features::reset() { m_has_real = false; m_has_bv = false; m_has_fpa = false; + m_has_sr = false; m_has_str = false; m_has_seq_non_str = false; m_has_arrays = false; @@ -274,6 +276,8 @@ void static_features::update_core(expr * e) { m_has_bv = true; if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e))) m_has_fpa = true; + if (is_app(e) && to_app(e)->get_family_id() == m_srfid) + m_has_sr = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; if (!m_has_ext_arrays && m_arrayutil.is_array(e) && @@ -281,9 +285,8 @@ void static_features::update_core(expr * e) { m_has_ext_arrays = true; if (!m_has_str && m_sequtil.str.is_string_term(e)) m_has_str = true; - if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) { + if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) m_has_seq_non_str = true; - } if (is_app(e)) { family_id fid = to_app(e)->get_family_id(); mark_theory(fid); diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 197947026..047c429b7 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -25,6 +25,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/seq_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "util/map.h" struct static_features { @@ -38,6 +39,7 @@ struct static_features { family_id m_afid; family_id m_lfid; family_id m_arrfid; + family_id m_srfid; ast_mark m_already_visited; bool m_cnf; unsigned m_num_exprs; // @@ -79,6 +81,7 @@ struct static_features { bool m_has_real; // bool m_has_bv; // bool m_has_fpa; // + bool m_has_sr; // has special relations bool m_has_str; // has String-typed terms bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 89213c86d..5f916899b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -955,7 +955,7 @@ namespace smt { setup_seq_str(st); setup_card(); setup_fpa(); - setup_special_relations(); + if (st.m_has_sr) setup_special_relations(); } void setup::setup_unknown(static_features & st) { @@ -972,6 +972,7 @@ namespace smt { setup_card(); setup_fpa(); setup_recfuns(); + if (st.m_has_sr) setup_special_relations(); return; } diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index af2d56cf1..cc7ec0e36 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -460,7 +460,7 @@ namespace smt { } void theory_recfun::display(std::ostream & out) const { - out << "recfun{}"; + out << "recfun{}\n"; } void theory_recfun::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 6e8c04a97..e8c276206 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -655,11 +655,11 @@ namespace smt { func_decl_ref fst(m), snd(m), pair(m); sort_ref tup(dt.mk_pair_datatype(listS, m.mk_bool_sort(), fst, snd, pair), m); sort* dom1[5] = { s, s, listS, s, s }; - recfun::promise_def c1 = p.mk_def(symbol("connected1"), 5, dom1, tup); + recfun::promise_def c1 = p.ensure_def(symbol("connected1"), 5, dom1, tup); sort* dom2[3] = { s, s, listS }; - recfun::promise_def c2 = p.mk_def(symbol("connected2"), 3, dom2, tup); + recfun::promise_def c2 = p.ensure_def(symbol("connected2"), 3, dom2, tup); sort* dom3[2] = { s, listS }; - recfun::promise_def mem = p.mk_def(symbol("member"), 2, dom3, m.mk_bool_sort()); + recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom3, m.mk_bool_sort()); var_ref xV(m.mk_var(1, s), m); var_ref SV(m.mk_var(0, listS), m); var_ref yV(m), vV(m), wV(m); @@ -718,7 +718,6 @@ namespace smt { SASSERT(ctx.get_assignment(a.var()) == l_true); expr* n1 = get_enode(a.v1())->get_root()->get_owner(); expr* n2 = get_enode(a.v2())->get_root()->get_owner(); - expr* Sr = connected_rec_body; expr* args[5] = { x, y, m.mk_app(fst, Sr), n1, n2}; expr* Sc = m.mk_app(conn1, 5, args);