Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4

src/api/java/ReExpr.java

@@ -0,0 +1,33 @@
+/**
+Copyright (c) 2012-2016 Microsoft Corporation
+   
+Module Name:
+
+    ReExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+/**
+ * Re expressions
+ **/
+public class ReExpr extends Expr
+{
+    /**
+     * Constructor for ReExpr
+     * @throws Z3Exception on error
+     **/
+    ReExpr(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+}

src/api/java/ReSort.java

@@ -0,0 +1,29 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ReSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+/**
+ * A Regular expression sort
+ **/
+public class ReSort extends Sort
+{
+    ReSort(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+}

src/api/java/SeqExpr.java

@@ -0,0 +1,33 @@
+/**
+Copyright (c) 2012-2016 Microsoft Corporation
+   
+Module Name:
+
+    SeqExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+/**
+ * Seq expressions
+ **/
+public class SeqExpr extends Expr
+{
+    /**
+     * Constructor for SeqExpr
+     * @throws Z3Exception on error
+     **/
+    SeqExpr(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+}

src/api/java/SeqSort.java

@@ -0,0 +1,29 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    SeqSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+/**
+ * A Sequence sort
+ **/
+public class SeqSort extends Sort
+{
+    SeqSort(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+}

src/ast/seq_decl_plugin.cpp

@@ -80,8 +80,9 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     return result;
 }
 
-static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
-                               "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
+static const char esc_table[32][3] =
+    { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
+      "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
  
 std::string zstring::encode() const {
     SASSERT(m_encoding == ascii);

src/smt/theory_arith.h

@@ -429,6 +429,7 @@ namespace smt {
         arith_util              m_util;
         arith_eq_solver         m_arith_eq_solver;
         bool                    m_found_unsupported_op;
+        bool                    m_found_underspecified_op;
         arith_eq_adapter        m_arith_eq_adapter;
         vector<row>             m_rows;
         svector<unsigned>       m_dead_rows;
@@ -510,6 +511,7 @@ namespace smt {
         virtual theory_var mk_var(enode * n);
 
         void found_unsupported_op(app * n);
+        void found_underspecified_op(app * n);
 
         bool has_var(expr * v) const { return get_context().e_internalized(v) && get_context().get_enode(v)->get_th_var(get_id()) != null_theory_var; }
         theory_var expr2var(expr * v) const { SASSERT(get_context().e_internalized(v)); return get_context().get_enode(v)->get_th_var(get_id()); }

src/smt/theory_arith_aux.h

@@ -2153,6 +2153,9 @@ namespace smt {
     */
     template<typename Ext>
     bool theory_arith<Ext>::is_shared(theory_var v) const {
+        if (!m_found_underspecified_op) {
+            return false;
+        }
         enode * n      = get_enode(v);
         enode * r      = n->get_root();
         enode_vector::const_iterator it  = r->begin_parents();

src/smt/theory_arith_core.h

@@ -37,6 +37,15 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    void theory_arith<Ext>::found_underspecified_op(app * n) {
+        if (!m_found_underspecified_op) {
+            TRACE("arith", tout << "found non underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
+            get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
+            m_found_underspecified_op = true;
+        }
+    }
+
     template<typename Ext>
     bool theory_arith<Ext>::process_atoms() const {
         if (!adaptive())
@@ -308,6 +317,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
+        found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -317,6 +327,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_idiv(app * n) {
+        found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         app * mod         = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
@@ -329,6 +340,7 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
+        found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -338,6 +350,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
+        found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
         if (!ctx.relevancy()) {
@@ -1514,6 +1527,7 @@ namespace smt {
         m_util(m),
         m_arith_eq_solver(m),
         m_found_unsupported_op(false),
+        m_found_underspecified_op(false),
         m_arith_eq_adapter(*this, params, m_util),
         m_asserted_qhead(0),
         m_to_patch(1024),

src/smt/theory_seq.cpp

@@ -159,7 +159,6 @@ theory_seq::theory_seq(ast_manager& m):
     m_exclude(m),
     m_axioms(m),
     m_axioms_head(0),
-    m_branch_variable_head(0),
     m_mg(0),
     m_rewrite(m), 
     m_util(m),
@@ -234,8 +233,9 @@ bool theory_seq::branch_variable() {
     context& ctx = get_context();
     unsigned sz = m_eqs.size();
     expr_ref_vector ls(m), rs(m);
+    int start = ctx.get_random_value();
     for (unsigned i = 0; i < sz; ++i) {
-        unsigned k = (i + m_branch_variable_head) % sz;
+        unsigned k = (i + start) % sz;
         eq e = m_eqs[k];
         TRACE("seq", tout << e.m_lhs << " = " << e.m_rhs << "\n";);
         ls.reset(); rs.reset();
@@ -243,21 +243,17 @@ bool theory_seq::branch_variable() {
         m_util.str.get_concat(e.m_rhs, rs);
 
 #if 1       
-        if (!ls.empty() && find_branch_candidate(e.m_dep, ls[0].get(), rs)) {
-            m_branch_variable_head = k;
+        if (find_branch_candidate(e.m_dep, ls, rs)) {
             return true;
         }
-        if (!rs.empty() && find_branch_candidate(e.m_dep, rs[0].get(), ls)) {
-            m_branch_variable_head = k;
+        if (find_branch_candidate(e.m_dep, rs, ls)) {
             return true;
         }
 #else
-        if (ls.size() > 1 && find_branch_candidate(e.m_dep, ls.back(), rs)) {
-            m_branch_variable_head = k;
+        if (find_branch_candidate(e.m_dep, ls.back(), rs)) {
             return true;
         }
-        if (rs.size() > 1 && find_branch_candidate(e.m_dep, rs.back(), ls)) {
-            m_branch_variable_head = k;
+        if (find_branch_candidate(e.m_dep, rs.back(), ls)) {
             return true;
         }
 #endif
@@ -273,10 +269,12 @@ bool theory_seq::branch_variable() {
     return ctx.inconsistent();
 }
 
-bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs) {
+bool theory_seq::find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
 
-    TRACE("seq", tout << mk_pp(l, m) << " " 
-          << (is_var(l)?"var":"not var") << "\n";);
+    if (ls.empty()) {
+        return false;
+    }
+    expr* l = ls[0];
 
     if (!is_var(l)) {
         return false;
@@ -286,7 +284,8 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
     expr_ref_vector cases(m);
     expr_ref v0(m), v(m);
     v0 = m_util.str.mk_empty(m.get_sort(l));
-    if (l_false != assume_equality(l, v0)) {
+    if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr()) && l_false != assume_equality(l, v0)) {
+        TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
         return true;
     }
     for (unsigned j = 0; j < rs.size(); ++j) {
@@ -295,8 +294,12 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
         }
         SASSERT(!m_util.str.is_string(rs[j]));
         all_units &= m_util.str.is_unit(rs[j]);
+        if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
+            continue;
+        }
         v0 = m_util.str.mk_concat(j + 1, rs.c_ptr());
         if (l_false != assume_equality(l, v0)) {
+            TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
             return true;
         }
     }           
@@ -308,11 +311,37 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
             lits.push_back(~mk_eq(l, v0, false));
         }
         set_conflict(dep, lits);
+        TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
         return true;
     }
     return false;
 }
 
+bool theory_seq::can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const {
+    unsigned i = 0;
+    for (; i < szl && i < szr; ++i) {
+        if (m.are_distinct(ls[i], rs[i])) {
+            return false;
+        }
+        if (!m.are_equal(ls[i], rs[i])) {
+            break;
+        }
+    }
+    if (i == szr) {
+        std::swap(ls, rs);
+        std::swap(szl, szr);
+    }
+    if (i == szl && i < szr) {
+        for (; i < szr; ++i) {
+            if (m_util.str.is_unit(rs[i])) {
+                return false;
+            }
+        }
+    }
+    return true;
+}
+
+
 lbool theory_seq::assume_equality(expr* l, expr* r) {
     context& ctx = get_context();
     if (m_exclude.contains(l, r)) {

src/smt/theory_seq.h

@@ -304,7 +304,6 @@ namespace smt {
         expr_ref_vector            m_axioms;     // list of axioms to add.
         obj_hashtable<expr>        m_axiom_set;
         unsigned                   m_axioms_head; // index of first axiom to add.
-        unsigned        m_branch_variable_head;   // index of first equation to examine.
         bool            m_incomplete;             // is the solver (clearly) incomplete for the fragment.
         obj_hashtable<expr> m_length;             // is length applied
         scoped_ptr_vector<apply> m_replay;        // set of actions to replay
@@ -387,7 +386,8 @@ namespace smt {
         void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
         void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
-        bool find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs);
+        bool find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
         lbool assume_equality(expr* l, expr* r);
 
         // variable solving utilities