From 01ddb2044109e5eb668b00546b8b7d995a2df5e0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Nov 2012 10:42:59 -0800
Subject: [PATCH] recognize array and bv theories in HORN format

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  6 ++++--
 src/muz_qe/qe_lite.cpp          | 20 ++++++++++++--------
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 225f0be87..165ecfcba 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -477,7 +477,8 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
         s == "QF_UFBV" ||
         s == "QF_ABV" ||
         s == "QF_AUFBV" ||
-        s == "QF_BVRE";
+        s == "QF_BVRE" ||
+        s == "HORN";
 }
 
 bool cmd_context::logic_has_horn(symbol const& s) const {
@@ -518,7 +519,8 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
         s == "AUFBV" || 
         s == "ABV" || 
         s == "QF_ABV" ||
-        s == "QF_AUFBV";
+        s == "QF_AUFBV" ||
+        s == "HORN";
 }
 
 bool cmd_context::logic_has_array() const {
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index 97f55fb6f..8a14aeb4c 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -340,15 +340,23 @@ class der2 {
         }
     }
 
-    void apply_substitution(quantifier * q, expr_ref & r) {
+    void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
         expr * e = q->get_expr();
-        unsigned num_args = 1;
-        expr* const* args = &e;
+         num_args = 1;
+        args = &e;
         if ((q->is_forall() && m.is_or(e)) ||
             (q->is_exists() && m.is_and(e))) {
             num_args = to_app(e)->get_num_args();
             args     = to_app(e)->get_args();
         }
+    }
+
+    void apply_substitution(quantifier * q, expr_ref & r) {
+        
+        expr * e = q->get_expr();
+        unsigned num_args = 1;
+        expr* const* args = &e;
+        flatten_args(q, num_args, args);
         bool_rewriter rw(m);
         
         // get a new expression
@@ -395,11 +403,7 @@ class der2 {
         set_is_variable_proc(is_v);
         unsigned num_args = 1;
         expr* const* args = &e;
-        if ((q->is_forall() && m.is_or(e)) ||
-            (q->is_exists() && m.is_and(e))) {
-            num_args = to_app(e)->get_num_args();
-            args     = to_app(e)->get_args();
-        }
+        flatten_args(q, num_args, args);
         
         unsigned def_count = 0;
         unsigned largest_vinx = 0;