mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-01 11:57:07 -07:00
parent 3afe081f62
commit 4fb867a49c
7 changed files with 28 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/recfun_decl_plugin.cpp
View file

@ -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);
}