From 28ce701e17853d58310648614b5d1d2973d1f195 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 May 2019 15:31:55 +0200
Subject: [PATCH] fixing 2267

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp            |  4 +-
 src/ast/ast.h                    |  8 ++++
 src/ast/rewriter/seq_rewriter.h  |  1 +
 src/math/interval/interval.h     |  5 +++
 src/math/interval/interval_def.h | 10 +++++
 src/model/func_interp.cpp        | 32 ++++++++++++++
 src/model/func_interp.h          |  2 +
 src/model/model.cpp              | 18 +++++++-
 src/model/model.h                |  1 +
 src/model/model_evaluator.cpp    |  4 ++
 src/model/model_evaluator.h      |  1 +
 src/model/model_smt2_pp.cpp      | 10 +++--
 src/smt/theory_array_base.cpp    | 51 ++++++----------------
 src/smt/theory_array_base.h      |  2 +-
 src/smt/theory_seq.cpp           | 73 ++++++++++++++++++++++++++++++--
 15 files changed, 174 insertions(+), 48 deletions(-)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 812d80b23..8b84e0848 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -162,7 +162,9 @@ extern "C" {
         model * _m = to_model_ref(m);
         params_ref p;
         ast_manager& mgr = mk_c(c)->m();
-        _m->set_solver(alloc(api::seq_expr_solver, mgr, p));
+        if (!_m->has_solver()) {
+            _m->set_solver(alloc(api::seq_expr_solver, mgr, p));
+        }
         expr_ref result(mgr);
         model::scoped_model_completion _scm(*_m, model_completion);
         result = (*_m)(to_expr(t));
diff --git a/src/ast/ast.h b/src/ast/ast.h
index baefc4685..5ba3a900e 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1846,6 +1846,14 @@ public:
         return mk_func_decl(name, 2, d, range, assoc, comm, false);
     }
 
+    bool is_considered_uninterpreted(func_decl* f) {
+        if (f->get_family_id() == null_family_id) {
+            return true;
+        }
+        decl_plugin* p = get_plugin(f->get_family_id());
+        return !p || p->is_considered_uninterpreted(f);        
+    }
+
     app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
 
     app * mk_app(func_decl * decl, expr * const * args) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 73ab26591..acc494b09 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -167,6 +167,7 @@ public:
     static void get_param_descrs(param_descrs & r) {}
 
     void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
+    bool has_solver() { return m_re2aut.has_solver(); }
 
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h
index db3c5a850..695c1c78e 100644
--- a/src/math/interval/interval.h
+++ b/src/math/interval/interval.h
@@ -234,6 +234,11 @@ public:
 
     bool check_invariant(interval const & n) const;
 
+    /**
+       \brief b <- k
+    */
+    void set(numeral const& k, interval & b);
+
     /**
        \brief b <- -a
     */
diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h
index de3a5fa19..a1c8df7a8 100644
--- a/src/math/interval/interval_def.h
+++ b/src/math/interval/interval_def.h
@@ -664,6 +664,16 @@ bool interval_manager<C>::check_invariant(interval const & n) const {
     return true;
 }
 
+template<typename C>
+void interval_manager<C>::set(numeral const& k, interval & b) {
+    set_lower_is_inf(b, false);
+    set_upper_is_inf(b, false);
+    m().set(lower(b), k);
+    m().set(upper(b), k);
+    set_lower_is_open(b, false);
+    set_upper_is_open(b, false);
+}
+
 template<typename C>
 void interval_manager<C>::set(interval & t, interval const & s) {
     if (&t == &const_cast<interval&>(s))
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index e1d90516c..58c7f7ddc 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_util.h"
 #include "model/func_interp.h"
+#include "ast/array_decl_plugin.h"
 
 func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result):
     m_args_are_values(true),
@@ -316,6 +317,37 @@ bool func_interp::is_identity() const {
     return (sz.size() == m_entries.size() + 1);
 }
 
+expr_ref func_interp::get_array_interp(sort_ref_vector const& domain) const {
+    if (m_else == nullptr) 
+        return expr_ref(m_manager);
+    if (!is_ground(m_else)) {
+        return expr_ref(m_manager);
+    }
+    array_util autil(m_manager);
+    sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager);
+    expr_ref r(autil.mk_const_array(A, m_else), m_manager);
+    expr_ref_vector args(m_manager);
+    for (func_entry * curr : m_entries) {
+        expr * res = curr->get_result();
+
+        if (m_else == res) {
+            continue;
+        }
+        args.reset();
+        args.push_back(r);        
+        for (unsigned i = 0; i < m_arity; i++) {
+            expr* arg = curr->get_arg(i);
+            if (!is_ground(arg)) {
+                return expr_ref(m_manager);
+            }
+            args.push_back(arg);
+        }
+        args.push_back(res);
+        r = autil.mk_store(args.size(), args.c_ptr());
+    }
+    return r;    
+}
+
 expr * func_interp::get_interp_core() const {
     if (m_else == nullptr)
         return nullptr;
diff --git a/src/model/func_interp.h b/src/model/func_interp.h
index 543124793..3fd82b59a 100644
--- a/src/model/func_interp.h
+++ b/src/model/func_interp.h
@@ -112,6 +112,8 @@ public:
 
     expr * get_interp() const;
 
+    expr_ref get_array_interp(sort_ref_vector const& domain) const;
+
     func_interp * translate(ast_translation & translator) const;
 
 private:
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 756fe2251..af30b6179 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -401,15 +401,25 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
                 continue;
             }
             fi = nullptr;
+            new_t = nullptr;
+            sort_ref_vector domain(m);
             if (autil.is_as_array(a)) {
                 func_decl* f = autil.get_as_array_func_decl(a);
                 // only expand auxiliary definitions that occur once.
                 if (can_inline_def(ts, f)) {
                     fi = get_func_interp(f);
+                    for (sort* s : *f) {
+                        domain.push_back(s);
+                    }
+                    new_t = fi->get_array_interp(domain);
+                    TRACE("model", tout << new_t << "\n";);
                 }
             }
-            
-            if (fi && fi->get_interp()) {
+
+            if (new_t) {
+                // noop
+            }
+            else if (fi && fi->get_interp()) {
                 f = autil.get_as_array_func_decl(a);
                 expr_ref_vector sargs(m);
                 sort_ref_vector vars(m);
@@ -484,6 +494,10 @@ void model::set_solver(expr_solver* s) {
     m_mev.set_solver(s);
 }
 
+bool model::has_solver() {
+    return m_mev.has_solver();
+}
+
 expr_ref_vector model::operator()(expr_ref_vector const& ts) {
     expr_ref_vector rs(m);
     for (expr* t : ts) rs.push_back((*this)(t));
diff --git a/src/model/model.h b/src/model/model.h
index 2599a3fcd..a7a356be0 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -95,6 +95,7 @@ public:
     bool is_false(expr* t);
     bool is_true(expr_ref_vector const& ts);
     void reset_eval_cache();
+    bool has_solver(); 
     void set_solver(expr_solver* solver);
 
     class scoped_model_completion {
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index a060be8cf..1991fc4d2 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -695,3 +695,7 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
 void model_evaluator::set_solver(expr_solver* solver) {
     m_imp->m_cfg.m_seq_rw.set_solver(solver);
 }
+
+bool model_evaluator::has_solver() {
+    return m_imp->m_cfg.m_seq_rw.has_solver();
+}
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index 1959af246..2ffcf2e0b 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -57,6 +57,7 @@ public:
     bool is_true(expr_ref_vector const& ts);
 
     void set_solver(expr_solver* solver);
+    bool has_solver();
 
     /**
      * best effort evaluator of extensional array equality.
diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp
index 196843de4..ef51ec949 100644
--- a/src/model/model_smt2_pp.cpp
+++ b/src/model/model_smt2_pp.cpp
@@ -194,11 +194,13 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
     ptr_buffer<format> f_entry_conds;
     ptr_buffer<func_decl> func_decls;
     sort_fun_decls(m, md, func_decls);
-    for (unsigned i = 0; i < func_decls.size(); i++) {
-        func_decl * f     = func_decls[i]; 
+    for (func_decl * f : func_decls) {
         if (recfun_util.is_defined(f) && !recfun_util.is_generated(f)) {
             continue;
         }
+        if (!m.is_considered_uninterpreted(f)) {
+            continue;            
+        }
         func_interp * f_i = md.get_func_interp(f);
         SASSERT(f->get_arity() == f_i->get_arity());
         format_ref body(fm(m));
@@ -216,8 +218,8 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
         }
         TRACE("model_smt2_pp", for (unsigned i = 0; i < var_names.size(); i++) tout << var_names[i] << "\n";);
         f_var_names.reset();
-        for (unsigned i = 0; i < f->get_arity(); i++)
-            f_var_names.push_back(mk_string(m, var_names[i].bare_str()));
+        for (auto const& vn : var_names) 
+            f_var_names.push_back(mk_string(m, vn.bare_str()));
         f_arg_decls.reset();
         for (unsigned i = 0; i < f->get_arity(); i++) {
             format_ref f_domain(fm(m));
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index a9418f3b6..bb3ed9992 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -34,11 +34,7 @@ namespace smt {
 
     void theory_array_base::found_unsupported_op(expr * n) {
         if (!get_context().get_fparams().m_array_fake_support && !m_found_unsupported_op) {
-            //array_util autil(get_manager());
-            //func_decl* f = 0;
-            //if (autil.is_as_array(n, f) && f->is_skolem()) return;
-            TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);
-            
+            TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);            
             get_context().push_trail(value_trail<context, bool>(m_found_unsupported_op));
             m_found_unsupported_op = true;
         }
@@ -266,10 +262,7 @@ namespace smt {
 
         m_array_value.reset();
         // populate m_array_value if the select(a, i) parent terms of r1
-        enode_vector::const_iterator it  = r1->begin_parents();
-        enode_vector::const_iterator end = r1->end_parents();
-        for (; it != end; ++it) {
-            enode* parent = *it;            
+        for (enode* parent : r1->get_const_parents()) {
             if (parent->is_cgr() &&
                 ctx.is_relevant(parent) &&
                 is_select(parent->get_owner()) &&
@@ -278,10 +271,7 @@ namespace smt {
             }
         }
         // traverse select(a, i) parent terms of r2 trying to find a match.
-        it  = r2->begin_parents();
-        end = r2->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r2->get_const_parents()) {
             enode * other;
             if (parent->is_cgr() && 
                 ctx.is_relevant(parent) &&
@@ -712,10 +702,7 @@ namespace smt {
         for (theory_var v = 0; v < num_vars; ++v) {
             enode * r = get_enode(v)->get_root();                
             if (is_representative(v) && get_context().is_relevant(r)) {
-                enode_vector::iterator it  = r->begin_parents();
-                enode_vector::iterator end = r->end_parents();
-                for (; it != end; ++it) {
-                    enode * parent = *it;
+                for (enode * parent : r->get_const_parents()) {
                     if (parent->get_cg() == parent &&
                         get_context().is_relevant(parent) &&
                         is_select(parent) &&
@@ -735,10 +722,7 @@ namespace smt {
         if (!get_context().is_relevant(r)) {
             return;
         }
-        ptr_vector<enode>::const_iterator it  = r->begin_parents();
-        ptr_vector<enode>::const_iterator end = r->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r->get_const_parents()) {
             if (get_context().is_relevant(parent) &&
                 is_store(parent) &&
                 parent->get_arg(0)->get_root() == r) {
@@ -770,10 +754,7 @@ namespace smt {
 
     void theory_array_base::propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo) {
         select_set * sel_set = get_select_set(r);
-        select_set::iterator it2  = sel_set->begin();
-        select_set::iterator end2 = sel_set->end();
-        for (; it2 != end2; ++it2) {
-            enode * sel = *it2;
+        for (enode* sel : *sel_set) {
             SASSERT(is_select(sel));
             propagate_select_to_store_parents(r, sel, todo);
         }
@@ -781,10 +762,7 @@ namespace smt {
 
     void theory_array_base::propagate_selects() {
         enode_pair_vector todo;
-        enode_vector::const_iterator it  = m_selects_domain.begin();
-        enode_vector::const_iterator end = m_selects_domain.end();
-        for (; it != end; ++it) {
-            enode * r = *it;
+        for (enode * r : m_selects_domain) {
             propagate_selects_to_store_parents(r, todo);
         }
         for (unsigned qhead = 0; qhead < todo.size(); qhead++) {
@@ -901,6 +879,10 @@ namespace smt {
         }
     };
 
+    bool theory_array_base::include_func_interp(func_decl* f) {
+        return is_decl_of(f, get_id(), OP_ARRAY_EXT);
+    }
+
     model_value_proc * theory_array_base::mk_value(enode * n, model_generator & m) {
         SASSERT(get_context().is_relevant(n));
         theory_var v       = n->get_th_var(get_id());
@@ -948,10 +930,7 @@ namespace smt {
         m_selects.find(n->get_root(), sel_set);
         if (sel_set != nullptr) {
             ptr_buffer<enode> args;
-            select_set::iterator it  = sel_set->begin();
-            select_set::iterator end = sel_set->end();
-            for (; it != end; ++it) {
-                enode * select = *it;
+            for (enode * select : *sel_set) {
                 args.reset();
                 unsigned num = select->get_num_args();
                 for (unsigned j = 1; j < num; ++j)
@@ -963,10 +942,8 @@ namespace smt {
         TRACE("array", 
               tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n";
               if (sel_set) {
-                  select_set::iterator it  = sel_set->begin();
-                  select_set::iterator end = sel_set->end();
-                  for (; it != end; ++it) {
-                      tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n";
+                  for (enode* s : *sel_set) {
+                      tout << "#" << s->get_root()->get_owner()->get_id() << " " << mk_pp(s->get_owner(), get_manager()) << "\n";
                   }
               }
               if (else_val_n) {
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index 3fc8be613..bf35bdd1b 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -194,7 +194,7 @@ namespace smt {
         select_set * get_select_set(enode * n);
         void finalize_model(model_generator & m) override;
         model_value_proc * mk_value(enode * n, model_generator & m) override;
-        
+        bool include_func_interp(func_decl* f) override;
     public:
         theory_array_base(ast_manager & m);
         ~theory_array_base() override { restore_sorts(0); }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 71f98b22b..116d5759f 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -13,7 +13,76 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2015-6-12
 
-Revision History:
+Outline:
+
+ A cascading sequence of solvers:
+ 
+ - simplify_and_solve_eqs
+   - canonize equality
+   - solve_unit_eq: x = t, where x not in t.
+   - solve_binary_eq: xa = bx -> a = b, xa = bx
+   - solve_nth_eq: x = unit(nth(x,0)).unit(nth(x,1)).unit(nth(x,2)...unit(nth(x,n-1))
+   - solve_itos: itos(i) = "" -> i < 0   
+
+ - check_contains
+   - (f,dep) = canonize(contains(a, b))
+     lit := |b| > |a|
+     f := true -> conflict
+     f := false -> solved
+     value(lit) = l_true -> solved
+     f := s = t -> dep -> s != t
+     f := f1 & f2 -> dep -> ~f1 | ~f2
+     f := f1 | f2 -> dep -> ~f1 & ~f2
+
+ - solve_nqs
+   - s_i = t_i, d_i <- solve(s = t)
+   - create literals for s_i = t_i
+   - if one of created literals is false, done.
+   - conflict if all created literals are true
+
+ - fixed_length
+   - len(s) = k -> s = unit(nth(0,s)).unit(nth(1,s))....unit(nth(n-1,s))
+
+ - len_based_split
+   s = x.xs t = y.ys, len(x) = len(y) -> x = y & xs = ys
+   s = x.xs t = y.ys, len(x) = len(y) + offset -> y = x*Z, Z*xs = ys
+   s = x.x'.xs, t = y.y'.ys, len(xs) = len(ys) -> xs = ys
+   
+ - check_int_string
+   e := itos(n), len(e) = v, v > 0 ->      
+   n := stoi(e), len(e) = v, v > 0 -> 
+   -  n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
+   -  n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
+   -  n < 0  & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
+   -  10^k <= n < 10^{k+1}-1 => len(e) => k
+
+ - reduce_length_eq
+   x1...xn = y1...ym, len(x1...xk) = len(y1...yj) -> x1...xk = y1..yj, x{k+1}..xn = y{j+1}..ym
+
+ - branch_unit_variable
+   len(x) = n -> x = unit(a1)unit(a2)...unit(a_n)
+
+ - branch_binary_variable
+   x ++ units1 = units2 ++ y -> x is prefix of units2 or x = units2 ++ y1, y = y1 ++ y2, y2 = units2
+
+ - branch_variable
+   - branch_variable_mb
+     s = xs, t = ys, each x_i, y_j has a length.
+     based on length comparisons decompose into smaller equalities.
+
+   - branch_variable_eq
+     cycle through branch options
+
+   - branch_ternary_variable1
+     
+   - branch_ternary_variable2
+
+ - check_length_coherence
+   len(e) >= lo => e = unit(nth(0,e)).unit(nth(1,e))....unit(nth(lo-1,e)).seq
+   len(e) <= lo => seq = empty
+   len(e) <= hi => len(seq) <= hi - lo
+
+ - check_extensionality
 
 
 --*/
@@ -454,8 +523,6 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
     if (ls.empty() || !is_var(ls[0])) {
         return false;
     }
-    //std::function<bool(expr*)> is_unit = [&](expr* elem) { return m_util.str.is_unit(elem); }
-    //return rs.forall(is_unit);
 
     for (auto const& elem : rs) {
         if (!m_util.str.is_unit(elem)) {