From 3478cdb75693801b97bc0aa92a819e9cc5e9dac9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 3 Feb 2015 12:30:42 +0000
Subject: [PATCH] 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 |  6 ++++++
 src/ast/static_features.h   |  8 +++++++-
 src/smt/smt_setup.cpp       | 25 +++++++++++++++++++++++--
 3 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index cba31665c..e725df691 100644
--- a/src/ast/static_features.cpp
+++ b/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);
diff --git a/src/ast/static_features.h b/src/ast/static_features.h
index bbbea65bf..2d6213ded 100644
--- a/src/ast/static_features.h
+++ b/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
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index d17e4b803..7abd40399 100644
--- a/src/smt/smt_setup.cpp
+++ b/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();
     }