add selected updates #4981

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/theory_str.cpp

@@ -89,8 +89,7 @@ namespace smt {
         m_library_aware_trail_stack(*this),
         m_find(*this),
         fixed_length_subterm_trail(m),
-        fixed_length_assumptions(m),
+        fixed_length_assumptions(m)
-        bitvector_character_constants(m)
     {
     }
 
@@ -103,7 +102,6 @@ namespace smt {
     }
 
     void theory_str::init() {
-        initialize_charset();
         m_mk_aut.set_solver(alloc(seq_expr_solver, get_manager(), ctx.get_fparams()));
     }
 
@@ -168,7 +166,6 @@ namespace smt {
         uninterpreted_to_char_subterm_map.reset();
         fixed_length_lesson.reset();
         candidate_model.reset();
-        bitvector_character_constants.reset();
     }
 
     expr * theory_str::mk_string(zstring const& str) {
@@ -200,79 +197,6 @@ namespace smt {
         st.update("str refine negated function", m_stats.m_refine_nf);
     }
 
-    void theory_str::initialize_charset() {
-        bool defaultCharset = true;
-        if (defaultCharset) {
-            // valid C strings can't contain the null byte ('\0')
-            charSetSize = 255;
-            char_set.resize(256, 0);
-            int idx = 0;
-            // small letters
-            for (int i = 97; i < 123; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // caps
-            for (int i = 65; i < 91; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // numbers
-            for (int i = 48; i < 58; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // printable marks - 1
-            for (int i = 32; i < 48; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // printable marks - 2
-            for (int i = 58; i < 65; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // printable marks - 3
-            for (int i = 91; i < 97; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // printable marks - 4
-            for (int i = 123; i < 127; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // non-printable - 1
-            for (int i = 1; i < 32; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-            // non-printable - 2
-            for (int i = 127; i < 256; i++) {
-                char_set[idx] = (char) i;
-                charSetLookupTable[char_set[idx]] = idx;
-                idx++;
-            }
-        } else {
-            const char setset[] = { 'a', 'b', 'c' };
-            int fSize = sizeof(setset) / sizeof(char);
-            char_set.resize(fSize, 0);
-            charSetSize = fSize;
-            for (int i = 0; i < charSetSize; i++) {
-                char_set[i] = setset[i];
-                charSetLookupTable[setset[i]] = i;
-            }
-        }
-    }
-
     void theory_str::assert_axiom(expr * _e) {
         if (_e == nullptr) 
             return;

src/smt/theory_str.h

@@ -509,9 +509,6 @@ protected:
 
     obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i
 
-    svector<char> char_set;
-    std::map<char, int>  charSetLookupTable;
-    int           charSetSize;
 
     obj_pair_map<expr, expr, expr*> concat_astNode_map;
 
@@ -545,8 +542,6 @@ protected:
     obj_map<expr, std::tuple<rational, expr*, expr*>> fixed_length_lesson; //keep track of information for the lesson
     unsigned preprocessing_iteration_count; // number of attempts we've made to solve by preprocessing length information
     obj_map<expr, zstring> candidate_model;
-
-    expr_ref_vector bitvector_character_constants; // array-indexed map of bv.mk_numeral terms
     
     stats m_stats;
 
@@ -766,7 +761,6 @@ protected:
     bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity);
 
     void dump_assignments();
-    void initialize_charset();
 
     void check_variable_scope();
     void recursive_check_variable_scope(expr * ex);

src/smt/theory_str_mc.cpp

@@ -626,7 +626,7 @@ namespace smt {
         zstring strConst;
         if (u.str.is_string(term, strConst)) {
             for (unsigned i = 0; i < strConst.length(); ++i) {
-                expr_ref chTerm(bitvector_character_constants.get(strConst[i]), m);
+                expr_ref chTerm(u.mk_char(strConst[i]), m);
                 eqc_chars.push_back(chTerm);
             }
         } else if (to_app(term)->get_num_args() == 0 && !u.str.is_string(term)) {
@@ -770,7 +770,7 @@ namespace smt {
                 // convert iValue to a constant
                 zstring iValue_str(iValue.to_string());
                 for (unsigned idx = 0; idx < iValue_str.length(); ++idx) {
-                    expr_ref chTerm(bitvector_character_constants.get(iValue_str[idx]), sub_m);
+                    expr_ref chTerm(u.mk_char(iValue_str[idx]), sub_m);
                     eqc_chars.push_back(chTerm);
                 }
                 return true;
@@ -884,13 +884,6 @@ namespace smt {
 
         ast_manager & m = get_manager();
 
-        if (bitvector_character_constants.empty()) {
-            for (unsigned i = 0; i <= u.max_char(); ++i) {
-                expr_ref chTerm(u.mk_char(i), m);
-                bitvector_character_constants.push_back(chTerm);
-                fixed_length_subterm_trail.push_back(chTerm);
-            }
-        }
 
         TRACE("str",
             ast_manager & m = get_manager();
@@ -916,7 +909,7 @@ namespace smt {
 
         smt_params subsolver_params;
         smt::kernel subsolver(m, subsolver_params);
-        subsolver.set_logic(symbol("QF_BV"));
+        subsolver.set_logic(symbol("QF_S"));
 
         sort * str_sort = u.str.mk_string_sort();
         sort * bool_sort = m.mk_bool_sort();
@@ -1203,7 +1196,7 @@ namespace smt {
         }
 
         TRACE("str_fl",
-            tout << "formulas asserted to bitvector subsolver:" << std::endl;
+            tout << "formulas asserted  subsolver:" << std::endl;
             for (auto e : fixed_length_assumptions) {
                 tout << mk_pp(e, subsolver.m()) << std::endl;
             }