z3str3: remove legacy code (#4215)

* z3str3: remove legacy fixed-length overlap testing

parameter smt.str.fixed_length_overlap_models has been deprecated

* z3str3: remove legacy length/value testing algorithm and binary search heuristic

the following parameters are deprecated:
smt.str.use_binary_search
smt.str.binary_search_start
smt.str.fixed_length_models (the fixed-length model construction is now always used)

* z3str3: remove legacy regex unroll methods

* z3str3: remove unused methods and member variables

src/ast/seq_decl_plugin.cpp

@@ -553,7 +553,6 @@ void seq_decl_plugin::init() {
     sort* str2TintT[3] = { strT, strT, intT };
     sort* seqAintT[2] = { seqA, intT };
     sort* seq3A[3] = { seqA, seqA, seqA };
-    sort* reTintT[2] = { reT, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",     1, 1, &A, seqA);
@@ -604,7 +603,6 @@ void seq_decl_plugin::init() {
     m_sigs[_OP_REGEXP_EMPTY]      = alloc(psig, m, "re.nostr", 0, 0, nullptr, reT);
     m_sigs[_OP_REGEXP_FULL_CHAR]  = alloc(psig, m, "re.allchar", 0, 0, nullptr, reT);
     m_sigs[_OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
-    m_sigs[_OP_RE_UNROLL]         = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT);
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
@@ -772,11 +770,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         default:
             m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
         }
-        
-    case _OP_RE_UNROLL:
-        m_has_re = true;
-        match(*m_sigs[k], arity, domain, range, rng);
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {

src/ast/seq_decl_plugin.h

@@ -86,7 +86,6 @@ enum seq_op_kind {
     _OP_REGEXP_EMPTY,
     _OP_REGEXP_FULL_CHAR,
     _OP_SEQ_SKOLEM,
-    _OP_RE_UNROLL,
     LAST_SEQ_OP
 };
 
@@ -415,7 +414,6 @@ public:
         bool is_loop(expr const* n, expr*& body, unsigned& lo);
         bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi);
         bool is_loop(expr const* n, expr*& body, expr*& lo);
-        bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
     };
     str str;
     re  re;

src/smt/params/smt_params_helper.pyg

@@ -100,18 +100,13 @@ def_module_params(module_name='smt',
                           ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
                           ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
                           ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
-                          ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
-                          ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
-                          ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
                           ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'),
-                          ('str.regex_automata', BOOL, True, 'use automata-based reasoning for regular expressions (Z3str3 only)'),
                           ('str.regex_automata_difficulty_threshold', UINT, 1000, 'difficulty threshold for regex automata heuristics'),
                           ('str.regex_automata_intersection_difficulty_threshold', UINT, 1000, 'difficulty threshold for regex intersection heuristics'),
                           ('str.regex_automata_failed_automaton_threshold', UINT, 10, 'number of failed automaton construction attempts after which a full automaton is automatically built'),
                           ('str.regex_automata_failed_intersection_threshold', UINT, 10, 'number of failed automaton intersection attempts after which intersection is always computed'),
                           ('str.regex_automata_length_attempt_threshold', UINT, 10, 'number of length/path constraint attempts before checking unsatisfiability of regex terms'),
-                          ('str.fixed_length_models', BOOL, True, 'use fixed-length equation solver to construct models (Z3str3 only)'),
                           ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'),
                           ('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),

src/smt/params/theory_str_params.cpp

@@ -27,17 +27,12 @@ void theory_str_params::updt_params(params_ref const & _p) {
     m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
     m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
     m_StringConstantCache = p.str_string_constant_cache();
-    m_FiniteOverlapModels = p.str_finite_overlap_models();
-    m_UseBinarySearch = p.str_use_binary_search();
-    m_BinarySearchInitialUpperBound = p.str_binary_search_start();
     m_OverlapTheoryAwarePriority = p.str_overlap_priority();
-    m_RegexAutomata = p.str_regex_automata();
     m_RegexAutomata_DifficultyThreshold = p.str_regex_automata_difficulty_threshold();
     m_RegexAutomata_IntersectionDifficultyThreshold = p.str_regex_automata_intersection_difficulty_threshold();
     m_RegexAutomata_FailedAutomatonThreshold = p.str_regex_automata_failed_automaton_threshold();
     m_RegexAutomata_FailedIntersectionThreshold = p.str_regex_automata_failed_intersection_threshold();
     m_RegexAutomata_LengthAttemptThreshold = p.str_regex_automata_length_attempt_threshold();
-    m_FixedLengthModels = p.str_fixed_length_models();
     m_FixedLengthRefinement = p.str_fixed_length_refinement();
     m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex();
 }
@@ -52,15 +47,11 @@ void theory_str_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_UseFastLengthTesterCache);
     DISPLAY_PARAM(m_UseFastValueTesterCache);
     DISPLAY_PARAM(m_StringConstantCache);
-    DISPLAY_PARAM(m_UseBinarySearch);
-    DISPLAY_PARAM(m_BinarySearchInitialUpperBound);
     DISPLAY_PARAM(m_OverlapTheoryAwarePriority);
-    DISPLAY_PARAM(m_RegexAutomata);
     DISPLAY_PARAM(m_RegexAutomata_DifficultyThreshold);
     DISPLAY_PARAM(m_RegexAutomata_IntersectionDifficultyThreshold);
     DISPLAY_PARAM(m_RegexAutomata_FailedAutomatonThreshold);
     DISPLAY_PARAM(m_RegexAutomata_FailedIntersectionThreshold);
     DISPLAY_PARAM(m_RegexAutomata_LengthAttemptThreshold);
-    DISPLAY_PARAM(m_FixedLengthModels);
     DISPLAY_PARAM(m_FixedLengthNaiveCounterexamples);
 }

src/smt/params/theory_str_params.h

@@ -68,25 +68,8 @@ struct theory_str_params {
      */
     bool m_StringConstantCache;
 
-    /*
-     * If FiniteOverlapModels is set to true,
-     * arrangements that result in overlapping variables will generate a small number of models
-     * to test instead of completely giving up on the case.
-     */
-    bool m_FiniteOverlapModels;
-
-    bool m_UseBinarySearch;
-    unsigned m_BinarySearchInitialUpperBound;
-
     double m_OverlapTheoryAwarePriority;
 
-    /*
-     * If RegexAutomata is set to true,
-     * Z3str3 will use automata-based methods to reason about
-     * regular expression constraints.
-     */
-    bool m_RegexAutomata;
-
     /*
      * RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3
      * will not eagerly construct an automaton for a regular expression term.
@@ -116,13 +99,6 @@ struct theory_str_params {
      * before which we begin checking unsatisfiability of a regex term.
      */
     unsigned m_RegexAutomata_LengthAttemptThreshold;
-    
-    /*
-     * If FixedLengthModels is true, Z3str3 will use a fixed-length equation solver to construct models in final_check.
-     * If false, Z3str3 will use the legacy length tester and value tester procedure.
-     */
-    bool m_FixedLengthModels;
-
     /*
      * If FixedLengthRefinement is true and the fixed-length equation solver is enabled,
      * Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive
@@ -145,17 +121,12 @@ struct theory_str_params {
         m_UseFastLengthTesterCache(false),
         m_UseFastValueTesterCache(true),
         m_StringConstantCache(true),
-        m_FiniteOverlapModels(false),
-        m_UseBinarySearch(false),
-        m_BinarySearchInitialUpperBound(64),
         m_OverlapTheoryAwarePriority(-0.1),
-        m_RegexAutomata(true),
         m_RegexAutomata_DifficultyThreshold(1000),
         m_RegexAutomata_IntersectionDifficultyThreshold(1000),
         m_RegexAutomata_FailedAutomatonThreshold(10),
         m_RegexAutomata_FailedIntersectionThreshold(10),
         m_RegexAutomata_LengthAttemptThreshold(10),
-        m_FixedLengthModels(true),
         m_FixedLengthRefinement(false),
         m_FixedLengthNaiveCounterexamples(true)
     {

src/smt/theory_str.h

@@ -472,8 +472,6 @@ protected:
 
     int tmpStringVarCount;
     int tmpXorVarCount;
-    int tmpLenTestVarCount;
-    int tmpValTestVarCount;
     // obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
     std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
     bool avoidLoopCut;
@@ -484,41 +482,13 @@ protected:
 
     obj_hashtable<expr> variable_set;
     obj_hashtable<expr> internal_variable_set;
-    obj_hashtable<expr> regex_variable_set;
     std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
 
-    obj_hashtable<expr> internal_lenTest_vars;
-    obj_hashtable<expr> internal_valTest_vars;
-    obj_hashtable<expr> internal_unrollTest_vars;
-
-    obj_hashtable<expr> input_var_in_len;
-
-    obj_map<expr, unsigned int> fvar_len_count_map;
-    obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
-    obj_map<expr, expr*> lenTester_fvar_map;
-
-
-    obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
-
-    obj_map<expr, expr*> valueTester_fvar_map;
-
-    obj_map<expr, int_vector> val_range_map;
-
-    // This can't be an expr_ref_vector because the constructor is wrong,
-    // we would need to modify the allocator so we pass in ast_manager
-    obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
-    obj_map<expr, expr*> unroll_var_map;
-    obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
-
     expr_ref_vector contains_map;
 
     theory_str_contain_pair_bool_map_t contain_pair_bool_map;
     obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
 
-    // TBD: do a curried map for determinism.
-    std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
-    obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
-
     // regex automata
     scoped_ptr_vector<eautomaton> m_automata;
     ptr_vector<eautomaton> regex_automata;
@@ -554,11 +524,6 @@ protected:
     expr_ref_vector string_int_conversion_terms;
     obj_hashtable<expr> string_int_axioms;
 
-    // used when opt_FastLengthTesterCache is true
-    rational_map lengthTesterCache;
-    // used when opt_FastValueTesterCache is true
-    string_map valueTesterCache;
-
     string_map stringConstantCache;
     unsigned long totalCacheAccessCount;
     unsigned long cacheHitCount;
@@ -575,38 +540,6 @@ protected:
     expr * get_eqc_next(expr * n);
     app * get_ast(theory_var i);
 
-    // binary search heuristic data
-    struct binary_search_info {
-        rational lowerBound;
-        rational midPoint;
-        rational upperBound;
-        rational windowSize;
-
-        binary_search_info() : lowerBound(rational::zero()), midPoint(rational::zero()),
-                upperBound(rational::zero()), windowSize(rational::zero()) {}
-        binary_search_info(rational lower, rational mid, rational upper, rational windowSize) :
-            lowerBound(lower), midPoint(mid), upperBound(upper), windowSize(windowSize) {}
-
-        void calculate_midpoint() {
-            midPoint = floor(lowerBound + ((upperBound - lowerBound) / rational(2)) );
-        }
-    };
-    // maps a free string var to a stack of active length testers.
-    // can use binary_search_trail to record changes to this object
-    obj_map<expr, ptr_vector<expr> > binary_search_len_tester_stack;
-    // maps a length tester var to the *active* search window
-    obj_map<expr, binary_search_info> binary_search_len_tester_info;
-    // maps a free string var to the first length tester to be (re)used
-    obj_map<expr, expr*> binary_search_starting_len_tester;
-    // maps a length tester to the next length tester to be (re)used if the split is "low"
-    obj_map<expr, expr*> binary_search_next_var_low;
-    // maps a length tester to the next length tester to be (re)used if the split is "high"
-    obj_map<expr, expr*> binary_search_next_var_high;
-
-    // finite model finding data
-    // maps a finite model tester var to a list of variables that will be tested
-    obj_map<expr, ptr_vector<expr> > finite_model_test_varlists;
-
     // fixed length model construction
     expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver*
     expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these
@@ -657,10 +590,6 @@ protected:
     app * mk_int_var(std::string name);
     app_ref mk_nonempty_str_var();
     app * mk_internal_xor_var();
-    expr * mk_internal_valTest_var(expr * node, int len, int vTries);
-    app * mk_regex_rep_var();
-    app * mk_unroll_bound_var();
-    app * mk_unroll_test_var();
     void add_nonempty_constraint(expr * s);
 
     void instantiate_concat_axiom(enode * cat);
@@ -692,10 +621,6 @@ protected:
 
     expr * mk_RegexIn(expr * str, expr * regexp);
     void instantiate_axiom_RegexIn(enode * e);
-    app * mk_unroll(expr * n, expr * bound);
-    void process_unroll_eq_const_str(expr * unrollFunc, expr * constStr);
-    void unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr);
-    void process_concat_eq_unroll(expr * concat, expr * unroll);
 
     // regex automata and length-aware regex
     void solve_regex_automata();
@@ -812,26 +737,6 @@ protected:
     void classify_ast_by_type_in_positive_context(std::map<expr*, int> & varMap,
             std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
 
-    expr * mk_internal_lenTest_var(expr * node, int lTries);
-    expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue);
-    void process_free_var(std::map<expr*, int> & freeVar_map);
-    expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries);
-    expr * gen_free_var_options(expr * freeVar, expr * len_indicator,
-            zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr);
-    expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
-            zstring lenStr, int tries);
-    void print_value_tester_list(svector<std::pair<int, expr*> > & testerList);
-    bool get_next_val_encode(int_vector & base, int_vector & next);
-    zstring gen_val_string(int len, int_vector & encoding);
-
-    // binary search heuristic
-    expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue);
-    expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits);
-
-    bool free_var_attempt(expr * nn1, expr * nn2);
-    void more_len_tests(expr * lenTester, zstring lenTesterValue);
-    void more_value_tests(expr * valTester, zstring valTesterValue);
-
     expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node);
     expr * getMostLeftNodeInConcat(expr * node);
     expr * getMostRightNodeInConcat(expr * node);
@@ -858,18 +763,6 @@ protected:
     bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
     bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity);
 
-    // strRegex
-
-    void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
-    void get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
-    void gen_assign_unroll_reg(std::set<expr*> & unrolls);
-    expr * gen_assign_unroll_Str2Reg(expr * n, std::set<expr*> & unrolls);
-    expr * gen_unroll_conditional_options(expr * var, std::set<expr*> & unrolls, zstring lcmStr);
-    expr * gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h);
-    void reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items);
-    void check_regex_in(expr * nn1, expr * nn2);
-    zstring get_std_regex_str(expr * r);
-
     void dump_assignments();
     void initialize_charset();
 
@@ -884,9 +777,6 @@ protected:
     // TESTING
     void refresh_theory_var(expr * e);
 
-    expr_ref set_up_finite_model_test(expr * lhs, expr * rhs);
-    void finite_model_test(expr * v, expr * c);
-
 public:
     theory_str(ast_manager & m, theory_str_params const & params);
     ~theory_str() override;