mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

constant overflow forbidden interval

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-15 09:46:45 -08:00
parent a68bbb53e4
commit 677e261bb1
5 changed files with 28 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/sat/smt/polysat/core.cpp
View file

@ -154,7 +154,22 @@ namespace polysat {
lbool core::assign_variable() { lbool core::assign_variable() {
if (m_var_queue.empty()) if (m_var_queue.empty())
return l_true; return l_true;
m_var = m_var_queue.min_var();
for (auto v : m_var_queue) {
switch (assign_variable(v)) {
case l_false:
return l_false;
case l_true:
return l_true;
default:
break;
}
}
return l_undef;
}
lbool core::assign_variable(pvar v) {
m_var = v;
CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n");); CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n"););
SASSERT(!is_assigned(m_var)); SASSERT(!is_assigned(m_var));
@ -206,11 +221,11 @@ namespace polysat {
case l_false: case l_false:
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
case l_undef: case l_undef:
verbose_stream() << "giveup assign\n"; // verbose_stream() << "giveup assign\n";
return sat::check_result::CR_GIVEUP; // return sat::check_result::CR_GIVEUP;
// or: // or:
// r = l_undef; r = l_undef;
// break; break;
} }
saturation saturate(*this); saturation saturate(*this);

1
src/sat/smt/polysat/core.h
View file

@ -92,6 +92,7 @@ namespace polysat {
void add_watch(unsigned idx, unsigned var); void add_watch(unsigned idx, unsigned var);
lbool assign_variable(); lbool assign_variable();
lbool assign_variable(pvar v);
void add_opdef(signed_constraint sc); void add_opdef(signed_constraint sc);

4
src/sat/smt/polysat/forbidden_intervals.cpp
View file

@ -118,7 +118,7 @@ namespace polysat {
rational A = div(bound, b2.val()); rational A = div(bound, b2.val());
rational B = div(bound + A, A) - 1; rational B = div(bound + A, A) - 1;
if (A >= 4 && B >= 4) { if (!e2.is_val() && A >= 4 && B >= 4) {
_backtrack.released = false; _backtrack.released = false;
return false; return false;
} }
@ -149,7 +149,7 @@ namespace polysat {
// := div(2^N + A - 1, A) // := div(2^N + A - 1, A)
rational A = div(bound, b2.val()) + 1; rational A = div(bound, b2.val()) + 1;
rational B = div(bound + A, A); rational B = div(bound + A, A);
if (A >= 4 && B >= 4) { if (!e2.is_val() && A >= 4 && B >= 4) {
_backtrack.released = false; _backtrack.released = false;
return false; return false;
} }

4
src/sat/smt/polysat/saturation.cpp
View file

@ -28,9 +28,11 @@ namespace polysat {
lbool eval_value = c.strong_eval(sc); lbool eval_value = c.strong_eval(sc);
if (eval_value == l_true) if (eval_value == l_true)
continue; continue;
has_conflict = true;
if (eval_value == l_undef)
continue;
TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"); TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
SASSERT(eval_value != l_undef);
has_conflict = true; has_conflict = true;
auto vars = c.find_conflict_variables(idx); auto vars = c.find_conflict_variables(idx);

2
src/sat/smt/polysat/viable.cpp
View file

@ -148,7 +148,7 @@ namespace polysat {
} }
return find_t::multiple; return find_t::multiple;
} }
TRACE("bv", display(tout << "resource-out v" << v << "\n"));
return find_t::resource_out; return find_t::resource_out;
} }