Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/muz_qe/dl_context.cpp

@@ -45,6 +45,7 @@ Revision History:
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_array_blast.h"
+#include"dl_mk_karr_invariants.h"
 #include"datatype_decl_plugin.h"
 #include"expr_abstract.h"
 
@@ -223,6 +224,7 @@ namespace datalog {
         m_rewriter(m),
         m_var_subst(m),
         m_rule_manager(*this),
+        m_transf(*this),
         m_trail(*this),
         m_pinned(m),
         m_vars(m),
@@ -825,21 +827,21 @@ namespace datalog {
     }
 
     void context::transform_rules(model_converter_ref& mc, proof_converter_ref& pc) {
-        rule_transformer transf(*this);
+        m_transf.reset();
-        transf.register_plugin(alloc(mk_filter_rules,*this));
+        m_transf.register_plugin(alloc(mk_filter_rules,*this));
-        transf.register_plugin(alloc(mk_simple_joins,*this));
+        m_transf.register_plugin(alloc(mk_simple_joins,*this));
 
         if (unbound_compressor()) {
-            transf.register_plugin(alloc(mk_unbound_compressor,*this));
+            m_transf.register_plugin(alloc(mk_unbound_compressor,*this));
         }
 
         if (similarity_compressor()) {
-            transf.register_plugin(alloc(mk_similarity_compressor, *this, 
+            m_transf.register_plugin(alloc(mk_similarity_compressor, *this, 
                                          similarity_compressor_threshold()));
         }
-        transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
+        m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
 
-        transform_rules(transf, mc, pc);
+        transform_rules(m_transf, mc, pc);
     }
     
     void context::transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc) {
@@ -862,32 +864,33 @@ namespace datalog {
 
     void context::apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc) {
         ensure_closed();
-        datalog::rule_transformer transf(*this);
+        m_transf.reset();
-        transf.register_plugin(alloc(datalog::mk_coi_filter, *this));
+        m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this));
-        transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this));
+        m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this));
 
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 35005));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 35005));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 35000));
+        m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 35000));
-        transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34990));
+        m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34990));
-        transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34980));
+        m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34980));
 
         //and another round of inlining
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34975));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34975));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34970));
+        m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34970));
-        transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34960));
+        m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this, 34960));
-        transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34950));
+        m_transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, *this, 34950));
 
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34940));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34940));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34930));
+        m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34930));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34920));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34920));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34910));
+        m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34910));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34900));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34900));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890));
+        m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880));
+        m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880));
 
-        transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
+        m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
-        transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
+        m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
-        transform_rules(transf, mc, pc);
+        m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));
+        transform_rules(m_transf, mc, pc);
     }
 
     void context::collect_params(param_descrs& p) {
@@ -928,6 +931,7 @@ namespace datalog {
 
     void context::cancel() {
         m_cancel = true;
+        m_transf.cancel();
         if (m_pdr.get()) m_pdr->cancel();
         if (m_bmc.get()) m_bmc->cancel();
         if (m_rel.get()) m_rel->cancel();

src/muz_qe/dl_context.h

@@ -45,11 +45,10 @@ Revision History:
 #include"proof_converter.h"
 #include"model2expr.h"
 #include"smt_params.h"
+#include"dl_rule_transformer.h"
 
 namespace datalog {
 
-    class rule_transformer;
-
     enum execution_result {
         OK,
         TIMEOUT,
@@ -85,6 +84,7 @@ namespace datalog {
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
+        rule_transformer   m_transf;
 
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
@@ -314,7 +314,7 @@ namespace datalog {
         void ensure_opened();
 
         void transform_rules(model_converter_ref& mc, proof_converter_ref& pc);
-        void transform_rules(rule_transformer& trans, model_converter_ref& mc, proof_converter_ref& pc);
+        void transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc);
         void replace_rules(rule_set & rs);
 
         void apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc);

src/muz_qe/dl_mk_array_blast.h

@@ -49,7 +49,7 @@ namespace datalog {
 
     public:
         /**
-           \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
+           \brief Create rule transformer that removes array stores and selects by ackermannization.
         */
         mk_array_blast(context & ctx, unsigned priority);
 

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -0,0 +1,612 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_karr_invariants.cpp
+
+Abstract:
+
+    Extract integer linear invariants.
+
+    The linear invariants are extracted according to Karr's method.
+    A short description is in 
+    Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation 
+    of Invariants and Intermediate Assertions, in CP 95.
+
+    The algorithm is here adapted to Horn clauses.
+    The idea is to maintain two data-structures for each recursive relation.
+    We call them R and RD
+    - R  - set of linear congruences that are true of R.
+    - RD - the dual basis of of solutions for R.
+
+    RD is updated by accumulating basis vectors for solutions 
+    to R (the homogeneous dual of R)
+    R is updated from the inhomogeneous dual of RD.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-09
+
+Revision History:
+           
+--*/
+
+#include"dl_mk_karr_invariants.h"
+
+namespace datalog {
+
+    mk_karr_invariants::mk_karr_invariants(context & ctx, unsigned priority):
+        rule_transformer::plugin(priority, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()), 
+        rm(ctx.get_rule_manager()),
+        a(m) {
+    }
+
+    mk_karr_invariants::~mk_karr_invariants() {
+        obj_map<func_decl, matrix*>::iterator it = m_constraints.begin(), end = m_constraints.end();
+        for (; it != end; ++it) {
+            dealloc(it->m_value);
+        }
+        it = m_dual_constraints.begin();
+        end = m_dual_constraints.end();
+        for (; it != end; ++it) {
+            dealloc(it->m_value);
+        }
+    }
+
+    mk_karr_invariants::matrix& mk_karr_invariants::matrix::operator=(matrix const& other) {
+        reset();
+        append(other);
+        return *this;
+    }
+
+    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";
+        }
+    }
+
+    bool mk_karr_invariants::is_linear(expr* e, vector<rational>& row, rational& b, rational const& mul) {
+        if (!a.is_int(e)) {
+            return false;
+        }
+        if (is_var(e)) {
+            row[to_var(e)->get_idx()] += mul;
+            return true;
+        }
+        if (!is_app(e)) {
+            return false;
+        }
+        rational n;
+        if (a.is_numeral(e, n)) {
+            b += mul*n;
+            return true;
+        }
+        if (a.is_add(e)) {
+            for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
+                if (!is_linear(to_app(e)->get_arg(i), row, b, mul)) {
+                    return false;
+                }
+            }
+            return true;
+        }
+        expr* e1, *e2;
+        if (a.is_sub(e, e1, e2)) {
+            return is_linear(e1, row, b, mul) && is_linear(e2, row, b, -mul);
+        }
+        if (a.is_mul(e, e1, e2) && a.is_numeral(e1, n)) {
+            return is_linear(e2, row, b, mul*n);
+        }
+        if (a.is_mul(e, e1, e2) && a.is_numeral(e2, n)) {
+            return is_linear(e1, row, b, mul*n);
+        }
+        if (a.is_uminus(e, e1)) {
+            return is_linear(e1, row, b, -mul);
+        }
+        return false;        
+    }
+
+    mk_karr_invariants::matrix* mk_karr_invariants::get_constraints(func_decl* p) {
+        matrix* result = 0;
+        m_constraints.find(p, result);
+        return result;
+    }
+
+    mk_karr_invariants::matrix& mk_karr_invariants::get_dual_constraints(func_decl* p) {
+        matrix* result = 0;
+        if (!m_dual_constraints.find(p, result)) {
+            result = alloc(matrix);
+            m_dual_constraints.insert(p, result);
+        }
+        return *result;
+    }
+
+    bool mk_karr_invariants::is_eq(expr* e, var*& v, rational& n) {
+        expr* e1, *e2;
+        if (!m.is_eq(e, e1, e2)) {
+            return false;
+        }
+        if (!is_var(e1)) {
+            std::swap(e1, e2);
+        }
+        if (!is_var(e1)) {
+            return false;
+        }
+        v = to_var(e1);
+        if (!a.is_numeral(e2, n)) {
+            return false;
+        }
+        return true;
+    }
+    
+    bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) {
+        unsigned num_vars = rm.get_var_counter().get_max_var(r)+1;
+        unsigned arity = r.get_decl()->get_arity();
+        unsigned num_columns = arity + num_vars;        
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz  = r.get_tail_size();
+        M.reset();
+        
+        for (unsigned i = 0; i < utsz; ++i) {
+            matrix const* Mp = get_constraints(r.get_decl(i));
+            if (!Mp) {
+                return false;
+            }
+            TRACE("dl", Mp->display(tout << "Intersect\n"););
+            intersect_matrix(r.get_tail(i), *Mp, num_columns, M);
+        }
+
+        rational one(1), mone(-1);
+        expr* e1, *e2, *en;
+        var* v, *w;
+        rational n1, n2;
+        expr_ref_vector conjs(m);
+        for (unsigned i = utsz; i < tsz; ++i) {
+            conjs.push_back(r.get_tail(i));
+        }
+        datalog::flatten_and(conjs);
+
+        for (unsigned i = 0; i < conjs.size(); ++i) {
+            expr* e = conjs[i].get();
+            rational b(0);
+            vector<rational> row;
+            row.resize(num_columns, rational(0));
+            bool processed = true;
+            if (m.is_eq(e, e1, e2) && is_linear(e1, row, b, one) && is_linear(e2, row, b, mone)) {
+                M.A.push_back(row);
+                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)) {
+                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)) {
+                M.A.push_back(row);
+                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)) {
+                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)) {
+                M.A.push_back(row);
+                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) {
+                if (n1 > n2) {
+                    std::swap(n1, n2);
+                }
+                SASSERT(n1 <= n2);
+                row[v->get_idx()] = rational(1);
+                // v - n1 >= 0
+                M.A.push_back(row);
+                M.b.push_back(-n1);
+                M.eq.push_back(false);
+                // -v + n2 >= 0
+                row[v->get_idx()] = rational(-1);
+                M.A.push_back(row);
+                M.b.push_back(n2);
+                M.eq.push_back(false);
+            }
+            else {
+                processed = false;
+            }
+            TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";);
+        }
+        // intersect with the head predicate.
+        app* head = r.get_head();
+        unsigned sz0 = M.A.size();
+        for (unsigned i = 0; i < arity; ++i) {
+            rational n;
+            expr* arg = head->get_arg(i);
+            if (!a.is_int(arg)) { 
+                // no-op
+            }
+            else if (is_var(arg)) {
+                vector<rational> row;
+                row.resize(num_columns, rational(0));
+                unsigned idx = to_var(arg)->get_idx();
+                row[idx] = rational(-1);
+                row[num_vars + i] = rational(1);
+                M.A.push_back(row);
+                M.b.push_back(rational(0));
+                M.eq.push_back(true);
+            }
+            else if (a.is_numeral(arg, n)) {
+                vector<rational> row;
+                row.resize(num_columns, rational(0));
+                row[num_vars + i] = rational(1);
+                M.A.push_back(row);
+                M.b.push_back(-n);
+                M.eq.push_back(true);
+            }
+            else {
+                UNREACHABLE();
+            }
+        }
+        if (M.A.size() == sz0) {
+            return false;
+        }
+
+        TRACE("dl", M.display(tout << r.get_decl()->get_name() << "\n"););
+        matrix MD;
+        dualizeI(MD, M);
+        M.reset();
+        // project for variables in head.
+        for (unsigned i = 0; i < MD.size(); ++i) {
+            vector<rational> row;
+            row.append(arity, MD.A[i].c_ptr() + num_vars);
+            M.A.push_back(row);
+            M.b.push_back(MD.b[i]);
+            M.eq.push_back(true);
+        }
+        
+        return true;
+    }
+
+    void mk_karr_invariants::intersect_matrix(app* p, matrix const& Mp, unsigned num_columns, matrix& M) {
+        for (unsigned j = 0; j < Mp.size(); ++j) {
+            rational b = Mp.b[j], n;
+            vector<rational> row;
+            row.resize(num_columns, rational(0));
+            for (unsigned i = 0; i < p->get_num_args(); ++i) {
+                expr* arg = p->get_arg(i);
+                if (!a.is_int(arg)) {
+                    // no-op
+                }
+                else if (is_var(arg)) {
+                    unsigned idx = to_var(arg)->get_idx();
+                    row[idx] += Mp.A[j][i];
+                }
+                else if (a.is_numeral(arg, n)) {
+                    b += Mp.A[j][i]*n;
+                }
+                else {
+                    UNREACHABLE();
+                }
+            }
+            M.A.push_back(row);
+            M.b.push_back(b);
+            M.eq.push_back(Mp.eq[j]);
+        }
+    }
+
+    // treat src as a homogeneous matrix.
+    void mk_karr_invariants::dualizeH(matrix& dst, matrix const& src) {
+        dst.reset();
+        if (src.size() == 0) {
+            return;
+        }
+        m_hb.reset();
+        for (unsigned i = 0; i < src.size(); ++i) {
+            vector<rational> v(src.A[i]);
+            v.append(src.b[i]);
+            if (src.eq[i]) {
+                m_hb.add_eq(v, rational(0));
+            }
+            else {
+                m_hb.add_ge(v, rational(0));
+            }
+        }
+        for (unsigned i = 0; i < 1 + src.A[0].size(); ++i) {
+            m_hb.set_is_int(i);
+        }
+        lbool is_sat = m_hb.saturate();
+        TRACE("dl", m_hb.display(tout););
+        SASSERT(is_sat == l_true);
+        unsigned basis_size = m_hb.get_basis_size();
+        bool first_initial = true;
+        for (unsigned i = 0; i < basis_size; ++i) {
+            bool is_initial;
+            vector<rational> soln;
+            m_hb.get_basis_solution(i, soln, is_initial);
+            if (!is_initial) {
+                dst.b.push_back(soln.back());
+                dst.eq.push_back(true);
+                soln.pop_back();
+                dst.A.push_back(soln);
+            }
+        }
+    }
+
+    // treat src as an inhomegeneous matrix.
+    void mk_karr_invariants::dualizeI(matrix& dst, matrix const& src) {
+        m_hb.reset();
+        for (unsigned i = 0; i < src.size(); ++i) {
+            if (src.eq[i]) {
+                m_hb.add_eq(src.A[i], -src.b[i]);
+            }
+            else {
+                m_hb.add_ge(src.A[i], -src.b[i]);
+            }
+        }
+        for (unsigned i = 0; !src.A.empty() && i < src.A[0].size(); ++i) {
+            m_hb.set_is_int(i);
+        }
+        lbool is_sat = m_hb.saturate();
+        TRACE("dl", m_hb.display(tout););
+        SASSERT(is_sat == l_true);
+        dst.reset();
+        unsigned basis_size = m_hb.get_basis_size();
+        bool first_initial = true;
+        for (unsigned i = 0; i < basis_size; ++i) {
+            bool is_initial;
+            vector<rational> soln;
+            m_hb.get_basis_solution(i, soln, is_initial);
+            if (is_initial && first_initial) {
+                dst.A.push_back(soln);
+                dst.b.push_back(rational(1));
+                dst.eq.push_back(true);
+                first_initial = false;
+            }
+            else if (!is_initial) {
+                dst.A.push_back(soln);
+                dst.b.push_back(rational(0));
+                dst.eq.push_back(true);
+            }
+        }
+    }
+
+    void mk_karr_invariants::update_body(rule_set& rules, rule& r){
+        func_decl* p = r.get_decl();        
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz  = r.get_tail_size();
+        app_ref_vector tail(m);
+        for (unsigned i = 0; i < tsz; ++i) {
+            tail.push_back(r.get_tail(i));
+        }
+        for (unsigned i = 0; i < utsz; ++i) {
+            func_decl* q = r.get_decl(i);            
+            matrix* N = get_constraints(q);
+            if (!N) {
+                continue;
+            }
+            expr_ref zero(m), lhs(m);
+            zero = a.mk_numeral(rational(0), true);
+            for (unsigned j = 0; j < N->size(); ++j) {
+                rational n;
+                SASSERT(N->A[j].size() == q->get_arity());
+                expr_ref_vector sum(m);
+                for (unsigned k = 0; k < N->A[j].size(); ++k) {
+                    n = N->A[j][k];
+                    if (!n.is_zero()) {
+                        expr* arg = r.get_tail(i)->get_arg(k);
+                        sum.push_back(a.mk_mul(a.mk_numeral(n, true), arg));
+                    }
+                }
+                n = N->b[j];
+                if (!n.is_zero()) {
+                    sum.push_back(a.mk_numeral(n, true));
+                }               
+                lhs = a.mk_add(sum.size(), sum.c_ptr());
+                if (N->eq[j]) {
+                    tail.push_back(m.mk_eq(lhs, zero));
+                }
+                else {
+                    tail.push_back(a.mk_ge(lhs, zero));
+                }
+            }            
+        }
+        rule* new_rule = &r;
+        if (tail.size() != tsz) {
+            new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name());
+        }
+        rules.add_rule(new_rule);
+    }
+
+    class mk_karr_invariants::add_invariant_model_converter : public model_converter {
+        ast_manager&          m;
+        arith_util            a;
+        func_decl_ref_vector  m_funcs;
+        ptr_vector<matrix>    m_invs;
+    public:
+        
+        add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m) {}
+
+        virtual ~add_invariant_model_converter() {
+            for (unsigned i = 0; i < m_invs.size(); ++i) {
+                dealloc(m_invs[i]);
+            }
+        }
+
+        void add(func_decl* p, matrix& M) {
+            m_funcs.push_back(p);
+            m_invs.push_back(alloc(matrix, M));
+        }
+
+        virtual void operator()(model_ref & mr) {
+            for (unsigned i = 0; i < m_funcs.size(); ++i) {
+                func_decl* p = m_funcs[i].get();
+                func_interp* f = mr->get_func_interp(p);
+                expr_ref body(m);                
+                unsigned arity = p->get_arity();
+                SASSERT(0 < arity);
+                if (f) {
+                    matrix const& M = *m_invs[i];
+                    mk_body(M, body);
+                    SASSERT(f->num_entries() == 0);
+                    if (!f->is_partial()) {
+                        body = m.mk_and(f->get_else(), body);
+                    }
+                }
+                else {
+                    f = alloc(func_interp, m, arity);
+                    mr->register_decl(p, f);
+                    body = m.mk_false();  // fragile: assume that relation was pruned by being infeasible.
+                }
+                f->set_else(body);
+            }            
+        }
+    
+        virtual model_converter * translate(ast_translation & translator) {
+            add_invariant_model_converter* mc = alloc(add_invariant_model_converter, m);
+            for (unsigned i = 0; i < m_funcs.size(); ++i) {
+                mc->add(translator(m_funcs[i].get()), *m_invs[i]);
+            }
+            return mc;
+        }
+
+    private:
+        void mk_body(matrix const& M, expr_ref& body) {
+            expr_ref_vector conj(m);
+            for (unsigned i = 0; i < M.size(); ++i) {
+                mk_body(M.A[i], M.b[i], M.eq[i], conj);
+            }
+            body = m.mk_and(conj.size(), conj.c_ptr());
+        }
+
+        void mk_body(vector<rational> const& row, rational const& b, bool is_eq, expr_ref_vector& conj) {
+            expr_ref_vector sum(m);
+            expr_ref zero(m), lhs(m);
+            zero = a.mk_numeral(rational(0), true);
+
+            for (unsigned i = 0; i < row.size(); ++i) {
+                if (row[i].is_zero()) {
+                    continue;
+                }
+                var* var = m.mk_var(i, a.mk_int());
+                if (row[i].is_one()) {
+                    sum.push_back(var);
+                }
+                else {
+                    sum.push_back(a.mk_mul(a.mk_numeral(row[i], true), var));
+                }
+            }
+            if (!b.is_zero()) {
+                sum.push_back(a.mk_numeral(b, true));
+            }
+            lhs = a.mk_add(sum.size(), sum.c_ptr());
+            if (is_eq) {
+                conj.push_back(m.mk_eq(lhs, zero));
+            }
+            else {
+                conj.push_back(a.mk_ge(lhs, zero));
+            }
+        }
+
+    };
+
+    void mk_karr_invariants::cancel() {
+        rule_transformer::plugin::cancel();
+        m_hb.set_cancel(true);
+    }
+    
+    rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+        if (!m_ctx.get_params().karr()) {
+            return 0;
+        }
+        rule_set::iterator it = source.begin(), end = source.end();
+        for (; it != end; ++it) {
+            rule const& r = **it;
+            if (r.has_negation()) {
+                return 0;
+            }
+        }
+        bool change = true, non_empty = false;
+        while (!m_cancel && change) {
+            change = false;
+            it = source.begin();            
+            for (; it != end; ++it) {
+                rule const& r = **it;
+                TRACE("dl", r.display(m_ctx, tout););
+                matrix MD, P;
+                if (!get_transition_relation(r, MD)) {
+                    continue;
+                }
+                non_empty = true;
+                func_decl* p = r.get_decl();
+                matrix& ND = get_dual_constraints(p);
+                matrix* N  = get_constraints(p);
+                ND.append(MD);
+                dualizeH(P, ND);
+
+                TRACE("dl",
+                           MD.display(tout << "MD\n");
+                           P.display(tout << "P\n"););
+
+                if (!N) {
+                    change = true;
+                    N = alloc(matrix, P);
+                    m_constraints.insert(p, N);
+                }
+                else if (P.size() != N->size()) {
+                    change = true;
+                    *N = P;
+                }
+            }
+        }
+
+        if (!non_empty) {
+            return 0;
+        }
+
+        if (m_cancel) {
+            return 0;
+        }
+
+        TRACE("dl",
+                   rule_set::decl2rules::iterator git  = source.begin_grouped_rules();
+                   rule_set::decl2rules::iterator gend = source.end_grouped_rules();
+                   for (; git != gend; ++git) {
+                       func_decl* p = git->m_key;
+                       matrix* M = get_constraints(p);
+                       tout << p->get_name() << "\n";
+                       if (M) {
+                           M->display(tout);
+                       }
+                   });
+        
+        rule_set* rules = alloc(rule_set, m_ctx);
+        it = source.begin();            
+        for (; it != end; ++it) {
+            update_body(*rules, **it);
+        }
+        if (mc) {
+            add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m);
+            rule_set::decl2rules::iterator git  = source.begin_grouped_rules();
+            rule_set::decl2rules::iterator gend = source.end_grouped_rules();
+            for (; git != gend; ++git) {
+                func_decl* p = git->m_key;
+                matrix* M = get_constraints(p);
+                if (M) {
+                    kmc->add(p, *M);
+                }
+            }
+            mc = concat(mc.get(), kmc);
+        }
+        TRACE("dl", rules->display(tout););
+        return rules;
+    }
+
+};
+

src/muz_qe/dl_mk_karr_invariants.h

@@ -0,0 +1,79 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_karr_invariants.h
+
+Abstract:
+
+    Extract integer linear invariants.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-08
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_KARR_INVARIANTS_H_
+#define _DL_MK_KARR_INVARIANTS_H_
+
+#include"dl_context.h"
+#include"dl_rule_set.h"
+#include"dl_rule_transformer.h"
+#include"arith_decl_plugin.h"
+#include"hilbert_basis.h"
+
+namespace datalog {
+
+    /**
+       \brief Rule transformer that strengthens bodies with invariants.
+    */
+    class mk_karr_invariants : public rule_transformer::plugin {
+
+        struct matrix {
+            vector<vector<rational> > A;
+            vector<rational>          b;
+            svector<bool>             eq;
+            unsigned size() const { return A.size(); }
+            void reset() { A.reset(); b.reset(); eq.reset(); }
+            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;
+        };
+        class add_invariant_model_converter;
+
+        context&        m_ctx;
+        ast_manager&    m;
+        rule_manager&   rm;
+        arith_util      a;
+        obj_map<func_decl, matrix*> m_constraints;
+        obj_map<func_decl, matrix*> m_dual_constraints;
+        hilbert_basis   m_hb;
+
+        bool is_linear(expr* e, vector<rational>& row, rational& b, rational const& mul);
+        bool is_eq(expr* e, var*& v, rational& n);
+        bool get_transition_relation(rule const& r, matrix& M);
+        void intersect_matrix(app* p, matrix const& Mp, unsigned num_columns, matrix& M);
+        matrix* get_constraints(func_decl* p);   
+        matrix& get_dual_constraints(func_decl* p);     
+        void dualizeH(matrix& dst, matrix const& src);
+        void dualizeI(matrix& dst, matrix const& src);
+        void update_body(rule_set& rules, rule& r);
+
+    public:
+        mk_karr_invariants(context & ctx, unsigned priority);
+
+        virtual ~mk_karr_invariants();
+
+        virtual void cancel(); 
+        
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+
+    };
+
+};
+
+#endif /* _DL_MK_KARR_INVARIANTS_H_ */
+

src/muz_qe/dl_rule.cpp

@@ -927,6 +927,15 @@ namespace datalog {
         return exist || univ;
     }
 
+    bool rule::has_negation() const {
+        for (unsigned i = 0; i < get_uninterpreted_tail_size(); ++i) {
+            if (is_neg_tail(i)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
     void rule::get_used_vars(used_vars& used) const {
         used.process(get_head());
         unsigned sz = get_tail_size();

src/muz_qe/dl_rule.h

@@ -237,6 +237,7 @@ namespace datalog {
         bool has_uninterpreted_non_predicates(func_decl*& f) const;
         void has_quantifiers(bool& existential, bool& universal) const;
         bool has_quantifiers() const;
+        bool has_negation() const;
 
         /**
            \brief Store in d the (direct) dependencies of the given rule.

src/muz_qe/dl_rule_transformer.cpp

@@ -16,40 +16,55 @@ Author:
 Revision History:
 
 --*/
+
 #include <algorithm>
 #include<typeinfo>
 
 #include"dl_context.h"
-
 #include"dl_rule_transformer.h"
 
 namespace datalog {
 
     rule_transformer::rule_transformer(context & ctx) 
-        : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false) {
+        : m_context(ctx), m_rule_manager(m_context.get_rule_manager()), m_dirty(false), m_cancel(false) {
     }
 
 
     rule_transformer::~rule_transformer() {
-        plugin_vector::iterator it=m_plugins.begin();
+        reset();
-        plugin_vector::iterator end=m_plugins.end();
+    }
+
+    void rule_transformer::reset() {
+        plugin_vector::iterator it = m_plugins.begin();
+        plugin_vector::iterator end = m_plugins.end();
         for(; it!=end; ++it) {
             dealloc(*it);
         }
+        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) {
+            (*it)->cancel();
+        }
     }
 
     struct rule_transformer::plugin_comparator {
         bool operator()(rule_transformer::plugin * p1, rule_transformer::plugin * p2) {
-            return p1->get_priority()>p2->get_priority();
+            return p1->get_priority() > p2->get_priority();
         }
     };
 
     void rule_transformer::ensure_ordered() {
-        if (!m_dirty) {
+        if (m_dirty) {
-            return;
-        }
             std::sort(m_plugins.begin(), m_plugins.end(), plugin_comparator());
-        m_dirty=false;
+            m_dirty = false;
+        }
     }
 
     void rule_transformer::register_plugin(plugin * p) {
@@ -67,9 +82,9 @@ namespace datalog {
             tout<<"init:\n";
             rules.display(tout);
         );
-        plugin_vector::iterator it=m_plugins.begin();
+        plugin_vector::iterator it = m_plugins.begin();
-        plugin_vector::iterator end=m_plugins.end();
+        plugin_vector::iterator end = m_plugins.end();
-        for(; it!=end; ++it) {
+        for(; it!=end && !m_cancel; ++it) {
             plugin & p = **it;
 
             rule_set * new_rules = p(rules, mc, pc);

src/muz_qe/dl_rule_transformer.h

@@ -28,6 +28,8 @@ Revision History:
 
 namespace datalog {
 
+    class context;
+
     class rule_transformer {
     public:
         class plugin;
@@ -40,6 +42,7 @@ namespace datalog {
         context &        m_context;
         rule_manager &   m_rule_manager;
         bool             m_dirty;
+        volatile bool    m_cancel;
         svector<plugin*> m_plugins;
         
         void ensure_ordered();
@@ -48,6 +51,13 @@ namespace datalog {
         rule_transformer(context & ctx);
         ~rule_transformer();
 
+        /**
+           \brief Reset all registered transformers.
+         */
+        void reset();
+
+        void cancel();
+        
         /**
            \brief Add a plugin for rule transformation.
 
@@ -72,6 +82,8 @@ namespace datalog {
         void attach(rule_transformer & transformer) { m_transformer = &transformer; }
 
     protected:
+        volatile bool m_cancel;
+
         /**
            \brief Create a plugin object for rule_transformer.
 
@@ -79,7 +91,8 @@ 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_can_destratify_negation(can_destratify_negation), m_transformer(0), m_cancel(false) {}
+
     public:
         virtual ~plugin() {}
 
@@ -96,6 +109,8 @@ namespace datalog {
                                       model_converter_ref& mc,
                                       proof_converter_ref& pc) = 0;
 
+        virtual void cancel() { m_cancel = true; }
+
         /**
            Removes duplicate tails.
         */

src/muz_qe/fixedpoint_params.pyg

@@ -41,6 +41,7 @@ def_module_params('fixedpoint',
                           ('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"),
                           ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
                           ('slice', BOOL, True, "PDR: simplify clause set using slicing"),
+	                  ('karr',  BOOL, False, "Add linear invariants to clauses using Karr's method"),
                           ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),

src/muz_qe/hilbert_basis.cpp

@@ -686,6 +686,7 @@ void hilbert_basis::reset() {
     m_passive2->reset();
     m_zero.reset();
     m_index->reset();
+    m_ints.reset();
     m_cancel = false;
 }
 

src/muz_qe/pdr_context.cpp

@@ -1425,6 +1425,7 @@ namespace pdr {
             bool ok = checker.check(pr, side_conditions);
             if (!ok) {
                 msg << "proof validation failed";
+                IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
                 throw default_exception(msg.str());
             }
             for (unsigned i = 0; i < side_conditions.size(); ++i) {
@@ -1437,6 +1438,7 @@ namespace pdr {
                 lbool res = solver.check();
                 if (res != l_false) {
                     msg << "rule validation failed when checking: " << mk_pp(cond, m);
+                    IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
                     throw default_exception(msg.str());
                 }                                
             }
@@ -1488,6 +1490,7 @@ namespace pdr {
                     lbool res = solver.check();
                     if (res != l_false) {
                         msg << "rule validation failed when checking: " << mk_pp(tmp, m);
+                        IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
                         throw default_exception(msg.str());
                     }
                 }
@@ -1595,6 +1598,7 @@ namespace pdr {
         catch (unknown_exception) {
             return l_undef;
         }
+        UNREACHABLE();
         return l_undef;
     }
 

src/muz_qe/pdr_util.cpp

@@ -32,7 +32,6 @@ Notes:
 #include "for_each_expr.h"
 #include "smt_params.h"
 #include "model.h"
-#include "model_v2_pp.h"
 #include "ref_vector.h"
 #include "rewriter.h"
 #include "rewriter_def.h"
@@ -42,6 +41,7 @@ Notes:
 #include "pdr_util.h"
 #include "arith_decl_plugin.h"
 #include "expr_replacer.h"
+#include "model_smt2_pp.h"
 
 
 namespace pdr {
@@ -511,12 +511,23 @@ namespace pdr {
         }
     }
 
+    void model_evaluator::eval_exprs(expr_ref_vector& es) {
+        model_ref mr(m_model);
+        for (unsigned j = 0; j < es.size(); ++j) {
+            if (m_array.is_as_array(es[j].get())) {
+                es[j] = eval(mr, es[j].get());
+            }
+        }
+    }
+    
     bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
         SASSERT(m_array.is_array(a));
         
+        TRACE("pdr", tout << mk_pp(a, m) << "\n";);
         while (m_array.is_store(a)) {
             expr_ref_vector store(m);
             store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
+            eval_exprs(store);
             stores.push_back(store);
             a = to_app(a)->get_arg(0);
         }
@@ -526,7 +537,7 @@ namespace pdr {
             return true;
         }
         
-        if (m_array.is_as_array(a)) {
+        while (m_array.is_as_array(a)) {
             func_decl* f = m_array.get_as_array_func_decl(to_app(a));
             func_interp* g = m_model->get_func_interp(f);
             unsigned sz = g->num_entries();
@@ -538,20 +549,30 @@ namespace pdr {
                 store.push_back(fe->get_result());
                 for (unsigned j = 0; j < store.size(); ++j) {
                     if (!is_ground(store[j].get())) {
+                        TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
                         return false;
                     }
                 }
+                eval_exprs(store);
                 stores.push_back(store);
             }        
             else_case = g->get_else();
             if (!else_case) {
+                TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";);
                 return false;
             }
             if (!is_ground(else_case)) {
+                TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";);
                 return false;
             }
+            if (m_array.is_as_array(else_case)) {
+                model_ref mr(m_model);
+                else_case = eval(mr, else_case);
+            }
+            TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";);
             return true;
         }
+        TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";);
         
         return false;
     }
@@ -570,7 +591,8 @@ namespace pdr {
         }
         sort* s = m.get_sort(arg1);
         sort* r = get_array_range(s);
-        if (!r->is_infinite() && !r->is_very_big()) {
+        // give up evaluating finite domain/range arrays
+        if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) {
             TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
             set_x(e);
             return;
@@ -591,6 +613,9 @@ namespace pdr {
                       << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
                 set_false(e);
             }
+            else if (m_array.is_array(else1)) {
+                eval_array_eq(e, else1, else2);
+            }
             else {
                 TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
                 set_x(e);
@@ -614,18 +639,23 @@ namespace pdr {
             if (w1 == w2) {
                 continue;
             }
-            else if (m.is_value(w1) && m.is_value(w2)) {
+            if (m.is_value(w1) && m.is_value(w2)) {
                 TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n"; 
                       tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
                       tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
                 set_false(e);
-                return;
+            }
+            else if (m_array.is_array(w1)) {
+                eval_array_eq(e, w1, w2);
+                if (is_true(e)) {
+                    continue;
+                }
             }
             else {
                 TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
                 set_x(e);
-                return;
             }
+            return;
         }
         set_true(e);
     }
@@ -869,6 +899,7 @@ namespace pdr {
             }
             if (is_x(form)) {
                 IF_VERBOSE(0, verbose_stream() << "formula undetermined in model: " << mk_pp(form, m) << "\n";);
+                TRACE("pdr", model_smt2_pp(tout, m, *m_model, 0);); 
                 has_x = true;
             }
         }

src/muz_qe/pdr_util.h

@@ -105,6 +105,8 @@ namespace pdr {
 
         bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
 
+        void eval_exprs(expr_ref_vector& es);
+        
     public:
         model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}