mirror of
https://github.com/Z3Prover/z3
synced 2025-07-21 03:42:04 +00:00
Disable simplify_clause::try_recognize_bailout for now
This commit is contained in:
parent
596a53c14b
commit
c08866dcec
2 changed files with 12 additions and 5 deletions
|
@ -66,14 +66,18 @@ namespace polysat {
|
||||||
{}
|
{}
|
||||||
|
|
||||||
bool simplify_clause::apply(clause& cl) {
|
bool simplify_clause::apply(clause& cl) {
|
||||||
|
LOG_H1("Simplifying clause: " << cl);
|
||||||
|
#if 0
|
||||||
if (try_recognize_bailout(cl))
|
if (try_recognize_bailout(cl))
|
||||||
return true;
|
return true;
|
||||||
|
#endif
|
||||||
if (try_equal_body_subsumptions(cl))
|
if (try_equal_body_subsumptions(cl))
|
||||||
return true;
|
return true;
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
// If x != k appears among the new literals, all others are superfluous.
|
// If x != k appears among the new literals, all others are superfluous.
|
||||||
|
// TODO: this seems to work for lemmas coming from forbidden intervals, but in general it's too naive (esp. for side lemmas).
|
||||||
bool simplify_clause::try_recognize_bailout(clause& cl) {
|
bool simplify_clause::try_recognize_bailout(clause& cl) {
|
||||||
LOG_H2("Try to find bailout literal");
|
LOG_H2("Try to find bailout literal");
|
||||||
pvar v = null_var;
|
pvar v = null_var;
|
||||||
|
|
|
@ -97,11 +97,13 @@ namespace polysat {
|
||||||
out << " ";
|
out << " ";
|
||||||
for (size_t i = r.m_name.length(); i < max_name_len; ++i)
|
for (size_t i = r.m_name.length(); i < max_name_len; ++i)
|
||||||
out << ' ';
|
out << ' ';
|
||||||
// auto d = std::chrono::duration_cast<std::chrono::milliseconds>(r.end - r.start);
|
|
||||||
std::chrono::duration<double> d = r.end - r.start;
|
std::chrono::duration<double> d = r.end - r.start;
|
||||||
// d.count()
|
if (d.count() >= 0.15) {
|
||||||
out << std::fixed << std::setprecision(1);
|
out << std::fixed << std::setprecision(1);
|
||||||
out << std::setw(4) << d.count() << "s ";
|
out << std::setw(4) << d.count() << "s ";
|
||||||
|
}
|
||||||
|
else
|
||||||
|
out << " ";
|
||||||
switch (r.m_answer) {
|
switch (r.m_answer) {
|
||||||
case l_undef: out << " "; break;
|
case l_undef: out << " "; break;
|
||||||
case l_true: out << "SAT "; break;
|
case l_true: out << "SAT "; break;
|
||||||
|
@ -1558,7 +1560,8 @@ void tst_polysat() {
|
||||||
|
|
||||||
#if 0 // Enable this block to run a single unit test with detailed output.
|
#if 0 // Enable this block to run a single unit test with detailed output.
|
||||||
collect_test_records = false;
|
collect_test_records = false;
|
||||||
test_polysat::test_ineq_axiom5(32, 0);
|
// test_polysat::test_ineq1();
|
||||||
|
test_polysat::test_quot_rem();
|
||||||
return;
|
return;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue