From 7c6540e18f37bf8b514299b4d2f229bd1ce61942 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Mar 2016 07:59:03 -0800
Subject: [PATCH] recursive function definitions; combine model-building
functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/array_decl_plugin.cpp | 11 ++++++
src/ast/array_decl_plugin.h | 3 +-
src/ast/ast.cpp | 9 +++--
src/ast/ast.h | 5 +++
src/cmd_context/cmd_context.cpp | 12 +++++--
src/model/model.cpp | 51 --------------------------
src/model/model.h | 5 +--
src/model/model_core.cpp | 56 +++++++++++++++++++++++++++++
src/model/model_core.h | 10 ++++--
src/model/model_evaluator.cpp | 10 +++---
src/model/model_evaluator.h | 2 +-
src/smt/proto_model/proto_model.cpp | 52 ++++-----------------------
src/smt/proto_model/proto_model.h | 10 ++----
src/smt/smt_model_checker.cpp | 13 +++----
src/smt/smt_model_finder.cpp | 4 +--
src/smt/smt_model_generator.cpp | 37 -------------------
src/smt/smt_quantifier.cpp | 6 ++--
src/smt/theory_datatype.cpp | 4 +++
src/smt/theory_datatype.h | 2 ++
19 files changed, 129 insertions(+), 173 deletions(-)
diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 49b1b18c5..9634e17cb 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -40,6 +40,15 @@ array_decl_plugin::array_decl_plugin():
#define ARRAY_SORT_STR "Array"
sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+
+ if (k == _SET_SORT) {
+ if (num_parameters != 1) {
+ m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
+ return 0;
+ }
+ parameter params[2] = { parameters[0], parameter(m_manager->mk_bool_sort()) };
+ return mk_sort(ARRAY_SORT, 2, params);
+ }
SASSERT(k == ARRAY_SORT);
if (num_parameters < 2) {
m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
@@ -506,6 +515,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT));
+ // TBD: this could easily break users even though it is already used in CVC4:
+ // sort_names.push_back(builtin_name("Set", _SET_SORT));
}
void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 60adc3ae6..36a8d50a5 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -35,7 +35,8 @@ inline sort* get_array_domain(sort const * s, unsigned idx) {
}
enum array_sort_kind {
- ARRAY_SORT
+ ARRAY_SORT,
+ _SET_SORT
};
enum array_op_kind {
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a74ab90c1..2cf33941e 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1308,7 +1308,8 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(m),
m_trace_stream(0),
- m_trace_stream_owner(false) {
+ m_trace_stream_owner(false),
+ m_rec_fun(":rec-fun") {
if (trace_file) {
m_trace_stream = alloc(std::fstream, trace_file, std::ios_base::out);
@@ -1329,7 +1330,8 @@ ast_manager::ast_manager(proof_gen_mode m, std::fstream * trace_stream, bool is_
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(m),
m_trace_stream(trace_stream),
- m_trace_stream_owner(false) {
+ m_trace_stream_owner(false),
+ m_rec_fun(":rec-fun") {
if (!is_format_manager)
m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true);
@@ -1345,7 +1347,8 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode),
m_trace_stream(src.m_trace_stream),
- m_trace_stream_owner(false) {
+ m_trace_stream_owner(false),
+ m_rec_fun(":rec-fun") {
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 861fb997d..c386ccd63 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1455,6 +1455,7 @@ protected:
bool slow_not_contains(ast const * n);
#endif
ast_manager * m_format_manager; // hack for isolating format objects in a different manager.
+ symbol m_rec_fun;
void init();
@@ -1561,6 +1562,10 @@ public:
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; }
+
+ symbol const& rec_fun_qid() const { return m_rec_fun; }
+
unsigned get_num_asts() const { return m_ast_table.size(); }
void debug_ref_count() { m_debug_ref_count = true; }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index cdc1df6be..24c19a27a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -837,10 +837,16 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
eq = m().mk_eq(lhs, e);
if (!ids.empty()) {
expr* pat = m().mk_pattern(lhs);
- eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, symbol(":rec-fun"), symbol::null, 1, &pat);
+ eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat);
}
- if (!ids.empty() && !m_rec_fun_declared) {
- warning_msg("recursive functions are currently only partially supported: they are translated into recursive equations without special handling");
+
+ //
+ // disable warning given the current way they are used
+ // (Z3 will here silently assume and not check the definitions to be well founded,
+ // and please use HSF for everything else).
+ //
+ if (false && !ids.empty() && !m_rec_fun_declared) {
+ warning_msg("recursive function definitions are assumed well-founded");
m_rec_fun_declared = true;
}
assert_expr(eq);
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 73a39a8eb..f4f9af873 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -30,20 +30,6 @@ model::model(ast_manager & m):
}
model::~model() {
- decl2expr::iterator it1 = m_interp.begin();
- decl2expr::iterator end1 = m_interp.end();
- for (; it1 != end1; ++it1) {
- m_manager.dec_ref(it1->m_key);
- m_manager.dec_ref(it1->m_value);
- }
-
- decl2finterp::iterator it2 = m_finterp.begin();
- decl2finterp::iterator end2 = m_finterp.end();
- for (; it2 != end2; ++it2) {
- m_manager.dec_ref(it2->m_key);
- dealloc(it2->m_value);
- }
-
sort2universe::iterator it3 = m_usort2universe.begin();
sort2universe::iterator end3 = m_usort2universe.end();
for (; it3 != end3; ++it3) {
@@ -53,43 +39,6 @@ model::~model() {
}
}
-void model::register_decl(func_decl * d, expr * v) {
- SASSERT(d->get_arity() == 0);
- decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
- if (entry->get_data().m_value == 0) {
- // new entry
- m_decls.push_back(d);
- m_const_decls.push_back(d);
- m_manager.inc_ref(d);
- m_manager.inc_ref(v);
- entry->get_data().m_value = v;
- }
- else {
- // replacing entry
- m_manager.inc_ref(v);
- m_manager.dec_ref(entry->get_data().m_value);
- entry->get_data().m_value = v;
- }
-}
-
-void model::register_decl(func_decl * d, func_interp * fi) {
- SASSERT(d->get_arity() > 0);
- SASSERT(&fi->m() == &m_manager);
- decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
- if (entry->get_data().m_value == 0) {
- // new entry
- m_decls.push_back(d);
- m_func_decls.push_back(d);
- m_manager.inc_ref(d);
- entry->get_data().m_value = fi;
- }
- else {
- // replacing entry
- if (fi != entry->get_data().m_value)
- dealloc(entry->get_data().m_value);
- entry->get_data().m_value = fi;
- }
-}
void model::copy_const_interps(model const & source) {
diff --git a/src/model/model.h b/src/model/model.h
index 68ddc4015..338b6ad74 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -44,8 +44,7 @@ public:
bool eval(func_decl * f, expr_ref & r) const { return model_core::eval(f, r); }
bool eval(expr * e, expr_ref & result, bool model_completion = false);
- expr * get_some_value(sort * s);
-
+ virtual expr * get_some_value(sort * s);
virtual ptr_vector<expr> const & get_universe(sort * s) const;
virtual unsigned get_num_uninterpreted_sorts() const;
virtual sort * get_uninterpreted_sort(unsigned idx) const;
@@ -54,8 +53,6 @@ public:
//
// Primitives for building models
//
- void register_decl(func_decl * d, expr * v);
- void register_decl(func_decl * f, func_interp * fi);
void register_usort(sort * s, unsigned usize, expr * const * universe);
// Model translation
diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index 4351713db..5c2fd81d4 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -18,6 +18,23 @@ Revision History:
--*/
#include"model_core.h"
+model_core::~model_core() {
+ decl2expr::iterator it1 = m_interp.begin();
+ decl2expr::iterator end1 = m_interp.end();
+ for (; it1 != end1; ++it1) {
+ m_manager.dec_ref(it1->m_key);
+ m_manager.dec_ref(it1->m_value);
+ }
+
+ decl2finterp::iterator it2 = m_finterp.begin();
+ decl2finterp::iterator end2 = m_finterp.end();
+ for (; it2 != end2; ++it2) {
+ func_decl* d = it2->m_key;
+ m_manager.dec_ref(it2->m_key);
+ dealloc(it2->m_value);
+ }
+}
+
bool model_core::eval(func_decl* f, expr_ref & r) const {
if (f->get_arity() == 0) {
r = get_const_interp(f);
@@ -32,3 +49,42 @@ bool model_core::eval(func_decl* f, expr_ref & r) const {
return false;
}
}
+
+void model_core::register_decl(func_decl * d, expr * v) {
+ SASSERT(d->get_arity() == 0);
+ decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
+ if (entry->get_data().m_value == 0) {
+ // new entry
+ m_decls.push_back(d);
+ m_const_decls.push_back(d);
+ m_manager.inc_ref(d);
+ m_manager.inc_ref(v);
+ entry->get_data().m_value = v;
+ }
+ else {
+ // replacing entry
+ m_manager.inc_ref(v);
+ m_manager.dec_ref(entry->get_data().m_value);
+ entry->get_data().m_value = v;
+ }
+}
+
+void model_core::register_decl(func_decl * d, func_interp * fi) {
+ SASSERT(d->get_arity() > 0);
+ SASSERT(&fi->m() == &m_manager);
+ decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
+ if (entry->get_data().m_value == 0) {
+ // new entry
+ m_decls.push_back(d);
+ m_func_decls.push_back(d);
+ m_manager.inc_ref(d);
+ entry->get_data().m_value = fi;
+ }
+ else {
+ // replacing entry
+ if (fi != entry->get_data().m_value)
+ dealloc(entry->get_data().m_value);
+ entry->get_data().m_value = fi;
+ }
+}
+
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 9925582f3..8527a0bca 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -36,8 +36,8 @@ protected:
ptr_vector<func_decl> m_func_decls;
public:
- model_core(ast_manager & m):m_manager(m), m_ref_count(0) {}
- virtual ~model_core() {}
+ model_core(ast_manager & m):m_manager(m), m_ref_count(0) { }
+ virtual ~model_core();
ast_manager & get_manager() const { return m_manager; }
@@ -58,6 +58,11 @@ public:
virtual unsigned get_num_uninterpreted_sorts() const = 0;
virtual sort * get_uninterpreted_sort(unsigned idx) const = 0;
+ void register_decl(func_decl * d, expr * v);
+ void register_decl(func_decl * f, func_interp * fi);
+
+ virtual expr * get_some_value(sort * s) = 0;
+
//
// Reference counting
//
@@ -68,6 +73,7 @@ public:
dealloc(this);
}
}
+
};
#endif
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 1697b74ed..d417adc1b 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -32,7 +32,7 @@ Revision History:
#include"cooperate.h"
struct evaluator_cfg : public default_rewriter_cfg {
- model & m_model;
+ model_core & m_model;
bool_rewriter m_b_rw;
arith_rewriter m_a_rw;
bv_rewriter m_bv_rw;
@@ -46,7 +46,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool m_model_completion;
bool m_cache;
- evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
+ evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
m_model(md),
m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
@@ -231,7 +231,7 @@ template class rewriter_tpl<evaluator_cfg>;
struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
evaluator_cfg m_cfg;
- imp(model & md, params_ref const & p):
+ imp(model_core & md, params_ref const & p):
rewriter_tpl<evaluator_cfg>(md.get_manager(),
false, // no proofs for evaluator
m_cfg),
@@ -239,7 +239,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
}
};
-model_evaluator::model_evaluator(model & md, params_ref const & p) {
+model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
m_imp = alloc(imp, md, p);
}
@@ -269,7 +269,7 @@ unsigned model_evaluator::get_num_steps() const {
void model_evaluator::cleanup(params_ref const & p) {
- model & md = m_imp->cfg().m_model;
+ model_core & md = m_imp->cfg().m_model;
#pragma omp critical (model_evaluator)
{
dealloc(m_imp);
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index e0d76ec01..7fafbe14d 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -30,7 +30,7 @@ class model_evaluator {
struct imp;
imp * m_imp;
public:
- model_evaluator(model & m, params_ref const & p = params_ref());
+ model_evaluator(model_core & m, params_ref const & p = params_ref());
~model_evaluator();
ast_manager & m () const;
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 024de9f15..485fe1751 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -29,7 +29,6 @@ Revision History:
proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
model_core(m),
- m_asts(m),
m_simplifier(s),
m_afid(m.mk_family_id(symbol("array"))) {
register_factory(alloc(basic_factory, m));
@@ -39,45 +38,11 @@ proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
m_model_partial = model_params(p).partial();
}
-void proto_model::reset_finterp() {
- decl2finterp::iterator it = m_finterp.begin();
- decl2finterp::iterator end = m_finterp.end();
- for (; it != end; ++it) {
- dealloc(it->m_value);
- }
-}
-proto_model::~proto_model() {
- reset_finterp();
-}
-void proto_model::register_decl(func_decl * d, expr * v) {
- SASSERT(d->get_arity() == 0);
- if (m_interp.contains(d)) {
- DEBUG_CODE({
- expr * old_v = 0;
- m_interp.find(d, old_v);
- SASSERT(old_v == v);
- });
- return;
- }
- SASSERT(!m_interp.contains(d));
- m_decls.push_back(d);
- m_asts.push_back(d);
- m_asts.push_back(v);
- m_interp.insert(d, v);
- m_const_decls.push_back(d);
-}
-
-void proto_model::register_decl(func_decl * d, func_interp * fi, bool aux) {
- SASSERT(d->get_arity() > 0);
- SASSERT(!m_finterp.contains(d));
- m_decls.push_back(d);
- m_asts.push_back(d);
- m_finterp.insert(d, fi);
- m_func_decls.push_back(d);
- if (aux)
- m_aux_decls.insert(d);
+void proto_model::register_aux_decl(func_decl * d, func_interp * fi) {
+ model_core::register_decl(d, fi);
+ m_aux_decls.insert(d);
}
/**
@@ -486,6 +451,7 @@ void proto_model::cleanup() {
m_finterp.find(faux, fi);
SASSERT(fi != 0);
m_finterp.erase(faux);
+ m_manager.dec_ref(faux);
dealloc(fi);
}
}
@@ -666,20 +632,16 @@ model * proto_model::mk_model() {
decl2finterp::iterator end2 = m_finterp.end();
for (; it2 != end2; ++it2) {
m->register_decl(it2->m_key, it2->m_value);
+ m_manager.dec_ref(it2->m_key);
}
+
m_finterp.reset(); // m took the ownership of the func_interp's
unsigned sz = get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++) {
sort * s = get_uninterpreted_sort(i);
TRACE("proto_model", tout << "copying uninterpreted sorts...\n" << mk_pp(s, m_manager) << "\n";);
- ptr_buffer<expr> buf;
- obj_hashtable<expr> const & u = get_known_universe(s);
- obj_hashtable<expr>::iterator it = u.begin();
- obj_hashtable<expr>::iterator end = u.end();
- for (; it != end; ++it) {
- buf.push_back(*it);
- }
+ ptr_vector<expr> const& buf = get_universe(s);
m->register_usort(s, buf.size(), buf.c_ptr());
}
diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h
index d26f4d70d..1b63f8b20 100644
--- a/src/smt/proto_model/proto_model.h
+++ b/src/smt/proto_model/proto_model.h
@@ -38,7 +38,6 @@ Revision History:
#include"params.h"
class proto_model : public model_core {
- ast_ref_vector m_asts;
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;
simplifier & m_simplifier;
@@ -48,8 +47,6 @@ class proto_model : public model_core {
bool m_model_partial;
- void reset_finterp();
-
expr * mk_some_interp_for(func_decl * d);
// Invariant: m_decls subset m_func_decls union m_const_decls union union m_value_decls
@@ -63,7 +60,7 @@ class proto_model : public model_core {
public:
proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
- virtual ~proto_model();
+ virtual ~proto_model() {}
void register_factory(value_factory * f) { m_factories.register_plugin(f); }
@@ -73,7 +70,7 @@ public:
value_factory * get_factory(family_id fid);
- expr * get_some_value(sort * s);
+ virtual expr * get_some_value(sort * s);
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
@@ -84,8 +81,7 @@ public:
//
// Primitives for building models
//
- void register_decl(func_decl * d, expr * v);
- void register_decl(func_decl * f, func_interp * fi, bool aux = false);
+ void register_aux_decl(func_decl * f, func_interp * fi);
void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
void compress();
void cleanup();
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index d67b6a3eb..c1befd545 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -322,20 +322,17 @@ namespace smt {
for (; it != end; ++it) {
if (m_context->is_relevant(*it)) {
app* e = (*it)->get_owner();
- for (unsigned i = 0; i < e->get_num_args(); ++i) {
- args[num_decls - i - 1] = e->get_arg(i);
+ SASSERT(e->get_num_args() == num_decls);
+ for (unsigned i = 0; i < num_decls; ++i) {
+ args[i] = e->get_arg(i);
}
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
m_curr_model->eval(tmp, result, true);
- if (m.is_true(result)) {
- continue;
- }
if (m.is_false(result)) {
+ TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
add_instance(q, args, 0);
return false;
}
- TRACE("model_checker", tout << tmp << "evaluates to undetermined " << result << "\n";);
- is_undef = true;
}
}
return !is_undef;
@@ -395,7 +392,7 @@ namespace smt {
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
}
found_relevant = true;
- if (q->get_qid() == symbol(":rec-fun")) {
+ if (m.is_rec_fun_def(q)) {
if (!check_rec_fun(q)) {
num_failures++;
}
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index d7dc4d806..a425475c2 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -915,7 +915,7 @@ namespace smt {
}
func_interp * rpi = alloc(func_interp, m_manager, 1);
rpi->set_else(pi);
- m_model->register_decl(p, rpi, true);
+ m_model->register_aux_decl(p, rpi);
n->set_proj(p);
}
@@ -928,7 +928,7 @@ namespace smt {
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
func_interp * pi = alloc(func_interp, m_manager, 1);
pi->set_else(else_val);
- m_model->register_decl(p, pi, true);
+ m_model->register_aux_decl(p, pi);
ptr_buffer<expr>::const_iterator it = values.begin();
ptr_buffer<expr>::const_iterator end = values.end();
for (; it != end; ++it) {
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 88e9761b4..42fb8f1b5 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -516,43 +516,6 @@ namespace smt {
}
}
- /**
- \brief Auxiliary functor for method register_indirect_elim_decls.
- */
- class mk_interp_proc {
- context & m_context;
- proto_model & m_model;
- public:
- mk_interp_proc(context & ctx, proto_model & m):
- m_context(ctx),
- m_model(m) {
- }
-
- void operator()(var * n) {
- }
-
- void operator()(app * n) {
- if (!is_uninterp(n))
- return; // n is interpreted
- func_decl * d = n->get_decl();
- if (m_model.has_interpretation(d))
- return; // declaration already has an interpretation.
- if (n->get_num_args() == 0) {
- sort * r = d->get_range();
- expr * v = m_model.get_some_value(r);
- m_model.register_decl(d, v);
- }
- else {
- func_interp * fi = alloc(func_interp, m_context.get_manager(), d->get_arity());
- m_model.register_decl(d, fi);
- }
- }
-
- void operator()(quantifier * n) {
- }
-
- };
-
proto_model * model_generator::mk_model() {
SASSERT(!m_model);
TRACE("func_interp_bug", m_context->display(tout););
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 0501714ee..ad2c25e63 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -40,7 +40,6 @@ namespace smt {
ptr_vector<quantifier> m_quantifiers;
scoped_ptr<quantifier_manager_plugin> m_plugin;
unsigned m_num_instances;
- symbol m_rec_fun;
imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin):
m_wrapper(wrapper),
@@ -48,8 +47,7 @@ namespace smt {
m_params(p),
m_qi_queue(m_wrapper, ctx, p),
m_qstat_gen(ctx.get_manager(), ctx.get_region()),
- m_plugin(plugin),
- m_rec_fun(":rec-fun") {
+ m_plugin(plugin) {
m_num_instances = 0;
m_qi_queue.setup();
}
@@ -187,7 +185,7 @@ namespace smt {
}
bool check_quantifier(quantifier* q) {
- return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && q->get_qid() != m_rec_fun;
+ return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q);
}
bool quick_check_quantifiers() {
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 89a19da65..02b8f9514 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -547,6 +547,10 @@ namespace smt {
out << "\n";
}
+ bool theory_datatype::include_func_interp(func_decl* f) {
+ return false; // return m_util.is_accessor(f);
+ }
+
void theory_datatype::init_model(model_generator & m) {
m_factory = alloc(datatype_factory, get_manager(), m.get_model());
m.register_factory(m_factory);
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 8f47a3fc3..95c729dc2 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -111,6 +111,8 @@ namespace smt {
static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
void unmerge_eh(theory_var v1, theory_var v2);
virtual char const * get_name() const { return "datatype"; }
+ virtual bool include_func_interp(func_decl* f);
+
};
};