Merge pull request #907 from mtrberzi/release-1.0

theory_str for Z3 based on the Z3str2 framework

src/ast/rewriter/rewriter.txt

@@ -7,6 +7,7 @@ The following classes implement theory specific rewriting rules:
   - array_rewriter
   - datatype_rewriter
   - fpa_rewriter
+  - seq_rewriter
 
 Each of them provide the method
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)

src/parsers/smt2/smt2parser.cpp

@@ -66,7 +66,7 @@ namespace smt2 {
 
         scoped_ptr<bv_util>               m_bv_util;
         scoped_ptr<arith_util>            m_arith_util;
-        scoped_ptr<seq_util>              m_seq_util;
+        scoped_ptr<seq_util>              m_seq_util;      
         scoped_ptr<pattern_validator>     m_pattern_validator;
         scoped_ptr<var_shifter>           m_var_shifter;
 

src/smt/params/smt_params.cpp

@@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_restart_factor = p.restart_factor();
     m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
     m_theory_case_split = p.theory_case_split();
+    m_theory_aware_branching = p.theory_aware_branching();
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter

src/smt/params/smt_params.h

@@ -25,6 +25,7 @@ Revision History:
 #include"theory_arith_params.h"
 #include"theory_array_params.h"
 #include"theory_bv_params.h"
+#include"theory_str_params.h"
 #include"theory_pb_params.h"
 #include"theory_datatype_params.h"
 #include"preprocessor_params.h"
@@ -76,6 +77,7 @@ struct smt_params : public preprocessor_params,
                     public theory_arith_params, 
                     public theory_array_params, 
                     public theory_bv_params,
+                    public theory_str_params,
                     public theory_pb_params,
                     public theory_datatype_params {
     bool             m_display_proof;
@@ -111,6 +113,7 @@ struct smt_params : public preprocessor_params,
     unsigned            m_rel_case_split_order;
     bool                m_lookahead_diseq;
     bool                m_theory_case_split;
+    bool                m_theory_aware_branching;
 
     // -----------------------------------
     //
@@ -248,6 +251,8 @@ struct smt_params : public preprocessor_params,
         m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
         m_rel_case_split_order(0),
         m_lookahead_diseq(false),
+        m_theory_case_split(false),
+        m_theory_aware_branching(false),
         m_delay_units(false),
         m_delay_units_threshold(32),
         m_theory_resolve(false),
@@ -290,7 +295,7 @@ struct smt_params : public preprocessor_params,
         m_check_at_labels(false),
         m_dump_goal_as_smt(false),
         m_auto_config(true),
-        m_string_solver(symbol("seq")){
+        m_string_solver(symbol("auto")){
         updt_local_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -64,6 +64,18 @@ def_module_params(module_name='smt',
                           ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
                           ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('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'),
+                          ('str.aggressive_unroll_testing', BOOL, True, 'prioritize testing concrete regex unroll counts over generating more options'),
+                          ('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'),
                           ('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

@@ -0,0 +1,34 @@
+/*++
+Module Name:
+
+    theory_str_params.cpp
+
+Abstract:
+
+    Parameters for string theory plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2016-12-13
+
+Revision History:
+
+--*/
+
+#include"theory_str_params.h"
+#include"smt_params_helper.hpp"
+
+void theory_str_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_StrongArrangements = p.str_strong_arrangements();
+    m_AggressiveLengthTesting = p.str_aggressive_length_testing();
+    m_AggressiveValueTesting = p.str_aggressive_value_testing();
+    m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
+    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();
+}

src/smt/params/theory_str_params.h

@@ -0,0 +1,102 @@
+/*++
+Module Name:
+
+    theory_str_params.h
+
+Abstract:
+
+    Parameters for string theory plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2016-12-13
+
+Revision History:
+
+--*/
+
+#ifndef THEORY_STR_PARAMS_H
+#define THEORY_STR_PARAMS_H
+
+#include"params.h"
+
+struct theory_str_params {
+    /*
+     * If AssertStrongerArrangements is set to true,
+     * the implications that would normally be asserted during arrangement generation
+     * will instead be asserted as equivalences.
+     * This is a stronger version of the standard axiom.
+     * The Z3str2 axioms can be simulated by setting this to false.
+     */
+    bool m_StrongArrangements;
+
+    /*
+     * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
+     * to prioritize trying concrete length options over choosing the "more" option.
+     */
+    bool m_AggressiveLengthTesting;
+
+    /*
+     * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
+     * to prioritize trying concrete value options over choosing the "more" option.
+     */
+    bool m_AggressiveValueTesting;
+
+    /*
+     * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
+     * to prioritize trying concrete unroll counts over choosing the "more" option.
+     */
+    bool m_AggressiveUnrollTesting;
+
+    /*
+     * If UseFastLengthTesterCache is set to true,
+     * length tester terms will not be generated from scratch each time they are needed,
+     * but will be saved in a map and looked up.
+     */
+    bool m_UseFastLengthTesterCache;
+
+    /*
+     * If UseFastValueTesterCache is set to true,
+     * value tester terms will not be generated from scratch each time they are needed,
+     * but will be saved in a map and looked up.
+     */
+    bool m_UseFastValueTesterCache;
+
+    /*
+     * If StringConstantCache is set to true,
+     * all string constants in theory_str generated from anywhere will be cached and saved.
+     */
+    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;
+
+    theory_str_params(params_ref const & p = params_ref()):
+        m_StrongArrangements(true),
+        m_AggressiveLengthTesting(false),
+        m_AggressiveValueTesting(false),
+        m_AggressiveUnrollTesting(true),
+        m_UseFastLengthTesterCache(false),
+        m_UseFastValueTesterCache(true),
+        m_StringConstantCache(true),
+        m_FiniteOverlapModels(false),
+        m_UseBinarySearch(false),
+        m_BinarySearchInitialUpperBound(64),
+        m_OverlapTheoryAwarePriority(-0.1)
+    {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+};
+
+#endif /* THEORY_STR_PARAMS_H */

src/smt/smt_context.cpp

@@ -2448,8 +2448,9 @@ namespace smt {
         
         ptr_vector<theory>::iterator it  = m_theory_set.begin();
         ptr_vector<theory>::iterator end = m_theory_set.end();
-        for (; it != end; ++it)
+        for (; it != end; ++it) {
             (*it)->pop_scope_eh(num_scopes);
+        }
 
         del_justifications(m_justifications, s.m_justifications_lim);
 
@@ -3013,6 +3014,10 @@ namespace smt {
         }
     }
 
+    void context::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
+        m_case_split_queue->add_theory_aware_branching_info(v, priority, phase);
+    }
+
     void context::undo_th_case_split(literal l) {
         m_all_th_case_split_literals.remove(l.index());
         if (m_literal2casesplitsets.contains(l.index())) {
@@ -3022,10 +3027,6 @@ namespace smt {
         }
     }
 
-    void context::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
-        m_case_split_queue->add_theory_aware_branching_info(v, priority, phase);
-    }
-
     bool context::propagate_th_case_split(unsigned qhead) {
         if (m_all_th_case_split_literals.empty())
             return true;
@@ -3034,7 +3035,7 @@ namespace smt {
         // not counting any literals that get assigned by this method
         // this relies on bcp() to give us its old m_qhead and therefore
         // bcp() should always be called before this method
-
+	
         unsigned assigned_literal_end = m_assigned_literals.size();
         for (; qhead < assigned_literal_end; ++qhead) {
             literal l = m_assigned_literals[qhead];

src/smt/smt_setup.cpp

@@ -33,6 +33,7 @@ Revision History:
 #include"theory_seq.h"
 #include"theory_pb.h"
 #include"theory_fpa.h"
+#include"theory_str.h"
 
 namespace smt {
 
@@ -205,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) {
@@ -705,7 +706,8 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        setup_seq();
+        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+        m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
     }
 
     bool is_arith(static_features const & st) {
@@ -853,7 +855,8 @@ namespace smt {
     }
 
     void setup::setup_str() {
-        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+        setup_arith();
+        m_context.register_plugin(alloc(theory_str, m_manager, m_params));
     }
 
     void setup::setup_seq() {

src/smt/smt_theory.h

@@ -186,13 +186,13 @@ namespace smt {
         }
 
         /**
-           \brief This method is called from smt_context when an unsat core is generated.
+           \brief This method is called from the smt_context when an unsat core is generated.
            The theory may change the answer to UNKNOWN by returning l_undef from this method.
         */
         virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
             return l_false;
         }
-
+	
         /**
            \brief This method is invoked before the search starts.
         */

src/smt/theory_str.h

@@ -0,0 +1,652 @@
+/*++
+Module Name:
+
+    theory_str.h
+
+Abstract:
+
+    String Theory Plugin
+
+Author:
+
+    Murphy Berzish and Yunhui Zheng
+
+Revision History:
+
+--*/
+#ifndef _THEORY_STR_H_
+#define _THEORY_STR_H_
+
+#include"smt_theory.h"
+#include"theory_str_params.h"
+#include"trail.h"
+#include"th_rewriter.h"
+#include"value_factory.h"
+#include"smt_model_generator.h"
+#include"arith_decl_plugin.h"
+#include<set>
+#include<stack>
+#include<vector>
+#include<map>
+#include"seq_decl_plugin.h"
+#include"union_find.h"
+
+namespace smt {
+
+    typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
+
+    class str_value_factory : public value_factory {
+        seq_util u;
+        symbol_set m_strings;
+        std::string delim;
+        unsigned m_next;
+    public:
+        str_value_factory(ast_manager & m, family_id fid) :
+            value_factory(m, fid),
+            u(m), delim("!"), m_next(0) {}
+        virtual ~str_value_factory() {}
+        virtual expr * get_some_value(sort * s) {
+            return u.str.mk_string(symbol("some value"));
+        }
+        virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+            v1 = u.str.mk_string(symbol("value 1"));
+            v2 = u.str.mk_string(symbol("value 2"));
+            return true;
+        }
+        virtual expr * get_fresh_value(sort * s) {
+            if (u.is_string(s)) {
+                while (true) {
+                    std::ostringstream strm;
+                    strm << delim << std::hex << (m_next++) << std::dec << delim;
+                    symbol sym(strm.str().c_str());
+                    if (m_strings.contains(sym)) continue;
+                    m_strings.insert(sym);
+                    return u.str.mk_string(sym);
+                }
+            }
+            sort* seq = 0;
+            if (u.is_re(s, seq)) {
+                expr* v0 = get_fresh_value(seq);
+                return u.re.mk_to_re(v0);
+            }
+            TRACE("t_str", tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
+            UNREACHABLE(); return NULL;
+        }
+        virtual void register_value(expr * n) { /* Ignore */ }
+    };
+
+    // rather than modify obj_pair_map I inherit from it and add my own helper methods
+    class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
+    public:
+        expr * operator[](std::pair<expr*, expr*> key) const {
+            expr * value;
+            bool found = this->find(key.first, key.second, value);
+            if (found) {
+                return value;
+            } else {
+                TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
+                return NULL;
+            }
+        }
+
+        bool contains(std::pair<expr*, expr*> key) const {
+            expr * unused;
+            return this->find(key.first, key.second, unused);
+        }
+    };
+
+    template<typename Ctx>
+    class binary_search_trail : public trail<Ctx> {
+        obj_map<expr, ptr_vector<expr> > & target;
+        expr * entry;
+    public:
+        binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
+            target(target), entry(entry) {}
+        virtual ~binary_search_trail() {}
+        virtual void undo(Ctx & ctx) {
+            TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
+            if (target.contains(entry)) {
+                if (!target[entry].empty()) {
+                    target[entry].pop_back();
+                } else {
+                    TRACE("t_str_binary_search", tout << "WARNING: attempt to remove length tester from an empty stack" << std::endl;);
+                }
+            } else {
+                TRACE("t_str_binary_search", tout << "WARNING: attempt to access length tester map via invalid key" << std::endl;);
+            }
+        }
+    };
+
+
+    class nfa {
+    protected:
+        bool m_valid;
+        unsigned m_next_id;
+
+        unsigned next_id() {
+            unsigned retval = m_next_id;
+            ++m_next_id;
+            return retval;
+        }
+
+        unsigned m_start_state;
+        unsigned m_end_state;
+
+        std::map<unsigned, std::map<char, unsigned> > transition_map;
+        std::map<unsigned, std::set<unsigned> > epsilon_map;
+
+        void make_transition(unsigned start, char symbol, unsigned end) {
+            transition_map[start][symbol] = end;
+        }
+
+        void make_epsilon_move(unsigned start, unsigned end) {
+            epsilon_map[start].insert(end);
+        }
+
+        // Convert a regular expression to an e-NFA using Thompson's construction
+        void convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u);
+
+    public:
+        nfa(seq_util & u, expr * e)
+    : m_valid(true), m_next_id(0), m_start_state(0), m_end_state(0) {
+            convert_re(e, m_start_state, m_end_state, u);
+        }
+
+        nfa() : m_valid(false), m_next_id(0), m_start_state(0), m_end_state(0) {}
+
+        bool is_valid() const {
+            return m_valid;
+        }
+
+        void epsilon_closure(unsigned start, std::set<unsigned> & closure);
+
+        bool matches(zstring input);
+    };
+
+    class theory_str : public theory {
+        struct T_cut
+        {
+            int level;
+            std::map<expr*, int> vars;
+
+            T_cut() {
+              level = -100;
+            }
+        };
+
+        typedef trail_stack<theory_str> th_trail_stack;
+        typedef union_find<theory_str> th_union_find;
+
+        typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
+        struct zstring_hash_proc {
+            unsigned operator()(zstring const & s) const {
+            	return string_hash(s.encode().c_str(), static_cast<unsigned>(s.length()), 17);
+            }
+        };
+        typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
+
+    protected:
+        theory_str_params const & m_params;
+
+        /*
+         * Setting EagerStringConstantLengthAssertions to true allows some methods,
+         * in particular internalize_term(), to add
+         * length assertions about relevant string constants.
+         * Note that currently this should always be set to 'true', or else *no* length assertions
+         * will be made about string constants.
+         */
+        bool opt_EagerStringConstantLengthAssertions;
+
+        /*
+         * If VerifyFinalCheckProgress is set to true, continuing after final check is invoked
+         * without asserting any new axioms is considered a bug and will throw an exception.
+         */
+        bool opt_VerifyFinalCheckProgress;
+
+        /*
+         * This constant controls how eagerly we expand unrolls in unbounded regex membership tests.
+         */
+        int opt_LCMUnrollStep;
+
+        /*
+         * If NoQuickReturn_IntegerTheory is set to true,
+         * integer theory integration checks that assert axioms
+         * will not return from the function after asserting their axioms.
+         * The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect.
+         */
+        bool opt_NoQuickReturn_IntegerTheory;
+
+        /*
+         * If DisableIntegerTheoryIntegration is set to true,
+         * ALL calls to the integer theory integration methods
+         * (get_value, get_len_value, lower_bound, upper_bound)
+         * will ignore what the arithmetic solver believes about length terms,
+         * and will return no information.
+         *
+         * This reduces performance significantly, but can be useful to enable
+         * if it is suspected that string-integer integration, or the arithmetic solver itself,
+         * might have a bug.
+         *
+         * The default behaviour of Z3str2 is to set this to 'false'.
+         */
+        bool opt_DisableIntegerTheoryIntegration;
+
+        /*
+         * If DeferEQCConsistencyCheck is set to true,
+         * expensive calls to new_eq_check() will be deferred until final check,
+         * at which time the consistency of *all* string equivalence classes will be validated.
+         */
+        bool opt_DeferEQCConsistencyCheck;
+
+        /*
+         * If CheckVariableScope is set to true,
+         * pop_scope_eh() and final_check_eh() will run extra checks
+         * to determine whether the current assignment
+         * contains references to any internal variables that are no longer in scope.
+         */
+        bool opt_CheckVariableScope;
+
+        /*
+         * If ConcatOverlapAvoid is set to true,
+         * the check to simplify Concat = Concat in handle_equality() will
+         * avoid simplifying wrt. pairs of Concat terms that will immediately
+         * result in an overlap. (false = Z3str2 behaviour)
+         */
+        bool opt_ConcatOverlapAvoid;
+
+        bool search_started;
+        arith_util m_autil;
+        seq_util u;
+        int sLevel;
+
+        bool finalCheckProgressIndicator;
+
+        expr_ref_vector m_trail; // trail for generated terms
+
+        str_value_factory * m_factory;
+
+        // terms we couldn't go through set_up_axioms() with because they weren't internalized
+        expr_ref_vector m_delayed_axiom_setup_terms;
+
+        ptr_vector<enode> m_basicstr_axiom_todo;
+        svector<std::pair<enode*,enode*> > m_str_eq_todo;
+        ptr_vector<enode> m_concat_axiom_todo;
+        ptr_vector<enode> m_string_constant_length_todo;
+        ptr_vector<enode> m_concat_eval_todo;
+
+        // enode lists for library-aware/high-level string terms (e.g. substr, contains)
+        ptr_vector<enode> m_library_aware_axiom_todo;
+
+        // hashtable of all exprs for which we've already set up term-specific axioms --
+        // this prevents infinite recursive descent with respect to axioms that
+        // include an occurrence of the term for which axioms are being generated
+        obj_hashtable<expr> axiomatized_terms;
+
+        int tmpStringVarCount;
+        int tmpXorVarCount;
+        int tmpLenTestVarCount;
+        int tmpValTestVarCount;
+        std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
+
+        bool avoidLoopCut;
+        bool loopDetected;
+        obj_map<expr, std::stack<T_cut*> > cut_var_map;
+        expr_ref m_theoryStrOverlapAssumption_term;
+
+        obj_hashtable<expr> variable_set;
+        obj_hashtable<expr> internal_variable_set;
+        obj_hashtable<expr> regex_variable_set;
+        std::map<int, std::set<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;
+        std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+        obj_map<expr, expr*> lenTester_fvar_map;
+
+        std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
+        std::map<expr*, expr*> valueTester_fvar_map;
+
+        std::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
+        std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
+        std::map<expr*, expr*> unroll_var_map;
+        std::map<std::pair<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, obj_pair_set<expr, expr> > contain_pair_idx_map;
+        std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
+
+        std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
+        std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
+
+        std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+
+        char * char_set;
+        std::map<char, int> charSetLookupTable;
+        int charSetSize;
+
+        obj_pair_map<expr, expr, expr*> concat_astNode_map;
+
+        // all (str.to-int) and (int.to-str) terms
+        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;
+        unsigned long cacheMissCount;
+
+        // cache mapping each string S to Length(S)
+        obj_map<expr, app*> length_ast_map;
+
+        th_union_find m_find;
+        th_trail_stack m_trail_stack;
+        theory_var get_var(expr * n) const;
+        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;
+    protected:
+        void assert_axiom(expr * e);
+        void assert_implication(expr * premise, expr * conclusion);
+        expr * rewrite_implication(expr * premise, expr * conclusion);
+
+        expr * mk_string(zstring const& str);
+        expr * mk_string(const char * str);
+
+        app * mk_strlen(expr * e);
+        expr * mk_concat(expr * n1, expr * n2);
+        expr * mk_concat_const_str(expr * n1, expr * n2);
+        app * mk_contains(expr * haystack, expr * needle);
+        app * mk_indexof(expr * haystack, expr * needle);
+
+        literal mk_literal(expr* _e);
+        app * mk_int(int n);
+        app * mk_int(rational & q);
+
+        void check_and_init_cut_var(expr * node);
+        void add_cut_info_one_node(expr * baseNode, int slevel, expr * node);
+        void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode);
+        bool has_self_cut(expr * n1, expr * n2);
+
+        // for ConcatOverlapAvoid
+        bool will_result_in_overlap(expr * lhs, expr * rhs);
+
+        void track_variable_scope(expr * var);
+        app * mk_str_var(std::string name);
+        app * mk_int_var(std::string name);
+        app * 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);
+        void try_eval_concat(enode * cat);
+        void instantiate_basic_string_axioms(enode * str);
+        void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
+
+        void instantiate_axiom_CharAt(enode * e);
+        void instantiate_axiom_prefixof(enode * e);
+        void instantiate_axiom_suffixof(enode * e);
+        void instantiate_axiom_Contains(enode * e);
+        void instantiate_axiom_Indexof(enode * e);
+        void instantiate_axiom_Indexof2(enode * e);
+        void instantiate_axiom_LastIndexof(enode * e);
+        void instantiate_axiom_Substr(enode * e);
+        void instantiate_axiom_Replace(enode * e);
+        void instantiate_axiom_str_to_int(enode * e);
+        void instantiate_axiom_int_to_str(enode * e);
+
+        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);
+
+        void set_up_axioms(expr * ex);
+        void handle_equality(expr * lhs, expr * rhs);
+
+        app * mk_value_helper(app * n);
+        expr * get_eqc_value(expr * n, bool & hasEqcValue);
+        expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
+        bool in_same_eqc(expr * n1, expr * n2);
+        expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
+
+        bool get_value(expr* e, rational& val) const;
+        bool get_len_value(expr* e, rational& val);
+        bool lower_bound(expr* _e, rational& lo);
+        bool upper_bound(expr* _e, rational& hi);
+
+        bool can_two_nodes_eq(expr * n1, expr * n2);
+        bool can_concat_eq_str(expr * concat, zstring& str);
+        bool can_concat_eq_concat(expr * concat1, expr * concat2);
+        bool check_concat_len_in_eqc(expr * concat);
+        bool check_length_consistency(expr * n1, expr * n2);
+        bool check_length_const_string(expr * n1, expr * constStr);
+        bool check_length_eq_var_concat(expr * n1, expr * n2);
+        bool check_length_concat_concat(expr * n1, expr * n2);
+        bool check_length_concat_var(expr * concat, expr * var);
+        bool check_length_var_var(expr * var1, expr * var2);
+        void check_contain_in_new_eq(expr * n1, expr * n2);
+        void check_contain_by_eqc_val(expr * varNode, expr * constNode);
+        void check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass);
+        void check_contain_by_eq_nodes(expr * n1, expr * n2);
+        bool in_contain_idx_map(expr * n);
+        void compute_contains(std::map<expr*, expr*> & varAliasMap,
+                std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
+                std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
+        expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
+        void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
+                std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
+                std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
+                std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+        void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+        void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
+            std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+        bool is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec);
+
+        void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
+        expr * simplify_concat(expr * node);
+
+        void simplify_parent(expr * nn, expr * eq_str);
+
+        void simplify_concat_equality(expr * lhs, expr * rhs);
+        void solve_concat_eq_str(expr * concat, expr * str);
+
+        void infer_len_concat_equality(expr * nn1, expr * nn2);
+        bool infer_len_concat(expr * n, rational & nLen);
+        void infer_len_concat_arg(expr * n, rational len);
+
+        bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
+        bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
+        bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);
+        bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2);
+        bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2);
+        bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2);
+
+        void process_concat_eq_type1(expr * concatAst1, expr * concatAst2);
+        void process_concat_eq_type2(expr * concatAst1, expr * concatAst2);
+        void process_concat_eq_type3(expr * concatAst1, expr * concatAst2);
+        void process_concat_eq_type4(expr * concatAst1, expr * concatAst2);
+        void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
+        void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
+
+        void print_cut_var(expr * node, std::ofstream & xout);
+
+        void generate_mutual_exclusion(expr_ref_vector & exprs);
+        void add_theory_aware_branching_info(expr * term, double priority, lbool phase);
+
+        bool new_eq_check(expr * lhs, expr * rhs);
+        void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
+
+        int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
+        		std::map<expr*, std::set<expr*> > & unrollGroupMap, std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
+        void trace_ctx_dep(std::ofstream & tout,
+                std::map<expr*, expr*> & aliasIndexMap,
+                std::map<expr*, expr*> & var_eq_constStr_map,
+                std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
+				std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
+                std::map<expr*, expr*> & concat_eq_constStr_map,
+                std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map,
+				std::map<expr*, std::set<expr*> > & unrollGroupMap);
+
+        void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,
+        		std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
+        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);
+        void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
+        void get_concats_in_eqc(expr * n, std::set<expr*> & concats);
+        void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
+        expr * eval_concat(expr * n1, expr * n2);
+
+        bool finalcheck_str2int(app * a);
+        bool finalcheck_int2str(app * a);
+
+        // 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();
+
+        void check_variable_scope();
+        void recursive_check_variable_scope(expr * ex);
+
+        void collect_var_concat(expr * node, std::set<expr*> & varSet, std::set<expr*> & concatSet);
+        bool propagate_length(std::set<expr*> & varSet, std::set<expr*> & concatSet, std::map<expr*, int> & exprLenMap);
+        void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
+        bool propagate_length_within_eqc(expr * var);
+
+        // 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);
+        virtual ~theory_str();
+
+        virtual char const * get_name() const { return "seq"; }
+        virtual void display(std::ostream & out) const;
+
+        bool overlapping_variables_detected() const { return loopDetected; }
+
+        th_trail_stack& get_trail_stack() { return m_trail_stack; }
+        void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
+        void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
+        void unmerge_eh(theory_var v1, theory_var v2) {}
+    protected:
+        virtual bool internalize_atom(app * atom, bool gate_ctx);
+        virtual bool internalize_term(app * term);
+        virtual enode* ensure_enode(expr* e);
+        virtual theory_var mk_var(enode * n);
+
+        virtual void new_eq_eh(theory_var, theory_var);
+        virtual void new_diseq_eh(theory_var, theory_var);
+
+        virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager(), m_params); }
+        virtual void init_search_eh();
+        virtual void add_theory_assumptions(expr_ref_vector & assumptions);
+        virtual lbool validate_unsat_core(expr_ref_vector & unsat_core);
+        virtual void relevant_eh(app * n);
+        virtual void assign_eh(bool_var v, bool is_true);
+        virtual void push_scope_eh();
+        virtual void pop_scope_eh(unsigned num_scopes);
+        virtual void reset_eh();
+
+        virtual bool can_propagate();
+        virtual void propagate();
+
+        virtual final_check_status final_check_eh();
+        virtual void attach_new_th_var(enode * n);
+
+        virtual void init_model(model_generator & m);
+        virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+        virtual void finalize_model(model_generator & mg);
+    };
+
+};
+
+#endif /* _THEORY_STR_H_ */

src/test/smt2print_parse.cpp

@@ -13,8 +13,9 @@ Copyright (c) 2015 Microsoft Corporation
 void test_print(Z3_context ctx, Z3_ast a) {
     Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
     char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a);
-    std::cout << spec1 << "\n";
+    std::cout << "spec1: benchmark->string\n" << spec1 << "\n";
 
+    std::cout << "attempting to parse spec1...\n";
     Z3_ast b = 
         Z3_parse_smtlib2_string(ctx, 
                                 spec1,
@@ -24,14 +25,14 @@ void test_print(Z3_context ctx, Z3_ast a) {
                                 0,
                                 0,
                                 0);
-
+    std::cout << "parse successful, converting ast->string\n";
     char const* spec2 = Z3_ast_to_string(ctx, b);
-    std::cout << spec2 << "\n";    
+    std::cout << "spec2: string->ast->string\n" << spec2 << "\n";
 }
 
 void test_parseprint(char const* spec) {
     Z3_context ctx = Z3_mk_context(0);
-    std::cout << spec << "\n";
+    std::cout << "spec:\n" << spec << "\n";
 
     Z3_ast a = 
         Z3_parse_smtlib2_string(ctx, 
@@ -43,8 +44,12 @@ void test_parseprint(char const* spec) {
                                 0,
                                 0);
     
+    std::cout << "done parsing\n";
+
     test_print(ctx, a);
 
+    std::cout << "done printing\n";
+
     Z3_del_context(ctx);
 }
 
@@ -104,6 +109,12 @@ void tst_smt2print_parse() {
 
     test_parseprint(spec5);
 
+    // Test strings
+    char const* spec6 =
+        "(assert (= \"abc\" \"abc\"))";
+
+    test_parseprint(spec6);
+
     // Test ?     
 
 }