From 172cf8478fb1c4867a8a43468c7ffceebb318e7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Mar 2021 09:07:51 -0700 Subject: [PATCH] add testing stubs Signed-off-by: Nikolaj Bjorner --- src/math/polysat/polysat.cpp | 8 +++ src/math/polysat/polysat.h | 12 +++-- src/smt/theory_seq.cpp | 2 +- src/test/CMakeLists.txt | 2 +- src/test/main.cpp | 1 + src/test/polysat.cpp | 98 ++++++++++++++++++++++++++++++++++-- 6 files changed, 114 insertions(+), 9 deletions(-) diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index cddbd8846..a7f0c2166 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -156,6 +156,14 @@ namespace polysat { // save for later } + void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) { + // save for later + } + + void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) { + // save for later + } + void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) { m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index); m_trail.push(vector_value_trail(m_vdeps, var)); diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index 9aed7cfcc..2b5925afc 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -181,6 +181,7 @@ namespace polysat { * by pushing an undo action on the trail stack. */ solver(trail_stack& s); + ~solver(); /** @@ -205,10 +206,13 @@ namespace polysat { * Each constraint is tracked by a dependency. * assign sets the 'index'th bit of var. */ - void add_eq(pdd const& p, unsigned dep); - void add_diseq(pdd const& p, unsigned dep); - void add_ule(pdd const& p, pdd const& q, unsigned dep); - void add_sle(pdd const& p, pdd const& q, unsigned dep); + void add_eq(pdd const& p, unsigned dep = 0); + void add_diseq(pdd const& p, unsigned dep = 0); + void add_ule(pdd const& p, pdd const& q, unsigned dep = 0); + void add_ult(pdd const& p, pdd const& q, unsigned dep = 0); + void add_sle(pdd const& p, pdd const& q, unsigned dep = 0); + void add_slt(pdd const& p, pdd const& q, unsigned dep = 0); + void assign(unsigned var, unsigned index, bool value, unsigned dep); /** diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4baa1f476..61dca74e0 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2731,7 +2731,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter } void theory_seq::add_axiom(literal_vector & lits) { - TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";); + TRACE("seq", ctx.display_literals_smt2(tout << "assert:", lits) << "\n";); for (literal lit : lits) ctx.mark_as_relevant(lit); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 5e55adbd5..0f84117a6 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -3,7 +3,7 @@ add_subdirectory(lp) ################################################################################ # z3-test executable ################################################################################ -set(z3_test_deps api fuzzing simplex) +set(z3_test_deps api fuzzing simplex polysat) z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps}) set (z3_test_extra_object_files "") foreach (component ${z3_test_expanded_deps}) diff --git a/src/test/main.cpp b/src/test/main.cpp index 7bea9d746..9acf42f27 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -263,4 +263,5 @@ int main(int argc, char ** argv) { //TST_ARGV(hs); TST(finder); TST(polysat); + TST_ARGV(polysat_argv); } diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 823563cc6..20ca10831 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1,15 +1,107 @@ #include "math/polysat/polysat.h" +#include "ast/ast.h" namespace polysat { // test resolve, factoring routines // auxiliary - static void test1() { + + + /** + * This one is unsat because a*a*(a*a - 1) + * is 0 for all values of a. + */ + static void test_eq1() { + trail_stack stack; + solver s(stack); + auto a = s.var(s.add_var(2)); + auto p = a*a*(a*a - 1) + 1; + s.add_eq(p); + std::cout << s.check_sat() << "\n"; + } + + /** + * has solution a = 3 + */ + static void test_eq2() { + trail_stack stack; + solver s(stack); + auto a = s.var(s.add_var(2)); + auto p = a*(a-1) + 2; + s.add_eq(p); + std::cout << s.check_sat() << "\n"; + } + + /** + * Check unsat of: + * u = v*q + r + * r < u + * v*q > u + */ + static void test_ineq1() { + trail_stack stack; + solver s(stack); + auto u = s.var(s.add_var(5)); + auto v = s.var(s.add_var(5)); + auto q = s.var(s.add_var(5)); + auto r = s.var(s.add_var(5)); + s.add_eq(u - (v*q) - r, 0); + s.add_ult(r, u, 0); + s.add_ult(u, v*q, 0); + std::cout << s.check_sat() << "\n"; + } + + /** + * Check unsat of: + * n*q1 = a - b + * n*q2 + r2 = c*a - c*b + * n > r2 > 0 + */ + static void test_ineq2() { + trail_stack stack; + solver s(stack); + auto n = s.var(s.add_var(5)); + auto q1 = s.var(s.add_var(5)); + auto a = s.var(s.add_var(5)); + auto b = s.var(s.add_var(5)); + auto c = s.var(s.add_var(5)); + auto q2 = s.var(s.add_var(5)); + auto r2 = s.var(s.add_var(5)); + s.add_eq(n*q1 - a + b); + s.add_eq(n*q2 + r2 - c*a + c*b); + s.add_ult(r2, n); + s.add_diseq(n); + std::cout << s.check_sat() << "\n"; + } + + // convert assertions into internal solver state + // support small grammar of formulas. + void internalize(solver& s, expr_ref_vector& fmls) { } } -// also add test that loads from a file and runs the polysat engine. void tst_polysat() { - polysat::test1(); + polysat::test_eq1(); + polysat::test_eq2(); + polysat::test_ineq1(); + polysat::test_ineq2(); +} + +// TBD also add test that loads from a file and runs the polysat engine. +// sketch follows below: + +void tst_polysat_argv(char** argv, int argc, int& i) { + // set up SMT2 parser to extract assertions + // assume they are simple bit-vector equations (and inequations) + // convert to solver state. + // std::ifstream is(argv[0]); + // cmd_context ctx(false, &m); + // ctx.set_ignore_check(true); + // VERIFY(parse_smt2_commands(ctx, is)); + // auto fmls = ctx.assertions(); + // trail_stack stack; + // solver s(stack); + // polysat::internalize(s, fmls); + // std::cout << s.check() << "\n"; }