From 3da37f4fb52e64243eaba2dce65558b26b5e8fc4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Jun 2021 10:58:42 -0700 Subject: [PATCH] add unit test driver Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.h | 16 ++++++ src/math/polysat/solver.cpp | 5 ++ src/math/polysat/solver.h | 5 ++ src/test/polysat.cpp | 111 ++++++++++++++++++++++++++++++++---- 4 files changed, 125 insertions(+), 12 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index e780ad7a7..38456be3f 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -343,6 +343,14 @@ public: bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); } bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); } bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); } + bool is_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); } + bool is_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); } + bool is_ult(expr const * e) const { return is_app_of(e, get_fid(), OP_ULT); } + bool is_slt(expr const * e) const { return is_app_of(e, get_fid(), OP_SLT); } + bool is_ugt(expr const * e) const { return is_app_of(e, get_fid(), OP_UGT); } + bool is_sgt(expr const * e) const { return is_app_of(e, get_fid(), OP_SGT); } + bool is_uge(expr const * e) const { return is_app_of(e, get_fid(), OP_UGEQ); } + bool is_sge(expr const * e) const { return is_app_of(e, get_fid(), OP_SGEQ); } bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); } bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); } bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); } @@ -359,6 +367,14 @@ public: MATCH_BINARY(is_bv_mul); MATCH_BINARY(is_bv_sle); MATCH_BINARY(is_bv_ule); + MATCH_BINARY(is_ule); + MATCH_BINARY(is_sle); + MATCH_BINARY(is_ult); + MATCH_BINARY(is_slt); + MATCH_BINARY(is_uge); + MATCH_BINARY(is_sge); + MATCH_BINARY(is_ugt); + MATCH_BINARY(is_sgt); MATCH_BINARY(is_bv_ashr); MATCH_BINARY(is_bv_lshr); MATCH_BINARY(is_bv_shl); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 0711a32d6..51ef9db00 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -154,6 +154,11 @@ namespace polysat { return v; } + pdd solver::value(rational const& v, unsigned sz) { + return sz2pdd(sz).mk_val(v); + } + + void solver::del_var() { // TODO also remove v from all learned constraints. pvar v = m_viable.size() - 1; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 730fd3e27..2763c1b78 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -325,6 +325,11 @@ namespace polysat { */ pdd var(pvar v) { return m_vars[v]; } + /** + * Create polynomial constant. + */ + pdd value(rational const& v, unsigned sz); + /** * Return value of v in the current model (only meaningful if check_sat() returned l_true). */ diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index dd7864d88..15d95c638 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -720,8 +720,92 @@ namespace polysat { // convert assertions into internal solver state // support small grammar of formulas. - void internalize(solver& s, expr_ref_vector& fmls) { + pdd to_pdd(ast_manager& m, solver& s, obj_map& expr2pdd, expr* e) { + pdd* r = nullptr; + if (expr2pdd.find(e, r)) + return *r; + bv_util bv(m); + rational n; + unsigned sz; + expr* a, *b; + if (bv.is_bv_add(e, a, b)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + r = alloc(pdd, pa + pb); + } + else if (bv.is_bv_mul(e, a, b)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + r = alloc(pdd, pa * pb); + } + else if (bv.is_bv_udiv(e, a, b)) { + std::cout << "TODO udiv\n"; + } + else if (bv.is_numeral(e, n, sz)) { + r = alloc(pdd, s.value(n, sz)); + } + else if (is_uninterp(e)) { + sz = bv.get_bv_size(e); + r = alloc(pdd, s.var(s.add_var(sz))); + } + else + std::cout << "unknown " << mk_pp(e, m) << "\n"; + + if (!r) { + sz = bv.get_bv_size(e); + r = alloc(pdd, s.var(s.add_var(sz))); + } + expr2pdd.insert(e, r); + return *r; + } + + void internalize(ast_manager& m, solver& s, ptr_vector& fmls) { + bv_util bv(m); + obj_map expr2pdd; + for (expr* fm : fmls) { + bool is_not = m.is_not(fm, fm); + expr* a, *b; + if (m.is_eq(fm, a, b)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + if (is_not) + s.add_diseq(pa - pb); + else + s.add_eq(pa - pb); + } + else if (bv.is_ult(fm, a, b) || bv.is_ugt(fm, b, a)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + if (is_not) + s.add_ule(pb, pa); + else + s.add_ult(pa, pb); + } + else if (bv.is_ule(fm, a, b) || bv.is_uge(fm, b, a)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + if (is_not) + s.add_ult(pb, pa); + else + s.add_ule(pa, pb); + } + else if (bv.is_slt(fm, a, b) || bv.is_sgt(fm, b, a)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + std::cout << "slt\n"; + } + else if (bv.is_sle(fm, a, b) || bv.is_sge(fm, b, a)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + std::cout << "sle\n"; + } + else { + std::cout << "formula: " << is_not << " " << mk_pp(fm, m) << "\n"; + } + } + for (auto [k,v] : expr2pdd) + dealloc(v); } } @@ -761,29 +845,32 @@ void tst_polysat() { // TBD also add test that loads from a file and runs the polysat engine. // sketch follows below: +#include "ast/bv_decl_plugin.h" + + 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. - if (argc != 2) { + + std::cout << "argc " << argc << "\n"; + if (argc < 3) { std::cerr << "Usage: " << argv[0] << " FILE\n"; return; } - std::ifstream is(argv[1]); - // cmd_context ctx(false, &m); + std::cout << "processing " << argv[2] << "\n"; + std::ifstream is(argv[2]); + if (is.bad() || is.fail()) { + std::cout << "failed to open " << argv[2] << "\n"; + return; + } cmd_context ctx(false); + ast_manager& m = ctx.m(); ctx.set_ignore_check(true); VERIFY(parse_smt2_commands(ctx, is)); auto fmls = ctx.assertions(); polysat::scoped_solver s("polysat"); - for (expr* fm : fmls) { - // fm->get_kind() - if (is_app(fm)) { - // is_app_of - } - } - // polysat::internalize(s, fmls); - // std::cout << s.check() << "\n"; + polysat::internalize(m, s, fmls); s.check(); }