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

doc/footer.html

@@ -1,3 +1,4 @@
-<div class="tabs"></div>
+<div id="nav">
+</div>
 </body>
 </html>

doc/update_website.cmd

@@ -0,0 +1,4 @@
+REM Script for updating the website containing the Z3 API documentation.
+REM You must be inside the Microsoft network to execute this script, and 
+REM robocopy must be in your PATH.
+robocopy /S html \\research\root\web\external\en-us\UM\redmond\projects\z3

doc/website.dox

@@ -6,10 +6,12 @@
    
    <b>The Z3 website moved to <a class="el" href="http://z3.codeplex.com">z3.codeplex.com</a>.</b>
 
+   The old Z3 website can be found <a class="el" href="http://research.microsoft.com/en-us/um/redmond/projects/z3/old/index.html">here</a>.
+
    This website hosts the automatically generated documentation for the Z3 APIs.
 
    - \ref capi 
    - <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
    - <a class="el" href="z3.html">Python API</a>
-   - Try Z3 online at <a href="http://rise4fun.com/z3py">RiSE4Fun</a>.
+   - Try Z3 online at <a href="http://rise4fun.com/z3py">RiSE4Fun</a> using <a href="http://rise4fun.com/z3py">Python</a> or <a href="http://rise4fun.com/z3">SMT 2.0</a>.
 */

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 {

src/muz_qe/horn_tactic.cpp

@@ -90,6 +90,24 @@ class horn_tactic : public tactic {
             m_ctx.register_predicate(to_app(a)->get_decl(), true);
         }
 
+        void check_predicate(expr* a) {
+            expr* a1 = 0;
+            while (true) {
+                if (is_quantifier(a)) {
+                    a = to_quantifier(a)->get_expr();
+                    continue;
+                }
+                if (m.is_not(a, a1)) {
+                    a = a1;
+                    continue;
+                }
+                if (is_predicate(a)) {
+                    register_predicate(a);
+                }
+                break;
+            }
+        }
+
         enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
 
         formula_kind get_formula_kind(expr_ref& f) {
@@ -100,12 +118,11 @@ class horn_tactic : public tactic {
             datalog::flatten_or(f, args);
             for (unsigned i = 0; i < args.size(); ++i) {
                 a = args[i].get();    
+                check_predicate(a);
                 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;
                     }

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;
+         num_args = 1;
-        expr* const* args = &e;
+        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)) ||
+        flatten_args(q, num_args, args);
-            (q->is_exists() && m.is_and(e))) {
-            num_args = to_app(e)->get_num_args();
-            args     = to_app(e)->get_args();
-        }
         
         unsigned def_count = 0;
         unsigned largest_vinx = 0;