add abstraction and instantiation

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

src/muz_qe/dl_mk_quantifier_instantiation.cpp

@@ -0,0 +1,295 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_quantifier_instantiation.cpp
+
+Abstract:
+
+    Convert Quantified Horn clauses into non-quantified clauses using
+    instantiation.
+
+Author:
+
+    Ken McMillan 
+    Andrey Rybalchenko
+    Nikolaj Bjorner (nbjorner) 2013-04-02
+
+Revision History:
+
+    Based on approach suggested in SAS 2013 paper 
+    "On Solving Universally Quantified Horn Clauses"    
+
+--*/
+
+#include "dl_mk_quantifier_instantiation.h"
+#include "dl_context.h"
+
+namespace datalog {
+
+    mk_quantifier_instantiation::mk_quantifier_instantiation(
+        context & ctx, unsigned priority):
+        plugin(priority),
+        m(ctx.get_manager()),
+        m_ctx(ctx),
+        m_var2cnst(m),
+        m_cnst2var(m),
+        a(m) {        
+    }
+
+    mk_quantifier_instantiation::~mk_quantifier_instantiation() {
+        
+    }
+
+    void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) {
+        conjs.reset();
+        qs.reset();
+        unsigned tsz = r.get_tail_size();
+        for (unsigned j = 0; j < tsz; ++j) {
+            conjs.push_back(r.get_tail(j));
+            
+        }
+        datalog::flatten_and(conjs);
+        for (unsigned j = 0; j < conjs.size(); ++j) {
+            expr* e = conjs[j].get();
+            quantifier* q;
+            if (rule_manager::is_forall(m, e, q)) {
+                qs.push_back(q);
+                conjs[j] = conjs.back();
+                conjs.pop_back();
+                --j;
+            }
+        }
+    }
+
+    void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) {
+        expr_ref qe(m);
+        qe = q;
+        m_var2cnst(qe);
+        q = to_quantifier(qe);
+        unsigned num_patterns = q->get_num_patterns();
+        for (unsigned i = 0; i < num_patterns; ++i) {
+            expr * pat = q->get_pattern(i);
+            SASSERT(m.is_pattern(pat));
+            instantiate_quantifier(q, to_app(pat), conjs);
+        }
+    }
+
+
+    void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs) {
+        unsigned sz = pat->get_num_args();
+        m_binding.reset();
+        m_binding.resize(q->get_num_decls());
+        term_pairs todo;
+        match(0, pat, 0, todo, q, conjs);
+    }
+
+    void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs) {
+        while (j < todo.size()) {
+            expr* p = todo[j].first;
+            expr* t = todo[j].second;
+            if (is_var(p)) {
+                unsigned idx = to_var(p)->get_idx();
+                expr* t2 = 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 += 1;
+                continue;
+            }
+            if (!is_app(p)) {
+                return;
+            }
+            app* a1 = to_app(p);
+            unsigned id = t->get_id();
+            unsigned next_id = id;
+            unsigned sz = todo.size();
+            do {
+                expr* t2 = m_terms[next_id];
+                if (is_app(t2)) {
+                    app* a2 = to_app(t2);
+                    if (a1->get_decl() == a2->get_decl() &&
+                        a1->get_num_args() == a2->get_num_args()) {
+                        for (unsigned k = 0; k < a1->get_num_args(); ++k) {
+                            todo.push_back(std::make_pair(a1->get_arg(k), a2->get_arg(k)));
+                        }
+                        match(i, pat, j + 1, todo, q, conjs);
+                        todo.resize(sz);
+                    }                    
+                }
+                next_id = m_uf.next(id);
+            }
+            while (next_id != id);
+            return;
+        }
+
+        if (i == pat->get_num_args()) {
+            yield_binding(q, conjs);
+            return;
+        }
+        expr* arg = pat->get_arg(i);
+        ptr_vector<expr>* terms = 0;
+    
+        if (m_funs.find(to_app(arg)->get_decl(), terms)) {
+            for (unsigned k = 0; k < terms->size(); ++k) {
+                todo.push_back(std::make_pair(arg, (*terms)[k]));
+                match(i + 1, pat, j, todo, q, conjs);
+                todo.pop_back();
+            }
+        }
+    }
+
+    void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs) {
+        DEBUG_CODE(
+            for (unsigned i = 0; i < m_binding.size(); ++i) {
+                SASSERT(m_binding[i]);
+            });
+        m_binding.reverse();
+        expr_ref res(m);
+        instantiate(m, q, m_binding.c_ptr(), res);
+        m_binding.reverse();
+        conjs.push_back(res);
+    }
+
+    void mk_quantifier_instantiation::merge(expr* e1, expr* e2) {
+        unsigned i1 = e1->get_id();
+        unsigned i2 = e2->get_id();
+        unsigned n = std::max(i1, i2);
+        while (n >= m_uf.get_num_vars()) {
+            m_uf.mk_var();            
+        }
+        m_uf.merge(i1, i2);
+    }
+
+    void mk_quantifier_instantiation::collect_egraph(expr* e) {
+        expr* e1, *e2;
+        m_todo.push_back(e);
+        expr_fast_mark1 visited;
+        while (!m_todo.empty()) {
+            e = m_todo.back();
+            m_todo.pop_back();
+            if (visited.is_marked(e)) {
+                continue;
+            }
+            if (e->get_id() >= m_terms.size()) {
+                m_terms.resize(e->get_id()+1);
+            }
+            m_terms[e->get_id()] = e;
+            visited.mark(e);
+            if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) {
+                merge(e1, e2);
+            }
+            if (is_app(e)) {
+                app* ap = to_app(e);
+                ptr_vector<expr>* terms = 0;
+                if (m_funs.find(ap->get_decl(), terms)) {
+                    terms = alloc(ptr_vector<expr>);
+                    m_funs.insert(ap->get_decl(), terms);
+                }
+                terms->push_back(e);
+                m_todo.append(ap->get_num_args(), ap->get_args());
+            }
+        }
+    }
+
+    void mk_quantifier_instantiation::instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules) {
+        rule_manager& rm = m_ctx.get_rule_manager();
+        expr_ref fml(m), cnst(m);
+        var_ref var(m);
+        ptr_vector<sort> sorts;
+        r.get_vars(sorts);
+        m_uf.reset();
+        m_terms.reset();
+        m_var2cnst.reset();
+        m_cnst2var.reset();
+        fml = m.mk_and(conjs.size(), conjs.c_ptr());
+
+        for (unsigned i = 0; i < sorts.size(); ++i) {
+            if (!sorts[i]) {
+                sorts[i] = m.mk_bool_sort();
+            }
+            var = m.mk_var(i, sorts[i]);
+            cnst = m.mk_fresh_const("C", sorts[i]);
+            m_var2cnst.insert(var, cnst);
+            m_cnst2var.insert(cnst, var);
+        }
+
+        fml = m.mk_and(conjs.size(), conjs.c_ptr());
+        m_var2cnst(fml);
+        collect_egraph(fml);
+
+        for (unsigned i = 0; i < qs.size(); ++i) {
+            instantiate_quantifier(qs[i].get(), conjs);
+        }
+        obj_map<func_decl, ptr_vector<expr>*>::iterator it = m_funs.begin(), end = m_funs.end();
+        for (; it != end; ++it) {
+            dealloc(it->m_value);
+        }
+        m_funs.reset();
+
+        fml = m.mk_and(conjs.size(), conjs.c_ptr());
+        fml = m.mk_implies(fml, r.get_head());
+        
+        rule_ref_vector added_rules(rm);
+        proof_ref pr(m); // proofs are TBD.
+        rm.mk_rule(fml, pr, added_rules);
+        rules.add_rules(added_rules.size(), added_rules.c_ptr());
+    }
+        
+    rule_set * mk_quantifier_instantiation::operator()(rule_set const & source) {
+        if (!m_ctx.get_params().instantiate_quantifiers()) {
+            return 0;
+        }
+        bool has_quantifiers = false;
+        unsigned sz = source.get_num_rules();
+        for (unsigned i = 0; !has_quantifiers && i < sz; ++i) {
+            rule& r = *source.get_rule(i);
+            has_quantifiers = has_quantifiers || r.has_quantifiers();   
+            if (r.has_negation()) {
+                return 0;
+            }
+        }
+        if (!has_quantifiers) {
+            return 0;
+        }
+
+        expr_ref_vector conjs(m);
+        quantifier_ref_vector qs(m);
+        rule_set * result = alloc(rule_set, m_ctx);
+
+        bool instantiated = false;
+
+        for (unsigned i = 0; i < sz; ++i) {       
+            rule * r = source.get_rule(i);
+            extract_quantifiers(*r, conjs, qs);
+            if (qs.empty()) {
+                result->add_rule(r);
+            }
+            else {
+                instantiate_rule(*r, conjs, qs, *result);
+                instantiated = true;
+            }
+        }
+
+        // model converter: TBD.
+        // proof converter: TBD.
+
+        if (!instantiated) {
+            dealloc(result);
+            result = 0;
+        }
+        return result;
+    }
+
+
+};
+
+