adding model convertion to quantifier transformation

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

src/api/api_datalog.cpp

@@ -358,7 +358,7 @@ extern "C" {
             v->m_ast_vector.push_back(coll.m_queries[i].get());
         }
         for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
-            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get());
+            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get(), true);
         }
         for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
             to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
@@ -415,7 +415,7 @@ extern "C" {
     void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f) {
         Z3_TRY;
         LOG_Z3_fixedpoint_register_relation(c, d, f);
-        to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f));
+        to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f), true);
         Z3_CATCH;
     }
 

src/muz_qe/datalog_parser.cpp

@@ -441,6 +441,7 @@ protected:
     unsigned          m_sym_idx;
     std::string       m_path;
     str2sort          m_sort_dict;
+
     
     // true if an error occured during the current call to the parse_stream
     // function
@@ -812,7 +813,8 @@ protected:
             }
             f = m_manager.mk_func_decl(s, domain.size(), domain.c_ptr(), m_manager.mk_bool_sort());
 
-            m_context.register_predicate(f);
+            m_context.register_predicate(f, true);
+        
             while (tok == TK_ID) {
                 char const* pred_pragma = m_lexer->get_token_data();
                 if(strcmp(pred_pragma, "printtuples")==0 || strcmp(pred_pragma, "outputtuples")==0) {

src/muz_qe/dl_cmds.cpp

@@ -229,6 +229,7 @@ public:
                 status = dlctx.query(m_target);
             }
             catch (z3_error & ex) {
+                ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
                 throw ex;
             }
             catch (z3_exception& ex) {

src/muz_qe/dl_context.cpp

@@ -302,14 +302,6 @@ namespace datalog {
         return m_preds.contains(pred);
     }
 
-    func_decl * context::try_get_predicate_decl(symbol pred_name) const {
-        func_decl * res;
-        if (!m_preds_by_name.find(pred_name, res)) {
-            return 0;
-        }
-        return res;
-    }
-
     void context::register_variable(func_decl* var) {
         m_vars.push_back(m.mk_const(var));
     }
@@ -361,7 +353,6 @@ namespace datalog {
         m_pinned.push_back(decl);
         m_preds.insert(decl);
         if (named) {
-            SASSERT(!m_preds_by_name.contains(decl->get_name()));
             m_preds_by_name.insert(decl->get_name(), decl);
         }
     }
@@ -448,7 +439,7 @@ namespace datalog {
         func_decl* new_pred = 
             m.mk_fresh_func_decl(prefix, suffix, arity, domain, m.mk_bool_sort());
 
-        register_predicate(new_pred);
+        register_predicate(new_pred, true);
 
         if (m_rel.get()) {
             m_rel->inherit_predicate_kind(new_pred, orig_pred);

src/muz_qe/dl_context.h

@@ -183,18 +183,22 @@ namespace datalog {
            retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced
            e.g. by rule transformations do not need to be named.
          */
-        void register_predicate(func_decl * pred, bool named = true);
+        void register_predicate(func_decl * pred, bool named);
 
         bool is_predicate(func_decl * pred) const;
-        
+
         /**
            \brief If a predicate name has a \c func_decl object assigned, return pointer to it;
            otherwise return 0.
-
+           
            Not all \c func_decl object used as relation identifiers need to be assigned to their
            names. Generally, the names coming from the parses are registered here.
-         */
+        */
-        func_decl * try_get_predicate_decl(symbol pred_name) const;
+        func_decl * try_get_predicate_decl(symbol const& pred_name) const {
+            func_decl * res = 0;
+            m_preds_by_name.find(pred_name, res);
+            return res;
+        }        
 
         /**
            \brief Create a fresh head predicate declaration.

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -206,7 +206,7 @@ namespace datalog {
         for (; it != end; ++it) {
             rule_ref r(*it, m_inner_ctx.get_rule_manager());
             m_inner_ctx.add_rule(r);
-            m_inner_ctx.register_predicate(r->get_decl());
+            m_inner_ctx.register_predicate(r->get_decl(), false);
         }
         m_inner_ctx.close();
         rule_set::decl2rules::iterator dit  = source.begin_grouped_rules();

src/muz_qe/dl_mk_loop_counter.cpp

@@ -72,14 +72,14 @@ namespace datalog {
             for (unsigned j = 0; j < utsz; ++j, ++cnt) {
                 tail.push_back(add_arg(r.get_tail(j), cnt));                
                 neg.push_back(r.is_neg_tail(j));
-                ctx.register_predicate(tail.back()->get_decl());
+                ctx.register_predicate(tail.back()->get_decl(), false);
             }
             for (unsigned j = utsz; j < tsz; ++j) {
                 tail.push_back(r.get_tail(j));
                 neg.push_back(false);
             }
             head = add_arg(r.get_head(), cnt);
-            ctx.register_predicate(head->get_decl());
+            ctx.register_predicate(head->get_decl(), false);
             // set the loop counter to be an increment of the previous 
             bool found = false;
             unsigned last = head->get_num_args()-1;

src/muz_qe/dl_mk_quantifier_abstraction.cpp

@@ -21,9 +21,110 @@ Revision History:
 
 #include "dl_mk_quantifier_abstraction.h"
 #include "dl_context.h"
+#include "expr_safe_replace.h"
+#include "expr_abstract.h"
 
 namespace datalog {
 
+
+    // model converter: 
+    // Given model for P^(x, y, i, a[i])
+    // create model: P(x,y,a) == forall i . P^(x,y,i,a[i])
+    // requires substitution and list of bound variables.
+
+    class mk_quantifier_abstraction::qa_model_converter : public model_converter {
+        ast_manager&            m;
+        func_decl_ref_vector    m_old_funcs;
+        func_decl_ref_vector    m_new_funcs;
+        vector<expr_ref_vector> m_subst;
+        vector<svector<bool> >  m_bound;
+
+    public:
+
+        qa_model_converter(ast_manager& m):
+            m(m), m_old_funcs(m), m_new_funcs(m) {}
+
+        virtual ~qa_model_converter() {}
+
+        virtual model_converter * translate(ast_translation & translator) { 
+            return alloc(qa_model_converter, m);
+        }
+
+        void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, svector<bool> const& bound) {
+            m_old_funcs.push_back(old_p);
+            m_new_funcs.push_back(new_p);
+            m_subst.push_back(sub);
+            m_bound.push_back(bound);
+        }
+
+        virtual void operator()(model_ref & model) {
+            for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
+                func_decl* p = m_new_funcs[i].get();
+                func_decl* q = m_old_funcs[i].get();
+                expr_ref_vector const& s = m_subst[i];
+                svector<bool> const& is_bound  = m_bound[i];
+                func_interp* f = model->get_func_interp(p);
+                expr_ref body(m);                
+                unsigned arity_p = p->get_arity();
+                unsigned arity_q = q->get_arity();
+                SASSERT(0 < arity_p);
+                model->register_decl(p, f);
+                func_interp* g = alloc(func_interp, m, arity_q);
+
+                if (f) {
+                    body = f->get_interp();
+                    SASSERT(!f->is_partial());
+                    SASSERT(body);                    
+                }
+                else {
+                    body = m.mk_false();  
+                }
+                // TBD. create quantifier wrapper around body.
+
+                // 1. replace variables by the compound terms from 
+                //    the original predicate.
+                expr_safe_replace sub(m);
+                for (unsigned i = 0; i < s.size(); ++i) {
+                    sub.insert(m.mk_var(i, m.get_sort(s[i])), s[i]);
+                }
+                sub(body);
+                sub.reset();
+
+                // 2. replace bound variables by constants.
+                expr_ref_vector consts(m), bound(m), free(m);
+                ptr_vector<sort> sorts;
+                svector<symbol> names;
+                for (unsigned i = 0; i < q->get_arity(); ++i) {
+                    sort* s = q->get_domain(i);
+                    consts.push_back(m.mk_fresh_const("C", s));
+                    sub.insert(m.mk_var(i, s), consts.back());
+                    if (is_bound[i]) {
+                        bound.push_back(consts.back());
+                        names.push_back(symbol(i));
+                        sorts.push_back(s);
+                    }
+                    else {
+                        free.push_back(consts.back());
+                    }
+                }
+                sub(body);                
+                sub.reset();
+
+                // 3. abstract and quantify those variables that should be bound.
+                expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body);
+                body = m.mk_forall(names.size(), sorts.c_ptr(), names.c_ptr(), body);
+
+                // 4. replace remaining constants by variables.                                
+                for (unsigned i = 0; i < free.size(); ++i) {
+                    sub.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get())));
+                }
+                sub(body);                
+                g->set_else(body);
+                model->register_decl(q, g);
+            }  
+        }                        
+    };
+
     mk_quantifier_abstraction::mk_quantifier_abstraction(
         context & ctx, unsigned priority):
         plugin(priority),
@@ -33,8 +134,7 @@ namespace datalog {
         m_refs(m) {        
     }
 
-    mk_quantifier_abstraction::~mk_quantifier_abstraction() {
+    mk_quantifier_abstraction::~mk_quantifier_abstraction() {        
-        
     }
 
     func_decl* mk_quantifier_abstraction::declare_pred(func_decl* old_p) {
@@ -52,22 +152,41 @@ namespace datalog {
 
         func_decl* new_p = 0;
         if (!m_old2new.find(old_p, new_p)) {
+            expr_ref_vector sub(m);
+            svector<bool> bound;
             sort_ref_vector domain(m);
+            expr_ref arg(m);
             for (unsigned i = 0; i < sz; ++i) {
                 sort* s = old_p->get_domain(i);
+                unsigned lookahead = 0;
+                sort* s0 = s;
+                while (a.is_array(s0)) {
+                    lookahead += get_array_arity(s0);
+                    s0 = get_array_range(s0);
+                }
+                arg = m.mk_var(bound.size() + lookahead, s);
                 while (a.is_array(s)) {
                     unsigned arity = get_array_arity(s);
+                    expr_ref_vector args(m);
                     for (unsigned j = 0; j < arity; ++j) {
                         domain.push_back(get_array_domain(s, j));
+                        args.push_back(m.mk_var(bound.size(), domain.back()));
+                        bound.push_back(true);
                     }
+                    arg = mk_select(arg, args.size(), args.c_ptr());
                     s = get_array_range(s);
                 }
                 domain.push_back(s);
+                bound.push_back(false);
+                sub.push_back(arg);
             }          
             SASSERT(old_p->get_range() == m.mk_bool_sort());
             new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range());
             m_refs.push_back(new_p);
-            m_ctx.register_predicate(new_p);
+            m_ctx.register_predicate(new_p, false);
+            if (m_mc) {
+                m_mc->insert(old_p, new_p, sub, bound);
+            }
         }
         return new_p;
     }
@@ -88,10 +207,7 @@ namespace datalog {
                 for (unsigned j = 0; j < arity; ++j) {
                     args.push_back(m.mk_var(idx++, get_array_domain(s, j)));
                 }
-                ptr_vector<expr> args2;
+                arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity);
-                args2.push_back(arg);
-                args2.append(arity, args.c_ptr()-arity);
-                arg = a.mk_select(args2.size(), args2.c_ptr());
                 s = get_array_range(s);
             }
             args.push_back(arg);
@@ -130,10 +246,7 @@ namespace datalog {
                     names.push_back(symbol(idx));
                     args.push_back(m.mk_var(idx++, vars.back()));
                 }
-                ptr_vector<expr> args2;
+                arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity);
-                args2.push_back(arg);
-                args2.append(arity, args.c_ptr()-arity);
-                arg = a.mk_select(args2.size(), args2.c_ptr());
                 s = get_array_range(s);
             }
             if (is_pattern) {
@@ -151,8 +264,16 @@ namespace datalog {
         result = m.mk_eq(m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), result, 1, qid, skid, 1, &pat), m.mk_true());
         return result;
     }
+
+    expr * mk_quantifier_abstraction::mk_select(expr* arg, unsigned num_args, expr* const* args) {
+        ptr_vector<expr> args2;
+        args2.push_back(arg);
+        args2.append(num_args, args);
+        return a.mk_select(args2.size(), args2.c_ptr());                
+    }
         
     rule_set * mk_quantifier_abstraction::operator()(rule_set const & source) {
+        TRACE("dl", tout << "quantify " << source.get_num_rules() << " " << m_ctx.get_params().quantify_arrays() << "\n";);
         if (!m_ctx.get_params().quantify_arrays()) {
             return 0;
         }
@@ -168,6 +289,10 @@ namespace datalog {
         svector<bool> neg;
         rule_counter& vc = rm.get_counter();
 
+        if (m_ctx.get_model_converter()) {
+            m_mc = alloc(qa_model_converter, m);
+        }
+
         for (unsigned i = 0; i < sz; ++i) {            
             tail.reset();
             neg.reset();
@@ -186,17 +311,22 @@ namespace datalog {
             head = mk_head(r.get_head(), cnt);
 
             new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
+            TRACE("dl", r.display(m_ctx, tout); new_rule->display(m_ctx, tout););
             result->add_rule(new_rule);
-
         }        
-
+        
-        // model converter: TBD.
+        // proof converter: proofs are not necessarily preserved using this transformation.
-        // proof converter: TBD.
 
         if (m_old2new.empty()) {
             dealloc(result);
+            dealloc(m_mc);
             result = 0;
         }
+        else {
+            m_ctx.add_model_converter(m_mc);
+        }
+        m_mc = 0;
+
         return result;
     }
 

src/muz_qe/dl_mk_quantifier_abstraction.h

@@ -34,16 +34,19 @@ namespace datalog {
     class context;
 
     class mk_quantifier_abstraction : public rule_transformer::plugin {
+        class qa_model_converter;
         ast_manager& m;
         context&     m_ctx;
         array_util   a;
-        func_decl_ref_vector m_refs;
+        func_decl_ref_vector           m_refs;
         obj_map<func_decl, func_decl*> m_new2old;
         obj_map<func_decl, func_decl*> m_old2new;
+        qa_model_converter*            m_mc;
 
         func_decl* declare_pred(func_decl* old_p);
         app_ref mk_head(app* p, unsigned idx);
         app_ref mk_tail(app* p);
+        expr*   mk_select(expr* a, unsigned num_args, expr* const* args);
 
     public:
         mk_quantifier_abstraction(context & ctx, unsigned priority);

src/muz_qe/dl_mk_quantifier_instantiation.cpp

@@ -46,8 +46,7 @@ namespace datalog {
         qs.reset();
         unsigned tsz = r.get_tail_size();
         for (unsigned j = 0; j < tsz; ++j) {
-            conjs.push_back(r.get_tail(j));
+            conjs.push_back(r.get_tail(j));            
-            
         }
         datalog::flatten_and(conjs);
         for (unsigned j = 0; j < conjs.size(); ++j) {
@@ -98,17 +97,12 @@ namespace datalog {
             expr* t = todo[j].second;
             if (is_var(p)) {
                 unsigned idx = to_var(p)->get_idx();
-                expr* t2 = m_binding[idx];
+                if (!m_binding[idx]) {
-                if (!t2) {
                     m_binding[idx] = t;
                     match(i, pat, j + 1, todo, q, conjs);
                     m_binding[idx] = 0;
                     return;
                 }
-                else if (m_uf.find(t2->get_id()) != m_uf.find(t->get_id())) {
-                    // matching failed.
-                    return;
-                }
                 ++j;
                 continue;
             }
@@ -168,12 +162,6 @@ namespace datalog {
         TRACE("dl", tout << mk_pp(q, m) << "\n==>\n" << mk_pp(res, m) << "\n";);
     }
 
-    void mk_quantifier_instantiation::merge(expr* e1, expr* e2) {
-        unsigned i1 = e1->get_id();
-        unsigned i2 = e2->get_id();
-        m_uf.merge(i1, i2);
-    }
-
     void mk_quantifier_instantiation::collect_egraph(expr* e) {
         expr* e1, *e2;
         m_todo.push_back(e);
@@ -186,12 +174,12 @@ namespace datalog {
             }
             unsigned n = e->get_id();
             if (n >= m_terms.size()) {
-                m_terms.resize(e->get_id()+1);
+                m_terms.resize(n+1);
             }
-            m_terms[e->get_id()] = e;
+            m_terms[n] = e;
             visited.mark(e);
             if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) {
-                merge(e1, e2);
+                m_uf.merge(e1->get_id(), e2->get_id());
             }
             if (is_app(e)) {
                 app* ap = to_app(e);
@@ -246,12 +234,23 @@ namespace datalog {
         TRACE("dl", r.display(m_ctx, tout); tout << mk_pp(fml, m) << "\n";);
         
         rule_ref_vector added_rules(rm);
-        proof_ref pr(m); // proofs are TBD.
+        proof_ref pr(m); 
         rm.mk_rule(fml, pr, added_rules);
+        if (r.get_proof()) {
+            // use def-axiom to encode that new rule is a weakening of the original.
+            proof* p1 = r.get_proof();
+            for (unsigned i = 0; i < added_rules.size(); ++i) {
+                rule* r2 = added_rules[i].get();
+                r2->to_formula(fml);
+                pr = m.mk_modus_ponens(m.mk_def_axiom(m.mk_implies(m.get_fact(p1), fml)), p1);
+                r2->set_proof(m, pr);
+            }
+        }
         rules.add_rules(added_rules.size(), added_rules.c_ptr());
     }
         
     rule_set * mk_quantifier_instantiation::operator()(rule_set const & source) {
+        TRACE("dl", tout << m_ctx.get_params().instantiate_quantifiers() << "\n";);
         if (!m_ctx.get_params().instantiate_quantifiers()) {
             return 0;
         }
@@ -286,8 +285,7 @@ namespace datalog {
             }
         }
 
-        // model converter: TBD.
+        // model convertion: identity function.
-        // proof converter: TBD.
 
         if (!instantiated) {
             dealloc(result);

src/muz_qe/dl_mk_quantifier_instantiation.h

@@ -112,7 +112,6 @@ namespace datalog {
         obj_map<func_decl, ptr_vector<expr>*> m_funs;
 
 
-        void merge(expr* e1, expr* e2);
         void extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs);
         void collect_egraph(expr* e);
         void instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules);

src/muz_qe/dl_rule.cpp

@@ -135,7 +135,7 @@ namespace datalog {
         h.set_name(name);
         h(fml, p, fmls, prs);
         for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
-            m_ctx.register_predicate(h.get_fresh_predicates()[i]);
+            m_ctx.register_predicate(h.get_fresh_predicates()[i], false);
         }
         for (unsigned i = 0; i < fmls.size(); ++i) {
             mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name);

src/muz_qe/horn_tactic.cpp

@@ -92,7 +92,7 @@ class horn_tactic : public tactic {
 
         void register_predicate(expr* a) {
             SASSERT(is_predicate(a));
-            m_ctx.register_predicate(to_app(a)->get_decl(), true);
+            m_ctx.register_predicate(to_app(a)->get_decl(), false);
         }
 
         void check_predicate(ast_mark& mark, expr* a) {