add pdr tactic

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

src/muz_qe/pdr_tactic.cpp

@@ -0,0 +1,286 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    pdr_tactic.h
+
+Abstract:
+
+    PDR as a tactic to solve Horn clauses.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-16.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"model_converter.h"
+#include"proof_converter.h"
+#include"pdr_tactic.h"
+#include"dl_context.h"
+
+class pdr_tactic : public tactic {
+    struct imp {
+        ast_manager&             m;
+        datalog::context         m_ctx;
+        front_end_params         m_fparams;
+
+        imp(ast_manager & m, params_ref const & p):
+            m(m),
+            m_ctx(m, m_fparams) {
+            updt_params(p);
+        }
+
+        void updt_params(params_ref const & p) {
+            m_ctx.updt_params(p);
+        }
+
+        void collect_param_descrs(param_descrs & r) {
+            m_ctx.collect_params(r);
+        }
+
+        void reset_statistics() {
+            m_ctx.reset_statistics();
+        }
+
+        void collect_statistics(statistics & st) const {
+            m_ctx.collect_statistics(st);
+        }
+
+        void set_cancel(bool f) {
+            if (f) {
+                m_ctx.cancel();
+            }
+        }
+
+        void normalize(expr_ref& f) {
+            bool is_positive = true;
+            expr* e = 0;
+            while (true) {
+                if (is_forall(f) && is_positive) {
+                    f = to_quantifier(f)->get_expr();
+                }
+                else if (is_exists(f) && !is_positive) {
+                    f = to_quantifier(f)->get_expr();                    
+                }
+                else if (m.is_not(f, e)) {
+                    is_positive = !is_positive;
+                    f = e;
+                }
+                else {
+                    break;
+                }
+            }
+            if (!is_positive) {
+                f = m.mk_not(f);
+            }
+            
+        }
+
+        bool is_predicate(expr* a) {
+            SASSERT(m.is_bool(a));
+            return is_app(a) && to_app(a)->get_decl()->get_family_id() == null_family_id;
+        }
+
+        void register_predicate(expr* a) {
+            SASSERT(is_predicate(a));
+            m_ctx.register_predicate(to_app(a)->get_decl(), true);
+        }
+
+        enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
+
+        formula_kind get_formula_kind(expr_ref& f) {
+            normalize(f);
+            expr_ref_vector args(m), body(m);
+            expr_ref head(m);
+            expr* a = 0, *a1 = 0;
+            datalog::flatten_or(f, args);
+            for (unsigned i = 0; i < args.size(); ++i) {
+                a = args[i].get();                
+                if (m.is_not(a, a1) && is_predicate(a1)) {
+                    register_predicate(a1);
+                    body.push_back(a1);
+                }
+                else if (is_predicate(a)) {
+                    register_predicate(a);
+                    if (head) {
+                        return IS_NONE;
+                    }
+                    head = a;
+                }
+                else if (m.is_not(a, a1)) {
+                    body.push_back(a1);
+                }
+                else {
+                    body.push_back(m.mk_not(a));
+                }
+            }
+            f = m.mk_and(body.size(), body.c_ptr());
+            if (head) {
+                f = m.mk_implies(f, head);
+                return IS_RULE;
+            }
+            else {
+                return IS_QUERY;
+            }
+        }
+
+        expr_ref mk_rule(expr* body, expr* head) {
+            return expr_ref(m.mk_implies(body, head), m);
+        }
+
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("pdr", *g);
+            bool produce_models = g->models_enabled();
+            bool produce_proofs = g->proofs_enabled();
+
+            if (produce_proofs) {
+                if (!m_ctx.get_params().get_bool(":generate-proof-trace", true)) {
+                    params_ref params = m_ctx.get_params();
+                    params.set_bool(":generate-proof-trace", true);
+                    updt_params(params);
+                }
+            }
+
+            unsigned sz = g->size();
+            expr_ref q(m), f(m);
+            expr_ref_vector queries(m);
+            std::stringstream msg;
+
+            for (unsigned i = 0; i < sz; i++) {
+                f = g->form(i);
+                formula_kind k = get_formula_kind(f);
+                switch(k) {
+                case IS_RULE:
+                    m_ctx.add_rule(f, symbol::null);
+                    break;
+                case IS_QUERY:
+                    queries.push_back(f);
+                    break;
+                default: 
+                    msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
+                    throw tactic_exception(msg.str().c_str());
+                }
+            }
+
+            if (queries.size() != 1) {
+                q = m.mk_fresh_const("query", m.mk_bool_sort());
+                for (unsigned i = 0; i < queries.size(); ++i) {
+                    f = mk_rule(queries[i].get(), q);
+                    m_ctx.add_rule(f, symbol::null);
+                }
+                queries.reset();
+                queries.push_back(q);
+            }
+            SASSERT(queries.size() == 1);
+            q = queries[0].get();
+            lbool is_reachable = m_ctx.query(q);
+            g->inc_depth();
+            result.push_back(g.get());
+            switch (is_reachable) {
+            case l_true: {
+                // goal is unsat
+                g->assert_expr(m.mk_false());
+                if (produce_proofs) {
+                    proof_ref proof = m_ctx.get_proof();
+                    pc = proof2proof_converter(m, proof);
+                }
+                break;    
+            }
+            case l_false: {                
+                // goal is sat
+                g->reset();
+                if (produce_models) {
+                    model_ref md = m_ctx.get_model();
+                    mc = model2model_converter(&*md);
+                }
+                break;    
+            }
+            case l_undef: 
+                // subgoal is unchanged.
+                break;    
+            }
+            TRACE("pdr", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    params_ref m_params;
+    imp *      m_imp;
+public:
+    pdr_tactic(ast_manager & m, params_ref const & p):
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(pdr_tactic, m, m_params);
+    }
+        
+    virtual ~pdr_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+   
+    virtual void collect_param_descrs(param_descrs & r) {
+        m_imp->collect_param_descrs(r);
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+
+    
+    virtual void collect_statistics(statistics & st) const {
+        m_imp->collect_statistics(st);
+    }
+
+    virtual void reset_statistics() {
+        m_imp->reset_statistics();
+    }
+
+    
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m;
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+    
+protected:
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(pdr_tactic, m, p));
+}
+

src/muz_qe/pdr_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    pdr_tactic.h
+
+Abstract:
+
+    PDR as a tactic to solve Horn clauses.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-16.
+
+Revision History:
+
+--*/
+#ifndef _PDR_TACTIC_H_
+#define _PDR_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+  ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)")
+*/
+#endif