From 980e74b4fffeefa7efb07ff41cc10d2b9c534970 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Aug 2015 06:39:11 -0700
Subject: [PATCH] add tactic to recognize small discrete domains and convert
them into bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_context.cpp | 5 +-
src/tactic/arith/eq2bv_tactic.cpp | 333 ++++++++++++++++++++++++++++++
src/tactic/arith/eq2bv_tactic.h | 34 +++
3 files changed, 370 insertions(+), 2 deletions(-)
create mode 100644 src/tactic/arith/eq2bv_tactic.cpp
create mode 100644 src/tactic/arith/eq2bv_tactic.h
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 857e0ae7e..86c5447a9 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -34,7 +34,7 @@ Notes:
#include "tactical.h"
#include "model_smt2_pp.h"
#include "card2bv_tactic.h"
-#include "nnf_tactic.h"
+#include "eq2bv_tactic.h"
#include "inc_sat_solver.h"
#include "bv_decl_plugin.h"
#include "pb_decl_plugin.h"
@@ -667,10 +667,11 @@ namespace opt {
if (optp.elim_01()) {
tac2 = mk_elim01_tactic(m);
tac3 = mk_lia2card_tactic(m);
+ tac4 = mk_eq2bv_tactic(m);
params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p);
- set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), mk_simplify_tactic(m)));
+ set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get(), mk_simplify_tactic(m)));
}
else {
tactic_ref tac1 =
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
new file mode 100644
index 000000000..fda51f0fa
--- /dev/null
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -0,0 +1,333 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ eq2bv_tactic.cpp
+
+Abstract:
+
+ Extract integer variables that are used as finite domain indicators.
+ The integer variables can only occur in equalities.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2015-8-19
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"cooperate.h"
+#include"bound_manager.h"
+#include"ast_pp.h"
+#include"arith_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"rewriter_def.h"
+#include"ast_util.h"
+#include"ast_pp_util.h"
+
+class eq2bv_tactic : public tactic {
+ struct eq_rewriter_cfg : public default_rewriter_cfg {
+ ast_manager& m;
+ eq2bv_tactic& t;
+
+ bool is_fd(expr* x, expr* y, expr_ref& result) {
+ expr* z;
+ rational r;
+ if (t.m_fd.find(x, z) && t.a.is_numeral(y, r)) {
+ result = m.mk_eq(z, t.bv.mk_numeral(r, m.get_sort(z)));
+ return true;
+ }
+ else {
+ return false;
+ }
+ }
+
+ br_status mk_app_core(func_decl* f, unsigned sz, expr*const* es, expr_ref& result) {
+ if (m.is_eq(f)) {
+ if (is_fd(es[0], es[1], result)) {
+ return BR_DONE;
+ }
+ else if (is_fd(es[1], es[0], result)) {
+ return BR_DONE;
+ }
+ }
+ return BR_FAILED;
+ }
+
+ 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 mk_app_core(f, num, args, result);
+ }
+ eq_rewriter_cfg(eq2bv_tactic& t):m(t.m), t(t) {}
+ };
+
+ class eq_rewriter : public rewriter_tpl<eq_rewriter_cfg> {
+ eq_rewriter_cfg m_cfg;
+ public:
+ eq_rewriter(eq2bv_tactic& t):
+ rewriter_tpl<eq_rewriter_cfg>(t.m, false, m_cfg),
+ m_cfg(t)
+ {}
+ };
+
+ class bvmc : public model_converter {
+ obj_map<func_decl, func_decl*> m_map;
+ public:
+
+ void insert(func_decl* c_new, func_decl* c_old) {
+ m_map.insert(c_new, c_old);
+ }
+
+ virtual void operator()(model_ref& mdl) {
+ ast_manager& m = mdl->get_manager();
+ bv_util bv(m);
+ arith_util a(m);
+ rational r;
+ model_ref new_m = alloc(model, m);
+ new_m->copy_func_interps(*mdl);
+ new_m->copy_usort_interps(*mdl);
+ unsigned sz = mdl->get_num_constants(), bvsz;
+ for (unsigned i = 0; i < sz; ++i) {
+ func_decl* f = mdl->get_constant(i), *g;
+ expr* val = mdl->get_const_interp(f);
+ if (m_map.find(f, g) && bv.is_numeral(val, r, bvsz)) {
+ val = a.mk_numeral(r, true);
+ new_m->register_decl(g, val);
+ }
+ else {
+ new_m->register_decl(f, val);
+ }
+ }
+ mdl = new_m;
+ }
+
+ virtual model_converter* translate(ast_translation & translator) {
+ bvmc* v = alloc(bvmc);
+ obj_map<func_decl, func_decl*>::iterator it = m_map.begin(), end = m_map.end();
+ for (; it != end; ++it) {
+ v->m_map.insert(translator(it->m_key), translator(it->m_value));
+ }
+ return v;
+ }
+ };
+
+public:
+ ast_manager & m;
+ arith_util a;
+ bv_util bv;
+ eq_rewriter m_rw;
+ expr_ref_vector m_trail;
+ bound_manager m_bounds;
+ obj_map<expr, expr*> m_fd;
+ obj_map<expr, unsigned> m_max;
+ expr_mark m_nonfd;
+ ptr_vector<expr> m_todo;
+
+ eq2bv_tactic(ast_manager & _m):
+ m(_m),
+ a(m),
+ bv(m),
+ m_rw(*this),
+ m_trail(m),
+ m_bounds(m) {
+ }
+
+ virtual ~eq2bv_tactic() {
+ }
+
+ void set_cancel(bool f) {
+ m_rw.set_cancel(f);
+ }
+
+ void updt_params(params_ref const & p) {
+ }
+
+ virtual void operator()(
+ goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
+ SASSERT(g->is_well_sorted());
+ mc = 0; pc = 0; core = 0;
+ m_trail.reset();
+ m_fd.reset();
+ m_max.reset();
+ m_nonfd.reset();
+ m_bounds.reset();
+ ref<bvmc> mc1 = alloc(bvmc);
+
+ tactic_report report("eq2bv", *g);
+
+ m_bounds(*g);
+
+ for (unsigned i = 0; i < g->size(); i++) {
+ collect_fd(g->form(i));
+ }
+ cleanup_fd(mc1);
+
+ if (m_max.empty()) {
+ result.push_back(g.get());
+ return;
+ }
+
+ for (unsigned i = 0; i < g->size(); i++) {
+ expr_ref new_curr(m);
+ proof_ref new_pr(m);
+ if (is_bound(g->form(i))) {
+ g->update(i, m.mk_true(), 0, 0);
+ continue;
+ }
+ m_rw(g->form(i), new_curr, new_pr);
+ if (m.proofs_enabled() && !new_pr) {
+ new_pr = m.mk_rewrite(g->form(i), new_curr);
+ new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
+ }
+ g->update(i, new_curr, new_pr, g->dep(i));
+ }
+ obj_map<expr, unsigned>::iterator it = m_max.begin(), end = m_max.end();
+ for (; it != end; ++it) {
+ expr* c = it->m_key;
+ bool strict;
+ rational r;
+ if (m_bounds.has_lower(c, r, strict)) {
+ SASSERT(!strict);
+ expr* d = m_fd.find(c);
+ g->assert_expr(bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d), m_bounds.lower_dep(c));
+ }
+ if (m_bounds.has_upper(c, r, strict)) {
+ SASSERT(!strict);
+ expr* d = m_fd.find(c);
+ g->assert_expr(bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d))), m_bounds.upper_dep(c));
+ }
+ }
+ g->inc_depth();
+ mc = mc1.get();
+ result.push_back(g.get());
+ TRACE("pb", g->display(tout););
+ SASSERT(g->is_well_sorted());
+ }
+
+
+ virtual tactic * translate(ast_manager & m) {
+ return alloc(eq2bv_tactic, m);
+ }
+
+ virtual void collect_param_descrs(param_descrs & r) {
+ }
+
+ virtual void cleanup() {
+ }
+
+ void cleanup_fd(ref<bvmc>& mc) {
+ SASSERT(m_fd.empty());
+ ptr_vector<expr> rm;
+ obj_map<expr, unsigned>::iterator it = m_max.begin(), end = m_max.end();
+ for (; it != end; ++it) {
+ if (m_nonfd.is_marked(it->m_key)) {
+ rm.push_back(it->m_key);
+ }
+ }
+ for (unsigned i = 0; i < rm.size(); ++i) {
+ m_max.erase(rm[i]);
+ }
+ it = m_max.begin();
+ end = m_max.end();
+ for (; it != end; ++it) {
+ // ensure there are enough elements.
+ bool strict;
+ rational val;
+ if (m_bounds.has_upper(it->m_key, val, strict)) {
+ SASSERT(!strict);
+ if (val.get_unsigned() > it->m_value) it->m_value = val.get_unsigned();
+ }
+ else {
+ ++it->m_value;
+ }
+ unsigned p = next_power_of_two(it->m_value);
+ if (p <= 1) p = 2;
+ unsigned n = log2(p);
+ app* z = m.mk_fresh_const("z", bv.mk_sort(n));
+ m_trail.push_back(z);
+ m_fd.insert(it->m_key, z);
+ mc->insert(z->get_decl(), to_app(it->m_key)->get_decl());
+ }
+ }
+
+ bool is_upper(expr* f) {
+ expr* e1, *e2;
+ rational r;
+ if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) &&
+ is_uninterp_const(e1) && a.is_numeral(e2, r) && r.is_unsigned() && !m_nonfd.is_marked(e1)) {
+ SASSERT(m_bounds.has_upper(e1));
+ return true;
+ }
+ return false;
+ }
+
+ bool is_lower(expr* f) {
+ expr* e1, *e2;
+ rational r;
+ if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) &&
+ is_uninterp_const(e2) && a.is_numeral(e1, r) && r.is_unsigned() && !m_nonfd.is_marked(e2)) {
+ SASSERT(m_bounds.has_lower(e2));
+ return true;
+ }
+ return false;
+ }
+
+ bool is_bound(expr* f) {
+ return is_lower(f) || is_upper(f);
+ }
+
+
+ void collect_fd(expr* f) {
+ if (is_bound(f)) return;
+ m_todo.push_back(f);
+ while (!m_todo.empty()) {
+ f = m_todo.back();
+ m_todo.pop_back();
+ if (m_nonfd.is_marked(f)) {
+ continue;
+ }
+ m_nonfd.mark(f, true);
+ expr* e1, *e2;
+ if (m.is_eq(f, e1, e2)) {
+ if (is_fd(e1, e2)) {
+ continue;
+ }
+ if (is_fd(e2, e1)) {
+ continue;
+ }
+ }
+ m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+ }
+ }
+
+ bool is_fd(expr* v, expr* c) {
+ unsigned val;
+ rational r;
+ if (is_uninterp_const(v) && a.is_numeral(c, r) && !m_nonfd.is_marked(v) && a.is_int(v) && r.is_unsigned()) {
+ val = r.get_unsigned();
+ add_fd(v, val);
+ return true;
+ }
+ return false;
+ }
+
+ void add_fd(expr* c, unsigned val) {
+ unsigned val2;
+ if (!m_max.find(c, val2) || val2 < val) {
+ m_max.insert(c, val);
+ }
+ }
+};
+
+tactic * mk_eq2bv_tactic(ast_manager & m) {
+ return clean(alloc(eq2bv_tactic, m));
+}
+
diff --git a/src/tactic/arith/eq2bv_tactic.h b/src/tactic/arith/eq2bv_tactic.h
new file mode 100644
index 000000000..e336b1e0a
--- /dev/null
+++ b/src/tactic/arith/eq2bv_tactic.h
@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ eq2bv_tactic.h
+
+Abstract:
+
+ Extract integer variables that are used as finite domain indicators.
+ The integer variables can only occur in equalities.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2015-8-19
+
+Notes:
+
+--*/
+#ifndef EQ2BV_TACTIC_H_
+#define EQ2BV_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_eq2bv_tactic(ast_manager & m);
+
+/*
+ ADD_TACTIC("eq2bv", "convert integer variables used as finite domain elements to bit-vectors.", "mk_eq2bv_tactic(m)")
+*/
+
+
+#endif