z3str3: add bitvector model construction algorithm

src/smt/params/smt_params.cpp

@@ -62,6 +62,7 @@ void smt_params::updt_params(params_ref const & p) {
     theory_pb_params::updt_params(p);
     // theory_array_params::updt_params(p);
     theory_datatype_params::updt_params(p);
+    theory_str_params::updt_params(p);
     updt_local_params(p);
 }
 
@@ -81,6 +82,7 @@ void smt_params::display(std::ostream & out) const {
     theory_bv_params::display(out);
     theory_pb_params::display(out);
     theory_datatype_params::display(out);
+    theory_str_params::display(out);
 
     DISPLAY_PARAM(m_display_proof);
     DISPLAY_PARAM(m_display_dot_proof);
@@ -139,6 +141,7 @@ void smt_params::display(std::ostream & out) const {
 
     DISPLAY_PARAM(m_smtlib_dump_lemmas);
     DISPLAY_PARAM(m_logic);
+    DISPLAY_PARAM(m_string_solver);
 
     DISPLAY_PARAM(m_profile_res_sub);
     DISPLAY_PARAM(m_display_bool_var2expr);

src/smt/params/smt_params_helper.pyg

@@ -90,6 +90,8 @@ def_module_params(module_name='smt',
                           ('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)'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),

src/smt/params/theory_str_params.cpp

@@ -37,4 +37,28 @@ void theory_str_params::updt_params(params_ref const & _p) {
     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();
+}
+
+#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+
+void theory_str_params::display(std::ostream & out) const {
+    DISPLAY_PARAM(m_StrongArrangements);
+    DISPLAY_PARAM(m_AggressiveLengthTesting);
+    DISPLAY_PARAM(m_AggressiveValueTesting);
+    DISPLAY_PARAM(m_AggressiveUnrollTesting);
+    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);
 }

src/smt/params/theory_str_params.h

@@ -116,6 +116,19 @@ 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
+     * reductions to fixed-length formulas.
+     */
+    bool m_FixedLengthRefinement;
 
     theory_str_params(params_ref const & p = params_ref()):
         m_StrongArrangements(true),
@@ -134,12 +147,15 @@ struct theory_str_params {
         m_RegexAutomata_IntersectionDifficultyThreshold(1000),
         m_RegexAutomata_FailedAutomatonThreshold(10),
         m_RegexAutomata_FailedIntersectionThreshold(10),
-        m_RegexAutomata_LengthAttemptThreshold(10)
+        m_RegexAutomata_LengthAttemptThreshold(10),
+        m_FixedLengthModels(true),
+        m_FixedLengthRefinement(false)
     {
         updt_params(p);
     }
 
     void updt_params(params_ref const & p);
+    void display(std::ostream & out) const;
 };
 
 #endif /* THEORY_STR_PARAMS_H */

src/smt/theory_str.h

@@ -31,10 +31,12 @@
 #include "smt/params/theory_str_params.h"
 #include "smt/smt_model_generator.h"
 #include "smt/smt_arith_value.h"
+#include "smt/smt_kernel.h"
 #include<set>
 #include<stack>
 #include<vector>
 #include<map>
+#include<functional>
 
 namespace smt {
 
@@ -106,6 +108,8 @@ public:
     }
 };
 
+struct c_hash { unsigned operator()(char u) const { return (unsigned)u; } };
+struct c_eq { bool operator()(char u1, char u2) const { return u1 == u2; } };
 
 class nfa {
 protected:
@@ -216,6 +220,113 @@ public:
     }
 };
 
+class char_union_find {
+    unsigned_vector   m_find;
+    unsigned_vector   m_size;
+    unsigned_vector   m_next;
+
+    integer_set char_const_set;
+
+    u_map<svector<expr*> > m_justification; // representative -> list of formulas justifying EQC
+
+    void ensure_size(unsigned v) {
+        while (v >= get_num_vars()) {
+            mk_var();
+        }
+    }
+ public:
+    unsigned mk_var() {
+        unsigned r = m_find.size();
+        m_find.push_back(r);
+        m_size.push_back(1);
+        m_next.push_back(r);
+        return r;
+    }
+    unsigned get_num_vars() const { return m_find.size(); }
+    void mark_as_char_const(unsigned r) {
+        char_const_set.insert((int)r);
+    }
+    bool is_char_const(unsigned r) {
+        return char_const_set.contains((int)r);
+    }
+
+    unsigned find(unsigned v) const {
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        while (true) {
+            unsigned new_v = m_find[v];
+            if (new_v == v)
+                return v;
+            v = new_v;
+        }
+    }
+
+    unsigned next(unsigned v) const {
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        return m_next[v];
+    }
+
+    bool is_root(unsigned v) const {
+        return v >= get_num_vars() || m_find[v] == v;
+    }
+
+    svector<expr*> get_justification(unsigned v) {
+        unsigned r = find(v);
+        svector<expr*> retval;
+        if (m_justification.find(r, retval)) {
+            return retval;
+        } else {
+            return svector<expr*>();
+        }
+    }
+
+    void merge(unsigned v1, unsigned v2, expr * justification) {
+        unsigned r1 = find(v1);
+        unsigned r2 = find(v2);
+        if (r1 == r2)
+            return;
+        ensure_size(v1);
+        ensure_size(v2);
+        // swap r1 and r2 if:
+        // 1. EQC of r1 is bigger than EQC of r2
+        // 2. r1 is a character constant and r2 is not.
+        // this maintains the invariant that if a character constant is in an eqc then it is the root of that eqc
+        if (m_size[r1] > m_size[r2] || (is_char_const(r1) && !is_char_const(r2))) {
+            std::swap(r1, r2);
+        }
+        m_find[r1] = r2;
+        m_size[r2] += m_size[r1];
+        std::swap(m_next[r1], m_next[r2]);
+
+        if (m_justification.contains(r1)) {
+            // add r1's justifications to r2
+            if (!m_justification.contains(r2)) {
+                m_justification.insert(r2, m_justification[r1]);
+            } else {
+                m_justification[r2].append(m_justification[r1]);
+            }
+            m_justification.remove(r1);
+        }
+        if (justification != nullptr) {
+            if (!m_justification.contains(r2)) {
+                m_justification.insert(r2, svector<expr*>());
+            }
+            m_justification[r2].push_back(justification);
+        }
+    }
+
+    void reset() {
+        m_find.reset();
+        m_next.reset();
+        m_size.reset();
+        char_const_set.reset();
+        m_justification.reset();
+    }
+};
+
 class theory_str : public theory {
     struct T_cut
     {
@@ -238,6 +349,17 @@ class theory_str : public theory {
     };
     typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
 
+    struct stats {
+        stats() { reset(); }
+        void reset() { memset(this, 0, sizeof(stats)); }
+        unsigned m_refine_eq;
+        unsigned m_refine_neq;
+        unsigned m_refine_f;
+        unsigned m_refine_nf;
+        unsigned m_solved_by;
+        unsigned m_fixed_length_iterations;
+    };
+
 protected:
     theory_str_params const & m_params;
 
@@ -484,6 +606,21 @@ protected:
     // 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
+    obj_map<expr, unsigned> fixed_length_used_len_terms; // constraints used in generating fixed length model
+    obj_map<expr, ptr_vector<expr> > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver*
+    obj_map<expr, ptr_vector<expr> > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver*
+    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;
+
 protected:
     void assert_axiom(expr * e);
     void assert_implication(expr * premise, expr * conclusion);
@@ -529,6 +666,14 @@ protected:
     void instantiate_basic_string_axioms(enode * str);
     void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
 
+    // for count abstraction and refinement
+    expr* refine(expr* lhs, expr* rhs, rational offset);
+    expr* refine_eq(expr* lhs, expr* rhs, unsigned offset);
+    expr* refine_dis(expr* lhs, expr* rhs);
+    expr* refine_function(expr* f);
+    bool flatten(expr* ex, expr_ref_vector & flat);
+    unsigned get_refine_length(expr* ex, expr_ref_vector& extra_deps);
+
     void instantiate_axiom_CharAt(enode * e);
     void instantiate_axiom_prefixof(enode * e);
     void instantiate_axiom_suffixof(enode * e);
@@ -696,6 +841,19 @@ protected:
     bool finalcheck_str2int(app * a);
     bool finalcheck_int2str(app * a);
 
+    lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
+            obj_map<expr, zstring> &model, expr_ref_vector &cex);
+    ptr_vector<expr> fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term);
+    bool fixed_length_get_len_value(expr * e, rational & val);
+    bool fixed_length_reduce_eq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
+    bool fixed_length_reduce_diseq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
+    bool fixed_length_reduce_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+    bool fixed_length_reduce_negative_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+    bool fixed_length_reduce_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+    bool fixed_length_reduce_negative_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+    bool fixed_length_reduce_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+    bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
+
     // strRegex
 
     void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
@@ -732,6 +890,8 @@ public:
     char const * get_name() const override { return "seq"; }
     void display(std::ostream & out) const override;
 
+    void collect_statistics(::statistics & st) const override;
+
     bool overlapping_variables_detected() const { return loopDetected; }
 
     th_trail_stack& get_trail_stack() { return m_trail_stack; }