mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-04 17:35:17 +00:00
Code Activity

add code for adding assumptions after sat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-25 11:45:43 -07:00
parent a0ba950987
commit af4677950b
2 changed files with 38 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/smt/theory_nseq.cpp
View file

@ -567,6 +567,11 @@ namespace smt {
<< (m_nielsen.sat_node() ? "set" : "null") << "\n";); << (m_nielsen.sat_node() ? "set" : "null") << "\n";);
// Nielsen found a consistent assignment for positive constraints. // Nielsen found a consistent assignment for positive constraints.
SASSERT(has_eq_or_mem); // we should have axiomatized them SASSERT(has_eq_or_mem); // we should have axiomatized them
#if 0
// TODO: add this pending review
if (!add_nielsen_assumptions())
return FC_CONTINUE;
#endif
if (!has_unhandled_preds()) if (!has_unhandled_preds())
return FC_DONE; return FC_DONE;
} }
@ -575,6 +580,38 @@ namespace smt {
return FC_GIVEUP; return FC_GIVEUP;
} }
bool theory_nseq::add_nielsen_assumptions() {
bool has_undef = false;
bool has_false = false;
for (auto const& c : m_nielsen.sat_node()->constraints()) {
auto lit = mk_literal(c.fml);
switch (ctx.get_assignment(lit)) {
case l_true: break;
case l_undef:
has_undef = true;
ctx.force_phase(lit);
IF_VERBOSE(2, verbose_stream() <<
"nseq final_check: adding nielsen assumption " << c.fml << "\n";);
break;
case l_false:
// do we really expect this to happen?
has_false = true;
IF_VERBOSE(1, verbose_stream()
<< "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
ctx.force_phase(lit);
break;
}
}
if (has_undef)
return false;
if (has_false) {
// fishy case.
return false;
}
return true;
}
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
// Conflict explanation // Conflict explanation
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------

1
src/smt/theory_nseq.h
View file

@ -114,6 +114,7 @@ namespace smt {
void populate_nielsen_graph(); void populate_nielsen_graph();
void explain_nielsen_conflict(); void explain_nielsen_conflict();
void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits); void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
bool add_nielsen_assumptions();
euf::snode* get_snode(expr* e); euf::snode* get_snode(expr* e);
// propagation dispatch helpers // propagation dispatch helpers