debugging karr invariants

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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"););
-        
+        rule_ref new_rule(rm);
-        rules.add_rule(new_rules[0].get());
+        if (m_simplifier.transform_rule(new_rules[0].get(), new_rule)) {
-        rm.mk_rule_rewrite_proof(r, *new_rules[0].get());
+            rules.add_rule(new_rule.get());
+            rm.mk_rule_rewrite_proof(r, *new_rule.get());
+        }
         return true;
     }
     

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;
 

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);

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();
+        modified |= itail.get() != simp_res.get();
-
+        
-        if (is_app(simp_res.get())) {
+        if (m.is_false(simp_res)) {
-            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
             TRACE("dl", r->display(m_context, tout << "rule is infeasible\n"););
             return false;
         }
-        if (!m.is_true(itail.get())) {
+        SASSERT(m.is_bool(simp_res));
-            //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(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);
         }

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) {
+            display_row(out, A[i], b[i], eq[i]);
-                out << A[i][j] << " ";
-            }
-            out << (eq[i]?" = ":" >= ") << -b[i] << "\n";
         }
     }
 
@@ -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");
+                      ND.display(tout << "ND\n");
-                           P.display(tout << "P\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;
         }
 

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);
 

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,

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);

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.
         */

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 (m_insert_cache.find(c, result)) {
-    if (kd.m_value != 0) {
+        return result;
-        return kd.m_value;
     }
 
     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();
         }

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_index2 value_index;
-    typedef value_index3 value_index;
+    // typedef value_index3 value_index;
 
     struct stats {
         unsigned m_num_find;

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();

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();
 }