mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 21:48:56 +00:00
Code Activity

fix #3434

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-23 11:51:21 -07:00
parent acb9376ea0
commit 519c0d5f11
1 changed files with 22 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tactic/aig/aig.cpp
View file

@ -546,14 +546,34 @@ struct aig_manager::imp {
} }
void mk_iff(unsigned spos) { void mk_iff(unsigned spos) {
if (spos + 2 != m_result_stack.size())
throw default_exception("aig conversion assumes expressions have been simplified");
SASSERT(spos + 2 == m_result_stack.size()); SASSERT(spos + 2 == m_result_stack.size());
aig_lit r = m.mk_iff(m_result_stack[spos], m_result_stack[spos+1]); aig_lit r = m.mk_iff(m_result_stack[spos], m_result_stack[spos+1]);
save_node_result(spos, r); save_node_result(spos, r);
} }
void mk_xor(unsigned spos) { void mk_xor(unsigned spos) {
SASSERT(spos + 2 == m_result_stack.size()); SASSERT(spos <= m_result_stack.size());
aig_lit r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]); unsigned num = m_result_stack.size() - spos;
aig_lit r;
switch (num) {
case 0:
r = m.m_true;
break;
case 1:
r = m_result_stack[spos];
break;
case 2:
r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
break;
default:
r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
for (unsigned i = 2; i < num; ++i) {
r = m.mk_xor(r, m_result_stack[spos + i]);
}
break;
}
save_node_result(spos, r); save_node_result(spos, r);
} }