mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

build fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-13 09:13:41 -07:00
parent 939bf1c725
commit b909b87acc
2 changed files with 30 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/ast/polymorphism_inst.cpp
View file

@ -38,29 +38,30 @@ namespace polymorphism {
if (!u.has_type_vars(e))
return;
// insert e into the occurs list for polymorphic roots
ast_mark seen;
for (auto* f : inst.m_poly_fns) {
f = m.poly_root(f);
if (seen.is_marked(f))
continue;
seen.mark(f, true);
if (!m_occurs.contains(f)) {
m_occurs.insert(f, ptr_vector<expr>());
t.push(insert_map(m_occurs, f));
}
auto& es = m_occurs.find(f);
es.push_back(e);
t.push(remove_back(m_occurs, f));
// insert e into the occurs list for polymorphic roots
ast_mark seen;
for (auto* f : inst.m_poly_fns) {
f = m.poly_root(f);
if (seen.is_marked(f))
continue;
seen.mark(f, true);
if (!m_occurs.contains(f)) {
m_occurs.insert(f, ptr_vector<expr>());
t.push(insert_map(m_occurs, f));
}
m_assertions.push_back(e);
t.push(push_back_vector(m_assertions));
u.collect_type_vars(e, inst.m_tvs);
inst.m_subst = alloc(substitutions);
inst.m_subst->insert(alloc(substitution, m));
m_instances.insert(e, inst);
t.push(new_obj_trail(inst.m_subst));
t.push(insert_map(m_instances, e));
auto& es = m_occurs.find(f);
es.push_back(e);
t.push(remove_back(m_occurs, f));
}
m_assertions.push_back(e);
t.push(push_back_vector(m_assertions));
u.collect_type_vars(e, inst.m_tvs);
inst.m_subst = alloc(substitutions);
inst.m_subst->insert(alloc(substitution, m));
m_instances.insert(e, inst);
t.push(new_obj_trail(inst.m_subst));
t.push(insert_map(m_instances, e));
}
void inst::collect_instantiations(expr* e) {

12
src/ast/polymorphism_util.cpp
View file

@ -41,8 +41,10 @@ namespace polymorphism {
vector<parameter> ps;
for (unsigned i = 0; i < n; ++i) {
auto p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast()))
ps.push_back(parameter((*this)(to_sort(p.get_ast()))));
if (p.is_ast() && is_sort(p.get_ast())) {
sort_ref s = (*this)(to_sort(p.get_ast()));
ps.push_back(parameter(s.get()));
}
else
ps.push_back(p);
}
@ -101,11 +103,11 @@ namespace polymorphism {
if (pending)
continue;
todo.pop_back();
ptr_buffer<sort> sorts;
domain.reset();
for (unsigned i = 0; i < q->get_num_decls(); ++i)
sorts.push_back((*this)(q->get_decl_sort(i)));
domain.push_back((*this)(q->get_decl_sort(i)));
quantifier* q2 =
m.mk_quantifier(q->get_kind(), q->get_num_decls(), sorts.data(), q->get_decl_names(), result.get(q->get_expr()->get_id()),
m.mk_quantifier(q->get_kind(), q->get_num_decls(), domain.data(), q->get_decl_names(), result.get(q->get_expr()->get_id()),
q->get_weight(),
q->get_qid(), q->get_skid(),
q->get_num_patterns(), patterns.data(), q->get_num_no_patterns(), no_patterns.data()