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

remove test code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-29 21:05:41 -07:00
parent fd66d2f26c
commit 487a544274
3 changed files with 9 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -212,11 +212,11 @@ namespace polysat {
sat::check_result core::check() { sat::check_result core::check() {
lbool r = l_true; lbool r = l_true;
verbose_stream() << "check-propagate\n"; //verbose_stream() << "check-propagate\n";
if (propagate()) if (propagate())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
verbose_stream() << "check-assign-variable\n"; //verbose_stream() << "check-assign-variable\n";
switch (assign_variable()) { switch (assign_variable()) {
case l_true: case l_true:
break; break;
@ -230,7 +230,7 @@ namespace polysat {
break; break;
} }
verbose_stream() << "check-saturate\n"; //verbose_stream() << "check-saturate\n";
saturation saturate(*this); saturation saturate(*this);
switch (saturate()) { switch (saturate()) {
case l_true: case l_true:
@ -239,12 +239,12 @@ namespace polysat {
TRACE("bv", tout << "saturate\n"); TRACE("bv", tout << "saturate\n");
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
case l_undef: case l_undef:
verbose_stream() << "giveup saturate\n"; //verbose_stream() << "giveup saturate\n";
r = l_undef; r = l_undef;
break; break;
} }
verbose_stream() << "check-refine\n"; //verbose_stream() << "check-refine\n";
switch (m_monomials.refine()) { switch (m_monomials.refine()) {
case l_true: case l_true:
break; break;
@ -252,12 +252,12 @@ namespace polysat {
TRACE("bv", tout << "refine\n"); TRACE("bv", tout << "refine\n");
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
case l_undef: case l_undef:
verbose_stream() << "giveup refine\n"; //verbose_stream() << "giveup refine\n";
r = l_undef; r = l_undef;
break; break;
} }
verbose_stream() << "check-blast\n"; //verbose_stream() << "check-blast\n";
switch (m_monomials.bit_blast()) { switch (m_monomials.bit_blast()) {
case l_true: case l_true:
break; break;
@ -265,7 +265,7 @@ namespace polysat {
TRACE("bv", tout << "blast\n"); TRACE("bv", tout << "blast\n");
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
case l_undef: case l_undef:
verbose_stream() << "giveup blast\n"; //verbose_stream() << "giveup blast\n";
r = l_undef; r = l_undef;
break; break;
} }

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

@ -456,7 +456,7 @@ namespace polysat {
auto rv = c.subst(r); auto rv = c.subst(r);
auto& C = c.cs(); auto& C = c.cs();
verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n"; //verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n";
if (!pv.is_val() || !qv.is_val() || !rv.is_val()) if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return false; return false;

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

@ -358,10 +358,7 @@ namespace polysat {
return; return;
if (a.degree(v) < r.degree(v)) if (a.degree(v) < r.degree(v))
return; return;
verbose_stream() << "resolve: " << a << " = " << b << " => " << r << "\n";
add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true); add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);
exit(0);
} }