mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
8bd0407adf
commit
ceca9fbef0
|
@ -148,7 +148,6 @@ namespace smt {
|
|||
m_node1(n1),
|
||||
m_node2(n2),
|
||||
m_js(js) {
|
||||
SASSERT(n1 != n2);
|
||||
}
|
||||
|
||||
virtual void get_antecedents(conflict_resolution & cr);
|
||||
|
|
|
@ -760,7 +760,7 @@ namespace smt {
|
|||
ptr_vector<expr> const & exceptions = n->get_exceptions();
|
||||
ptr_vector<node> const & avoid_set = n->get_avoid_set();
|
||||
obj_map<expr, unsigned> const & elems = s->get_elems();
|
||||
SASSERT(!elems.empty());
|
||||
if (elems.empty()) return;
|
||||
if (!exceptions.empty() || !avoid_set.empty()) {
|
||||
ptr_buffer<expr> ex_vals;
|
||||
collect_exceptions_values(n, ex_vals);
|
||||
|
@ -927,15 +927,14 @@ namespace smt {
|
|||
ptr_buffer<expr> values;
|
||||
get_instantiation_set_values(n, values);
|
||||
sort * s = n->get_sort();
|
||||
expr * else_val = eval(n->get_else(), true);
|
||||
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
|
||||
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
|
||||
func_interp * pi = alloc(func_interp, m_manager, 1);
|
||||
pi->set_else(else_val);
|
||||
m_model->register_aux_decl(p, pi);
|
||||
ptr_buffer<expr>::const_iterator it = values.begin();
|
||||
ptr_buffer<expr>::const_iterator end = values.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * v = *it;
|
||||
if (n->get_else()) {
|
||||
expr * else_val = eval(n->get_else(), true);
|
||||
pi->set_else(else_val);
|
||||
}
|
||||
for (expr * v : values) {
|
||||
pi->insert_new_entry(&v, v);
|
||||
}
|
||||
n->set_proj(p);
|
||||
|
|
Loading…
Reference in a new issue