mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

#5778

Browse source 
deal with recursive calls to internalization with the same formula
This commit is contained in:
Nikolaj Bjorner 2022-04-02 01:28:58 -07:00
parent 2fedcbd41e
commit ef28f0e2f0
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/tactic/goal2sat.cpp
View file

@ -405,6 +405,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_result_stack.shrink(old_sz);
}
else {
if (process_cached(t, root, sign))
return;
SASSERT(num <= m_result_stack.size());
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
@ -454,6 +456,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_result_stack.shrink(old_sz);
}
else {
if (process_cached(t, root, sign))
return;
SASSERT(num <= m_result_stack.size());
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
@ -507,6 +511,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
else {
if (process_cached(n, root, sign))
return;
sat::bool_var k = add_var(false, n);
sat::literal l(k, false);
cache(n, l);
@ -537,6 +543,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_root_clause(sign ? lit : ~lit);
}
else {
if (process_cached(t, root, sign))
return;
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
cache(t, l);
@ -567,6 +575,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
else {
if (process_cached(t, root, sign))
return;
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
cache(t, l);
@ -603,6 +613,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
else {
if (process_cached(t, root, sign))
return;
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
if (m.is_xor(t))