mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

debug simplify_clause

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-14 12:12:21 +02:00
parent e711808d3e
commit eca72ffda1
3 changed files with 43 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/polysat/simplify_clause.cpp
View file

@ -40,6 +40,21 @@ Notes:
==> drop 294 because it implies 295
==> drop 292 because it implies 295
TODO from bench0:
-43 \/ 3 \/ 4 \/ -0 \/ -44 \/ -52
-43: v3 + -1 != 0
3: v3 == 0
4: v3 <= v5
-0: v5 + v4*v3 + -1*v2*v1 != 0
-44: v4 + -1 != 0
-52: v2 != 0
Drop v3 == 0 because it implies v3 - 1 != 0
The try_recognize_bailout returns true, but fails to simplify any other literal.
Overall, why return true immediately if there are other literals that subsume each-other?
--*/
#include "math/polysat/solver.h"
#include "math/polysat/simplify_clause.h"
@ -110,6 +125,8 @@ namespace polysat {
});
}
}
if (j == cl.size())
return false;
cl.m_literals.shrink(j);
return true;
}

4
src/math/polysat/solver.cpp
View file

@ -890,8 +890,10 @@ namespace polysat {
UNREACHABLE();
}
}
for (auto cl : side_lemmas)
for (auto cl : side_lemmas) {
m_simplify_clause.apply(*cl);
add_clause(*cl);
}
SASSERT(lemma_invariant_part2(lemma_invariant_todo));
learn_lemma(lemma);
}

23
src/test/polysat.cpp
View file

@ -354,6 +354,27 @@ namespace polysat {
s.expect_sat();
}
//
// -43 \/ 3 \/ 4
// -43: v3 + -1 != 0
// 3: v3 == 0
// 4: v3 <= v5
static void test_clause_simplify1() {
scoped_solver s(__func__);
simplify_clause simp(s);
clause_builder cb(s);
auto u = s.var(s.add_var(4));
auto v = s.var(s.add_var(4));
cb.push(s.eq(u));
cb.push(~s.eq(u - 1));
cb.push(s.ule(u, v));
auto cl = cb.build();
simp.apply(*cl);
std::cout << *cl << "\n";
SASSERT(cl->size() == 2);
}
/**
* Check unsat of:
@ -1409,6 +1430,8 @@ namespace polysat {
void tst_polysat() {
using namespace polysat;
test_polysat::test_clause_simplify1();
// test_polysat::test_add_conflicts(); // ok
// test_polysat::test_wlist(); // ok
// test_polysat::test_cjust(); // uses viable_fallback; weak lemmas