diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index 048269c5a..adf08662a 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -30,7 +30,8 @@ namespace datalog {
m(ctx.get_manager()),
a(m),
rm(ctx.get_rule_manager()),
- m_rewriter(m, m_params){
+ m_rewriter(m, m_params),
+ m_simplifier(ctx) {
m_params.set_bool("expand_select_store",true);
m_rewriter.updt_params(m_params);
}
@@ -202,9 +203,11 @@ namespace datalog {
SASSERT(new_rules.size() == 1);
TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
-
- rules.add_rule(new_rules[0].get());
- rm.mk_rule_rewrite_proof(r, *new_rules[0].get());
+ rule_ref new_rule(rm);
+ if (m_simplifier.transform_rule(new_rules[0].get(), new_rule)) {
+ rules.add_rule(new_rule.get());
+ rm.mk_rule_rewrite_proof(r, *new_rule.get());
+ }
return true;
}
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 94eb64601..4680821a2 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -22,6 +22,7 @@ Revision History:
#include"dl_context.h"
#include"dl_rule_set.h"
#include"dl_rule_transformer.h"
+#include"dl_mk_interp_tail_simplifier.h"
#include "equiv_proof_converter.h"
#include "array_decl_plugin.h"
@@ -37,6 +38,7 @@ namespace datalog {
rule_manager& rm;
params_ref m_params;
th_rewriter m_rewriter;
+ mk_interp_tail_simplifier m_simplifier;
typedef obj_map<app, var*> defs_t;
diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp
index 338eed0b4..9dfd9deba 100644
--- a/src/muz_qe/dl_mk_bit_blast.cpp
+++ b/src/muz_qe/dl_mk_bit_blast.cpp
@@ -223,7 +223,9 @@ namespace datalog {
expr_ref fml1(m), fml2(m), fml3(m);
rule_ref r2(m_context.get_rule_manager());
// We need to simplify rule before bit-blasting.
- m_simplifier.transform_rule(r, r2);
+ if (!m_simplifier.transform_rule(r, r2)) {
+ r2 = r;
+ }
r2->to_formula(fml1);
m_blaster(fml1, fml2, pr);
m_rewriter(fml2, fml3);
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
index a48b7b32f..35fd630f9 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
@@ -469,7 +469,7 @@ namespace datalog {
start:
unsigned u_len = r->get_uninterpreted_tail_size();
unsigned len = r->get_tail_size();
- if (u_len==len) {
+ if (u_len == len) {
res = r;
return true;
}
@@ -504,34 +504,29 @@ namespace datalog {
expr_ref simp_res(m);
simplify_expr(itail.get(), simp_res);
- modified |= itail.get()!=simp_res.get();
-
- if (is_app(simp_res.get())) {
- itail = to_app(simp_res.get());
- }
- else if (m.is_bool(simp_res)) {
- itail = m.mk_eq(simp_res, m.mk_true());
- }
- else {
- throw default_exception("simplification resulted in non-boolean non-function");
- }
-
- if (m.is_false(itail.get())) {
- //the tail member is never true, so we may delete the rule
+ modified |= itail.get() != simp_res.get();
+
+ if (m.is_false(simp_res)) {
TRACE("dl", r->display(m_context, tout << "rule is infeasible\n"););
return false;
}
- if (!m.is_true(itail.get())) {
- //if the simplified tail is not a tautology, we add it to the rule
- tail.push_back(itail);
- tail_neg.push_back(false);
- }
- else {
- modified = true;
- }
+ SASSERT(m.is_bool(simp_res));
- SASSERT(tail.size() == tail_neg.size());
if (modified) {
+ expr_ref_vector conjs(m);
+ flatten_and(simp_res, conjs);
+ for (unsigned i = 0; i < conjs.size(); ++i) {
+ expr* e = conjs[i].get();
+ if (is_app(e)) {
+ tail.push_back(to_app(e));
+ }
+ else {
+ tail.push_back(m.mk_eq(e, m.mk_true()));
+ }
+ tail_neg.push_back(false);
+ }
+
+ SASSERT(tail.size() == tail_neg.size());
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
res->set_accounting_parent_object(m_context, r);
}
diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp
index d44b31979..013923045 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz_qe/dl_mk_karr_invariants.cpp
@@ -62,12 +62,38 @@ namespace datalog {
return *this;
}
+ void mk_karr_invariants::matrix::display_row(
+ std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq) {
+ for (unsigned j = 0; j < row.size(); ++j) {
+ out << row[j] << " ";
+ }
+ out << (is_eq?" = ":" >= ") << -b << "\n";
+ }
+
+ void mk_karr_invariants::matrix::display_ineq(
+ std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq) {
+ bool first = true;
+ for (unsigned j = 0; j < row.size(); ++j) {
+ if (!row[j].is_zero()) {
+ if (!first && row[j].is_pos()) {
+ out << "+ ";
+ }
+ if (row[j].is_minus_one()) {
+ out << "- ";
+ }
+ if (row[j] > rational(1) || row[j] < rational(-1)) {
+ out << row[j] << "*";
+ }
+ out << "x" << j << " ";
+ first = false;
+ }
+ }
+ out << (is_eq?"= ":">= ") << -b << "\n";
+ }
+
void mk_karr_invariants::matrix::display(std::ostream& out) const {
for (unsigned i = 0; i < A.size(); ++i) {
- for (unsigned j = 0; j < A[i].size(); ++j) {
- out << A[i][j] << " ";
- }
- out << (eq[i]?" = ":" >= ") << -b[i] << "\n";
+ display_row(out, A[i], b[i], eq[i]);
}
}
@@ -182,24 +208,28 @@ namespace datalog {
M.b.push_back(b);
M.eq.push_back(true);
}
- else if ((a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
+ else if ((a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) &&
+ is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
M.A.push_back(row);
M.b.push_back(b);
M.eq.push_back(false);
}
- else if ((a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
+ else if ((a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) &&
+ is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
M.A.push_back(row);
- M.b.push_back(b + rational(1));
+ M.b.push_back(b - rational(1));
M.eq.push_back(false);
}
- else if (m.is_not(e, en) && (a.is_lt(en, e2, e1) || a.is_gt(en, e1, e2)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
+ else if (m.is_not(e, en) && (a.is_lt(en, e2, e1) || a.is_gt(en, e1, e2)) &&
+ is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
M.A.push_back(row);
M.b.push_back(b);
M.eq.push_back(false);
}
- else if (m.is_not(e, en) && (a.is_le(en, e2, e1) || a.is_ge(en, e1, e2)) && is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
+ else if (m.is_not(e, en) && (a.is_le(en, e2, e1) || a.is_ge(en, e1, e2)) &&
+ is_linear(e1, row, b, mone) && is_linear(e2, row, b, one)) {
M.A.push_back(row);
- M.b.push_back(b + rational(1));
+ M.b.push_back(b - rational(1));
M.eq.push_back(false);
}
else if (m.is_or(e, e1, e2) && is_eq(e1, v, n1) && is_eq(e2, w, n2) && v == w) {
@@ -221,7 +251,9 @@ namespace datalog {
else {
processed = false;
}
- TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";);
+ TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";
+ if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back());
+ );
}
// intersect with the head predicate.
app* head = r.get_head();
@@ -270,6 +302,7 @@ namespace datalog {
M.b.push_back(MD.b[i]);
M.eq.push_back(true);
}
+ TRACE("dl", M.display(tout << r.get_decl()->get_name() << "\n"););
return true;
}
@@ -322,7 +355,7 @@ namespace datalog {
m_hb.set_is_int(i);
}
lbool is_sat = m_hb.saturate();
- TRACE("dl", m_hb.display(tout););
+ TRACE("dl_verbose", m_hb.display(tout););
SASSERT(is_sat == l_true);
unsigned basis_size = m_hb.get_basis_size();
for (unsigned i = 0; i < basis_size; ++i) {
@@ -353,7 +386,7 @@ namespace datalog {
m_hb.set_is_int(i);
}
lbool is_sat = m_hb.saturate();
- TRACE("dl", m_hb.display(tout););
+ TRACE("dl_verbose", m_hb.display(tout););
SASSERT(is_sat == l_true);
dst.reset();
unsigned basis_size = m_hb.get_basis_size();
@@ -532,7 +565,7 @@ namespace datalog {
}
}
bool change = true, non_empty = false;
- while (!m_cancel && change) {
+ while (!m_ctx.canceled() && change) {
change = false;
it = source.begin();
for (; it != end; ++it) {
@@ -550,8 +583,8 @@ namespace datalog {
dualizeH(P, ND);
TRACE("dl",
- MD.display(tout << "MD\n");
- P.display(tout << "P\n"););
+ ND.display(tout << "ND\n");
+ P.display(tout << "P\n"););
if (!N) {
change = true;
@@ -569,7 +602,7 @@ namespace datalog {
return 0;
}
- if (m_cancel) {
+ if (m_ctx.canceled()) {
return 0;
}
diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h
index 7cd26d495..d70fb374b 100644
--- a/src/muz_qe/dl_mk_karr_invariants.h
+++ b/src/muz_qe/dl_mk_karr_invariants.h
@@ -41,6 +41,10 @@ namespace datalog {
matrix& operator=(matrix const& other);
void append(matrix const& other) { A.append(other.A); b.append(other.b); eq.append(other.eq); }
void display(std::ostream& out) const;
+ static void display_row(
+ std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq);
+ static void display_ineq(
+ std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq);
};
class add_invariant_model_converter;
@@ -67,7 +71,7 @@ namespace datalog {
virtual ~mk_karr_invariants();
- virtual void cancel();
+ virtual void cancel();
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
diff --git a/src/muz_qe/dl_rule_set.h b/src/muz_qe/dl_rule_set.h
index fdbbf7626..3079c6072 100644
--- a/src/muz_qe/dl_rule_set.h
+++ b/src/muz_qe/dl_rule_set.h
@@ -46,7 +46,7 @@ namespace datalog {
ast_mark m_visited;
- //we need to take care with removing to aviod memory leaks
+ //we need to take care with removing to avoid memory leaks
void remove_m_data_entry(func_decl * key);
//sometimes we need to return reference to an empty set,
diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp
index 5ecbf2b45..7e0e951e1 100644
--- a/src/muz_qe/dl_rule_transformer.cpp
+++ b/src/muz_qe/dl_rule_transformer.cpp
@@ -26,7 +26,7 @@ Revision History:
namespace datalog {
rule_transformer::rule_transformer(context & ctx)
- : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false), m_cancel(false) {
+ : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false) {
}
@@ -42,11 +42,9 @@ namespace datalog {
}
m_plugins.reset();
m_dirty = false;
- m_cancel = false;
}
void rule_transformer::cancel() {
- m_cancel = true;
plugin_vector::iterator it = m_plugins.begin();
plugin_vector::iterator end = m_plugins.end();
for(; it!=end; ++it) {
@@ -84,7 +82,7 @@ namespace datalog {
);
plugin_vector::iterator it = m_plugins.begin();
plugin_vector::iterator end = m_plugins.end();
- for(; it!=end && !m_cancel; ++it) {
+ for(; it!=end && !m_context.canceled(); ++it) {
plugin & p = **it;
rule_set * new_rules = p(rules, mc);
diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h
index 3b2140caf..87ff10fb0 100644
--- a/src/muz_qe/dl_rule_transformer.h
+++ b/src/muz_qe/dl_rule_transformer.h
@@ -41,7 +41,6 @@ namespace datalog {
context & m_context;
rule_manager & m_rule_manager;
bool m_dirty;
- volatile bool m_cancel;
svector<plugin*> m_plugins;
void ensure_ordered();
@@ -81,7 +80,6 @@ namespace datalog {
void attach(rule_transformer & transformer) { m_transformer = &transformer; }
protected:
- volatile bool m_cancel;
/**
\brief Create a plugin object for rule_transformer.
@@ -90,7 +88,7 @@ namespace datalog {
(higher priority plugins will be applied first).
*/
plugin(unsigned priority, bool can_destratify_negation = false) : m_priority(priority),
- m_can_destratify_negation(can_destratify_negation), m_transformer(0), m_cancel(false) {}
+ m_can_destratify_negation(can_destratify_negation), m_transformer(0) {}
public:
virtual ~plugin() {}
@@ -98,6 +96,8 @@ namespace datalog {
unsigned get_priority() { return m_priority; }
bool can_destratify_negation() const { return m_can_destratify_negation; }
+ virtual void cancel() {}
+
/**
\brief Return \c rule_set object with containing transformed rules or 0 if no
transformation was done.
@@ -107,8 +107,6 @@ namespace datalog {
virtual rule_set * operator()(rule_set const & source,
model_converter_ref& mc) = 0;
- virtual void cancel() { m_cancel = true; }
-
/**
Removes duplicate tails.
*/
diff --git a/src/muz_qe/fdd.cpp b/src/muz_qe/fdd.cpp
index afb5206cc..6c3bc0974 100644
--- a/src/muz_qe/fdd.cpp
+++ b/src/muz_qe/fdd.cpp
@@ -97,14 +97,14 @@ node_id manager::mk_node(unsigned var, node_id lo, node_id hi) {
inc_ref(hi);
}
- TRACE("mtdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";);
+ TRACE("fdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";);
return result;
}
void manager::inc_ref(node_id n) {
- TRACE("mtdd", tout << "incref: " << n << "\n";);
+ TRACE("fdd", tout << "incref: " << n << "\n";);
if (!is_leaf(n)) {
m_nodes[n].inc_ref();
}
@@ -126,6 +126,7 @@ void manager::setup_keys(Key const* keys) {
void manager::insert(Key const* keys) {
setup_keys(keys);
+ m_insert_cache.reset();
node_id result = insert_sign(m_num_idx + m_num_keys, m_root);
inc_ref(result);
dec_ref(m_root);
@@ -161,7 +162,7 @@ node_id manager::insert_sign(unsigned idx, node_id n) {
node_id manager::insert(unsigned idx, node_id n) {
node_id result;
SASSERT(0 <= idx && idx <= m_num_idx);
- TRACE("mtdd", tout << "insert: " << idx << " " << n << "\n";);
+ TRACE("fdd", tout << "insert: " << idx << " " << n << "\n";);
if (is_leaf(n)) {
while (idx > 0) {
--idx;
@@ -176,9 +177,8 @@ node_id manager::insert(unsigned idx, node_id n) {
--idx;
config c(m_dont_cares, idx, n);
- insert_cache::key_data & kd = m_insert_cache.insert_if_not_there2(c, 0)->get_data();
- if (kd.m_value != 0) {
- return kd.m_value;
+ if (m_insert_cache.find(c, result)) {
+ return result;
}
node nd = m_nodes[n];
@@ -209,7 +209,7 @@ node_id manager::insert(unsigned idx, node_id n) {
}
result = mk_node(idx, lo, hi);
}
- kd.m_value = result;
+ m_insert_cache.insert(c, result);
return result;
}
@@ -263,11 +263,12 @@ bool manager::find_le(Key const* keys) {
SASSERT(idx > 0);
--idx;
while (nc.var() < idx) {
- if (idx2bit(idx)) {
+ if (idx2bit(idx) && is_dont_care(idx2key(idx))) {
set_dont_care(idx2key(idx));
}
--idx;
}
+ SASSERT(nc.var() == idx);
if (is_dont_care(idx2key(idx)) || idx2bit(idx)) {
n = nc.hi();
}
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index 221e9a706..69b8765a7 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -290,7 +290,7 @@ public:
}
void display(std::ostream& out) const {
- // m_fdd.display(out);
+ m_fdd.display(out);
}
@@ -302,8 +302,8 @@ class hilbert_basis::index {
// for positive weights a shared value index.
// typedef value_index1 value_index;
- // typedef value_index2 value_index;
- typedef value_index3 value_index;
+ typedef value_index2 value_index;
+ // typedef value_index3 value_index;
struct stats {
unsigned m_num_find;
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index a5f554e5e..2f58cc3c8 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -514,6 +514,15 @@ static void tst16() {
saturate_basis(hb);
}
+static void tst17() {
+ hilbert_basis hb;
+ hb.add_eq(vec(1, 0), R(0));
+ hb.add_eq(vec(-1, 0), R(0));
+ hb.add_eq(vec(0, 2), R(0));
+ hb.add_eq(vec(0, -2), R(0));
+ saturate_basis(hb);
+
+}
void tst_hilbert_basis() {
std::cout << "hilbert basis test\n";
@@ -522,6 +531,9 @@ void tst_hilbert_basis() {
g_use_ordered_support = true;
+ tst17();
+ return;
+
if (true) {
tst1();
tst2();
diff --git a/src/test/karr.cpp b/src/test/karr.cpp
index 3ac427a88..8770eac94 100644
--- a/src/test/karr.cpp
+++ b/src/test/karr.cpp
@@ -165,6 +165,28 @@ namespace karr {
return v;
}
+ static vector<rational> V(int i, int j, int k, int l, int m) {
+ vector<rational> v;
+ v.push_back(rational(i));
+ v.push_back(rational(j));
+ v.push_back(rational(k));
+ v.push_back(rational(l));
+ v.push_back(rational(m));
+ return v;
+ }
+
+ static vector<rational> V(int i, int j, int k, int l, int x, int y, int z) {
+ vector<rational> v;
+ v.push_back(rational(i));
+ v.push_back(rational(j));
+ v.push_back(rational(k));
+ v.push_back(rational(l));
+ v.push_back(rational(x));
+ v.push_back(rational(y));
+ v.push_back(rational(z));
+ return v;
+ }
+
#define R(_x_) rational(_x_)
@@ -206,8 +228,66 @@ namespace karr {
e2.display(std::cout << "e2\n");
}
+ void tst2() {
+ /**
+ 0 0 0 0 0 0 0 = 0
+ 0 0 0 0 0 0 0 = 0
+ 0 0 0 0 0 0 0 = 0
+ 0 0 0 0 0 0 0 = 0
+ 0 0 0 0 1 0 0 = 0
+ 0 0 0 0 -1 0 0 = 0
+ 0 1 0 0 0 0 0 = 0
+ 0 -1 0 0 0 0 0 = 0
+ 0 0 0 2 0 0 0 = 0
+ 0 0 0 -2 0 0 0 = 0
+ */
+
+ matrix ND;
+ ND.A.push_back(V(0,0,0,0,1,0,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,0,0,0,-1,0,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,1,0,0,0,0,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,-1,0,0,0,0,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,0,0,2,0,0,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,0,0,-2,0,0,0)); ND.b.push_back(R(0));
+
+ ND.display(std::cout << "ND\n");
+
+ matrix N;
+ dualizeH(N, ND);
+
+ N.display(std::cout << "N\n");
+
+
+ }
+
+ void tst3() {
+ /**
+ 0 0 0 0 1 0 0 = 0
+ 0 0 0 0 -1 0 0 = 0
+ 0 1 0 0 0 0 0 = 0
+ 0 -1 0 0 0 0 0 = 0
+ 0 0 0 2 0 0 0 = 0
+ 0 0 0 -2 0 0 0 = 0
+ */
+
+ matrix ND;
+ ND.A.push_back(V(1,0)); ND.b.push_back(R(0));
+ ND.A.push_back(V(0,2)); ND.b.push_back(R(0));
+
+ ND.display(std::cout << "ND\n");
+
+ matrix N;
+ dualizeH(N, ND);
+
+ N.display(std::cout << "N\n");
+
+
+ }
+
};
void tst_karr() {
+ karr::tst3();
+ return;
karr::tst1();
}