fix trace typos

src/ast/seq_decl_plugin.h

@@ -273,6 +273,10 @@ public:
         bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
 
+        bool is_string_term(expr const * n) const {
+            sort * s = get_sort(n);
+            return is_sort_of(s, m_fid, _STRING_SORT);
+        }
 
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);

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,10 @@ 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.is_seq(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/smt/params/smt_params.cpp

@@ -41,6 +41,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_max_conflicts = p.max_conflicts();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
+    m_string_solver = _p.get_sym("string_solver", m_string_solver);
     model_params mp(_p);
     m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))
@@ -157,4 +158,4 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_check_at_labels);
     DISPLAY_PARAM(m_dump_goal_as_smt);
     DISPLAY_PARAM(m_auto_config);
-}
+}

src/smt/params/smt_params.h

@@ -216,6 +216,13 @@ struct smt_params : public preprocessor_params,
     bool                m_dump_goal_as_smt;
     bool                m_auto_config;
 
+    // -----------------------------------
+    //
+    // Solver selection
+    //
+    // -----------------------------------
+    symbol m_string_solver;
+
     smt_params(params_ref const & p = params_ref()):
         m_display_proof(false),
         m_display_dot_proof(false),
@@ -286,7 +293,8 @@ struct smt_params : public preprocessor_params,
         m_at_labels_cex(false),
         m_check_at_labels(false),
         m_dump_goal_as_smt(false),
-        m_auto_config(true) {
+        m_auto_config(true),
+        m_string_solver(symbol("auto")){
         updt_local_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -62,6 +62,7 @@ def_module_params(module_name='smt',
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('string_solver', SYMBOL, 'auto', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
                           ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
                           ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),

src/smt/smt_setup.cpp

@@ -206,7 +206,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        setup_seq();
+        m_context.register_plugin(alloc(theory_seq, m_manager));
     }
 
     void setup::setup_QF_UF(static_features const & st) {
@@ -824,10 +824,21 @@ namespace smt {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
 
-    void setup::setup_seq() {
+    void setup::setup_seq(static_features const & st) {
-        // TODO proper negotiation of theory_str vs. theory_seq
+        // check params for what to do here when it's ambiguous
-        //m_context.register_plugin(alloc(theory_seq, m_manager));
+        if (m_params.m_string_solver == "z3str3") {
-        setup_str();
+            setup_str();
+        } else if (m_params.m_string_solver == "seq") {
+            m_context.register_plugin(alloc(theory_seq, m_manager));
+        } else if (m_params.m_string_solver == "auto") {
+            if (st.m_has_seq_non_str) {
+                m_context.register_plugin(alloc(theory_seq, m_manager));
+            } else {
+                setup_str();
+            }
+        } else {
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+        }
     }
 
     void setup::setup_card() {
@@ -850,10 +861,10 @@ namespace smt {
         setup_bv();
         setup_datatypes();
         setup_dl();
-        setup_seq();
+        // setup_seq()
+        m_context.register_plugin(alloc(theory_seq, m_manager));
         setup_card();
         setup_fpa();
-        setup_str();
     }
 
     void setup::setup_unknown(static_features & st) {
@@ -866,7 +877,7 @@ namespace smt {
             setup_datatypes();
             setup_bv();
             setup_dl();
-            setup_seq();
+            setup_seq(st);
             setup_card();
             setup_fpa();
             return;

src/smt/smt_setup.h

@@ -94,7 +94,7 @@ namespace smt {
         void setup_bv();
         void setup_arith();
         void setup_dl();
-        void setup_seq();
+        void setup_seq(static_features const & st);
         void setup_card();
         void setup_i_arith();
         void setup_mi_arith();

src/smt/theory_str.cpp

@@ -4844,7 +4844,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) {
             // we only want to inspect the Contains terms where either of strAst or substrAst
             // are equal to varNode.
 
-            TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;);
+            TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;);
 
             if (varNode != strAst && varNode != substrAst) {
                 TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;);
@@ -4873,7 +4873,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) {
                     zstring subStrConst;
                     u.str.is_string(substrValue, subStrConst);
 
-                    TRACE("t_str_detail", tout << "strConst = "str", subStrConst = " << subStrConst << "\n";);
+                    TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << "\n";);
 
                     if (strConst.contains(subStrConst)) {
                         //implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx));
@@ -4983,7 +4983,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE
             // we only want to inspect the Contains terms where either of strAst or substrAst
             // are equal to varNode.
 
-            TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;);
+            TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;);
 
             if (varNode != strAst && varNode != substrAst) {
                 TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;);
@@ -6181,7 +6181,6 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) {
             }
             make_transition(last, str[(str.length() - 1)], end);
             TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
-            TRACE("t_str_rw", tout << "str", end = " << end << std::endl;);
         } else {
             TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
             m_valid = false;