From 8d43d98710d63136cd4c6c235a1dff165acb8fa8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 04:23:05 -0700 Subject: [PATCH 1/2] prepare tests Signed-off-by: Nikolaj Bjorner --- src/test/fixplex.cpp | 112 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 112 insertions(+) diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp index 3ef9774b4..6d0967859 100644 --- a/src/test/fixplex.cpp +++ b/src/test/fixplex.cpp @@ -1,3 +1,4 @@ + #include "math/polysat/fixplex.h" #include "math/polysat/fixplex_def.h" #include "ast/bv_decl_plugin.h" @@ -367,6 +368,117 @@ namespace polysat { std::cout << "number of failures: " << num_bad << "\n"; } + + static void test_lp( + vector>> const& rows, + svector const& ineqs, + vector> const& bounds) { + + unsigned num_vars = 1; + for (auto const& row : rows) + for (auto [v, c] : row) + num_vars = std::max(num_vars, v + 1); + for (auto const& i : ineqs) + num_vars = std::max(num_vars, std::max(i.v, i.w)); + num_vars = std::max(bounds.size(), num_vars); + + ast_manager m; + reg_decl_plugins(m); + bv_util bv(m); + smt_params pa; + smt::kernel solver(m, pa); + expr_ref_vector variables(m); + for (unsigned i = 0; i < num_vars; ++i) + variables.push_back(m.mk_fresh_const("v", bv.mk_sort(32))); + auto mk_ult = [&](expr* a, expr* b) { + return m.mk_not(bv.mk_ule(b, a)); + }; + + scoped_fp fp; + for (auto& row : rows) { + vector coeffs; + svector vars; + expr_ref term(m); + term = bv.mk_numeral(0, 32); + for (auto [v, c] : row) { + coeffs.push_back(rational(c, rational::ui64())); + vars.push_back(v); + term = bv.mk_bv_add(term, bv.mk_bv_mul(bv.mk_numeral(c, 32), variables.get(v))); + } + fp.add_row(row[0].first, row.size(), vars.data(), coeffs.data()); + solver.assert_expr(m.mk_eq(bv.mk_numeral(0, 32), term)); + } + unsigned index = 0; + for (auto const& i : ineqs) { + ++index; + if (i.strict) { + fp.add_lt(i.v, i.w, index); + solver.assert_expr(mk_ult(variables.get(i.v), variables.get(i.w))); + } + else { + fp.add_le(i.v, i.w, index); + solver.assert_expr(bv.mk_ule(variables.get(i.v), variables.get(i.w))); + } + } + unsigned v = 0; + for (auto const& b : bounds) { + ++index; + if (!b.is_free()) { + fp.set_bounds(v, rational(b.lo, rational::ui64()), rational(b.hi, rational::ui64()), index); + + if (b.lo < b.hi) { + solver.assert_expr(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v))); + solver.assert_expr(mk_ult(variables.get(v), bv.mk_numeral(b.hi, 32))); + } + else if (b.hi == 0) + solver.assert_expr(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v))); + else { + expr_ref a(mk_ult(variables.get(v), bv.mk_numeral(b.hi, 32)), m); + expr_ref b(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v)), m); + solver.assert_expr(m.mk_or(a, b)); + } + } + } + + solver.display(std::cout); + std::cout << fp << "\n"; + + lbool r1 = solver.check(); + lbool r2 = fp.make_feasible(); + + std::cout << r1 << " " << r2 << "\n" << fp << "\n"; + + if (r2 == l_true) { + std::cout << "TBD validate solution\n"; + } + if (r1 == r2) { + std::cout << "agree\n"; + } + else if (r1 == l_false && r2 == l_true) { + std::cout << "BUG should be unsat\n"; + solver.display(std::cout); + std::cout << fp << "\n"; + } + else if (r1 == l_true && r2 == l_false) { + std::cout << "BUG should be sat\n"; + solver.display(std::cout); + std::cout << fp << "\n"; + } + else { + std::cout << r2 << " missed with verdict " << r1 << "\n"; + } + } + + + static void test_lps(random_gen& r, unsigned num_vars, unsigned num_rows, unsigned num_vars_per_row, unsigned num_ineqs) { + + } + + static void test_lps() { + random_gen r; + test_lps(r, 6, 3, 3, 3); + + } } void tst_fixplex() { From 2b6308af7434de4d3da0839847d16ce34d1c3754 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 08:33:19 -0700 Subject: [PATCH 2/2] testing fixplex Signed-off-by: Nikolaj Bjorner --- src/math/polysat/fixplex_def.h | 2 +- src/test/fixplex.cpp | 89 ++++++++++++++++++++++++++-------- 2 files changed, 69 insertions(+), 22 deletions(-) diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 8b7955fa8..e822e92f3 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -608,7 +608,7 @@ namespace polysat { return; if (m_var_is_touched.get(v, false)) return; - m_var_is_touched.set(v, true); + m_var_is_touched.setx(v, true, false); for (auto idx : m_var2ineqs[v]) { if (!m_ineqs[idx].is_active) { m_ineqs[idx].is_active = true; diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp index 6d0967859..5240c605c 100644 --- a/src/test/fixplex.cpp +++ b/src/test/fixplex.cpp @@ -370,17 +370,17 @@ namespace polysat { } static void test_lp( - vector>> const& rows, + vector>> const& rows, svector const& ineqs, - vector> const& bounds) { + vector> const& bounds) { - unsigned num_vars = 1; + unsigned num_vars = 0; for (auto const& row : rows) for (auto [v, c] : row) - num_vars = std::max(num_vars, v + 1); + num_vars = std::max(num_vars, v); for (auto const& i : ineqs) num_vars = std::max(num_vars, std::max(i.v, i.w)); - num_vars = std::max(bounds.size(), num_vars); + num_vars = std::max(bounds.size(), num_vars + 1); ast_manager m; reg_decl_plugins(m); @@ -423,21 +423,20 @@ namespace polysat { unsigned v = 0; for (auto const& b : bounds) { ++index; - if (!b.is_free()) { - fp.set_bounds(v, rational(b.lo, rational::ui64()), rational(b.hi, rational::ui64()), index); + if (b.is_free()) + continue; - if (b.lo < b.hi) { - solver.assert_expr(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v))); - solver.assert_expr(mk_ult(variables.get(v), bv.mk_numeral(b.hi, 32))); - } - else if (b.hi == 0) - solver.assert_expr(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v))); - else { - expr_ref a(mk_ult(variables.get(v), bv.mk_numeral(b.hi, 32)), m); - expr_ref b(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v)), m); - solver.assert_expr(m.mk_or(a, b)); - } - } + fp.set_bounds(v, rational(b.lo, rational::ui64()), rational(b.hi, rational::ui64()), index); + + expr_ref A(mk_ult(variables.get(v), bv.mk_numeral(b.hi, 32)), m); + expr_ref B(bv.mk_ule(bv.mk_numeral(b.lo, 32), variables.get(v)), m); + + if (b.lo < b.hi) + solver.assert_expr(m.mk_and(A, B)); + else if (b.hi == 0) + solver.assert_expr(B); + else + solver.assert_expr(m.mk_or(A, B)); } solver.display(std::cout); @@ -449,7 +448,23 @@ namespace polysat { std::cout << r1 << " " << r2 << "\n" << fp << "\n"; if (r2 == l_true) { - std::cout << "TBD validate solution\n"; + for (auto const& row : rows) { + uint64_t sum = 0; + for (auto col : row) + sum += col.second * fp.value(col.first); + SASSERT(sum == 0); + } + for (unsigned i = 0; i < bounds.size(); ++i) { + uint64_t val = fp.value(i); + uint64_t lo = bounds[i].lo; + uint64_t hi = bounds[i].hi; + SASSERT(!(lo < hi || hi == 0) || lo <= val && val < hi); + SASSERT(!(hi > lo) || val < hi || lo <= val); + } + for (auto const& i : ineqs) { + SASSERT(fp.value(i.v) <= fp.value(i.w)); + SASSERT(!i.strict || fp.value(i.v) < fp.value(i.w)); + } } if (r1 == r2) { std::cout << "agree\n"; @@ -471,18 +486,50 @@ namespace polysat { static void test_lps(random_gen& r, unsigned num_vars, unsigned num_rows, unsigned num_vars_per_row, unsigned num_ineqs) { + vector>> rows; + svector ineqs; + vector> bounds; + for (unsigned i = 0; i < num_vars; ++i) { + uint64_t l = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); + uint64_t h = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); + bounds.push_back(mod_interval(l, h)); + } + for (unsigned i = 0; i < num_ineqs; ++i) { + var_t v = r() % num_vars; + var_t w = r() % num_vars; + ineqs.push_back(ineq(v, w, 0, 0 == r() % 2)); + } + for (unsigned i = 0; i < num_rows; ++i) { + svector> row; + uint64_t coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); + row.push_back(std::make_pair(i, coeff)); + for (unsigned j = 0; j + 1 < num_vars_per_row; ++j) { + var_t v = (r() % (num_vars - num_vars_per_row)) + num_vars_per_row; + coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); + row.push_back(std::make_pair(v, coeff)); + } + rows.push_back(row); + } + test_lp(rows, ineqs, bounds); } static void test_lps() { random_gen r; - test_lps(r, 6, 3, 3, 3); + for (unsigned i = 0; i < 10000; ++i) + test_lps(r, 6, 0, 0, 5); + for (unsigned i = 0; i < 10000; ++i) + test_lps(r, 6, 3, 3, 0); + for (unsigned i = 0; i < 10000; ++i) + test_lps(r, 6, 3, 3, 3); } } void tst_fixplex() { + polysat::test_lps(); + polysat::test_ineq_propagation1(); polysat::test_ineq_propagation2(); polysat::test_ineqs();