3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

move towards theory phase selection, implement getitem on lambda

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-13 13:49:21 -07:00
parent 0eafeb9342
commit 520ea65f32
3 changed files with 23 additions and 12 deletions

View file

@ -1861,6 +1861,15 @@ class QuantifierRef(BoolRef):
"""
return Z3_is_lambda(self.ctx_ref(), self.ast)
def __getitem__(self, arg):
"""Return the Z3 expression `self[arg]`.
"""
if z3_debug():
_z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
arg = self.sort().domain().cast(arg)
return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
def weight(self):
"""Return the weight annotation of `self`.
@ -4288,6 +4297,9 @@ def is_array(a):
"""
return isinstance(a, ArrayRef)
def is_array_sort(a):
return _ast_kind(a.ctx(), a.sort()) == Z3_ARRAY_SORT
def is_const_array(a):
"""Return `True` if `a` is a Z3 constant array.
@ -4412,7 +4424,7 @@ def Update(a, i, v):
proved
"""
if z3_debug():
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
i = a.domain().cast(i)
v = a.range().cast(v)
ctx = a.ctx
@ -4425,7 +4437,7 @@ def Default(a):
proved
"""
if z3_debug():
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
return a.default()
@ -4456,7 +4468,7 @@ def Select(a, i):
True
"""
if z3_debug():
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
return a[i]
@ -4476,7 +4488,7 @@ def Map(f, *args):
if z3_debug():
_z3_assert(len(args) > 0, "At least one Z3 array expression expected")
_z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
_z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
_z3_assert(all([is_array_sort(a) for a in args]), "Z3 array expected expected")
_z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
_args, sz = _to_ast_array(args)
ctx = f.ctx
@ -4511,7 +4523,7 @@ def Ext(a, b):
"""
ctx = a.ctx
if z3_debug():
_z3_assert(is_array(a) and is_array(b), "arguments must be arrays")
_z3_assert(is_array_sort(a) and is_array_sort(b), "arguments must be arrays")
return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
def SetHasSize(a, k):

View file

@ -3873,7 +3873,9 @@ namespace smt {
default:
break;
}
if (m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE || m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE2)
if (m_fparams.m_phase_selection == PS_THEORY ||
m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE ||
m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE2)
forget_phase_of_vars_in_current_level();
m_atom_propagation_queue.reset();
m_eq_propagation_queue.reset();

View file

@ -317,6 +317,7 @@ namespace smt {
// }
// else {
TRACE("rdl_bug", tout << "using theory_mi_arith\n";);
//setup_lra_arith();
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
// }
}
@ -477,13 +478,10 @@ namespace smt {
m_params.m_relevancy_lvl = 2;
m_params.m_relevancy_lemma = false;
}
if (st.m_cnf) {
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
}
else {
m_params.m_phase_selection = PS_THEORY;
if (!st.m_cnf) {
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_arith_stronger_lemmas = false;
m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_restart_adaptive = false;
}
m_params.m_arith_small_lemma_size = 32;
@ -533,7 +531,6 @@ namespace smt {
}
else {
m_params.m_eliminate_term_ite = true;
m_params.m_phase_selection = PS_CACHING;
m_params.m_restart_adaptive = false;
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;