Merge pull request #1705 from trinhmt/master

created pull from Trinh's seq solver

src/ast/rewriter/seq_rewriter.cpp

@@ -470,7 +470,7 @@ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
     if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
         // convert to string constant
         zstring str(n_val.get_unsigned());
-        TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
+        TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
         result = m_util.str.mk_string(str);
         return BR_DONE;
     }

src/smt/params/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(smt_params
     theory_array_params.cpp
     theory_bv_params.cpp
     theory_pb_params.cpp
+    theory_seq_params.cpp
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     ast

src/smt/params/smt_params.h

@@ -26,6 +26,7 @@ Revision History:
 #include "smt/params/theory_array_params.h"
 #include "smt/params/theory_bv_params.h"
 #include "smt/params/theory_str_params.h"
+#include "smt/params/theory_seq_params.h"
 #include "smt/params/theory_pb_params.h"
 #include "smt/params/theory_datatype_params.h"
 #include "smt/params/preprocessor_params.h"
@@ -79,6 +80,7 @@ struct smt_params : public preprocessor_params,
                     public theory_array_params,
                     public theory_bv_params,
                     public theory_str_params,
+                    public theory_seq_params,
                     public theory_pb_params,
                     public theory_datatype_params {
     bool             m_display_proof;

src/smt/params/smt_params_helper.pyg

@@ -71,6 +71,7 @@ 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'),
+                          ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('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/params/theory_seq_params.cpp

@@ -0,0 +1,23 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    theory_seq_params.cpp
+
+Abstract:
+
+    Parameters for sequence theory plugin
+
+Revision History:
+
+
+--*/
+
+#include "smt/params/theory_seq_params.h"
+#include "smt/params/smt_params_helper.hpp"
+
+void theory_seq_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_split_w_len = p.seq_split_w_len();
+}

src/smt/params/theory_seq_params.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    theory_seq_params.h
+
+Abstract:
+
+    Parameters for sequence theory plugin
+
+Revision History:
+
+
+--*/
+
+#ifndef THEORY_SEQ_PARAMS_H
+#define THEORY_SEQ_PARAMS_H
+
+#include "util/params.h"
+
+struct theory_seq_params {
+    /*
+     * Enable splitting guided by length constraints
+     */
+    bool m_split_w_len;
+
+
+    theory_seq_params(params_ref const & p = params_ref()):
+        m_split_w_len(true)
+    {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+};
+
+#endif /* THEORY_SEQ_PARAMS_H */

src/smt/smt_setup.cpp

@@ -222,7 +222,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        m_context.register_plugin(alloc(theory_seq, m_manager, m_params));
     }
 
     void setup::setup_QF_UF(static_features const & st) {        
@@ -721,8 +721,18 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+        if (m_params.m_string_solver == "z3str3") {
-        m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
+            setup_str();
+        }
+        else if (m_params.m_string_solver == "seq") {
+            setup_unknown();
+        }
+        else if (m_params.m_string_solver == "auto") {
+            setup_unknown();
+        }
+        else {
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+        }
     }
 
     bool is_arith(static_features const & st) {
@@ -885,7 +895,7 @@ namespace smt {
     }
 
     void setup::setup_seq() {
-        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+        m_context.register_plugin(alloc(smt::theory_seq, m_manager, m_params));
     }
 
     void setup::setup_unknown() {

src/smt/theory_seq.h

@@ -29,6 +29,7 @@ Revision History:
 #include "math/automata/automaton.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "util/union_find.h"
+#include "util/obj_ref_hashtable.h"
 
 namespace smt {
 
@@ -48,6 +49,8 @@ namespace smt {
         typedef union_find<theory_seq> th_union_find;
 
         class seq_value_proc;
+        
+        theory_seq_params const & m_params;
 
         // cache to track evaluations under equalities
         class eval_cache {
@@ -301,6 +304,12 @@ namespace smt {
         unsigned                   m_eq_id;
         th_union_find              m_find;
 
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap;
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap2;
+        obj_map<enode, obj_map<enode, int>>   m_len_offset;
+        int                                   m_len_prop_lvl;
+
+
         seq_factory*               m_factory;    // value factory
         exclusion_table            m_exclude;    // set of asserted disequalities.
         expr_ref_vector            m_axioms;     // list of axioms to add.
@@ -321,7 +330,7 @@ namespace smt {
         stats            m_stats;
         symbol           m_prefix, m_suffix, m_accept, m_reject;
         symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
-        symbol           m_pre, m_post, m_eq;
+        symbol           m_pre, m_post, m_eq, m_seq_align;
         ptr_vector<expr> m_todo;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
@@ -354,7 +363,7 @@ namespace smt {
         void pop_scope_eh(unsigned num_scopes) override;
         void restart_eh() override;
         void relevant_eh(app* n) override;
-        theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager()); }
+        theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
         char const * get_name() const override { return "seq"; }
         theory_var mk_var(enode* n) override;
         void apply_sort_cnstr(enode* n, sort* s) override;
@@ -366,23 +375,44 @@ namespace smt {
         void init_search_eh() override;
 
         void init_model(expr_ref_vector const& es);
+        
+        void len_offset(expr* const& e, rational val);
+        void prop_arith_to_len_offset();
+        int find_fst_non_empty_idx(expr_ref_vector const& x) const;
+        expr* find_fst_non_empty_var(expr_ref_vector const& x) const;
+        void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff);
+        bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned const& idx, dependency*& deps, expr_ref_vector & res);
+        
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
         bool reduce_length_eq();
         bool branch_unit_variable();     // branch on XYZ = abcdef
         bool branch_binary_variable();   // branch on abcX = Ydefg 
+        bool branch_ternary_variable1(); // branch on XabcY = Zdefg or XabcY = defgZ
+        bool branch_ternary_variable2(); // branch on XabcY = defgZmnpq
+        bool branch_quat_variable();     // branch on XabcY = ZdefgT
+        bool len_based_split();          // split based on len offset
         bool branch_variable_mb();       // branch on a variable, model based on length
         bool branch_variable();          // branch on a variable
-        bool split_variable();           // split a variable
         bool is_solved(); 
         bool check_length_coherence();
         bool check_length_coherence0(expr* e);
         bool check_length_coherence(expr* e);
-        bool fixed_length();
+        bool fixed_length(bool is_zero = false);
-        bool fixed_length(expr* e);
+        bool fixed_length(expr* e, bool is_zero);
         void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
         bool branch_variable(eq const& e);
         bool branch_binary_variable(eq const& e);
+        bool eq_unit(expr* const& l, expr* const &r) const;       
+        unsigned_vector overlap(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        unsigned_vector overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool branch_ternary_variable_base(dependency* dep, unsigned_vector indexes, expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
+        bool branch_ternary_variable_base2(dependency* dep, unsigned_vector indexes, expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
+        bool branch_ternary_variable(eq const& e, bool flag1 = false);
+        bool branch_ternary_variable2(eq const& e, bool flag1 = false);
+        bool branch_quat_variable(eq const& e);
+        bool len_based_split(eq const& e);
         bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool propagate_length_coherence(expr* e);  
         bool split_lengths(dependency* dep,
@@ -394,11 +424,14 @@ namespace smt {
         bool check_extensionality();
         bool check_contains();
         bool solve_eqs(unsigned start);
-        bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
+        bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, dependency* dep);
         bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
+        bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*& y2);
+        bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
+        bool is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr*& x, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
         bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool propagate_max_length(expr* l, expr* r, dependency* dep);
 
@@ -410,7 +443,7 @@ namespace smt {
         expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
         expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
         expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
-        expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return mk_concat(es.size(), es.c_ptr()); }
+        expr* mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return m_util.str.mk_concat(es.size(), es.c_ptr()); }
         expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); }
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
@@ -454,8 +487,9 @@ namespace smt {
         // variable solving utilities
         bool occurs(expr* a, expr* b);
         bool occurs(expr* a, expr_ref_vector const& b);
-        bool is_var(expr* b);
+        bool is_var(expr* b) const;
         bool add_solution(expr* l, expr* r, dependency* dep);
+        bool is_unit_nth(expr* a) const;
         bool is_nth(expr* a) const;
         bool is_nth(expr* a, expr*& e1, expr*& e2) const;
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
@@ -521,6 +555,7 @@ namespace smt {
         literal mk_seq_eq(expr* a, expr* b);
         void tightest_prefix(expr* s, expr* x);
         expr_ref mk_sub(expr* a, expr* b);
+        expr_ref mk_add(expr* a, expr* b);
         enode* ensure_enode(expr* a);
         
         dependency* mk_join(dependency* deps, literal lit);
@@ -530,11 +565,13 @@ namespace smt {
         // arithmetic integration
         bool get_num_value(expr* s, rational& val) const;
         bool lower_bound(expr* s, rational& lo) const;
+        bool lower_bound2(expr* s, rational& lo);
         bool upper_bound(expr* s, rational& hi) const;
         bool get_length(expr* s, rational& val) const;
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
-        expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, sort* range = nullptr);
+        expr* coalesce_chars(expr* const& str);
+        expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr);
         bool is_skolem(symbol const& s, expr* e) const;
 
         void set_incomplete(app* term);
@@ -586,7 +623,7 @@ namespace smt {
         void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
         void display_nc(std::ostream& out, nc const& nc) const;
     public:
-        theory_seq(ast_manager& m);
+        theory_seq(ast_manager& m, theory_seq_params const & params);
         ~theory_seq() override;
 
         // model building

src/util/obj_ref_hashtable.h

@@ -26,7 +26,7 @@ class obj_ref_map {
     M&                  m;
     obj_map<Key, Value> m_table;
 public:
-    typedef typename obj_map<Key, Value> iterator;
+    typedef typename obj_map<Key, Value>::iterator iterator;
     typedef Key key;
     typedef Value value;
     typedef typename obj_map<Key, Value>::key_data key_data;