fix parameters in utvpi and make Karr invariants use backward propagation

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

src/muz_qe/dl_compiler.cpp

@@ -499,8 +499,7 @@ namespace datalog {
                 expr * arg = a->get_arg(i);
                 if(is_app(arg)) {
                     app * c = to_app(arg); //argument is a constant
-                    SASSERT(c->get_num_args()==0);
+                    SASSERT(m.is_value(c));
-                    SASSERT(m_context.get_decl_util().is_numeral_ext(arg));
                     reg_idx new_reg;
                     make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc);
                     if(single_res!=t_reg) {

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -37,6 +37,7 @@ Revision History:
 #include"bool_rewriter.h"
 #include"dl_mk_backwards.h"
 #include"dl_mk_loop_counter.h"
+#include "for_each_expr.h"
 
 namespace datalog {
 
@@ -47,7 +48,8 @@ namespace datalog {
         m(ctx.get_manager()), 
         rm(ctx.get_rule_manager()),
         m_inner_ctx(m, ctx.get_fparams()),
-        a(m) {
+        a(m),
+        m_pinned(m) {
             params_ref params;
             params.set_sym("default_relation", symbol("karr_relation"));
             params.set_sym("engine", symbol("datalog"));
@@ -201,29 +203,27 @@ namespace datalog {
                 return 0;
             }
         }
-
         mk_loop_counter lc(m_ctx);
         mk_backwards bwd(m_ctx);
 
         scoped_ptr<rule_set> src_loop = lc(source);
         TRACE("dl", src_loop->display(tout << "source loop\n"););
 
-        // run propagation forwards, then backwards
+        get_invariants(*src_loop);
-        scoped_ptr<rule_set> src_annot = update_using_propagation(*src_loop, *src_loop);
-        TRACE("dl", src_annot->display(tout << "updated using propagation\n"););
 
-#if 0
         // figure out whether to update same rules as used for saturation.
-        scoped_ptr<rule_set> rev_source = bwd(*src_annot);
+        scoped_ptr<rule_set> rev_source = bwd(*src_loop);
-        src_annot = update_using_propagation(*src_annot, *rev_source);
+        get_invariants(*rev_source);        
-#endif
+        scoped_ptr<rule_set> src_annot = update_rules(*src_loop);
         rule_set* rules = lc.revert(*src_annot);
         rules->inherit_predicates(source);
         TRACE("dl", rules->display(tout););
+        m_pinned.reset();
+        m_fun2inv.reset();
         return rules;
     }
 
-    rule_set* mk_karr_invariants::update_using_propagation(rule_set const& src, rule_set const& srcref) {
+    void mk_karr_invariants::get_invariants(rule_set const& src) {
         m_inner_ctx.reset();
         rel_context& rctx = m_inner_ctx.get_rel_context();
         ptr_vector<func_decl> heads;
@@ -232,19 +232,41 @@ namespace datalog {
             m_inner_ctx.register_predicate(*fit, false);
         }
         m_inner_ctx.ensure_opened();
-        m_inner_ctx.replace_rules(srcref);
+        m_inner_ctx.replace_rules(src);
         m_inner_ctx.close();
-        rule_set::decl2rules::iterator dit  = srcref.begin_grouped_rules();
+        rule_set::decl2rules::iterator dit  = src.begin_grouped_rules();
-        rule_set::decl2rules::iterator dend = srcref.end_grouped_rules();
+        rule_set::decl2rules::iterator dend = src.end_grouped_rules();
         for (; dit != dend; ++dit) {
             heads.push_back(dit->m_key);
         }
         m_inner_ctx.rel_query(heads.size(), heads.c_ptr());
 
-        rule_set* dst = alloc(rule_set, m_ctx);
+        // retrieve invariants.
+        dit = src.begin_grouped_rules();
+        for (; dit != dend; ++dit) {
+            func_decl* p = dit->m_key;
+            relation_base* rb = rctx.try_get_relation(p);
+            if (rb) {
+                expr_ref fml(m);
+                rb->to_formula(fml);                
+                if (m.is_true(fml)) {
+                    continue;
+                }
+                expr* inv = 0;
+                if (m_fun2inv.find(p, inv)) {
+                    fml = m.mk_and(inv, fml);
+                }
+                m_pinned.push_back(fml);
+                m_fun2inv.insert(p, fml);
+            }
+        }
+    }        
+
+    rule_set* mk_karr_invariants::update_rules(rule_set const& src) {
+        scoped_ptr<rule_set> dst = alloc(rule_set, m_ctx);
         rule_set::iterator it = src.begin(), end = src.end();
         for (; it != end; ++it) {
-            update_body(rctx, *dst, **it);
+            update_body(*dst, **it);
         }
         if (m_ctx.get_model_converter()) {
             add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m);
@@ -252,10 +274,8 @@ namespace datalog {
             rule_set::decl2rules::iterator gend = src.end_grouped_rules();
             for (; git != gend; ++git) {
                 func_decl* p = git->m_key;
-                expr_ref fml(m);
+                expr* fml = 0;
-                relation_base* rb = rctx.try_get_relation(p);
+                if (m_fun2inv.find(p, fml)) {
-                if (rb) {
-                    rb->to_formula(fml);
                     kmc->add(p, fml);                    
                 }
             }
@@ -263,10 +283,10 @@ namespace datalog {
         }
 
         dst->inherit_predicates(src);
-        return dst;
+        return dst.detach();
     }
 
-    void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) { 
+    void mk_karr_invariants::update_body(rule_set& rules, rule& r) { 
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz  = r.get_tail_size();
         app_ref_vector tail(m);
@@ -276,16 +296,16 @@ namespace datalog {
         }
         for (unsigned i = 0; i < utsz; ++i) {
             func_decl* q = r.get_decl(i); 
-            relation_base* rb = rctx.try_get_relation(r.get_decl(i));
+            expr* fml = 0;
-            if (rb) {
+            if (m_fun2inv.find(q, fml)) {
-                rb->to_formula(fml);
                 expr_safe_replace rep(m);
                 for (unsigned j = 0; j < q->get_arity(); ++j) {
                     rep.insert(m.mk_var(j, q->get_domain(j)), 
                                r.get_tail(i)->get_arg(j));
                 }
-                rep(fml);
+                expr_ref tmp(fml, m);
-                tail.push_back(to_app(fml));
+                rep(tmp);
+                tail.push_back(to_app(tmp));
             }
         }
         rule* new_rule = &r;
@@ -1029,16 +1049,17 @@ namespace datalog {
     class karr_relation_plugin::filter_equal_fn : public relation_mutator_fn {
         unsigned m_col;
         rational m_value;
+        bool    m_valid;
     public:
         filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col) 
             : m_col(col) {
             arith_util arith(m.get_context().get_manager());
-            VERIFY(arith.is_numeral(value, m_value));            
+            m_valid = arith.is_numeral(value, m_value) && m_value.is_int();
         }
 
         virtual void operator()(relation_base & _r) {
             karr_relation & r = get(_r);
-            if (m_value.is_int()) {
+            if (m_valid) {
                 r.get_ineqs();
                 vector<rational> row;
                 row.resize(r.get_signature().size());
@@ -1054,7 +1075,7 @@ namespace datalog {
 
     relation_mutator_fn * karr_relation_plugin::mk_filter_equal_fn(const relation_base & r, 
         const relation_element & value, unsigned col) {
-        if(check_kind(r)) {
+        if (check_kind(r)) {
             return alloc(filter_equal_fn, get_manager(), value, col);
         }
         return 0;

src/muz_qe/dl_mk_karr_invariants.h

@@ -55,8 +55,13 @@ namespace datalog {
         rule_manager&   rm;
         context         m_inner_ctx;
         arith_util      a;
-        void update_body(rel_context& rctx, rule_set& result, rule& r);
+        obj_map<func_decl, expr*>      m_fun2inv;
-        rule_set* update_using_propagation(rule_set const& src, rule_set const& srcref);
+        ast_ref_vector m_pinned;
+
+        void get_invariants(rule_set const& src);
+
+        void update_body(rule_set& result, rule& r);
+        rule_set* update_rules(rule_set const& src);
     public:
         mk_karr_invariants(context & ctx, unsigned priority);
 
@@ -89,13 +94,8 @@ namespace datalog {
         {}            
         
         virtual bool can_handle_signature(const relation_signature & sig) {
-            for (unsigned i = 0; i < sig.size(); ++i) {
-                if (a.is_int(sig[i])) {
             return true;
         }
-            }
-            return false;
-        }
 
         static symbol get_name() { return symbol("karr_relation"); }
 

src/muz_qe/dl_product_relation.cpp

@@ -269,7 +269,7 @@ namespace datalog {
             unsigned_vector r1_tables_indexes;
             unsigned_vector r2_tables_indexes;
             for (unsigned i = 0; i < num_rels1; ++i) {
-                if(is_tableish_relation(*r1[i])) {
+                if (is_tableish_relation(*r1[i])) {
                     r1_tables_indexes.push_back(i);
                     continue;
                 }
@@ -291,7 +291,7 @@ namespace datalog {
                 if (!found) {
                     relation_plugin & r1_plugin = get_nonsieve_plugin(*r1[i]);
                     relation_base* rel2;
-                    if(r1_plugin.can_handle_signature(r2_sig)) {
+                    if (r1_plugin.can_handle_signature(r2_sig)) {
                         rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind);
                     }
                     else {
@@ -307,7 +307,7 @@ namespace datalog {
                 }
             }
             for (unsigned i = 0; i < num_rels2; ++i) {
-                if(is_tableish_relation(*r2[i])) {
+                if (is_tableish_relation(*r2[i])) {
                     r2_tables_indexes.push_back(i);
                     continue;
                 }
@@ -315,7 +315,7 @@ namespace datalog {
                     relation_plugin & r2_plugin = get_nonsieve_plugin(*r2[i]);
                     family_id r2_kind = get_nonsieve_kind(*r2[i]);
                     relation_base* rel1;
-                    if(r2_plugin.can_handle_signature(r1_sig)) {
+                    if (r2_plugin.can_handle_signature(r1_sig)) {
                         rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind);
                     }
                     else {
@@ -331,7 +331,7 @@ namespace datalog {
                 }
             }
 
-            if(!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) {
+            if (!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) {
                 //We may perhaps want to group the table relations by kinds so that tables of the same kind
                 //get joined...
 

src/muz_qe/dl_sieve_relation.cpp

@@ -246,7 +246,8 @@ namespace datalog {
 
     relation_base * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {
         relation_signature empty_sig;
-        relation_base * inner = get_manager().mk_full_relation(empty_sig, p, null_family_id);
+        relation_plugin& plugin = get_manager().get_appropriate_plugin(s);
+        relation_base * inner = plugin.mk_full(p, empty_sig, null_family_id);
         svector<bool> inner_cols;
         inner_cols.resize(s.size(), false);
         return mk_from_inner(s, inner_cols, inner);

src/smt/theory_utvpi.h

@@ -65,7 +65,7 @@ namespace smt {
         class parent_trail;
 
         struct GExt : public Ext {
-            typedef literal explanation;
+            typedef std::pair<literal,unsigned> explanation;
         };
 
         class atom {
@@ -113,15 +113,18 @@ namespace smt {
         // a negative cycle.
         class nc_functor {
             literal_vector m_antecedents;
+            unsigned_vector m_coeffs;
             theory_utvpi& m_super;
         public:
             nc_functor(theory_utvpi& s) : m_super(s) {}
-            void reset() { m_antecedents.reset(); }
+            void reset() { m_antecedents.reset(); m_coeffs.reset(); }
             literal_vector const& get_lits() const { return m_antecedents; }
+            unsigned_vector const& get_coeffs() const { return m_coeffs; }
 
-            void operator()(literal const & ex) {
+            void operator()(std::pair<literal,unsigned> const & ex) {
-                if (ex != null_literal) {
+                if (ex.first != null_literal) {
-                    m_antecedents.push_back(ex);
+                    m_antecedents.push_back(ex.first);
+                    m_coeffs.push_back(ex.second);
                 }
             }
 

src/smt/theory_utvpi_def.h

@@ -197,6 +197,15 @@ namespace smt {
         inc_conflicts();
         literal_vector const& lits = m_nc_functor.get_lits();
         context & ctx = get_context();
+        IF_VERBOSE(2, 
+                   verbose_stream() << "conflict:\n";
+                   for (unsigned i = 0; i < lits.size(); ++i) {
+                       ast_manager& m = get_manager();
+                       expr_ref e(m);
+                       ctx.literal2expr(lits[i], e);
+                       verbose_stream() << mk_pp(e, m) << "\n";
+                   }
+                   verbose_stream() << "\n";);                   
         TRACE("utvpi", 
               tout << "conflict: ";
               for (unsigned i = 0; i < lits.size(); ++i) {
@@ -213,7 +222,9 @@ namespace smt {
         vector<parameter> params;
         if (get_manager().proofs_enabled()) {
             params.push_back(parameter(symbol("farkas")));
-            params.resize(lits.size()+1, parameter(rational(1)));
+            for (unsigned i = 0; i < m_nc_functor.get_coeffs().size(); ++i) {
+                params.push_back(parameter(rational(m_nc_functor.get_coeffs()[i])));
+            }
         } 
         
         ctx.set_conflict(
@@ -620,28 +631,28 @@ namespace smt {
         edge_id id = m_graph.get_num_edges();
         th_var w1 = to_var(v1), w2 = to_var(v2);
         if (terms.size() == 1 && pos1) {
-            m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l);
+            m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));
-            m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l);
+            m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));
         }
         else if (terms.size() == 1 && !pos1) {
-            m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l);
+            m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2));
-            m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l);
+            m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2));
         }
         else if (pos1 && pos2) {
-            m_graph.add_edge(neg(w2), pos(w1), -weight, l);
+            m_graph.add_edge(neg(w2), pos(w1), -weight, std::make_pair(l,1));
-            m_graph.add_edge(neg(w1), pos(w2), -weight, l);
+            m_graph.add_edge(neg(w1), pos(w2), -weight, std::make_pair(l,1));
         }
         else if (pos1 && !pos2) {
-            m_graph.add_edge(pos(w2), pos(w1), -weight, l);
+            m_graph.add_edge(pos(w2), pos(w1), -weight, std::make_pair(l,1));
-            m_graph.add_edge(neg(w1), neg(w2), -weight, l);
+            m_graph.add_edge(neg(w1), neg(w2), -weight, std::make_pair(l,1));
         }
         else if (!pos1 && pos2) {
-            m_graph.add_edge(neg(w2), neg(w1), -weight, l);
+            m_graph.add_edge(neg(w2), neg(w1), -weight, std::make_pair(l,1));
-            m_graph.add_edge(pos(w1), pos(w2), -weight, l);
+            m_graph.add_edge(pos(w1), pos(w2), -weight, std::make_pair(l,1));
         }
         else {
-            m_graph.add_edge(pos(w1), neg(w2), -weight, l);
+            m_graph.add_edge(pos(w1), neg(w2), -weight, std::make_pair(l,1));
-            m_graph.add_edge(pos(w2), neg(w1), -weight, l);
+            m_graph.add_edge(pos(w2), neg(w1), -weight, std::make_pair(l,1));
         }        
         return id;
     }