From 3778048eb48296a4a7655f646ff83868e1c57a1d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Oct 2016 20:31:59 -0700
Subject: [PATCH] add bounded-int and pb2bv solvers to fd_solver, use sorting
networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module
and remove it from the pb2bv_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
contrib/cmake/src/ast/rewriter/CMakeLists.txt | 3 +-
.../cmake/src/tactic/portfolio/CMakeLists.txt | 3 +
contrib/cmake/src/test/CMakeLists.txt | 1 +
.../{fd_rewriter.cpp => enum2bv_rewriter.cpp} | 37 +-
src/ast/rewriter/pb2bv_rewriter.cpp | 453 ++++++++++++++++
.../{fd_rewriter.h => pb2bv_rewriter.h} | 24 +-
src/ast/rewriter/pb_rewriter.cpp | 7 +-
src/cmd_context/check_logic.cpp | 4 +-
src/cmd_context/cmd_context.cpp | 1 +
src/opt/opt_sls_solver.h | 31 +-
src/smt/smt_kernel.cpp | 6 +
src/smt/smt_kernel.h | 3 +-
src/smt/theory_pb.cpp | 17 +-
src/tactic/arith/bv2int_rewriter.h | 2 +-
src/tactic/arith/card2bv_tactic.cpp | 509 +-----------------
src/tactic/bv/dt2bv_tactic.cpp | 4 +-
.../portfolio/bounded_int2bv_solver.cpp | 296 ++++++++++
src/tactic/portfolio/bounded_int2bv_solver.h | 29 +
src/tactic/portfolio/enum2bv_solver.cpp | 162 ++++++
src/tactic/portfolio/enum2bv_solver.h | 29 +
src/tactic/portfolio/fd_solver.cpp | 144 +----
src/tactic/portfolio/pb2bv_solver.cpp | 127 +++++
src/tactic/portfolio/pb2bv_solver.h | 29 +
src/test/main.cpp | 1 +
src/test/pb2bv.cpp | 195 +++++++
src/util/sorting_network.h | 7 +-
26 files changed, 1424 insertions(+), 700 deletions(-)
rename src/ast/rewriter/{fd_rewriter.cpp => enum2bv_rewriter.cpp} (86%)
create mode 100644 src/ast/rewriter/pb2bv_rewriter.cpp
rename src/ast/rewriter/{fd_rewriter.h => pb2bv_rewriter.h} (52%)
create mode 100644 src/tactic/portfolio/bounded_int2bv_solver.cpp
create mode 100644 src/tactic/portfolio/bounded_int2bv_solver.h
create mode 100644 src/tactic/portfolio/enum2bv_solver.cpp
create mode 100644 src/tactic/portfolio/enum2bv_solver.h
create mode 100644 src/tactic/portfolio/pb2bv_solver.cpp
create mode 100644 src/tactic/portfolio/pb2bv_solver.h
create mode 100644 src/test/pb2bv.cpp
diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
index b01a0e016..74fddd2bb 100644
--- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt
+++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
@@ -9,14 +9,15 @@ z3_add_component(rewriter
datatype_rewriter.cpp
der.cpp
dl_rewriter.cpp
+ enum2bv_rewriter.cpp
expr_replacer.cpp
expr_safe_replace.cpp
factor_rewriter.cpp
- fd_rewriter.cpp
fpa_rewriter.cpp
label_rewriter.cpp
mk_simplified_app.cpp
pb_rewriter.cpp
+ pb2bv_rewriter.cpp
quant_hoist.cpp
rewriter.cpp
seq_rewriter.cpp
diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt
index 201cdcf0f..c6f621f25 100644
--- a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt
+++ b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt
@@ -1,6 +1,9 @@
z3_add_component(portfolio
SOURCES
default_tactic.cpp
+ enum2bv_solver.cpp
+ pb2bv_solver.cpp
+ bounded_int2bv_solver.cpp
fd_solver.cpp
smt_strategic_solver.cpp
COMPONENT_DEPENDENCIES
diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt
index acaf186ba..6f6615e0c 100644
--- a/contrib/cmake/src/test/CMakeLists.txt
+++ b/contrib/cmake/src/test/CMakeLists.txt
@@ -78,6 +78,7 @@ add_executable(test-z3
old_interval.cpp
optional.cpp
parray.cpp
+ pb2bv.cpp
pdr.cpp
permutation.cpp
polynomial.cpp
diff --git a/src/ast/rewriter/fd_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
similarity index 86%
rename from src/ast/rewriter/fd_rewriter.cpp
rename to src/ast/rewriter/enum2bv_rewriter.cpp
index 026387e22..bbe07f625 100644
--- a/src/ast/rewriter/fd_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation
Module Name:
- fd_rewriter.cpp
+ enum2bv_rewriter.cpp
Abstract:
@@ -19,11 +19,11 @@ Notes:
#include"rewriter.h"
#include"rewriter_def.h"
-#include"fd_rewriter.h"
+#include"enum2bv_rewriter.h"
#include"ast_util.h"
#include"ast_pp.h"
-struct fd_rewriter::imp {
+struct enum2bv_rewriter::imp {
ast_manager& m;
params_ref m_params;
obj_map<func_decl, func_decl*> m_enum2bv;
@@ -258,6 +258,7 @@ struct fd_rewriter::imp {
m_enum_defs.resize(lim);
m_enum_bvs.resize(lim);
}
+ m_rw.reset();
}
void flush_side_constraints(expr_ref_vector& side_constraints) {
@@ -275,18 +276,18 @@ struct fd_rewriter::imp {
};
-fd_rewriter::fd_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
-fd_rewriter::~fd_rewriter() { dealloc(m_imp); }
-void fd_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
-ast_manager & fd_rewriter::m() const { return m_imp->m; }
-unsigned fd_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
-void fd_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
-obj_map<func_decl, func_decl*> const& fd_rewriter::enum2bv() const { return m_imp->m_enum2bv; }
-obj_map<func_decl, func_decl*> const& fd_rewriter::bv2enum() const { return m_imp->m_bv2enum; }
-obj_map<func_decl, expr*> const& fd_rewriter::enum2def() const { return m_imp->m_enum2def; }
-void fd_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
-void fd_rewriter::push() { m_imp->push(); }
-void fd_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
-void fd_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
-unsigned fd_rewriter::num_translated() const { return m_imp->m_num_translated; }
-void fd_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); }
+enum2bv_rewriter::enum2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
+enum2bv_rewriter::~enum2bv_rewriter() { dealloc(m_imp); }
+void enum2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+ast_manager & enum2bv_rewriter::m() const { return m_imp->m; }
+unsigned enum2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
+void enum2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
+obj_map<func_decl, func_decl*> const& enum2bv_rewriter::enum2bv() const { return m_imp->m_enum2bv; }
+obj_map<func_decl, func_decl*> const& enum2bv_rewriter::bv2enum() const { return m_imp->m_bv2enum; }
+obj_map<func_decl, expr*> const& enum2bv_rewriter::enum2def() const { return m_imp->m_enum2def; }
+void enum2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void enum2bv_rewriter::push() { m_imp->push(); }
+void enum2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
+void enum2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
+unsigned enum2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
+void enum2bv_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); }
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
new file mode 100644
index 000000000..0aeeea81a
--- /dev/null
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -0,0 +1,453 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ pb2bv_rewriter.cpp
+
+Abstract:
+
+ Conversion from pseudo-booleans to bit-vectors.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+
+#include"rewriter.h"
+#include"rewriter_def.h"
+#include"statistics.h"
+#include"pb2bv_rewriter.h"
+#include"sorting_network.h"
+#include"ast_util.h"
+#include"ast_pp.h"
+
+
+struct pb2bv_rewriter::imp {
+
+ struct argc_t {
+ expr* m_arg;
+ rational m_coeff;
+ argc_t():m_arg(0), m_coeff(0) {}
+ argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
+ };
+
+ struct argc_gt {
+ bool operator()(argc_t const& a, argc_t const& b) const {
+ return a.m_coeff > b.m_coeff;
+ }
+ };
+
+ struct argc_entry {
+ unsigned m_index;
+ rational m_k;
+ expr* m_value;
+ argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
+ argc_entry():m_index(0), m_k(0), m_value(0) {}
+
+ struct eq {
+ bool operator()(argc_entry const& a, argc_entry const& b) const {
+ return a.m_index == b.m_index && a.m_k == b.m_k;
+ }
+ };
+ struct hash {
+ unsigned operator()(argc_entry const& a) const {
+ return a.m_index ^ a.m_k.hash();
+ }
+ };
+ };
+ typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
+
+ ast_manager& m;
+ params_ref m_params;
+ expr_ref_vector m_lemmas;
+ func_decl_ref_vector m_fresh; // all fresh variables
+ unsigned_vector m_fresh_lim;
+ unsigned m_num_translated;
+
+ struct card2bv_rewriter {
+ typedef expr* literal;
+ typedef ptr_vector<expr> literal_vector;
+ psort_nw<card2bv_rewriter> m_sort;
+ ast_manager& m;
+ imp& m_imp;
+ arith_util au;
+ pb_util pb;
+ bv_util bv;
+ expr_ref_vector m_trail;
+
+ unsigned get_num_bits(func_decl* f) {
+ rational r(0);
+ unsigned sz = f->get_arity();
+ for (unsigned i = 0; i < sz; ++i) {
+ r += pb.get_coeff(f, i);
+ }
+ r = r > pb.get_k(f)? r : pb.get_k(f);
+ return r.get_num_bits();
+ }
+
+ void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+
+ expr_ref zero(m), a(m), b(m);
+ expr_ref_vector es(m);
+ unsigned bw = get_num_bits(f);
+ zero = bv.mk_numeral(rational(0), bw);
+ for (unsigned i = 0; i < sz; ++i) {
+ es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
+ }
+ switch (es.size()) {
+ case 0: a = zero; break;
+ case 1: a = es[0].get(); break;
+ default:
+ a = es[0].get();
+ for (unsigned i = 1; i < es.size(); ++i) {
+ a = bv.mk_bv_add(a, es[i].get());
+ }
+ break;
+ }
+ b = bv.mk_numeral(pb.get_k(f), bw);
+
+ switch (f->get_decl_kind()) {
+ case OP_AT_MOST_K:
+ case OP_PB_LE:
+ result = bv.mk_ule(a, b);
+ break;
+ case OP_AT_LEAST_K:
+ case OP_PB_GE:
+ result = bv.mk_ule(b, a);
+ break;
+ case OP_PB_EQ:
+ result = m.mk_eq(a, b);
+ break;
+ default:
+ UNREACHABLE();
+ }
+ TRACE("pb", tout << result << "\n";);
+ }
+
+ bool mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+ decl_kind kind = f->get_decl_kind();
+ if (kind != OP_PB_GE && kind != OP_AT_LEAST_K) {
+ return false;
+ }
+ unsigned max_clauses = sz*10;
+ vector<argc_t> argcs;
+ for (unsigned i = 0; i < sz; ++i) {
+ argcs.push_back(argc_t(args[i], pb.get_coeff(f, i)));
+ }
+ std::sort(argcs.begin(), argcs.end(), argc_gt());
+ DEBUG_CODE(
+ for (unsigned i = 0; i + 1 < sz; ++i) {
+ SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
+ });
+ result = m.mk_app(f, sz, args);
+ TRACE("pb", tout << result << "\n";);
+ argc_cache cache;
+ expr_ref_vector trail(m);
+ vector<rational> todo_k;
+ unsigned_vector todo_i;
+ todo_k.push_back(pb.get_k(f));
+ todo_i.push_back(0);
+ argc_entry entry1;
+ while (!todo_i.empty()) {
+ SASSERT(todo_i.size() == todo_k.size());
+ if (cache.size() > max_clauses) {
+ return false;
+ }
+ unsigned i = todo_i.back();
+ rational k = todo_k.back();
+ argc_entry entry(i, k);
+ if (cache.contains(entry)) {
+ todo_i.pop_back();
+ todo_k.pop_back();
+ continue;
+ }
+ SASSERT(i < sz);
+ SASSERT(!k.is_neg());
+ rational const& coeff = argcs[i].m_coeff;
+ expr* arg = argcs[i].m_arg;
+ if (i + 1 == sz) {
+ if (k.is_zero()) {
+ entry.m_value = m.mk_true();
+ }
+ else if (coeff < k) {
+ entry.m_value = m.mk_false();
+ }
+ else if (coeff.is_zero()) {
+ entry.m_value = m.mk_true();
+ }
+ else {
+ SASSERT(coeff >= k && k.is_pos());
+ entry.m_value = arg;
+ }
+ todo_i.pop_back();
+ todo_k.pop_back();
+ cache.insert(entry);
+ continue;
+ }
+ entry.m_index++;
+ expr* lo = 0, *hi = 0;
+ if (cache.find(entry, entry1)) {
+ lo = entry1.m_value;
+ }
+ else {
+ todo_i.push_back(i+1);
+ todo_k.push_back(k);
+ }
+ entry.m_k -= coeff;
+ if (!entry.m_k.is_pos()) {
+ hi = m.mk_true();
+ }
+ else if (cache.find(entry, entry1)) {
+ hi = entry1.m_value;
+ }
+ else {
+ todo_i.push_back(i+1);
+ todo_k.push_back(entry.m_k);
+ }
+ if (hi && lo) {
+ todo_i.pop_back();
+ todo_k.pop_back();
+ entry.m_index = i;
+ entry.m_k = k;
+ entry.m_value = mk_ite(arg, hi, lo);
+ trail.push_back(entry.m_value);
+ cache.insert(entry);
+ }
+ }
+ argc_entry entry(0, pb.get_k(f));
+ VERIFY(cache.find(entry, entry));
+ result = entry.m_value;
+ TRACE("pb", tout << result << "\n";);
+ return true;
+ }
+
+ expr* negate(expr* e) {
+ if (m.is_not(e, e)) return e;
+ return m.mk_not(e);
+ }
+ expr* mk_ite(expr* c, expr* hi, expr* lo) {
+ while (m.is_not(c, c)) {
+ std::swap(hi, lo);
+ }
+ if (hi == lo) return hi;
+ if (m.is_true(hi) && m.is_false(lo)) return c;
+ if (m.is_false(hi) && m.is_true(lo)) return negate(c);
+ if (m.is_true(hi)) return m.mk_or(c, lo);
+ if (m.is_false(lo)) return m.mk_and(c, hi);
+ if (m.is_false(hi)) return m.mk_and(negate(c), lo);
+ if (m.is_true(lo)) return m.mk_implies(c, hi);
+ return m.mk_ite(c, hi, lo);
+ }
+
+ bool is_or(func_decl* f) {
+ switch (f->get_decl_kind()) {
+ case OP_AT_MOST_K:
+ case OP_PB_LE:
+ return false;
+ case OP_AT_LEAST_K:
+ case OP_PB_GE:
+ return pb.get_k(f).is_one();
+ case OP_PB_EQ:
+ return false;
+ default:
+ UNREACHABLE();
+ return false;
+ }
+ }
+
+
+ public:
+
+ card2bv_rewriter(imp& i, ast_manager& m):
+ m(m),
+ m_imp(i),
+ au(m),
+ pb(m),
+ bv(m),
+ m_sort(*this),
+ m_trail(m)
+ {}
+
+ br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+ if (f->get_family_id() == pb.get_family_id()) {
+ mk_pb(f, sz, args, result);
+ ++m_imp.m_num_translated;
+ return BR_DONE;
+ }
+ else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) {
+ ++m_imp.m_num_translated;
+ return BR_DONE;
+ }
+ else {
+ return BR_FAILED;
+ }
+ }
+
+ //
+ // NSB: review
+ // we should remove this code and rely on a layer above to deal with
+ // whatever it accomplishes. It seems to break types.
+ //
+ bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+ if (f->get_decl_kind() == OP_ADD) {
+ unsigned bits = 0;
+ for (unsigned i = 0; i < sz; i++) {
+ rational val1, val2;
+ if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
+ bits += val1.get_num_bits();
+ }
+ else if (m.is_ite(args[i]) &&
+ au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
+ au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
+ bits++;
+ }
+ else
+ return false;
+ }
+
+ result = 0;
+ for (unsigned i = 0; i < sz; i++) {
+ rational val1, val2;
+ expr * q;
+ if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
+ q = bv.mk_numeral(val1, bits);
+ else
+ q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
+ result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
+ }
+ return true;
+ }
+ else {
+ return false;
+ }
+ }
+
+ void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+ SASSERT(f->get_family_id() == pb.get_family_id());
+ if (is_or(f)) {
+ result = m.mk_or(sz, args);
+ }
+ else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
+ result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+ }
+ else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
+ result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+ }
+ else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+ result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args);
+ }
+ else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+ result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+ }
+ else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+ result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+ }
+ else if (!mk_shannon(f, sz, args, result)) {
+ mk_bv(f, sz, args, result);
+ }
+ }
+
+ // definitions used for sorting network
+ literal mk_false() { return m.mk_false(); }
+ literal mk_true() { return m.mk_true(); }
+ literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); }
+ literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
+ literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
+
+ std::ostream& pp(std::ostream& out, literal lit) { return out << mk_ismt2_pp(lit, m); }
+
+ literal trail(literal l) {
+ m_trail.push_back(l);
+ return l;
+ }
+ literal fresh() {
+ expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m);
+ m_imp.m_fresh.push_back(to_app(fr)->get_decl());
+ return trail(fr);
+ }
+
+ void mk_clause(unsigned n, literal const* lits) {
+ m_imp.m_lemmas.push_back(mk_or(m, n, lits));
+ }
+ };
+
+ struct card2bv_rewriter_cfg : public default_rewriter_cfg {
+ card2bv_rewriter m_r;
+ bool rewrite_patterns() const { return false; }
+ bool flat_assoc(func_decl * f) const { return false; }
+ br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+ result_pr = 0;
+ return m_r.mk_app_core(f, num, args, result);
+ }
+ card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
+ };
+
+ class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
+ public:
+ card2bv_rewriter_cfg m_cfg;
+ card_pb_rewriter(imp& i, ast_manager & m):
+ rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
+ m_cfg(i, m) {}
+ };
+
+ card_pb_rewriter m_rw;
+
+ imp(ast_manager& m, params_ref const& p):
+ m(m), m_params(p), m_lemmas(m),
+ m_fresh(m),
+ m_num_translated(0),
+ m_rw(*this, m) {
+ }
+
+ void updt_params(params_ref const & p) {}
+ unsigned get_num_steps() const { return m_rw.get_num_steps(); }
+ void cleanup() { m_rw.cleanup(); }
+ void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
+ m_rw(e, result, result_proof);
+ }
+ void push() {
+ m_fresh_lim.push_back(m_fresh.size());
+ }
+ void pop(unsigned num_scopes) {
+ SASSERT(m_lemmas.empty()); // lemmas must be flushed before pop.
+ if (num_scopes > 0) {
+ SASSERT(num_scopes <= m_fresh_lim.size());
+ unsigned new_sz = m_fresh_lim.size() - num_scopes;
+ unsigned lim = m_fresh_lim[new_sz];
+ m_fresh.resize(lim);
+ m_fresh_lim.resize(new_sz);
+ }
+ m_rw.reset();
+ }
+
+ void flush_side_constraints(expr_ref_vector& side_constraints) {
+ side_constraints.append(m_lemmas);
+ m_lemmas.reset();
+ }
+
+ void collect_statistics(statistics & st) const {
+ st.update("pb-aux-variables", m_fresh.size());
+ st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses);
+ }
+
+};
+
+
+pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
+pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
+void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
+unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
+void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
+func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
+void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void pb2bv_rewriter::push() { m_imp->push(); }
+void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
+void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
+unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
+
+void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }
diff --git a/src/ast/rewriter/fd_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h
similarity index 52%
rename from src/ast/rewriter/fd_rewriter.h
rename to src/ast/rewriter/pb2bv_rewriter.h
index 3d4ecae9c..47d8361cb 100644
--- a/src/ast/rewriter/fd_rewriter.h
+++ b/src/ast/rewriter/pb2bv_rewriter.h
@@ -3,46 +3,44 @@ Copyright (c) 2016 Microsoft Corporation
Module Name:
- fd_rewriter.h
+ pb2bv_rewriter.h
Abstract:
- Conversion from enumeration types to bit-vectors.
+ Conversion from pseudo-booleans to bit-vectors.
Author:
- Nikolaj Bjorner (nbjorner) 2016-10-18
+ Nikolaj Bjorner (nbjorner) 2016-10-23
Notes:
--*/
-#ifndef ENUM_REWRITER_H_
-#define ENUM_REWRITER_H_
+#ifndef PB2BV_REWRITER_H_
+#define PB2BV_REWRITER_H_
-#include"datatype_decl_plugin.h"
+#include"pb_decl_plugin.h"
#include"rewriter_types.h"
#include"expr_functors.h"
-class fd_rewriter {
+class pb2bv_rewriter {
struct imp;
imp* m_imp;
public:
- fd_rewriter(ast_manager & m, params_ref const& p);
- ~fd_rewriter();
+ pb2bv_rewriter(ast_manager & m, params_ref const& p);
+ ~pb2bv_rewriter();
void updt_params(params_ref const & p);
ast_manager & m() const;
unsigned get_num_steps() const;
void cleanup();
- obj_map<func_decl, func_decl*> const& enum2bv() const;
- obj_map<func_decl, func_decl*> const& bv2enum() const;
- obj_map<func_decl, expr*> const& enum2def() const;
+ func_decl_ref_vector const& fresh_constants() const;
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);
void flush_side_constraints(expr_ref_vector& side_constraints);
unsigned num_translated() const;
- void set_is_fd(i_sort_pred* sp) const;
+ void collect_statistics(statistics & st) const;
};
#endif
diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
index d233604f9..0fdbc858d 100644
--- a/src/ast/rewriter/pb_rewriter.cpp
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -257,7 +257,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
all_unit &= m_coeffs.back().is_one();
}
if (is_eq) {
- result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
+ if (sz == 0) {
+ result = k.is_zero()?m.mk_true():m.mk_false();
+ }
+ else {
+ result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
+ }
}
else if (all_unit && k.is_one()) {
result = mk_or(m, sz, m_args.c_ptr());
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 7a49f8fd0..d9fe9ab72 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -182,8 +182,8 @@ struct check_logic::imp {
m_quantifiers = false;
}
else if (logic == "QF_FD") {
- m_bvs = true;
- m_uf = true;
+ m_bvs = true;
+ m_uf = true;
m_ints = true;
}
else {
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 1df28b8e5..b7c80f65a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -547,6 +547,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_BVFP" ||
s == "QF_S" ||
s == "ALL" ||
+ s == "QF_FD" ||
s == "HORN";
}
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index 17c5a51bf..5b7f630b4 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -90,19 +90,6 @@ namespace opt {
virtual void get_labels(svector<symbol> & r) {
m_solver->get_labels(r);
}
- virtual void set_cancel(bool f) {
- m_solver->set_cancel(f);
- m_pb2bv.set_cancel(f);
- #pragma omp critical (sls_solver)
- {
- if (m_bvsls) {
- m_bvsls->set_cancel(f);
- }
- if (m_pbsls) {
- m_pbsls->set_cancel(f);
- }
- }
- }
virtual void set_progress_callback(progress_callback * callback) {
m_solver->set_progress_callback(callback);
}
@@ -203,14 +190,11 @@ namespace opt {
}
void pbsls_opt(model_ref& mdl) {
- #pragma omp critical (sls_solver)
- {
- if (m_pbsls) {
- m_pbsls->reset();
- }
- else {
- m_pbsls = alloc(smt::pb_sls, m);
- }
+ if (m_pbsls) {
+ m_pbsls->reset();
+ }
+ else {
+ m_pbsls = alloc(smt::pb_sls, m);
}
m_pbsls->set_model(mdl);
m_pbsls->updt_params(m_params);
@@ -226,10 +210,7 @@ namespace opt {
}
void bvsls_opt(model_ref& mdl) {
- #pragma omp critical (sls_solver)
- {
- m_bvsls = alloc(bvsls_opt_engine, m, m_params);
- }
+ m_bvsls = alloc(bvsls_opt_engine, m, m_params);
assertions2sls();
expr_ref objective = soft2bv(m_soft, m_weights);
TRACE("opt", tout << objective << "\n";);
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 3819f05cb..df39b4186 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -222,6 +222,12 @@ namespace smt {
m_imp->assert_expr(e);
}
+ void kernel::assert_expr(expr_ref_vector const& es) {
+ for (unsigned i = 0; i < es.size(); ++i) {
+ m_imp->assert_expr(es[i]);
+ }
+ }
+
void kernel::assert_expr(expr * e, proof * pr) {
m_imp->assert_expr(e, pr);
}
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 0fec4a21b..ea09081ec 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -70,7 +70,8 @@ namespace smt {
This method uses the "asserted" proof as a justification for e.
*/
void assert_expr(expr * e);
-
+
+ void assert_expr(expr_ref_vector const& es);
/**
\brief Assert the given assertion with the given proof as a justification.
*/
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7b032dce9..d53371c3c 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1270,28 +1270,25 @@ namespace smt {
TRACE("pb", tout << in << " >= " << k << "\n";);
+ psort_expr ps(ctx, *this);
+ psort_nw<psort_expr> sortnw(ps);
+ sortnw.m_stats.reset();
+
if (ctx.get_assignment(thl) == l_true &&
ctx.get_assign_level(thl) == ctx.get_base_level()) {
- psort_expr ps(ctx, *this);
- psort_nw<psort_expr> sortnw(ps);
- sortnw.m_stats.reset();
at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr());
TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
- m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars;
- m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses;
}
else {
- psort_expr ps(ctx, *this);
- psort_nw<psort_expr> sortnw(ps);
- sortnw.m_stats.reset();
literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr());
TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k));
- m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars;
- m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses;
}
+ m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars;
+ m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses;
+
IF_VERBOSE(1, verbose_stream()
<< "(smt.pb compile sorting network bound: "
<< k << " literals: " << in.size() << ")\n";);
diff --git a/src/tactic/arith/bv2int_rewriter.h b/src/tactic/arith/bv2int_rewriter.h
index 0f68257f1..15a425857 100644
--- a/src/tactic/arith/bv2int_rewriter.h
+++ b/src/tactic/arith/bv2int_rewriter.h
@@ -34,7 +34,7 @@ class bv2int_rewriter_ctx {
public:
bv2int_rewriter_ctx(ast_manager& m, params_ref const& p) :
- m_side_conditions(m), m_trail(m) { update_params(p); }
+ m_max_size(UINT_MAX), m_side_conditions(m), m_trail(m) { update_params(p); }
void reset() { m_side_conditions.reset(); m_trail.reset(); m_power2.reset(); }
void add_side_condition(expr* e) { m_side_conditions.push_back(e); }
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 5019b6550..096e52981 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -18,500 +18,22 @@ Notes:
--*/
#include"tactical.h"
#include"cooperate.h"
-#include"rewriter_def.h"
#include"ast_smt2_pp.h"
-#include"expr_substitution.h"
#include"card2bv_tactic.h"
-#include"pb_rewriter.h"
+#include"pb2bv_rewriter.h"
#include"ast_util.h"
#include"ast_pp.h"
-
-namespace pb {
- unsigned card2bv_rewriter::get_num_bits(func_decl* f) {
- rational r(0);
- unsigned sz = f->get_arity();
- for (unsigned i = 0; i < sz; ++i) {
- r += pb.get_coeff(f, i);
- }
- r = r > pb.get_k(f)? r : pb.get_k(f);
- return r.get_num_bits();
- }
-
- card2bv_rewriter::card2bv_rewriter(ast_manager& m):
- m(m),
- au(m),
- pb(m),
- bv(m),
- m_sort(*this),
- m_lemmas(m),
- m_trail(m)
- {}
-
- void card2bv_rewriter::mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas) {
- m_lemmas.reset();
- SASSERT(f->get_family_id() == pb.get_family_id());
- if (is_or(f)) {
- result = m.mk_or(sz, args);
- }
- else if (is_and(f)) {
- result = m.mk_and(sz, args);
- }
- else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
- result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args);
- }
- else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
- result = m_sort.le(false, pb.get_k(f).get_unsigned(), sz, args);
- }
- else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
- result = m_sort.ge(false, pb.get_k(f).get_unsigned(), sz, args);
- }
- else {
- br_status st = mk_shannon(f, sz, args, result);
- if (st == BR_FAILED) {
- mk_bv(f, sz, args, result);
- }
- }
- lemmas.append(m_lemmas);
- }
-
- std::ostream& card2bv_rewriter::pp(std::ostream& out, literal lit) {
- return out << mk_ismt2_pp(lit, m);
- }
-
- card2bv_rewriter::literal card2bv_rewriter::trail(literal l) {
- m_trail.push_back(l);
- return l;
- }
- card2bv_rewriter::literal card2bv_rewriter::fresh() {
- return trail(m.mk_fresh_const("sn", m.mk_bool_sort()));
- }
-
- void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) {
- m_lemmas.push_back(mk_or(m, n, lits));
- }
-
-
- br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
- if (f->get_family_id() == null_family_id) {
- if (sz == 1) {
- // Expecting minimize/maximize.
- func_decl_ref fd(m);
- fd = m.mk_func_decl(f->get_name(), m.get_sort(args[0]), f->get_range());
- result = m.mk_app(fd.get(), args[0]);
- return BR_DONE;
- }
- else
- return BR_FAILED;
- }
- else if (f->get_family_id() == m.get_basic_family_id()) {
- result = m.mk_app(f, sz, args);
- return BR_DONE;
- }
- else if (f->get_family_id() == pb.get_family_id()) {
- if (is_or(f)) {
- result = m.mk_or(sz, args);
- return BR_DONE;
- }
- if (is_and(f)) {
- result = m.mk_and(sz, args);
- return BR_DONE;
- }
- if (is_atmost1(f, sz, args, result)) {
- return BR_DONE;
- }
- br_status st = mk_shannon(f, sz, args, result);
- if (st == BR_FAILED) {
- mk_bv(f, sz, args, result);
- return BR_DONE;
- }
- else {
- return st;
- }
- }
- // NSB: review
- // we should remove this code and rely on a layer above to deal with
- // whatever it accomplishes. It seems to break types.
- //
- else if (f->get_family_id() == au.get_family_id()) {
- if (f->get_decl_kind() == OP_ADD) {
- unsigned bits = 0;
- for (unsigned i = 0; i < sz; i++) {
- rational val1, val2;
- if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
- bits += val1.get_num_bits();
- }
- else if (m.is_ite(args[i]) &&
- au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
- au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
- bits++;
- }
- else
- return BR_FAILED;
- }
-
- result = 0;
- for (unsigned i = 0; i < sz; i++) {
- rational val1, val2;
- expr * q;
- if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
- q = bv.mk_numeral(val1, bits);
- else
- q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
- result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
- }
- return BR_DONE;
- }
- else
- return BR_FAILED;
- }
- else
- return BR_FAILED;
- }
-
- expr_ref card2bv_rewriter::mk_atmost1(unsigned n, expr * const* xs) {
- expr_ref_vector result(m), in(m);
- in.append(n, xs);
- unsigned inc_size = 4;
- while (!in.empty()) {
- expr_ref_vector ors(m);
- unsigned i = 0;
- unsigned n = in.size();
- bool last = n <= inc_size;
- for (; i + inc_size < n; i += inc_size) {
- mk_at_most_1_small(last, inc_size, in.c_ptr() + i, result, ors);
- }
- if (i < n) {
- mk_at_most_1_small(last, n - i, in.c_ptr() + i, result, ors);
- }
- if (last) {
- break;
- }
- in.reset();
- in.append(ors);
- }
- return mk_and(result);
- }
-
- void card2bv_rewriter::mk_at_most_1_small(bool last, unsigned n, literal const* xs, expr_ref_vector& result, expr_ref_vector& ors) {
- if (!last) {
- ors.push_back(m.mk_or(n, xs));
- }
- for (unsigned i = 0; i < n; ++i) {
- for (unsigned j = i + 1; j < n; ++j) {
- result.push_back(m.mk_not(m.mk_and(xs[i], xs[j])));
- }
- }
- }
-
- bool card2bv_rewriter::is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result) {
- switch (f->get_decl_kind()) {
- case OP_AT_MOST_K:
- case OP_PB_LE:
- if (pb.get_k(f).is_one() && pb.has_unit_coefficients(f)) {
- result = mk_atmost1(sz, args);
- return true;
- }
- return false;
- case OP_AT_LEAST_K:
- case OP_PB_GE:
- if (pb.get_k(f) == rational(sz-1) && pb.has_unit_coefficients(f)) {
- expr_ref_vector nargs(m);
- for (unsigned i = 0; i < sz; ++i) {
- nargs.push_back(mk_not(args[i]));
- }
- result = mk_atmost1(nargs.size(), nargs.c_ptr());
- return true;
- }
- return false;
- case OP_PB_EQ:
- return false;
- default:
- UNREACHABLE();
- return false;
- }
- }
-
- bool card2bv_rewriter::is_or(func_decl* f) {
- switch (f->get_decl_kind()) {
- case OP_AT_MOST_K:
- case OP_PB_LE:
- return false;
- case OP_AT_LEAST_K:
- case OP_PB_GE:
- return pb.get_k(f).is_one();
- case OP_PB_EQ:
- return false;
- default:
- UNREACHABLE();
- return false;
- }
- }
-
- bool card2bv_rewriter::is_and(func_decl* f) {
- return false;
- }
-
- void card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
- expr_ref zero(m), a(m), b(m);
- expr_ref_vector es(m);
- unsigned bw = get_num_bits(f);
- zero = bv.mk_numeral(rational(0), bw);
- for (unsigned i = 0; i < sz; ++i) {
- es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
- }
- switch (es.size()) {
- case 0: a = zero; break;
- case 1: a = es[0].get(); break;
- default:
- a = es[0].get();
- for (unsigned i = 1; i < es.size(); ++i) {
- a = bv.mk_bv_add(a, es[i].get());
- }
- break;
- }
- b = bv.mk_numeral(pb.get_k(f), bw);
-
- switch (f->get_decl_kind()) {
- case OP_AT_MOST_K:
- case OP_PB_LE:
- UNREACHABLE();
- result = bv.mk_ule(a, b);
- break;
- case OP_AT_LEAST_K:
- UNREACHABLE();
- case OP_PB_GE:
- result = bv.mk_ule(b, a);
- break;
- case OP_PB_EQ:
- result = m.mk_eq(a, b);
- break;
- default:
- UNREACHABLE();
- }
- TRACE("card2bv", tout << result << "\n";);
- }
-
- struct argc_t {
- expr* m_arg;
- rational m_coeff;
- argc_t():m_arg(0), m_coeff(0) {}
- argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
- };
- struct argc_gt {
- bool operator()(argc_t const& a, argc_t const& b) const {
- return a.m_coeff > b.m_coeff;
- }
- };
- struct argc_entry {
- unsigned m_index;
- rational m_k;
- expr* m_value;
- argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
- argc_entry():m_index(0), m_k(0), m_value(0) {}
-
- struct eq {
- bool operator()(argc_entry const& a, argc_entry const& b) const {
- return a.m_index == b.m_index && a.m_k == b.m_k;
- }
- };
- struct hash {
- unsigned operator()(argc_entry const& a) const {
- return a.m_index ^ a.m_k.hash();
- }
- };
- };
- typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
-
- br_status card2bv_rewriter::mk_shannon(
- func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-
- unsigned max_clauses = sz*10;
- vector<argc_t> argcs;
- for (unsigned i = 0; i < sz; ++i) {
- argcs.push_back(argc_t(args[i], pb.get_coeff(f, i)));
- }
- std::sort(argcs.begin(), argcs.end(), argc_gt());
- DEBUG_CODE(
- for (unsigned i = 0; i + 1 < sz; ++i) {
- SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
- }
- );
- result = m.mk_app(f, sz, args);
- TRACE("card2bv", tout << result << "\n";);
- argc_cache cache;
- expr_ref_vector trail(m);
- vector<rational> todo_k;
- unsigned_vector todo_i;
- todo_k.push_back(pb.get_k(f));
- todo_i.push_back(0);
- decl_kind kind = f->get_decl_kind();
- argc_entry entry1;
- while (!todo_i.empty()) {
- SASSERT(todo_i.size() == todo_k.size());
- if (cache.size() > max_clauses) {
- return BR_FAILED;
- }
- unsigned i = todo_i.back();
- rational k = todo_k.back();
- argc_entry entry(i, k);
- if (cache.contains(entry)) {
- todo_i.pop_back();
- todo_k.pop_back();
- continue;
- }
- SASSERT(i < sz);
- SASSERT(!k.is_neg());
- rational const& coeff = argcs[i].m_coeff;
- expr* arg = argcs[i].m_arg;
- if (i + 1 == sz) {
- switch(kind) {
- case OP_AT_MOST_K:
- case OP_PB_LE:
- if (coeff <= k) {
- entry.m_value = m.mk_true();
- }
- else {
- entry.m_value = negate(arg);
- trail.push_back(entry.m_value);
- }
- break;
- case OP_AT_LEAST_K:
- case OP_PB_GE:
- if (k.is_zero()) {
- entry.m_value = m.mk_true();
- }
- else if (coeff < k) {
- entry.m_value = m.mk_false();
- }
- else if (coeff.is_zero()) {
- entry.m_value = m.mk_true();
- }
- else {
- SASSERT(coeff >= k && k.is_pos());
- entry.m_value = arg;
- }
- break;
- case OP_PB_EQ:
- if (coeff == k) {
- entry.m_value = arg;
- }
- else if (k.is_zero()) {
- entry.m_value = negate(arg);
- trail.push_back(entry.m_value);
- }
- else {
- entry.m_value = m.mk_false();
- }
- break;
- }
- todo_i.pop_back();
- todo_k.pop_back();
- cache.insert(entry);
- continue;
- }
- entry.m_index++;
- expr* lo = 0, *hi = 0;
- if (cache.find(entry, entry1)) {
- lo = entry1.m_value;
- }
- else {
- todo_i.push_back(i+1);
- todo_k.push_back(k);
- }
- entry.m_k -= coeff;
- if (kind != OP_PB_EQ && !entry.m_k.is_pos()) {
- switch (kind) {
- case OP_AT_MOST_K:
- case OP_PB_LE:
- hi = m.mk_false();
- break;
- case OP_AT_LEAST_K:
- case OP_PB_GE:
- hi = m.mk_true();
- break;
- default:
- UNREACHABLE();
- }
- }
- else if (cache.find(entry, entry1)) {
- hi = entry1.m_value;
- }
- else {
- todo_i.push_back(i+1);
- todo_k.push_back(entry.m_k);
- }
- if (hi && lo) {
- todo_i.pop_back();
- todo_k.pop_back();
- entry.m_index = i;
- entry.m_k = k;
- entry.m_value = mk_ite(arg, hi, lo);
- trail.push_back(entry.m_value);
- cache.insert(entry);
- }
- }
- argc_entry entry(0, pb.get_k(f));
- VERIFY(cache.find(entry, entry));
- result = entry.m_value;
- TRACE("card2bv", tout << result << "\n";);
- return BR_DONE;
- }
-
- expr* card2bv_rewriter::negate(expr* e) {
- if (m.is_not(e, e)) return e;
- return m.mk_not(e);
- }
-
- expr* card2bv_rewriter::mk_ite(expr* c, expr* hi, expr* lo) {
- while (m.is_not(c, c)) {
- std::swap(hi, lo);
- }
- if (hi == lo) return hi;
- if (m.is_true(hi) && m.is_false(lo)) return c;
- if (m.is_false(hi) && m.is_true(lo)) return negate(c);
- if (m.is_true(hi)) return m.mk_or(c, lo);
- if (m.is_false(lo)) return m.mk_and(c, hi);
- if (m.is_false(hi)) return m.mk_and(negate(c), lo);
- if (m.is_true(lo)) return m.mk_implies(c, hi);
- return m.mk_ite(c, hi, lo);
- }
-
- void card_pb_rewriter::rewrite(expr* e, expr_ref& result) {
- if (pb.is_eq(e)) {
- app* a = to_app(e);
- ast_manager& m = m_lemmas.get_manager();
- unsigned sz = a->get_num_args();
- expr_ref_vector args(m);
- expr_ref tmp(m);
- for (unsigned i = 0; i < sz; ++i) {
- (*this)(a->get_arg(i), tmp);
- args.push_back(tmp);
- }
- m_cfg.m_r.mk_assert(a->get_decl(), sz, args.c_ptr(), result, m_lemmas);
- }
- else {
- (*this)(e, result);
- }
- }
-
-};
-
-template class rewriter_tpl<pb::card2bv_rewriter_cfg>;
-
+#include"filter_model_converter.h"
class card2bv_tactic : public tactic {
ast_manager & m;
params_ref m_params;
- th_rewriter m_rw1;
- pb::card_pb_rewriter m_rw2;
public:
card2bv_tactic(ast_manager & m, params_ref const & p):
m(m),
- m_params(p),
- m_rw1(m),
- m_rw2(m) {
+ m_params(p) {
}
virtual tactic * translate(ast_manager & m) {
@@ -538,9 +60,8 @@ public:
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("card2bv", *g);
- m_rw1.reset();
- m_rw2.reset();
- m_rw2.lemmas().reset();
+ th_rewriter rw1(m, m_params);
+ pb2bv_rewriter rw2(m, m_params);
if (g->inconsistent()) {
result.push_back(g.get());
@@ -550,18 +71,28 @@ public:
expr_ref new_f1(m), new_f2(m);
proof_ref new_pr1(m), new_pr2(m);
for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
- m_rw1(g->form(idx), new_f1, new_pr1);
+ rw1(g->form(idx), new_f1, new_pr1);
TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
- m_rw2.rewrite(new_f1, new_f2);
+ rw2(new_f1, new_f2, new_pr2);
if (m.proofs_enabled()) {
new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1);
- new_pr2 = m.mk_rewrite(new_f1, new_f2);
new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2);
}
g->update(idx, new_f2, new_pr1, g->dep(idx));
}
- for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) {
- g->assert_expr(m_rw2.lemmas()[i].get());
+ expr_ref_vector fmls(m);
+ rw2.flush_side_constraints(fmls);
+ for (unsigned i = 0; !g->inconsistent() && i < fmls.size(); ++i) {
+ g->assert_expr(fmls[i].get());
+ }
+
+ func_decl_ref_vector const& fns = rw2.fresh_constants();
+ if (!fns.empty()) {
+ filter_model_converter* filter = alloc(filter_model_converter, m);
+ for (unsigned i = 0; i < fns.size(); ++i) {
+ filter->insert(fns[i]);
+ }
+ mc = filter;
}
g->inc_depth();
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 2ecc80980..2ccbe9712 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -29,7 +29,7 @@ Revision History:
#include "extension_model_converter.h"
#include "var_subst.h"
#include "ast_util.h"
-#include "fd_rewriter.h"
+#include "enum2bv_rewriter.h"
class dt2bv_tactic : public tactic {
@@ -132,7 +132,7 @@ public:
if (!m_fd_sorts.empty()) {
ref<extension_model_converter> ext = alloc(extension_model_converter, m);
ref<filter_model_converter> filter = alloc(filter_model_converter, m);
- fd_rewriter rw(m, m_params);
+ enum2bv_rewriter rw(m, m_params);
rw.set_is_fd(&m_is_fd);
expr_ref new_curr(m);
proof_ref new_pr(m);
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
new file mode 100644
index 000000000..f7236351c
--- /dev/null
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -0,0 +1,296 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ bounded_int2bv_solver.cpp
+
+Abstract:
+
+ This solver identifies bounded integers and rewrites them to bit-vectors.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+
+#include "bounded_int2bv_solver.h"
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "pb2bv_rewriter.h"
+#include "filter_model_converter.h"
+#include "extension_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+#include "bound_manager.h"
+#include "bv2int_rewriter.h"
+#include "expr_safe_replace.h"
+#include "bv_decl_plugin.h"
+#include "arith_decl_plugin.h"
+
+class bounded_int2bv_solver : public solver_na2as {
+ ast_manager& m;
+ params_ref m_params;
+ bv_util m_bv;
+ arith_util m_arith;
+ expr_ref_vector m_assertions;
+ ref<solver> m_solver;
+ ptr_vector<bound_manager> m_bounds;
+ func_decl_ref_vector m_bv_fns;
+ func_decl_ref_vector m_int_fns;
+ unsigned_vector m_bv_fns_lim;
+ obj_map<func_decl, func_decl*> m_int2bv;
+ obj_map<func_decl, func_decl*> m_bv2int;
+ obj_map<func_decl, rational> m_bv2offset;
+ bv2int_rewriter_ctx m_rewriter_ctx;
+ bv2int_rewriter_star m_rewriter;
+
+public:
+
+ bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+ solver_na2as(m),
+ m(m),
+ m_params(p),
+ m_bv(m),
+ m_arith(m),
+ m_assertions(m),
+ m_solver(s),
+ m_bv_fns(m),
+ m_int_fns(m),
+ m_rewriter_ctx(m, p),
+ m_rewriter(m, m_rewriter_ctx)
+ {
+ m_bounds.push_back(alloc(bound_manager, m));
+ }
+
+ virtual ~bounded_int2bv_solver() {
+ while (!m_bounds.empty()) {
+ dealloc(m_bounds.back());
+ m_bounds.pop_back();
+ }
+ }
+
+ virtual solver* translate(ast_manager& m, params_ref const& p) {
+ return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
+ }
+
+ virtual void assert_expr(expr * t) {
+ m_assertions.push_back(t);
+ }
+
+ virtual void push_core() {
+ flush_assertions();
+ m_solver->push();
+ m_bv_fns_lim.push_back(m_bv_fns.size());
+ m_bounds.push_back(alloc(bound_manager, m));
+ }
+
+ virtual void pop_core(unsigned n) {
+ m_assertions.reset();
+ m_solver->pop(n);
+
+ if (n > 0) {
+ SASSERT(n <= m_bv_fns_lim.size());
+ unsigned new_sz = m_bv_fns_lim.size() - n;
+ unsigned lim = m_bv_fns_lim[new_sz];
+ for (unsigned i = m_int_fns.size(); i > lim; ) {
+ --i;
+ m_int2bv.erase(m_int_fns[i].get());
+ m_bv2int.erase(m_bv_fns[i].get());
+ m_bv2offset.erase(m_bv_fns[i].get());
+ }
+ m_bv_fns_lim.resize(new_sz);
+ m_bv_fns.resize(lim);
+ m_int_fns.resize(lim);
+ }
+
+ while (n > 0) {
+ dealloc(m_bounds.back());
+ m_bounds.pop_back();
+ --n;
+ }
+ }
+
+ virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+ flush_assertions();
+ return m_solver->check_sat(num_assumptions, assumptions);
+ }
+
+ virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
+ virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
+ virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+ virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
+ virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
+ virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+ virtual void get_model(model_ref & mdl) {
+ m_solver->get_model(mdl);
+ if (mdl) {
+ extend_model(mdl);
+ filter_model(mdl);
+ }
+ }
+ virtual proof * get_proof() { return m_solver->get_proof(); }
+ virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+ virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+ virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+ virtual ast_manager& get_manager() const { return m; }
+ virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+ virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+ flush_assertions();
+ expr_ref_vector bvars(m);
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ expr* v = vars[i];
+ func_decl* f;
+ rational offset;
+ if (is_app(v) && is_uninterp_const(v) && m_int2bv.find(to_app(v)->get_decl(), f)) {
+ bvars.push_back(m.mk_const(f));
+ }
+ else {
+ bvars.push_back(v);
+ }
+ }
+ lbool r = m_solver->get_consequences(asms, bvars, consequences);
+
+ // translate bit-vector consequences back to integer values
+ for (unsigned i = 0; i < consequences.size(); ++i) {
+ expr* a, *b, *u, *v;
+ func_decl* f;
+ rational num;
+ unsigned bvsize;
+ rational offset;
+ VERIFY(m.is_implies(consequences[i].get(), a, b));
+ if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_bv2int.find(to_app(u)->get_decl(), f) && m_bv.is_numeral(v, num, bvsize)) {
+ SASSERT(num.is_unsigned());
+ expr_ref head(m);
+ VERIFY (m_bv2offset.find(to_app(u)->get_decl(), offset));
+ // f + offset == num
+ // f == num - offset
+ head = m.mk_eq(m.mk_const(f), m_arith.mk_numeral(num + offset, true));
+ consequences[i] = m.mk_implies(a, head);
+ }
+ }
+ return r;
+
+ }
+
+private:
+
+ void filter_model(model_ref& mdl) const {
+ if (m_bv_fns.empty()) {
+ return;
+ }
+ filter_model_converter filter(m);
+ func_decl_ref_vector const& fns = m_bv_fns;
+ for (unsigned i = 0; i < m_bv_fns.size(); ++i) {
+ filter.insert(m_bv_fns[i]);
+ }
+ filter(mdl, 0);
+ }
+
+ void extend_model(model_ref& mdl) {
+ extension_model_converter ext(m);
+ obj_map<func_decl, func_decl*>::iterator it = m_int2bv.begin(), end = m_int2bv.end();
+ for (; it != end; ++it) {
+ rational offset;
+ VERIFY (m_bv2offset.find(it->m_value, offset));
+ expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m);
+ if (!offset.is_zero()) {
+ value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
+ }
+ TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";);
+ ext.insert(it->m_key, value);
+ }
+ ext(mdl, 0);
+ }
+
+ void accumulate_sub(expr_safe_replace& sub) {
+ for (unsigned i = 0; i < m_bounds.size(); ++i) {
+ accumulate_sub(sub, *m_bounds[i]);
+ }
+ }
+
+ void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) {
+ bound_manager::iterator it = bm.begin(), end = bm.end();
+ for (; it != end; ++it) {
+ expr* e = *it;
+ rational lo, hi;
+ bool s1, s2;
+ SASSERT(is_uninterp_const(e));
+ func_decl* f = to_app(e)->get_decl();
+
+ if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
+ func_decl* fbv;
+ rational offset;
+ if (!m_int2bv.find(f, fbv)) {
+ rational n = hi - lo + rational::one();
+ unsigned num_bits = get_num_bits(n);
+ expr_ref b(m);
+ b = m.mk_fresh_const("b", m_bv.mk_sort(num_bits));
+ fbv = to_app(b)->get_decl();
+ offset = lo;
+ m_int2bv.insert(f, fbv);
+ m_bv2int.insert(fbv, f);
+ m_bv2offset.insert(fbv, offset);
+ m_bv_fns.push_back(fbv);
+ m_int_fns.push_back(f);
+ unsigned shift;
+ if (!offset.is_zero() && !n.is_power_of_two(shift)) {
+ m_assertions.push_back(m_bv.mk_ule(b, m_bv.mk_numeral(n-rational::one(), num_bits)));
+ }
+ }
+ else {
+ VERIFY(m_bv2offset.find(fbv, offset));
+ }
+ expr_ref t(m.mk_const(fbv), m);
+ t = m_bv.mk_bv2int(t);
+ if (!offset.is_zero()) {
+ t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true));
+ }
+ sub.insert(e, t);
+ }
+ }
+ }
+
+ unsigned get_num_bits(rational const& k) {
+ SASSERT(!k.is_neg());
+ SASSERT(k.is_int());
+ rational two(2);
+ rational bound(1);
+ unsigned num_bits = 1;
+ while (bound <= k) {
+ ++num_bits;
+ bound *= two;
+ }
+ return num_bits;
+ }
+
+ void flush_assertions() {
+ bound_manager& bm = *m_bounds.back();
+ for (unsigned i = 0; i < m_assertions.size(); ++i) {
+ bm(m_assertions[i].get());
+ }
+ expr_safe_replace sub(m);
+ accumulate_sub(sub);
+ proof_ref proof(m);
+ expr_ref fml1(m), fml2(m);
+ if (sub.empty()) {
+ m_solver->assert_expr(m_assertions);
+ }
+ else {
+ for (unsigned i = 0; i < m_assertions.size(); ++i) {
+ sub(m_assertions[i].get(), fml1);
+ m_rewriter(fml1, fml2, proof);
+ m_solver->assert_expr(fml2);
+ TRACE("int2bv", tout << fml2 << "\n";);
+ }
+ }
+ m_assertions.reset();
+ }
+};
+
+solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+ return alloc(bounded_int2bv_solver, m, p, s);
+}
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.h b/src/tactic/portfolio/bounded_int2bv_solver.h
new file mode 100644
index 000000000..5fcf2cd65
--- /dev/null
+++ b/src/tactic/portfolio/bounded_int2bv_solver.h
@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ bounded_int2bv_solver.h
+
+Abstract:
+
+ Finite domain solver.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+#ifndef BOUNDED_INT2BV_SOLVER_H_
+#define BOUNDED_INT2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
new file mode 100644
index 000000000..369402114
--- /dev/null
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -0,0 +1,162 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ enum2bv_solver.cpp
+
+Abstract:
+
+ Finite domain solver.
+
+ Enumeration data-types are translated into bit-vectors, and then
+ the incremental sat-solver is applied to the resulting assertions.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+
+--*/
+
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "bv_decl_plugin.h"
+#include "datatype_decl_plugin.h"
+#include "enum2bv_rewriter.h"
+#include "extension_model_converter.h"
+#include "filter_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+#include "enum2bv_solver.h"
+
+class enum2bv_solver : public solver_na2as {
+ ast_manager& m;
+ params_ref m_params;
+ ref<solver> m_solver;
+ enum2bv_rewriter m_rewriter;
+
+public:
+
+ enum2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+ solver_na2as(m),
+ m(m),
+ m_params(p),
+ m_solver(s),
+ m_rewriter(m, p)
+ {
+ }
+
+ virtual ~enum2bv_solver() {}
+
+ virtual solver* translate(ast_manager& m, params_ref const& p) {
+ return alloc(enum2bv_solver, m, p, m_solver->translate(m, p));
+ }
+
+ virtual void assert_expr(expr * t) {
+ expr_ref tmp(t, m);
+ expr_ref_vector bounds(m);
+ proof_ref tmp_proof(m);
+ m_rewriter(t, tmp, tmp_proof);
+ m_solver->assert_expr(tmp);
+ m_rewriter.flush_side_constraints(bounds);
+ m_solver->assert_expr(bounds);
+ }
+
+ virtual void push_core() {
+ m_rewriter.push();
+ m_solver->push();
+ }
+
+ virtual void pop_core(unsigned n) {
+ m_solver->pop(n);
+ m_rewriter.pop(n);
+ }
+
+ virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+ return m_solver->check_sat(num_assumptions, assumptions);
+ }
+
+ virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
+ virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
+ virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+ virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
+ virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
+ virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+ virtual void get_model(model_ref & mdl) {
+ m_solver->get_model(mdl);
+ if (mdl) {
+ extend_model(mdl);
+ filter_model(mdl);
+ }
+ }
+ virtual proof * get_proof() { return m_solver->get_proof(); }
+ virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+ virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+ virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+ virtual ast_manager& get_manager() const { return m; }
+ virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+
+ virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+
+ datatype_util dt(m);
+ bv_util bv(m);
+
+ // translate enumeration constants to bit-vectors.
+ expr_ref_vector bvars(m), conseq(m);
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ func_decl* f;
+ if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
+ bvars.push_back(m.mk_const(f));
+ }
+ else {
+ bvars.push_back(vars[i]);
+ }
+ }
+ lbool r = m_solver->get_consequences(asms, bvars, consequences);
+ std::cout << consequences.size() << "\n";
+
+
+ // translate bit-vector consequences back to enumeration types
+ for (unsigned i = 0; i < consequences.size(); ++i) {
+ expr* a, *b, *u, *v;
+ func_decl* f;
+ rational num;
+ unsigned bvsize;
+ VERIFY(m.is_implies(consequences[i].get(), a, b));
+ if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
+ SASSERT(num.is_unsigned());
+ expr_ref head(m);
+ ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
+ head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
+ consequences[i] = m.mk_implies(a, head);
+ }
+ }
+ return r;
+ }
+
+ void filter_model(model_ref& mdl) {
+ filter_model_converter filter(m);
+ obj_map<func_decl, func_decl*>::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end();
+ for (; it != end; ++it) {
+ filter.insert(it->m_value);
+ }
+ filter(mdl, 0);
+ }
+
+ void extend_model(model_ref& mdl) {
+ extension_model_converter ext(m);
+ obj_map<func_decl, expr*>::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end();
+ for (; it != end; ++it) {
+ ext.insert(it->m_key, it->m_value);
+
+ }
+ ext(mdl, 0);
+ }
+
+};
+
+solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+ return alloc(enum2bv_solver, m, p, s);
+}
diff --git a/src/tactic/portfolio/enum2bv_solver.h b/src/tactic/portfolio/enum2bv_solver.h
new file mode 100644
index 000000000..b113c6747
--- /dev/null
+++ b/src/tactic/portfolio/enum2bv_solver.h
@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ enum2bv_solver.h
+
+Abstract:
+
+ Finite domain solver.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+
+--*/
+#ifndef ENUM2BV_SOLVER_H_
+#define ENUM2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif
diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp
index 9447c158c..a534337bc 100644
--- a/src/tactic/portfolio/fd_solver.cpp
+++ b/src/tactic/portfolio/fd_solver.cpp
@@ -9,9 +9,6 @@ Abstract:
Finite domain solver.
- Enumeration data-types are translated into bit-vectors, and then
- the incremental sat-solver is applied to the resulting assertions.
-
Author:
Nikolaj Bjorner (nbjorner) 2016-10-17
@@ -21,141 +18,16 @@ Notes:
--*/
#include "fd_solver.h"
-#include "solver_na2as.h"
#include "tactic.h"
#include "inc_sat_solver.h"
-#include "bv_decl_plugin.h"
-#include "datatype_decl_plugin.h"
-#include "fd_rewriter.h"
-#include "extension_model_converter.h"
-#include "filter_model_converter.h"
-#include "ast_pp.h"
-#include "model_smt2_pp.h"
-
-class fd_solver : public solver_na2as {
- ast_manager& m;
- params_ref m_params;
- ref<solver> m_solver;
- fd_rewriter m_rewriter;
-
-public:
-
- fd_solver(ast_manager& m, params_ref const& p):
- solver_na2as(m),
- m(m),
- m_params(p),
- m_solver(mk_inc_sat_solver(m, p)),
- m_rewriter(m, p)
- {
- }
-
- virtual ~fd_solver() {}
-
- virtual solver* translate(ast_manager& m, params_ref const& p) {
- return alloc(fd_solver, m, p);
- }
-
- virtual void assert_expr(expr * t) {
- expr_ref tmp(t, m);
- expr_ref_vector bounds(m);
- proof_ref tmp_proof(m);
- m_rewriter(t, tmp, tmp_proof);
- m_solver->assert_expr(tmp);
- m_rewriter.flush_side_constraints(bounds);
- m_solver->assert_expr(bounds);
- }
-
- virtual void push_core() {
- m_rewriter.push();
- m_solver->push();
- }
-
- virtual void pop_core(unsigned n) {
- m_solver->pop(n);
- m_rewriter.pop(n);
- }
-
- virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
- return m_solver->check_sat(num_assumptions, assumptions);
- }
-
- virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
- virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
- virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
- virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
- virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
- virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
- virtual void get_model(model_ref & mdl) {
- m_solver->get_model(mdl);
- if (mdl) {
- extend_model(mdl);
- filter_model(mdl);
- }
- }
- virtual proof * get_proof() { return m_solver->get_proof(); }
- virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
- virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
- virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
- virtual ast_manager& get_manager() const { return m; }
- virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
-
- virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
-
- datatype_util dt(m);
- bv_util bv(m);
-
- // translate enumeration constants to bit-vectors.
- expr_ref_vector bvars(m), conseq(m);
- for (unsigned i = 0; i < vars.size(); ++i) {
- func_decl* f;
- if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
- bvars.push_back(m.mk_const(f));
- }
- else {
- bvars.push_back(vars[i]);
- }
- }
- lbool r = m_solver->get_consequences(asms, bvars, consequences);
-
- // translate bit-vector consequences back to enumeration types
- for (unsigned i = 0; i < consequences.size(); ++i) {
- expr* a, *b, *u, *v;
- func_decl* f;
- rational num;
- unsigned bvsize;
- VERIFY(m.is_implies(consequences[i].get(), a, b));
- if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
- SASSERT(num.is_unsigned());
- expr_ref head(m);
- ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
- head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
- consequences[i] = m.mk_implies(a, head);
- }
- }
- return r;
- }
-
- void filter_model(model_ref& mdl) {
- filter_model_converter filter(m);
- obj_map<func_decl, func_decl*>::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end();
- for (; it != end; ++it) {
- filter.insert(it->m_value);
- }
- filter(mdl, 0);
- }
-
- void extend_model(model_ref& mdl) {
- extension_model_converter ext(m);
- obj_map<func_decl, expr*>::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end();
- for (; it != end; ++it) {
- ext.insert(it->m_key, it->m_value);
-
- }
- ext(mdl, 0);
- }
-
-};
+#include "enum2bv_solver.h"
+#include "pb2bv_solver.h"
+#include "bounded_int2bv_solver.h"
solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
- return alloc(fd_solver, m, p);
+ solver* s = mk_inc_sat_solver(m, p);
+ s = mk_enum2bv_solver(m, p, s);
+ s = mk_pb2bv_solver(m, p, s);
+ s = mk_bounded_int2bv_solver(m, p, s);
+ return s;
}
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
new file mode 100644
index 000000000..bfd533e8a
--- /dev/null
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -0,0 +1,127 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ pb2bv_solver.cpp
+
+Abstract:
+
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+
+#include "pb2bv_solver.h"
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "pb2bv_rewriter.h"
+#include "filter_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+
+class pb2bv_solver : public solver_na2as {
+ ast_manager& m;
+ params_ref m_params;
+ expr_ref_vector m_assertions;
+ ref<solver> m_solver;
+ pb2bv_rewriter m_rewriter;
+
+public:
+
+ pb2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+ solver_na2as(m),
+ m(m),
+ m_params(p),
+ m_assertions(m),
+ m_solver(s),
+ m_rewriter(m, p)
+ {
+ }
+
+ virtual ~pb2bv_solver() {}
+
+ virtual solver* translate(ast_manager& m, params_ref const& p) {
+ return alloc(pb2bv_solver, m, p, m_solver->translate(m, p));
+ }
+
+ virtual void assert_expr(expr * t) {
+ m_assertions.push_back(t);
+ }
+
+ virtual void push_core() {
+ flush_assertions();
+ m_rewriter.push();
+ m_solver->push();
+ }
+
+ virtual void pop_core(unsigned n) {
+ m_assertions.reset();
+ m_solver->pop(n);
+ m_rewriter.pop(n);
+ }
+
+ virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+ flush_assertions();
+ return m_solver->check_sat(num_assumptions, assumptions);
+ }
+
+ virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
+ virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
+ virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+ virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
+ virtual void collect_statistics(statistics & st) const {
+ m_rewriter.collect_statistics(st);
+ m_solver->collect_statistics(st);
+ }
+ virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+ virtual void get_model(model_ref & mdl) {
+ m_solver->get_model(mdl);
+ if (mdl) {
+ filter_model(mdl);
+ }
+ }
+ virtual proof * get_proof() { return m_solver->get_proof(); }
+ virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+ virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+ virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+ virtual ast_manager& get_manager() const { return m; }
+ virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+ virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+ flush_assertions();
+ return m_solver->get_consequences(asms, vars, consequences); }
+
+ void filter_model(model_ref& mdl) {
+ if (m_rewriter.fresh_constants().empty()) {
+ return;
+ }
+ filter_model_converter filter(m);
+ func_decl_ref_vector const& fns = m_rewriter.fresh_constants();
+ for (unsigned i = 0; i < fns.size(); ++i) {
+ filter.insert(fns[i]);
+ }
+ filter(mdl, 0);
+ }
+
+private:
+ void flush_assertions() {
+ proof_ref proof(m);
+ expr_ref fml(m);
+ expr_ref_vector fmls(m);
+ for (unsigned i = 0; i < m_assertions.size(); ++i) {
+ m_rewriter(m_assertions[i].get(), fml, proof);
+ m_solver->assert_expr(fml);
+ }
+ m_rewriter.flush_side_constraints(fmls);
+ m_solver->assert_expr(fmls);
+ m_assertions.reset();
+ }
+};
+
+solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+ return alloc(pb2bv_solver, m, p, s);
+}
diff --git a/src/tactic/portfolio/pb2bv_solver.h b/src/tactic/portfolio/pb2bv_solver.h
new file mode 100644
index 000000000..e861e769b
--- /dev/null
+++ b/src/tactic/portfolio/pb2bv_solver.h
@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ pb2bv_solver.h
+
+Abstract:
+
+ Pseudo-Boolean to bit-vector solver.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+#ifndef PB2BV_SOLVER_H_
+#define PB2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 9c6cdd668..320eddd7b 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -229,6 +229,7 @@ int main(int argc, char ** argv) {
TST_ARGV(ddnf);
TST(model_evaluator);
TST(get_consequences);
+ TST(pb2bv);
//TST_ARGV(hs);
}
diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp
new file mode 100644
index 000000000..c114997c5
--- /dev/null
+++ b/src/test/pb2bv.cpp
@@ -0,0 +1,195 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+#include "trace.h"
+#include "vector.h"
+#include "ast.h"
+#include "ast_pp.h"
+#include "statistics.h"
+#include "reg_decl_plugins.h"
+#include "pb2bv_rewriter.h"
+#include "smt_kernel.h"
+#include "model_smt2_pp.h"
+#include "smt_params.h"
+#include "ast_util.h"
+#include "pb_decl_plugin.h"
+#include "th_rewriter.h"
+#include "fd_solver.h"
+#include "solver.h"
+
+static void test1() {
+ ast_manager m;
+ reg_decl_plugins(m);
+ pb_util pb(m);
+ params_ref p;
+ pb2bv_rewriter rw(m, p);
+ expr_ref_vector vars(m);
+ unsigned N = 5;
+ for (unsigned i = 0; i < N; ++i) {
+ std::stringstream strm;
+ strm << "b" << i;
+ vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+ }
+
+ for (unsigned k = 1; k <= N; ++k) {
+ expr_ref fml(m), result(m);
+ proof_ref proof(m);
+ fml = pb.mk_at_least_k(vars.size(), vars.c_ptr(), k);
+ rw(fml, result, proof);
+ std::cout << fml << " |-> " << result << "\n";
+ }
+ expr_ref_vector lemmas(m);
+ rw.flush_side_constraints(lemmas);
+ std::cout << lemmas << "\n";
+}
+
+static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
+ pb_util pb(m);
+ params_ref p;
+ pb2bv_rewriter rw(m, p);
+ unsigned N = vars.size();
+ expr_ref fml1(m), fml2(m), result1(m), result2(m);
+ proof_ref proof(m);
+ expr_ref_vector lemmas(m);
+ th_rewriter th_rw(m);
+
+ switch (kind) {
+ case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ }
+ rw(fml1, result1, proof);
+ rw.flush_side_constraints(lemmas);
+ std::cout << lemmas << "\n";
+ for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
+ smt_params fp;
+ smt::kernel solver(m, fp);
+ expr_ref_vector tf(m);
+ for (unsigned i = 0; i < N; ++i) {
+ bool is_true = 0 != (values & (1 << i));
+ tf.push_back(is_true ? m.mk_true() : m.mk_false());
+ solver.assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
+ }
+
+ solver.assert_expr(lemmas);
+ switch (kind) {
+ case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ }
+ std::cout << fml1 << " " << fml2 << "\n";
+ th_rw(fml2, result2, proof);
+ SASSERT(m.is_true(result2) || m.is_false(result2));
+ lbool res = solver.check();
+ SASSERT(res == l_true);
+ solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
+ res = solver.check();
+ SASSERT(res == l_false);
+ }
+}
+
+static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
+ test_semantics(m, vars, coeffs, k, 0);
+ test_semantics(m, vars, coeffs, k, 1);
+ test_semantics(m, vars, coeffs, k, 2);
+}
+
+static void test2() {
+ ast_manager m;
+ reg_decl_plugins(m);
+ expr_ref_vector vars(m);
+ unsigned N = 4;
+ for (unsigned i = 0; i < N; ++i) {
+ std::stringstream strm;
+ strm << "b" << i;
+ vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+ }
+ for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
+ vector<rational> coeffs;
+ for (unsigned i = 0; i < N; ++i) {
+ bool is_one = 0 != (coeff & (1 << i));
+ coeffs.push_back(is_one ? rational(1) : rational(2));
+ }
+ for (unsigned i = 0; i <= N; ++i) {
+ test_semantics(m, vars, coeffs, i);
+ }
+ }
+}
+
+
+static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
+ pb_util pb(m);
+ params_ref p;
+ unsigned N = vars.size();
+ expr_ref fml1(m), fml2(m), result1(m), result2(m);
+ proof_ref proof(m);
+ th_rewriter th_rw(m);
+
+ switch (kind) {
+ case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+ }
+ result1 = m.mk_fresh_const("xx", m.mk_bool_sort());
+ for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
+ ref<solver> slv = mk_fd_solver(m, p);
+ expr_ref_vector tf(m);
+ for (unsigned i = 0; i < N; ++i) {
+ bool is_true = 0 != (values & (1 << i));
+ tf.push_back(is_true ? m.mk_true() : m.mk_false());
+ slv->assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
+ }
+ slv->assert_expr(m.mk_eq(result1, fml1));
+
+ switch (kind) {
+ case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+ }
+ std::cout << fml1 << " " << fml2 << "\n";
+ th_rw(fml2, result2, proof);
+ SASSERT(m.is_true(result2) || m.is_false(result2));
+ lbool res = slv->check_sat(0,0);
+ SASSERT(res == l_true);
+ slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
+ res = slv->check_sat(0,0);
+ SASSERT(res == l_false);
+ }
+}
+
+static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
+ test_solver_semantics(m, vars, coeffs, k, 0);
+ test_solver_semantics(m, vars, coeffs, k, 1);
+ test_solver_semantics(m, vars, coeffs, k, 2);
+}
+
+static void test3() {
+ ast_manager m;
+ reg_decl_plugins(m);
+ expr_ref_vector vars(m);
+ unsigned N = 4;
+ for (unsigned i = 0; i < N; ++i) {
+ std::stringstream strm;
+ strm << "b" << i;
+ vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+ }
+ for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
+ vector<rational> coeffs;
+ for (unsigned i = 0; i < N; ++i) {
+ bool is_one = 0 != (coeff & (1 << i));
+ coeffs.push_back(is_one ? rational(1) : rational(2));
+ }
+ for (unsigned i = 0; i <= N; ++i) {
+ test_solver_semantics(m, vars, coeffs, i);
+ }
+ }
+}
+
+void tst_pb2bv() {
+ test1();
+ test2();
+ test3();
+}
+
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 31ad8a452..0f5d2838e 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -226,7 +226,12 @@ Notes:
m_t = EQ;
card(k+1, n, xs, out);
SASSERT(out.size() >= k+1);
- return ctx.mk_min(out[k-1], ctx.mk_not(out[k]));
+ if (k == 0) {
+ return ctx.mk_not(out[k]);
+ }
+ else {
+ return ctx.mk_min(out[k-1], ctx.mk_not(out[k]));
+ }
}
}