From 50876a4daefedd68704793426d1b38a07c52e053 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Sun, 12 Mar 2023 16:15:25 +0100 Subject: [PATCH] Add helper for printing polysat constraints --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/clause.cpp | 2 +- src/math/polysat/constraint.h | 1 + src/math/polysat/polysat_ast.cpp | 188 +++++++++++++++++++++++++++++++ src/math/polysat/polysat_ast.h | 76 +++++++++++++ src/math/polysat/solver.h | 1 + 6 files changed, 268 insertions(+), 1 deletion(-) create mode 100644 src/math/polysat/polysat_ast.cpp create mode 100644 src/math/polysat/polysat_ast.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 5d4d3f3f5..6b3e97aff 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(polysat linear_solver.cpp log.cpp op_constraint.cpp + polysat_ast.cpp restart.cpp saturation.cpp search_state.cpp diff --git a/src/math/polysat/clause.cpp b/src/math/polysat/clause.cpp index 286d5821a..263d4f174 100644 --- a/src/math/polysat/clause.cpp +++ b/src/math/polysat/clause.cpp @@ -8,7 +8,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index dce651bbc..9be3b0e81 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -146,6 +146,7 @@ namespace polysat { bool is_positive() const { return m_positive; } bool is_negative() const { return !is_positive(); } + bool sign() const { return is_negative(); } /** Evaluate the constraint under the empty assignment */ lbool eval() const { return is_positive() ? get()->eval() : ~get()->eval(); } diff --git a/src/math/polysat/polysat_ast.cpp b/src/math/polysat/polysat_ast.cpp new file mode 100644 index 000000000..82bffbad7 --- /dev/null +++ b/src/math/polysat/polysat_ast.cpp @@ -0,0 +1,188 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat to ast conversion + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#include "math/polysat/polysat_ast.h" +#include "math/polysat/solver.h" +#include "math/polysat/umul_ovfl_constraint.h" +#include "util/util.h" +#include "ast/ast.h" +#include "ast/reg_decl_plugins.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" +#include "util/uint_map.h" + +namespace polysat { + + struct polysat_ast_d { + ast_manager m; + scoped_ptr bv; + uint_map var_expr; + + decl_ref_vector decls; + expr_ref_vector formulas; + + // just keep all expressions alive + ast_ref_vector storage; + + polysat_ast_d(): m(), decls(m), formulas(m), storage(m) + { + reg_decl_plugins(m); + bv = alloc(bv_util, m); + } + + ~polysat_ast_d() = default; + + ast* store(ast* a) { storage.push_back(ast_ref{a, m}); return a; } + expr* store(expr* e) { storage.push_back(ast_ref{e, m}); return e; } + + }; + + polysat_ast::polysat_ast(solver& s) + : s(s) + , d(alloc(polysat_ast_d)) + { } + + polysat_ast::~polysat_ast() = default; + + ast_manager& polysat_ast::m() const { return d->m; } + bv_util& polysat_ast::bv() const { return *d->bv; } + + expr* polysat_ast::mk_val(rational const& val, unsigned bit_width) { + return d->store(bv().mk_numeral(val, bit_width)); + } + + expr* polysat_ast::mk_var(pvar x) { + expr* node; + if (!d->var_expr.find(x, node)) { + unsigned bit_width = s.size(x); + std::string name = "v"; + name += std::to_string(x); + auto decl = m().mk_const_decl(name, bv().mk_sort(bit_width)); + d->decls.push_back(decl); + node = d->store(m().mk_const(decl)); + d->var_expr.insert(x, node); + // if x is defined by an op_constraint, add it as background assumption. + signed_constraint c = s.m_constraints.find_op_by_result_var(x); + if (c) + add(mk_lit(c)); + } + return node; + } + + expr* polysat_ast::mk_mono(dd::pdd_monomial const& mono, unsigned bit_width) { + if (mono.vars.empty()) + return mk_val(mono.coeff, bit_width); + if (mono.coeff.is_one() && mono.vars.size() == 1) + return mk_var(mono.vars[0]); + ptr_vector args; + if (!mono.coeff.is_one()) + args.push_back(mk_val(mono.coeff, bit_width)); + for (pvar x : mono.vars) { + VERIFY_EQ(s.size(x), bit_width); + args.push_back(mk_var(x)); + } + return d->store(bv().mk_bv_mul(args)); + } + + expr* polysat_ast::mk_poly(pdd const& p) { + unsigned const N = p.power_of_2(); + if (p.is_val()) + return mk_val(p.val(), N); + if (p.is_var()) + return mk_var(p.var()); + if (p.is_monomial()) + return mk_mono(*p.begin(), N); + ptr_vector args; + for (auto const& mono : p) + args.push_back(mk_mono(mono, N)); + return d->store(bv().mk_bv_add(args)); + } + + expr* polysat_ast::mk_not(expr* e) { + return d->store(m().mk_not(e)); + } + + expr* polysat_ast::mk_ule(pdd const& p, pdd const& q) { + if (q.is_zero()) + return d->store(m().mk_eq(mk_poly(p), mk_poly(q))); + else + return d->store(bv().mk_ule(mk_poly(p), mk_poly(q))); + } + + expr* polysat_ast::mk_ule(pdd const& p, pdd const& q, bool sign) { + expr* e = mk_ule(p, q); + if (sign) + e = mk_not(e); + return e; + } + + expr* polysat_ast::mk_umul_ovfl(pdd const& p, pdd const& q, bool sign) { + expr* e = d->store(bv().mk_bvumul_no_ovfl(mk_poly(p), mk_poly(q))); + if (!sign) + e = mk_not(e); + return e; + } + + expr* polysat_ast::mk_lit(sat::literal lit) { + return mk_lit(s.lit2cnstr(lit)); + } + + expr* polysat_ast::mk_lit(signed_constraint c) { + if (c->is_ule()) + return mk_ule(c->to_ule().lhs(), c->to_ule().rhs(), c.sign()); + if (c->is_umul_ovfl()) + return mk_umul_ovfl(c->to_umul_ovfl().p(), c->to_umul_ovfl().q(), c.sign()); + verbose_stream() << "polysat_ast not yet supported: " << c << "\n"; + m_ok = false; + // NOT_IMPLEMENTED_YET(); + return d->store(m().mk_true()); + } + + expr* polysat_ast::mk_clause(clause& cl) { + ptr_vector args; + for (sat::literal lit : cl) + args.push_back(mk_lit(lit)); + return d->store(m().mk_or(args)); + } + + void polysat_ast::add(expr* e) { + d->formulas.push_back(e); + } + + std::ostream& polysat_ast::display(std::ostream& out) const { + if (m_status == l_true) + out << "(set-info :status sat)\n"; + else if (m_status == l_false) + out << "(set-info :status unsat)\n"; + if (!m_description.empty()) { + out << "(set-info :source |\n"; + out << m_description; + if (m_description.back() != '\n') + out << '\n'; + out << "|)\n"; + } + params_ref p; + p.set_uint("max_depth", 4294967295u); + p.set_uint("min_alias_size", 4294967295u); + for (decl* d : d->decls) + out << mk_pp(d, m(), p) << "\n"; + for (expr* e : d->formulas) { + out << "(assert\n"; + out << " " << mk_pp(e, m(), p, 4) << "\n"; + out << ")\n"; + } + out << "(check-sat)\n"; + return out; + } + +} diff --git a/src/math/polysat/polysat_ast.h b/src/math/polysat/polysat_ast.h new file mode 100644 index 000000000..755ed56bf --- /dev/null +++ b/src/math/polysat/polysat_ast.h @@ -0,0 +1,76 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat to ast conversion + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once +#include "math/polysat/types.h" + +class expr; +class ast_manager; +class bv_util; + +namespace polysat { + + struct polysat_ast_d; + class signed_constraint; + + class polysat_ast { + solver& s; + scoped_ptr d; + std::string m_description; + lbool m_status = l_undef; + bool m_ok = true; + + ast_manager& m() const; + bv_util& bv() const; + + public: + polysat_ast(solver&); + ~polysat_ast(); + + void set_description(std::string description) { m_description = description; } + void set_status(lbool status) { m_status = status; } + bool is_ok() { return m_ok; } + + expr* mk_val(rational const& val, unsigned bit_width); + expr* mk_var(pvar x); + expr* mk_mono(dd::pdd_monomial const& mono, unsigned bit_width); + expr* mk_poly(pdd const& p); + + // p <= q + expr* mk_ule(pdd const& p, pdd const& q); + expr* mk_ule(pdd const& p, pdd const& q, bool sign); + // p >= q + expr* mk_uge(pdd const& p, pdd const& q, bool sign) { return mk_ule(q, p, sign); } + // p > q + expr* mk_ugt(pdd const& p, pdd const& q, bool sign) { return mk_ule(p, q, !sign); } + // p < q + expr* mk_ult(pdd const& p, pdd const& q, bool sign) { return mk_ugt(q, p, sign); } + + // ovfl*(p, q) + expr* mk_umul_ovfl(pdd const& p, pdd const& q, bool sign); + + expr* mk_not(expr* e); + + expr* mk_lit(sat::literal lit); + expr* mk_lit(signed_constraint c); + + expr* mk_clause(clause& cl); + + void add(expr* e); + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, polysat_ast const& x) { return x.display(out); } + +} diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index e7d1463b6..9365e7200 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -140,6 +140,7 @@ namespace polysat { friend class test_polysat; friend class test_fi; friend struct inf_resolve_evaluated; + friend class polysat_ast; reslimit& m_lim; params_ref m_params;