mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

Fix compilation error in aig_exporter.cpp - use correct iterator API

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 20:32:41 +00:00
parent bef113254c
commit bc2441c1c4
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/rel/aig_exporter.cpp
View file

@ -23,8 +23,8 @@ namespace datalog {
m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m) m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m)
{ {
std::set<func_decl*> predicates; std::set<func_decl*> predicates;
for (auto& [pred, _] : m_rules.get_grouped_rules()) for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it)
predicates.insert(pred); predicates.insert(it->m_key);
for (auto& [pred, _] : *facts) for (auto& [pred, _] : *facts)
predicates.insert(pred); predicates.insert(pred);
@ -98,8 +98,8 @@ namespace datalog {
expr_ref_vector exprs(m); expr_ref_vector exprs(m);
substitution subst(m); substitution subst(m);
for (auto& [pred, rules] : m_rules.get_grouped_rules()) { for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it) {
for (rule* r : *rules) { for (rule* r : *it->get_value()) {
unsigned numqs = r->get_positive_tail_size(); unsigned numqs = r->get_positive_tail_size();
if (numqs > 1) { if (numqs > 1) {
throw default_exception("non-linear clauses not supported"); throw default_exception("non-linear clauses not supported");