mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-30 21:57:46 +00:00
Code Activity

turn on constraint integrity checking

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-29 19:30:13 -07:00
parent d7ee475bc3
commit 684cb23b40
2 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq/seq_nielsen.cpp
View file

@ -287,7 +287,7 @@ namespace seq {
expr* v = s.m_var->arg(0)->get_expr(); expr* v = s.m_var->arg(0)->get_expr();
expr* repl = s.m_replacement->arg(0)->get_expr(); expr* repl = s.m_replacement->arg(0)->get_expr();
expr* eq = sg.get_manager().mk_eq(v, repl); expr* eq = sg.get_manager().mk_eq(v, repl);
m_constraints.push_back(constraint(eq, s.m_dep, sg.get_manager())); add_constraint(constraint(eq, s.m_dep, sg.get_manager()));
} }
} }
@ -1496,12 +1496,7 @@ namespace seq {
if (!node->is_extended()) { if (!node->is_extended()) {
bool ext = generate_extensions(node); bool ext = generate_extensions(node);
IF_VERBOSE(1, display(verbose_stream(), node)); IF_VERBOSE(1, display(verbose_stream(), node));
if (!ext) { CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n");
#ifdef Z3DEBUG
std::string dot = to_dot();
std::cout << dot << std::endl;
#endif
}
VERIFY(ext); VERIFY(ext);
node->set_extended(true); node->set_extended(true);
++m_stats.m_num_extensions; ++m_stats.m_num_extensions;

12
src/smt/theory_nseq.cpp
View file

@ -90,7 +90,7 @@ namespace smt {
if (is_not) if (is_not)
lit.neg(); lit.neg();
if (ctx.get_assignment(lit) == l_false) { if (ctx.get_assignment(lit) == l_false) {
IF_VERBOSE(1, verbose_stream() << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n"); TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
return lit; return lit;
} }
return sat::null_literal; return sat::null_literal;
@ -626,18 +626,20 @@ namespace smt {
bool theory_nseq::add_nielsen_assumptions() { bool theory_nseq::add_nielsen_assumptions() {
return true; // return true;
bool has_undef = false; bool has_undef = false;
bool has_false = false; bool has_false = false;
for (auto const& c : m_nielsen.sat_node()->constraints()) { for (auto const& c : m_nielsen.sat_node()->constraints()) {
auto lit = mk_literal(c.fml); auto lit = mk_literal(c.fml);
switch (ctx.get_assignment(lit)) { switch (ctx.get_assignment(lit)) {
case l_true: break; case l_true:
break;
case l_undef: case l_undef:
has_undef = true; has_undef = true;
ctx.force_phase(lit); ctx.force_phase(lit);
IF_VERBOSE(0, verbose_stream() << IF_VERBOSE(2, verbose_stream() <<
"nseq final_check: adding nielsen assumption " << c.fml << "\n";); "nseq final_check: adding nielsen assumption " << c.fml << "\n";);
TRACE(seq, tout << "assign: " << c.fml << "\n");
break; break;
case l_false: case l_false:
// do we really expect this to happen? // do we really expect this to happen?
@ -645,6 +647,8 @@ namespace smt {
IF_VERBOSE(0, verbose_stream() IF_VERBOSE(0, verbose_stream()
<< "nseq final_check: nielsen assumption " << c.fml << " is false\n";); << "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
ctx.force_phase(lit); ctx.force_phase(lit);
TRACE(seq, tout << "assigned to false: " << c.fml << "\n");
UNREACHABLE();
break; break;
} }
} }