mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c7dc420b3b
commit
59f69bbe0d
|
@ -23,18 +23,16 @@ Revision History:
|
|||
namespace smt {
|
||||
|
||||
bool checker::all_args(app * a, bool is_true) {
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
if (!check(a->get_arg(i), is_true))
|
||||
for (expr* arg : *a) {
|
||||
if (!check(arg, is_true))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool checker::any_arg(app * a, bool is_true) {
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
if (check(a->get_arg(i), is_true))
|
||||
for (expr* arg : *a) {
|
||||
if (check(arg, is_true))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
|
@ -78,6 +78,19 @@ namespace smt {
|
|||
return t;
|
||||
}
|
||||
|
||||
expr * model_checker::get_type_compatible_term(expr * val) {
|
||||
for (auto const& kv : m_value2expr) {
|
||||
if (m.get_sort(kv.m_key) == m.get_sort(val) &&
|
||||
!contains_model_value(kv.m_key)) {
|
||||
return kv.m_key;
|
||||
}
|
||||
}
|
||||
app* fresh_term = m.mk_fresh_const("sk", m.get_sort(val));
|
||||
m_context->ensure_internalized(fresh_term);
|
||||
m_value2expr.insert(val, fresh_term);
|
||||
return fresh_term;
|
||||
}
|
||||
|
||||
void model_checker::init_value2expr() {
|
||||
if (m_value2expr.empty()) {
|
||||
// populate m_value2expr
|
||||
|
@ -207,8 +220,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
if (contains_model_value(sk_value)) {
|
||||
TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";);
|
||||
return false;
|
||||
sk_value = get_type_compatible_term(sk_value);
|
||||
}
|
||||
func_decl * f = nullptr;
|
||||
if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f)) {
|
||||
|
|
|
@ -60,6 +60,7 @@ namespace smt {
|
|||
void init_aux_context();
|
||||
void init_value2expr();
|
||||
expr * get_term_from_ctx(expr * val);
|
||||
expr * get_type_compatible_term(expr * val);
|
||||
expr_ref replace_value_from_ctx(expr * e);
|
||||
void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
|
||||
void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
|
||||
|
|
Loading…
Reference in a new issue