mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix crash in model construction from finite domain theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1e774064bc
commit
49f9f4b3b5
|
@ -599,7 +599,23 @@ namespace datalog {
|
|||
return 0;
|
||||
}
|
||||
result = mk_compare(OP_DL_LT, m_lt_sym, domain);
|
||||
break;
|
||||
break;
|
||||
|
||||
case OP_DL_REP: {
|
||||
if (!check_domain(0, 0, num_parameters) ||
|
||||
!check_domain(1, 1, arity)) return 0;
|
||||
func_decl_info info(m_family_id, k, 0, 0);
|
||||
result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
|
||||
break;
|
||||
}
|
||||
|
||||
case OP_DL_ABS: {
|
||||
if (!check_domain(0, 0, num_parameters) ||
|
||||
!check_domain(1, 1, arity)) return 0;
|
||||
func_decl_info info(m_family_id, k, 0, 0);
|
||||
result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
|
||||
break;
|
||||
}
|
||||
|
||||
default:
|
||||
m_manager->raise_exception("operator not recognized");
|
||||
|
|
|
@ -48,6 +48,8 @@ namespace datalog {
|
|||
OP_RA_CLONE,
|
||||
OP_DL_CONSTANT,
|
||||
OP_DL_LT,
|
||||
OP_DL_REP,
|
||||
OP_DL_ABS,
|
||||
LAST_RA_OP
|
||||
};
|
||||
|
||||
|
|
|
@ -102,6 +102,7 @@ namespace smt {
|
|||
if (th && th->build_models()) {
|
||||
if (r->get_th_var(th->get_id()) != null_theory_var) {
|
||||
proc = th->mk_value(r, *this);
|
||||
SASSERT(proc);
|
||||
}
|
||||
else {
|
||||
TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
|
||||
|
@ -110,6 +111,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
proc = mk_model_value(r);
|
||||
SASSERT(proc);
|
||||
}
|
||||
}
|
||||
SASSERT(proc);
|
||||
|
|
|
@ -162,7 +162,7 @@ namespace smt {
|
|||
m.register_factory(alloc(dl_factory, m_util, m.get_model()));
|
||||
}
|
||||
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n) {
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
|
||||
return alloc(dl_value_proc, *this, n);
|
||||
}
|
||||
|
||||
|
@ -201,9 +201,8 @@ namespace smt {
|
|||
if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
|
||||
SASSERT(!m_reps.contains(s));
|
||||
sort* bv = b().mk_sort(64);
|
||||
// TBD: filter these from model.
|
||||
r = m().mk_fresh_func_decl("rep",1, &s,bv);
|
||||
v = m().mk_fresh_func_decl("val",1, &bv,s);
|
||||
r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
|
||||
v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
|
||||
m_reps.insert(s, r);
|
||||
m_vals.insert(s, v);
|
||||
add_trail(r);
|
||||
|
|
Loading…
Reference in a new issue