mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Re-enable saturation

Browse source
This commit is contained in:
Jakob Rath 2022-11-29 10:00:25 +01:00
parent 4aa04fa475
commit 630276dbad
3 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/conflict.cpp
View file

@ -57,13 +57,13 @@ TODO:
namespace polysat { namespace polysat {
class conflict_resolver { class conflict_resolver {
saturation m_saturate; saturation m_saturation;
ex_polynomial_superposition m_poly_sup; ex_polynomial_superposition m_poly_sup;
free_variable_elimination m_free_variable_elimination; free_variable_elimination m_free_variable_elimination;
public: public:
conflict_resolver(solver& s) conflict_resolver(solver& s)
: m_saturate(s) : m_saturation(s)
, m_poly_sup(s) , m_poly_sup(s)
, m_free_variable_elimination(s) , m_free_variable_elimination(s)
{} {}
@ -71,8 +71,8 @@ namespace polysat {
bool try_resolve_value(pvar v, conflict& core) { bool try_resolve_value(pvar v, conflict& core) {
if (m_poly_sup.perform(v, core)) if (m_poly_sup.perform(v, core))
return true; return true;
// if (m_saturate.perform(v, core)) if (m_saturation.perform(v, core))
// return true; return true;
return false; return false;
} }

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

@ -80,7 +80,7 @@ namespace polysat {
// return false; // return false;
SASSERT(c.bvalue(s) != l_true); SASSERT(c.bvalue(s) != l_true);
m_lemma.insert(c); m_lemma.insert_eval(c);
core.add_lemma(m_rule, m_lemma.build()); core.add_lemma(m_rule, m_lemma.build());
return true; return true;
} }
@ -91,7 +91,7 @@ namespace polysat {
} }
void saturation::insert_omega(pdd const& x, pdd const& y) { void saturation::insert_omega(pdd const& x, pdd const& y) {
m_lemma.insert(s.umul_ovfl(x, y)); m_lemma.insert_eval(s.umul_ovfl(x, y));
} }
/* /*

5
src/test/polysat.cpp
View file

@ -1059,7 +1059,7 @@ namespace polysat {
// xy < xz and !Omega(x*y) => y < z // xy < xz and !Omega(x*y) => y < z
static void test_ineq_axiom1(unsigned bw = 32, std::optional<unsigned> perm = std::nullopt) { static void test_ineq_axiom1(unsigned bw = 32, std::optional<unsigned> perm = std::nullopt) {
if (perm) { if (perm) {
scoped_solver s(std::string(__func__) + " perm=" + std::to_string(*perm)); scoped_solver s(concat(__func__, " bw=", bw, " perm=", *perm));
auto const bound = rational::power_of_two(bw/2); auto const bound = rational::power_of_two(bw/2);
auto x = s.var(s.add_var(bw)); auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw)); auto y = s.var(s.add_var(bw));
@ -1544,7 +1544,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_pop_conflict(); // test_polysat::test_ineq_axiom1(32, 1);
// test_polysat::test_pop_conflict();
// test_polysat::test_l2(); // test_polysat::test_l2();
// test_polysat::test_ineq1(); // test_polysat::test_ineq1();
// test_polysat::test_quot_rem(); // test_polysat::test_quot_rem();