fix #2659

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/seq_rewriter.cpp

@@ -18,16 +18,16 @@ Notes:
 
 --*/
 
+#include "util/uint_set.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_util.h"
-#include "util/uint_set.h"
-#include "math/automata/automaton.h"
 #include "ast/well_sorted.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "math/automata/automaton.h"
 #include "math/automata/symbolic_automata_def.h"
 
 
@@ -810,6 +810,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
             result = m_util.str.mk_concat(_len, as.c_ptr() + offset);
             return BR_DONE;
         }
+        if (i == as.size()) {
+            result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset);
+            return BR_DONE;
+        }
     }
     if (offset == 0) {
         return BR_FAILED;

src/ast/seq_decl_plugin.cpp

@@ -667,6 +667,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
     match_right_assoc(*m_sigs[k], arity, domain, range, rng);
     func_decl_info info(m_family_id, k_seq);
     info.set_right_associative(true);
+    info.set_left_associative(true);
     return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
 }
 

src/math/polynomial/polynomial.cpp

@@ -5810,6 +5810,7 @@ namespace polynomial {
                 ps = coeff(B, x, d-1);
                 if (!is_zero(ps))
                     S.push_back(ps);
+                SASSERT(d >= e);
                 unsigned delta = d - e;
                 if (delta > 1) {
                     // C <- S_e
@@ -5932,8 +5933,8 @@ namespace polynomial {
 
         void psc_chain(polynomial const * A, polynomial const * B, var x, polynomial_ref_vector & S) {
             // psc_chain1(A, B, x, S);
-            // psc_chain2(A, B, x, S);
+            //psc_chain2(A, B, x, S);
-            // psc_chain_classic(A, B, x, S);
+            //psc_chain_classic(A, B, x, S);
             psc_chain_optimized(A, B, x, S);
         }
 

src/nlsat/nlsat_explain.cpp

@@ -312,6 +312,7 @@ namespace nlsat {
             polynomial_ref lc(m_pm);
             polynomial_ref reduct(m_pm);
             while (true) {
+                TRACE("nlsat_explain", tout << "elim vanishing x" << x << " k:" << k << " " << p << "\n";);
                 if (is_const(p))
                     return;
                 if (k == 0) {
@@ -320,9 +321,22 @@ namespace nlsat {
                     SASSERT(x != null_var);
                     k = degree(p, x);
                 }
-                if (m_pm.nonzero_const_coeff(p, x, k))
+#if 0
+                anum const & x_val = m_assignment.value(x);
+                if (m_am.is_zero(x_val)) {
+                    // add_zero_assumption(lc);
+                    lc = m_pm.coeff(p, x, k, reduct);
+                    k--;
+                    p = reduct;
+                    continue;
+                }
+#endif
+                if (m_pm.nonzero_const_coeff(p, x, k)) {
+                    TRACE("nlsat_explain", tout << "nonzero const x" << x << "\n";);
                     return; // lc is a nonzero constant
+                }
                 lc = m_pm.coeff(p, x, k, reduct);
+                TRACE("nlsat_explain", tout << "lc: " << lc << " reduct: " << reduct << "\n";);
                 if (!is_zero(lc)) {
                     if (sign(lc) != polynomial::sign_zero)
                         return;
@@ -630,7 +644,7 @@ namespace nlsat {
 
             for (unsigned i = 0; i < sz; i++) {
                 s = S.get(i);
-                TRACE("nlsat_explain", tout << "processing psc(" << i << ")\n"; display(tout, s); tout << "\n";); 
+                TRACE("nlsat_explain", display(tout << "processing psc(" << i << ")\n", s) << "\n";); 
                 if (is_zero(s)) {
                     TRACE("nlsat_explain", tout << "skipping psc is the zero polynomial\n";);
                     continue;

src/smt/proto_model/proto_model.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/well_sorted.h"
+#include "ast/array_decl_plugin.h"
 #include "ast/used_symbols.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/var_subst.h"
@@ -119,19 +120,23 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
    \brief Replace uninterpreted constants occurring in fi->get_else()
    by their interpretations.
 */
-void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs) {
+void proto_model::cleanup_func_interp(expr_ref_vector& trail, func_interp * fi, func_decl_set & found_aux_fs) {
-    if (fi->is_partial())
+    if (!fi->is_partial()) {
-        return;
+        expr * fi_else = fi->get_else();    
-    expr * fi_else = fi->get_else();
+        fi->set_else(cleanup_expr(trail, fi_else, found_aux_fs));
-    TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m) << "\n";);
+    }
+}
 
+expr* proto_model::cleanup_expr(expr_ref_vector& trail, expr* fi_else, func_decl_set& found_aux_fs) {
+    TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m) << "\n";);
+    trail.reset();
     obj_map<expr, expr*> cache;
-    expr_ref_vector trail(m);
     ptr_buffer<expr, 128> todo;
     ptr_buffer<expr> args;
     todo.push_back(fi_else);
-
     expr * a;
+    expr_ref new_t(m);
+
     while (!todo.empty()) {
         a = todo.back();
         if (is_uninterp_const(a)) {
@@ -168,8 +173,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
                     TRACE("model_bug", tout << f->get_name() << "\n";);
                     found_aux_fs.insert(f);
                 }
-                expr_ref new_t(m);
+                new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr());                
-                new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr());
                 if (t != new_t.get())
                     trail.push_back(new_t);
                 todo.pop_back();
@@ -177,7 +181,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
                 break;
             }
             default:
-                SASSERT(a != 0);
+                SASSERT(a != nullptr);
                 cache.insert(a, a);
                 todo.pop_back();
                 break;
@@ -187,17 +191,14 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
 
     VERIFY(cache.find(fi_else, a));
 
-    fi->set_else(a);
+    return a;
 }
 
 void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s) {
-    unsigned sz = decls.size();
     unsigned j  = 0;
-    for (unsigned i = 0; i < sz; i++) {
+    for (func_decl* f : decls) {
-        func_decl * f = decls[i];
         if (!m_aux_decls.contains(f) || s.contains(f)) {
-            decls[j] = f;
+            decls[j++] = f;
-            j++;
         }
     }
     decls.shrink(j);
@@ -211,12 +212,21 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, fun
 void proto_model::cleanup() {
     TRACE("model_bug", model_v2_pp(tout, *this););
     func_decl_set found_aux_fs;
+    expr_ref_vector trail(m);
     for (auto const& kv : m_finterp) {
         TRACE("model_bug", tout << kv.m_key->get_name() << "\n";);
         func_interp * fi = kv.m_value;
-        cleanup_func_interp(fi, found_aux_fs);
+        cleanup_func_interp(trail, fi, found_aux_fs);
     }
-
+    for (unsigned i = 0; i < m_const_decls.size(); ++i) {
+        func_decl* d = m_const_decls[i];
+        expr* e = m_interp[d];
+        expr* r = cleanup_expr(trail, e, found_aux_fs);
+        if (e != r) {
+            register_decl(d, r);
+        }        
+    }
+    // TRACE("model_bug", model_v2_pp(tout, *this););
     // remove auxiliary declarations that are not used.
     if (found_aux_fs.size() != m_aux_decls.size()) {
         remove_aux_decls_not_in_set(m_decls, found_aux_fs);
@@ -224,12 +234,13 @@ void proto_model::cleanup() {
 
         for (func_decl* faux : m_aux_decls) {
             if (!found_aux_fs.contains(faux)) {
-                TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";);
+                TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << " " << faux->get_ref_count() << "\n";);
                 unregister_decl(faux);
             }
         }
         m_aux_decls.swap(found_aux_fs);
     }
+    TRACE("model_bug", model_v2_pp(tout, *this););
 }
 
 value_factory * proto_model::get_factory(family_id fid) {

src/smt/proto_model/proto_model.h

@@ -55,8 +55,8 @@ class proto_model : public model_core {
     // Invariant: m_const_decls subset m_decls
     
     void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
-    void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
+    void cleanup_func_interp(expr_ref_vector& trail, func_interp * fi, func_decl_set & found_aux_fs);
-
+    expr* cleanup_expr(expr_ref_vector& trail, expr* fi_else, func_decl_set& found_aux_fs);
 
 public:
     proto_model(ast_manager & m, params_ref const & p = params_ref());