mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5429

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-27 19:11:16 -07:00
parent 16413b4f9a
commit 442d1d28ea
1 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -544,6 +544,29 @@ struct goal2sat::imp : public sat::sat_internalizer {
} }
} }
void convert_not(app* t, bool root, bool sign) {
SASSERT(t->get_num_args() == 1);
unsigned sz = m_result_stack.size();
SASSERT(sz >= 1);
sat::literal lit = m_result_stack[sz - 1];
m_result_stack.shrink(sz - 1);
if (root) {
SASSERT(sz == 1);
mk_root_clause(sign ? lit : ~lit);
}
else {
sat::bool_var k = add_var(false, t);
sat::literal l(k, false);
cache(t, l);
// l <=> ~lit
mk_clause(lit, l);
mk_clause(~lit, ~l);
if (sign)
l.neg();
m_result_stack.push_back(l);
}
}
void convert_implies(app* t, bool root, bool sign) { void convert_implies(app* t, bool root, bool sign) {
SASSERT(t->get_num_args() == 2); SASSERT(t->get_num_args() == 2);
unsigned sz = m_result_stack.size(); unsigned sz = m_result_stack.size();
@ -702,6 +725,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
case OP_IMPLIES: case OP_IMPLIES:
convert_implies(t, root, sign); convert_implies(t, root, sign);
break; break;
case OP_NOT:
convert_not(t, root, sign);
break;
default: default:
UNREACHABLE(); UNREACHABLE();
} }
@ -767,7 +793,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_frame_stack.pop_back(); m_frame_stack.pop_back();
continue; continue;
} }
if (m.is_not(t)) { if (m.is_not(t) && !m.is_not(t->get_arg(0))) {
m_frame_stack.pop_back(); m_frame_stack.pop_back();
visit(t->get_arg(0), root, !sign); visit(t->get_arg(0), root, !sign);
continue; continue;