Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/muz_qe/dl_mk_extract_quantifiers.cpp

@@ -0,0 +1,97 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_extract_quantifiers.cpp
+
+Abstract:
+
+    Remove universal quantifiers over interpreted predicates in the body.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-21
+
+Revision History:
+
+--*/
+
+#include"dl_mk_extract_quantifiers.h"
+#include"ast_pp.h"
+
+namespace datalog {
+
+
+    mk_extract_quantifiers::mk_extract_quantifiers(context & ctx) : 
+        rule_transformer::plugin(101, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()),
+        rm(ctx.get_rule_manager()) 
+    {}
+
+    mk_extract_quantifiers::~mk_extract_quantifiers() {
+        for (unsigned i = 0; i < m_refs.size(); ++i) {
+            dealloc(m_refs[i]);
+        }
+        m_quantifiers.reset();
+        m_refs.reset();
+    }
+
+
+    void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
+        app_ref_vector tail(m);
+        svector<bool>  neg_tail;
+        quantifier_ref_vector quantifiers(m);
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz = r.get_tail_size();
+        for (unsigned i = 0; i < utsz; ++i) {
+            tail.push_back(r.get_tail(i));
+            neg_tail.push_back(r.is_neg_tail(i));
+        }
+        for (unsigned i = utsz; i < tsz; ++i) {
+            SASSERT(!r.is_neg_tail(i));
+            app* t = r.get_tail(i);
+            expr_ref_vector conjs(m);
+            datalog::flatten_and(t, conjs);
+            for (unsigned j = 0; j < conjs.size(); ++j) {
+                expr* e = conjs[j].get();
+                quantifier* q = 0;
+                if (rule_manager::is_forall(m, e, q)) {
+                    quantifiers.push_back(q);
+                }
+                else {
+                    tail.push_back(is_app(e)?to_app(e):m.mk_eq(e, m.mk_true()));
+                    neg_tail.push_back(false);
+                }
+            }
+        }
+        if (quantifiers.empty()) {
+            new_rules.add_rule(&r);
+        }
+        else {
+            rule* new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg_tail.c_ptr(), r.name(), false);
+            new_rules.add_rule(new_rule);
+            quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
+            m_quantifiers.insert(new_rule, qs);
+            m_refs.push_back(qs);
+        }
+    }
+    
+    rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+        m_quantifiers.reset();
+        rule_set* rules = alloc(rule_set, m_ctx);
+        rule_set::iterator it = source.begin(), end = source.end();
+        for (; it != end; ++it) {
+            extract(**it, *rules);
+        }
+        if (m_quantifiers.empty()) {
+            dealloc(rules);
+            rules = 0;
+        }        
+        return rules;        
+    }
+
+};
+
+

src/muz_qe/dl_mk_extract_quantifiers.h

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_extract_quantifiers.h
+
+Abstract:
+
+    Remove universal quantifiers over interpreted predicates in the body.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-21
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_EXTRACT_QUANTIFIERS_H_
+#define _DL_MK_EXTRACT_QUANTIFIERS_H_
+
+#include"dl_context.h"
+#include"dl_rule_set.h"
+#include"dl_rule_transformer.h"
+
+namespace datalog {
+
+    /**
+       \brief Extract universal quantifiers from rules.
+    */
+    class mk_extract_quantifiers : public rule_transformer::plugin {
+        context&        m_ctx;
+        ast_manager&    m;
+        rule_manager&   rm;
+        ptr_vector<quantifier_ref_vector> m_refs;
+        obj_map<rule const, quantifier_ref_vector*> m_quantifiers;
+
+        void extract(rule& r, rule_set& new_rules);
+
+    public:
+        /**
+           \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
+         */
+        mk_extract_quantifiers(context & ctx);
+
+        virtual ~mk_extract_quantifiers();
+        
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+
+        obj_map<rule const, quantifier_ref_vector*>& quantifiers() { return m_quantifiers; }
+
+        bool has_quantifiers() const { return !m_quantifiers.empty(); }
+
+    };
+
+};
+
+#endif /* _DL_MK_EXTRACT_QUANTIFIERS_H_ */
+

src/muz_qe/pdr_dl_interface.cpp

@@ -25,7 +25,7 @@ Revision History:
 #include "dl_mk_rule_inliner.h"
 #include "dl_rule.h"
 #include "dl_rule_transformer.h"
-//include "dl_mk_extract_quantifiers.h"
+#include "dl_mk_extract_quantifiers.h"
 #include "smt2parser.h"
 #include "pdr_context.h"
 #include "pdr_dl_interface.h"
@@ -146,7 +146,6 @@ lbool dl_interface::query(expr * query) {
             --num_unfolds;
         }
     }
-#if 0
     // remove universal quantifiers from body.
     datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
     datalog::rule_transformer extract_q_tr(m_ctx);
@@ -186,8 +185,7 @@ lbool dl_interface::query(expr * query) {
             return result;
         }
     }
-#endif
+
-    return l_undef;
 }
 
 expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {