mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix sort retrieval for lambdas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-01 09:18:40 -07:00
parent 6dcec4ce79
commit aaba1b9b15
2 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -1749,7 +1749,9 @@ class QuantifierRef(BoolRef):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def sort(self): def sort(self):
"""Return the Boolean sort.""" """Return the Boolean sort or sort of Lambda."""
if self.is_lambda():
return _sort(self.ctx, self.as_ast())
return BoolSort(self.ctx) return BoolSort(self.ctx)
def is_forall(self): def is_forall(self):

15
src/smt/theory_array_full.cpp
View file

@ -339,6 +339,7 @@ namespace smt {
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);
v = find(v); v = find(v);
var_data* d = m_var_data[v]; var_data* d = m_var_data[v];
TRACE("array", tout << "v" << v << "\n";);
for (enode * store : d->m_stores) { for (enode * store : d->m_stores) {
SASSERT(is_store(store)); SASSERT(is_store(store));
instantiate_default_store_axiom(store); instantiate_default_store_axiom(store);
@ -383,13 +384,21 @@ namespace smt {
void theory_array_full::relevant_eh(app* n) { void theory_array_full::relevant_eh(app* n) {
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";); TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
theory_array::relevant_eh(n); theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)) { if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_store(n)) {
return; return;
} }
context & ctx = get_context(); context & ctx = get_context();
enode* node = ctx.get_enode(n); enode* node = ctx.get_enode(n);
if (is_store(n)) {
if (is_select(n)) { enode * arg = ctx.get_enode(n->get_arg(0));
if (is_const(arg)) {
TRACE("array", tout << expr_ref(arg->get_owner(), get_manager()) << " " << is_const(arg) << "\n";);
theory_var v = arg->get_th_var(get_id());
set_prop_upward(v);
add_parent_default(v);
}
}
else if (is_select(n)) {
enode * arg = ctx.get_enode(n->get_arg(0)); enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id()); theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);