Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr

src/tactic/ackr/qfufbv_ackr_tactic.cpp

@@ -23,7 +23,7 @@ Revision History:
 #include"max_bv_sharing_tactic.h"
 #include"bv_size_reduction_tactic.h"
 #include"ctx_simplify_tactic.h"
-#include"nnf_tactic.h"
+#include"smt_tactic.h"
 ///////////////
 #include"model_smt2_pp.h"
 #include"cooperate.h"
@@ -111,7 +111,7 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
         using_params(mk_simplify_tactic(m), simp2_p)
         );
 
-    return and_then(
+    tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
-        preamble_t,
+    return and_then(preamble_t,
-        alloc(qfufbv_ackr_tactic, m, p));
+        cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
 }

src/tactic/probe.cpp

@@ -301,6 +301,7 @@ public:
     }
 };
 
+
 class is_qfbv_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
@@ -356,6 +357,46 @@ probe * mk_is_qfaufbv_probe() {
     return alloc(is_qfaufbv_probe);
 }
 
+
+struct is_non_qfufbv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       m_bv_util;
+
+    is_non_qfufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        if (!m.is_bool(n) && !m_bv_util.is_bv(n))
+            throw found();
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == m_bv_util.get_family_id())
+            return;
+        if (is_uninterp(n))
+            return;
+
+        throw found();
+    }
+};
+
+class is_qfufbv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qfufbv_predicate>(g);
+    }
+};
+
+probe * mk_is_qfufbv_probe() {
+    return alloc(is_qfufbv_probe);
+}
+
+
+
 class num_consts_probe : public probe {
     bool         m_bool;   // If true, track only boolean constants. Otherwise, track only non boolean constants.
     char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.

src/tactic/probe.h

@@ -112,6 +112,7 @@ probe * mk_div(probe * p1, probe * p2);
 probe * mk_is_propositional_probe();
 probe * mk_is_qfbv_probe();
 probe * mk_is_qfaufbv_probe();
+probe * mk_is_qfufbv_probe();
 
 /*
   ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()")