Merge pull request #992 from mtrberzi/theory_str-static-features

theory_str static features and cmd_context

src/ast/static_features.cpp

@@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m):
     m_bvutil(m),
     m_arrayutil(m),
     m_fpautil(m),
+    m_sequtil(m),
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
     m_lfid(m.mk_family_id("label")),
@@ -77,6 +78,8 @@ void static_features::reset() {
     m_has_real                             = false; 
     m_has_bv                               = false;
     m_has_fpa                              = false;
+    m_has_str                              = false;
+    m_has_seq_non_str                      = false;
     m_has_arrays                           = false;
     m_arith_k_sum                          .reset();
     m_num_arith_terms                      = 0;
@@ -279,6 +282,11 @@ void static_features::update_core(expr * e) {
         m_has_fpa = true;
     if (!m_has_arrays && m_arrayutil.is_array(e))
         m_has_arrays = true;
+    if (!m_has_str && m_sequtil.str.is_string_term(e))
+        m_has_str = true;
+    if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
+        m_has_seq_non_str = true;
+    }
     if (is_app(e)) {
         family_id fid = to_app(e)->get_family_id();
         mark_theory(fid);

src/ast/static_features.h

@@ -24,6 +24,7 @@ Revision History:
 #include"bv_decl_plugin.h"
 #include"array_decl_plugin.h"
 #include"fpa_decl_plugin.h"
+#include"seq_decl_plugin.h"
 #include"map.h"
 
 struct static_features {
@@ -32,6 +33,7 @@ struct static_features {
     bv_util                  m_bvutil;
     array_util               m_arrayutil;
     fpa_util                 m_fpautil;
+    seq_util                 m_sequtil;
     family_id                m_bfid;
     family_id                m_afid;
     family_id                m_lfid;    
@@ -77,6 +79,8 @@ struct static_features {
     bool                     m_has_real;        //
     bool                     m_has_bv;          //
     bool                     m_has_fpa;         //
+    bool                     m_has_str;         // has String-typed terms
+    bool                     m_has_seq_non_str; // has non-String-typed Sequence terms
     bool                     m_has_arrays;      //
     rational                 m_arith_k_sum;     // sum of the numerals in arith atoms.
     unsigned                 m_num_arith_terms;

src/cmd_context/cmd_context.cpp

@@ -249,6 +249,7 @@ protected:
     array_util    m_arutil;
     fpa_util      m_futil;
     seq_util      m_sutil;
+
     datalog::dl_decl_util m_dlutil;
 
     format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
@@ -277,6 +278,7 @@ public:
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
     virtual seq_util & get_sutil() { return m_sutil; }
+
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const {
         return
@@ -527,6 +529,9 @@ bool cmd_context::logic_has_fpa() const {
     return !has_logic() || smt_logics::logic_has_fpa(m_logic);
 }
 
+bool cmd_context::logic_has_str() const {
+    return !has_logic() || m_logic == "QF_S";
+}
 
 bool cmd_context::logic_has_array() const {
     return !has_logic() || smt_logics::logic_has_array(m_logic);
@@ -568,7 +573,6 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
-
         svector<family_id>::iterator it  = fids.begin();
         svector<family_id>::iterator end = fids.end();
         for (; it != end; ++it) {
@@ -616,7 +620,6 @@ void cmd_context::init_external_manager() {
     init_manager_core(false);
 }
 
-
 bool cmd_context::set_logic(symbol const & s) {
     if (has_logic())
         throw cmd_exception("the logic has already been set");

src/cmd_context/cmd_context.h

@@ -257,6 +257,7 @@ protected:
     bool logic_has_array() const;
     bool logic_has_datatype() const;
     bool logic_has_fpa() const;
+    bool logic_has_str() const;
 
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
     void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}