From a2d8fd4c4b5f415edc35dd0d3e71181b52da862e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Sep 2014 09:33:12 -0700
Subject: [PATCH] local opts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.cpp | 50 +++++++++++++++++++++++++++++++++++++
 src/muz/base/dl_rule.cpp    | 11 ++++----
 2 files changed, 55 insertions(+), 6 deletions(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index f79a65705..a3ab9a1c2 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -639,6 +639,56 @@ namespace datalog {
         }
     }
 
+#if 0
+    void context::check_rules(rule_set& r) {
+        switch(get_engine()) {
+        case DATALOG_ENGINE:
+            collect_properties(r);
+            check_quantifier_free(r);
+            check_uninterpreted_free(r);
+            check_existential_tail(r); 
+            break;
+        case PDR_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            check_uninterpreted_free(r);
+            break;
+        case QPDR_ENGINE:
+            check_positive_predicates(r);
+            check_uninterpreted_free(r);
+            break;
+        case BMC_ENGINE:
+            check_positive_predicates(r);
+            break;            
+        case QBMC_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;         
+        case TAB_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;
+	case DUALITY_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;
+        case CLP_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;
+        case DDNF_ENGINE:
+            break;
+        case LAST_ENGINE:
+        default:
+            UNREACHABLE();
+            break;
+        }
+        if (generate_proof_trace() && !r.get_proof()) {
+            m_rule_manager.mk_rule_asserted_proof(r);
+        }
+    }
+#endif
+
     void context::check_rule(rule& r) {
         switch(get_engine()) {
         case DATALOG_ENGINE:
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 2015d4eea..ee14898ab 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -252,17 +252,16 @@ namespace datalog {
 
     unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) {
         expr* e1, *e2;
-        unsigned index = m_counter.get_next_var(fml);
         if (::is_forall(fml)) {
-            index += to_quantifier(fml)->get_num_decls();
             fml = to_quantifier(fml)->get_expr();
         }
+        unsigned index = m_counter.get_next_var(fml);
         if (m.is_implies(fml, e1, e2)) {
-            expr_ref_vector es(m);
+            m_args.reset();
             head = ensure_app(e2);
-            qe::flatten_and(e1, es);
-            for (unsigned i = 0; i < es.size(); ++i) {
-                body.push_back(ensure_app(es[i].get()));
+            qe::flatten_and(e1, m_args);
+            for (unsigned i = 0; i < m_args.size(); ++i) {
+                body.push_back(ensure_app(m_args[i].get()));
             }
         } 
         else {