add loop counter v1

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

src/muz_qe/dl_mk_bit_blast.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    <abstract>
+    Functor for bit-blasting a rule set
 
 Author:
 
@@ -19,31 +19,16 @@ Revision History:
 #ifndef _DL_MK_BIT_BLAST_H_
 #define _DL_MK_BIT_BLAST_H_
 
-#include<utility>
-
-#include"map.h"
-#include"obj_pair_hashtable.h"
-#include"dl_context.h"
-#include"dl_rule_set.h"
 #include"dl_rule_transformer.h"
 
 namespace datalog {
 
-    /**
-       \brief Functor for bit-blasting a rule set.
-    */
-
     class mk_bit_blast : public rule_transformer::plugin {
         class impl;
-
-        impl*            m_impl;
-        void blast(expr_ref& b);
-        void reset();
-
+        impl* m_impl;
     public:
         mk_bit_blast(context & ctx, unsigned priority = 35000);
-        ~mk_bit_blast();
-        
+        ~mk_bit_blast();        
         rule_set * operator()(rule_set const & source);
     };
 

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -204,7 +204,7 @@ namespace datalog {
         m_inner_ctx.ensure_opened();
         it = source.begin();
         for (; it != end; ++it) {
-            rule_ref r(*it, m_ctx.get_rule_manager());
+            rule_ref r(*it, m_inner_ctx.get_rule_manager());
             m_inner_ctx.add_rule(r);
             m_inner_ctx.register_predicate(r->get_decl());
         }

src/muz_qe/dl_mk_loop_counter.cpp

@@ -0,0 +1,104 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_loop_counter.cpp
+
+Abstract:
+
+    Add loop counter argument to relations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-31
+
+Revision History:
+
+--*/
+
+#include"dl_mk_loop_counter.h"
+#include"dl_context.h"
+
+namespace datalog {
+
+    mk_loop_counter::mk_loop_counter(context & ctx, unsigned priority):
+        plugin(priority) {        
+    }
+
+    mk_loop_counter::~mk_loop_counter() { }
+
+    app_ref mk_loop_counter::add_arg(ast_manager& m, app* fn, unsigned idx) {
+        arith_util a(m);
+        ptr_vector<sort> domain;
+        expr_ref_vector args(m);
+        domain.append(fn->get_num_args(), fn->get_decl()->get_domain());
+        domain.push_back(a.mk_int());
+        args.append(fn->get_num_args(), fn->get_args());
+        args.push_back(m.mk_var(idx, a.mk_int()));
+        func_decl_ref new_fn(m);
+        new_fn = m.mk_func_decl(fn->get_decl()->get_name(), domain.size(), domain.c_ptr(), m.mk_bool_sort());
+        return app_ref(m.mk_app(new_fn, args.size(), args.c_ptr()), m);
+    }
+        
+    rule_set * mk_loop_counter::operator()(rule_set const & source) {
+        context& ctx = source.get_context();
+        ast_manager& m = source.get_manager();
+        rule_manager& rm = source.get_rule_manager();
+        arith_util a(m);
+        rule_set * result = alloc(rule_set, ctx);
+        unsigned sz = source.get_num_rules();
+        rule_ref new_rule(rm);
+        app_ref_vector tail(m);
+        app_ref head(m);
+        svector<bool> neg;
+        rule_counter& vc = rm.get_counter();
+        for (unsigned i = 0; i < sz; ++i) {            
+            tail.reset();
+            neg.reset();
+            rule & r = *source.get_rule(i);
+            unsigned cnt = vc.get_max_rule_var(r)+1;
+            unsigned utsz = r.get_uninterpreted_tail_size();
+            unsigned tsz = r.get_tail_size();
+            for (unsigned j = 0; j < utsz; ++j, ++cnt) {
+                tail.push_back(add_arg(m, r.get_tail(j), cnt));                
+                neg.push_back(r.is_neg_tail(j));
+                ctx.register_predicate(tail.back()->get_decl());
+            }
+            for (unsigned j = utsz; j < tsz; ++j) {
+                tail.push_back(r.get_tail(j));
+                neg.push_back(false);
+            }
+            head = add_arg(m, r.get_head(), cnt);
+            ctx.register_predicate(head->get_decl());
+            // set the loop counter to be an increment of the previous 
+            bool found = false;
+            unsigned last = head->get_num_args()-1;
+            for (unsigned j = 0; !found && j < utsz; ++j) {
+                if (head->get_decl() == tail[j]->get_decl()) {
+                    tail.push_back(m.mk_eq(head->get_arg(last), 
+                                           a.mk_add(tail[j]->get_arg(last),
+                                                    a.mk_numeral(rational(1), true))));
+                    neg.push_back(false);
+                    found = true;
+                }
+            }
+            // initialize loop counter to 0 if none was found.
+            if (!found) {
+                expr_ref_vector args(m);
+                args.append(head->get_num_args(), head->get_args());
+                args[last] = a.mk_numeral(rational(0), true);
+                head = m.mk_app(head->get_decl(), args.size(), args.c_ptr());
+            }            
+
+            new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
+            result->add_rule(new_rule);
+        }
+
+        // model converter: remove references to extra argument.
+        // proof converter: etc.
+
+        return result;
+    }
+
+};

src/muz_qe/dl_mk_loop_counter.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_loop_counter.h
+
+Abstract:
+
+    Add loop counter argument to relations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-31
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_LOOP_COUNTER_H_
+#define _DL_MK_LOOP_COUNTER_H_
+
+#include"dl_rule_transformer.h"
+
+namespace datalog {
+
+    class mk_loop_counter : public rule_transformer::plugin {
+        app_ref add_arg(ast_manager& m, app* fn, unsigned idx);        
+    public:
+        mk_loop_counter(context & ctx, unsigned priority = 33000);
+        ~mk_loop_counter();
+        
+        rule_set * operator()(rule_set const & source);
+    };
+
+};
+
+#endif /* _DL_MK_LOOP_COUNTER_H_ */
+