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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-26 10:41:20 -07:00
parent c21a2fcf9f
commit 1a36d44450
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -173,7 +173,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
if (!is_uninterp_const(t)) {
if (m_euf) {
convert_euf(t, root, sign);
convert_euf(t, root, sign);
return;
}
else
@ -186,6 +186,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
l = sat::literal(v, sign);
m_solver.set_eliminated(v, false);
}
if (root)
m_result_stack.reset();
SASSERT(l != sat::null_literal);
if (root)
mk_clause(l);
@ -331,7 +333,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_cache.insert(t, l);
sat::literal * lits = m_result_stack.end() - num;
// l => /\ lits
for (unsigned i = 0; i < num; i++) {
mk_clause(~l, lits[i]);
@ -481,6 +482,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::literal lit = internalize.internalize(*this, t, sign, root);
if (root)
m_result_stack.reset();
else
m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
if (lit == sat::null_literal)
return;
if (root)
@ -507,6 +510,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
default:
UNREACHABLE();
}
SASSERT(!root || m_result_stack.empty());
}
else if (pb.is_pb(t)) {
convert_ba(t, root, sign);
@ -781,7 +785,6 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
flush_gmc();
}
void sat2goal::mc::flush_gmc() {
sat::literal_vector updates;
m_smc.expand(updates);