Added smt kernel setup for QF_FP(BV). Thanks to codeplex user smccamant for reporting this performance problem.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/ast/static_features.cpp

@@ -22,6 +22,8 @@ Revision History:
 static_features::static_features(ast_manager & m):
     m_manager(m),
     m_autil(m),
+    m_bvutil(m),
+    m_fpautil(m),
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
     m_lfid(m.mk_family_id("label")),
@@ -266,6 +268,10 @@ void static_features::update_core(expr * e) {
         m_has_int  = true;
     if (!m_has_real && m_autil.is_real(e))
         m_has_real = true;
+    if (!m_has_bv && m_bvutil.is_bv(e))
+        m_has_bv = true;
+    if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
+        m_has_fpa = true;
     if (is_app(e)) {
         family_id fid = to_app(e)->get_family_id();
         mark_theory(fid);

src/ast/static_features.h

@@ -21,14 +21,18 @@ Revision History:
 
 #include"ast.h"
 #include"arith_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"fpa_decl_plugin.h"
 #include"map.h"
 
 struct static_features {
     ast_manager &            m_manager;
     arith_util               m_autil;
+    bv_util                  m_bvutil;
+    fpa_util                 m_fpautil;
     family_id                m_bfid;
     family_id                m_afid;
-    family_id                m_lfid;
+    family_id                m_lfid;    
     ast_mark                 m_already_visited;
     bool                     m_cnf;
     unsigned                 m_num_exprs;             // 
@@ -68,6 +72,8 @@ struct static_features {
     bool                     m_has_rational;    //
     bool                     m_has_int;         //
     bool                     m_has_real;        //
+    bool                     m_has_bv;         //
+    bool                     m_has_fpa;        //
     rational                 m_arith_k_sum;     // sum of the numerals in arith atoms.
     unsigned                 m_num_arith_terms;
     unsigned                 m_num_arith_eqs;   // equalities of the form t = k where k is a numeral

src/smt/smt_setup.cpp

@@ -113,6 +113,10 @@ namespace smt {
             setup_UFLRA();
         else if (m_logic == "LRA")
             setup_LRA();
+        else if (m_logic == "QF_FP")
+            setup_QF_FP();
+        else if (m_logic == "QF_FPBV")
+            setup_QF_FPBV();
         else
             setup_unknown();
     }
@@ -680,7 +684,8 @@ namespace smt {
         setup_mi_arith();
     }
 
-    void setup::setup_QF_FP() {        
+    void setup::setup_QF_FP() {
+        setup_QF_BV();
         m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
     }
 
@@ -791,6 +796,7 @@ namespace smt {
     }
 
     void setup::setup_fpa() {
+        setup_bv();
         m_context.register_plugin(alloc(theory_fpa, m_manager));
     }
 
@@ -867,7 +873,22 @@ namespace smt {
             return;
         }
 
-        // TODO QF_BV, QF_AUFBV, QF_AUFLIA
+        if (st.num_theories() == 1 && st.m_has_bv) {
+            setup_QF_BV();
+            return;
+        }
+
+        if (st.num_theories() == 1 && st.m_has_fpa) {
+            setup_QF_FP();
+            return;
+        }
+
+        if (st.num_theories() == 2 && st.m_has_fpa && st.m_has_bv) {
+            setup_QF_FPBV();
+            return;
+        }
+
+        // TODO QF_AUFBV, QF_AUFLIA
         setup_unknown();
     }