fixing #2448

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

src/ast/ast.cpp

@@ -1814,7 +1814,6 @@ ast * ast_manager::register_node_core(ast * n) {
         SASSERT(m_ast_table.contains(n));
     }
 
-
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);

src/ast/rewriter/seq_rewriter.cpp

@@ -478,7 +478,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         st = mk_seq_at(args[0], args[1], result); 
         break;
-#if 0
+#if 1
     case OP_SEQ_NTH:
         SASSERT(num_args == 2);
         return mk_seq_nth(args[0], args[1], result); 
@@ -1805,6 +1805,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     bool changed = false;
     if (!reduce_eq(l, r, lhs, rhs, changed)) {
         result = m().mk_false();
+        TRACE("seq", tout << result << "\n";);
         return BR_DONE;
     }
     if (!changed) {
@@ -1814,6 +1815,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
         res.push_back(m().mk_eq(lhs.get(i), rhs.get(i)));
     }
     result = mk_and(res);
+    TRACE("seq", tout << result << "\n";);
     return BR_REWRITE3;
 }
 

src/smt/smt_model_generator.cpp

@@ -291,7 +291,7 @@ namespace smt {
         ptr_vector<model_value_proc> procs;
         svector<source> sources;
         buffer<model_value_dependency> dependencies;
-        ptr_vector<expr> dependency_values;
+        expr_ref_vector dependency_values(m_manager);
         mk_value_procs(root2proc, roots, procs);
         top_sort_sources(roots, root2proc, sources);
         TRACE("sorted_sources",
@@ -307,6 +307,9 @@ namespace smt {
                       tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
                   }
               });
+
+        scoped_reset _scoped_reset(*this, procs);
+
         for (source const& curr : sources) {
             if (curr.is_fresh_value()) {
                 sort * s = curr.get_value()->get_sort();
@@ -336,22 +339,15 @@ namespace smt {
                         enode * child = d.get_enode();
                         TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
                         child = child->get_root();
-                        app * val = nullptr;
-                        m_root2value.find(child, val);
-                        SASSERT(val);
-                        dependency_values.push_back(val);
+                        dependency_values.push_back(m_root2value[child]);
                     }
                 }
                 app * val = proc->mk_value(*this, dependency_values); 
                 register_value(val);
                 m_asts.push_back(val);
                 m_root2value.insert(n, val);
             }
-        }
-        std::for_each(procs.begin(), procs.end(), delete_proc<model_value_proc>());
-        std::for_each(m_extra_fresh_values.begin(), m_extra_fresh_values.end(), delete_proc<extra_fresh_value>());
-        m_extra_fresh_values.reset();
-
+        }        
         // send model
         for (enode * n : m_context->enodes()) {
             if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
@@ -364,11 +360,17 @@ namespace smt {
         }
     }
 
+    model_generator::scoped_reset::scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs): 
+        mg(mg), procs(procs) {}
+
+    model_generator::scoped_reset::~scoped_reset() {
+        std::for_each(procs.begin(), procs.end(), delete_proc<model_value_proc>());
+        std::for_each(mg.m_extra_fresh_values.begin(), mg.m_extra_fresh_values.end(), delete_proc<extra_fresh_value>());
+        mg.m_extra_fresh_values.reset();
+    }
+
     app * model_generator::get_value(enode * n) const {
-        app * val = nullptr;
-        m_root2value.find(n->get_root(), val);
-        SASSERT(val);
-        return val;
+        return m_root2value[n->get_root()];
     }
 
     /**
@@ -490,7 +492,7 @@ namespace smt {
         finalize_theory_models();
         register_macros();
         TRACE("model", model_v2_pp(tout, *m_model, true););
-        return m_model;
+        return m_model.get();
     }
 
 };

src/smt/smt_model_generator.h

@@ -32,6 +32,7 @@ Revision History:
 #include "smt/smt_types.h"
 #include "util/obj_hashtable.h"
 #include "util/map.h"
+#include "util/ref.h"
 
 class value_factory;
 class proto_model;
@@ -146,7 +147,7 @@ namespace smt {
            \brief The array values has size equal to the size of the argument \c result in get_dependencies.
            It contain the values built for the dependencies.
         */
-        virtual app * mk_value(model_generator & m, ptr_vector<expr> & values) = 0;
+        virtual app * mk_value(model_generator & m, expr_ref_vector const & values) = 0;
         /**
            \brief Return true if it is associated with a fresh value.
         */
@@ -161,15 +162,15 @@ namespace smt {
         app * m_value;
     public:
         expr_wrapper_proc(app * v):m_value(v) {}
-        app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return m_value; }
+        app * mk_value(model_generator & m, expr_ref_vector const & values) override { return m_value; }
     };
 
     class fresh_value_proc : public model_value_proc {
         extra_fresh_value * m_value;
     public:
         fresh_value_proc(extra_fresh_value * v):m_value(v) {}
         void get_dependencies(buffer<model_value_dependency> & result) override;
-        app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
+        app * mk_value(model_generator & m, expr_ref_vector const & values) override { return to_app(values[0]); }
         bool is_fresh() const override { return true; }
     };
 
@@ -183,7 +184,7 @@ namespace smt {
         unsigned                      m_fresh_idx;
         obj_map<enode, app *>         m_root2value;
         ast_ref_vector                m_asts;
-        proto_model *                 m_model;
+        ref<proto_model>              m_model;
         obj_hashtable<func_decl>      m_hidden_ufs;
 
         void init_model();
@@ -205,6 +206,13 @@ namespace smt {
 
         void top_sort_sources(ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc, svector<source> & sorted_sources);
 
+        struct scoped_reset {
+            model_generator& mg;
+            ptr_vector<model_value_proc>& procs;
+            scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs);
+            ~scoped_reset();            
+        };
+
     public:
         model_generator(ast_manager & m);
         ~model_generator();
@@ -219,7 +227,7 @@ namespace smt {
         proto_model & get_model() { SASSERT(m_model); return *m_model; }
         void register_value(expr * val);
         ast_manager & get_manager() { return m_manager; }
-        proto_model * mk_model();
+        proto_model* mk_model();
 
         obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
         app * get_value(enode * n) const;

src/smt/theory_array_base.cpp

@@ -910,7 +910,7 @@ namespace smt {
             result.append(m_dependencies.size(), m_dependencies.c_ptr());
         }
 
-        app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
+        app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
             // values must have size = m_num_entries * (m_dim + 1) + ((m_else || m_unspecified_else) ? 0 : 1) 
             // an array value is a lookup table + else_value
             // each entry has m_dim indexes that map to a value.

src/smt/theory_datatype.cpp

@@ -691,7 +691,7 @@ namespace smt {
         void get_dependencies(buffer<model_value_dependency> & result) override {
             result.append(m_dependencies.size(), m_dependencies.c_ptr());
         }
-        app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
+        app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
             SASSERT(values.size() == m_dependencies.size());
             return mg.get_manager().mk_app(m_constructor, values.size(), values.c_ptr());
         }

src/smt/theory_dl.cpp

@@ -76,7 +76,7 @@ namespace smt {
 
             void get_dependencies(buffer<smt::model_value_dependency> & result) override {}
 
-            app * mk_value(smt::model_generator & mg, ptr_vector<expr> & ) override {
+            app * mk_value(smt::model_generator & mg, expr_ref_vector const & ) override {
                 smt::context& ctx = m_th.get_context();
                 app* result = nullptr;
                 expr* n = m_node->get_owner();

src/smt/theory_fpa.cpp

@@ -125,7 +125,7 @@ namespace smt {
         m_is_initialized = true;
     }
 
-    app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
+    app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) {
         TRACE("t_fpa_detail",
               ast_manager & m = m_th.get_manager();
               for (unsigned i = 0; i < values.size(); i++)
@@ -200,7 +200,7 @@ namespace smt {
         return result;
     }
 
-    app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
+    app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) {
         SASSERT(values.size() == 1);
 
         TRACE("t_fpa_detail",

src/smt/theory_fpa.h

@@ -120,7 +120,7 @@ namespace smt {
                 result.append(m_deps);
             }
 
-            app * mk_value(model_generator & mg, ptr_vector<expr> & values) override;
+            app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
         };
 
         class fpa_rm_value_proc : public model_value_proc {
@@ -141,7 +141,7 @@ namespace smt {
             }
 
             ~fpa_rm_value_proc() override {}
-            app * mk_value(model_generator & mg, ptr_vector<expr> & values) override;
+            app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
         };
 
     protected:

src/smt/theory_pb.cpp

@@ -2326,7 +2326,7 @@ namespace smt {
             result.append(m_dependencies.size(), m_dependencies.c_ptr());
         }
 
-        app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
+        app * mk_value(model_generator & mg, expr_ref_vector const& values) override {
             ast_manager& m = mg.get_manager();
             SASSERT(values.size() == m_dependencies.size());
             SASSERT(values.size() == m_app->get_num_args());

src/smt/theory_seq.cpp

@@ -2113,12 +2113,14 @@ bool theory_seq::check_extensionality() {
                 m_lhs.reset(); m_rhs.reset();
                 bool change = false;
                 if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
+                    TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
                     m_exclude.update(o1, o2);
                     continue;
                 }
                 bool excluded = false;
                 for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
-                    if (m_exclude.contains(m_lhs[j].get(), m_rhs[j].get())) {
+                    if (m_exclude.contains(m_lhs.get(j), m_rhs.get(j))) {
+                        TRACE("seq", tout << "excluded " << j << " " << m_lhs << " " << m_rhs << "\n";);
                         excluded = true;
                     }
                 }
@@ -2517,15 +2519,22 @@ bool theory_seq::occurs(expr* a, expr* b) {
         b = m_todo.back();
         if (a == b || m.is_ite(b)) {
             m_todo.reset();
+            std::cout << " yes\n";
             return true;
         }
         m_todo.pop_back();
         if (m_util.str.is_concat(b, e1, e2)) {
             m_todo.push_back(e1);
             m_todo.push_back(e2);
         }
+        else if (m_util.str.is_unit(b, e1)) {
+            m_todo.push_back(e1);
+        }
+        else if (m_util.str.is_nth(b, e1, e2)) {
+            m_todo.push_back(e1);
+        }
     }
-     return false;
+    return false;
 }
 
 
@@ -2536,7 +2545,7 @@ bool theory_seq::is_var(expr* a) const {
         !m_util.str.is_empty(a)  &&
         !m_util.str.is_string(a) &&
         !m_util.str.is_unit(a) &&
-        !m_util.str.is_itos(a) && 
+        !m_util.str.is_itos(a) &&
         // !m_util.str.is_extract(a) && 
         !m.is_ite(a);
 }
@@ -3981,7 +3990,7 @@ class theory_seq::seq_value_proc : public model_value_proc {
         }
     }
 
-    app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
+    app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
         SASSERT(values.size() == m_dependencies.size());
         expr_ref_vector args(th.m);
         unsigned j = 0, k = 0;
@@ -5182,8 +5191,8 @@ void theory_seq::add_at_axiom(expr* e) {
     }
     else {
         expr_ref len_e = mk_len(e);
-        expr_ref x = mk_skolem(m_pre, s, i);
-        expr_ref y = mk_skolem(m_tail, s, i);
+        expr_ref x =     mk_skolem(m_pre, s, i);
+        expr_ref y =     mk_skolem(m_tail, s, i);
         expr_ref xey   = mk_concat(x, e, y);
         expr_ref len_x = mk_len(x);
         add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
@@ -5208,7 +5217,10 @@ void theory_seq::add_nth_axiom(expr* e) {
         expr_ref zero(m_autil.mk_int(0), m);
         literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
         literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
-        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));        
+        // at(s,i) = [nth(s,i)]
+        expr_ref rhs(s, m);
+        if (!m_util.str.is_at(s)) rhs = m_util.str.mk_at(s, i);
+        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), rhs, false));        
     }
 }
 

src/smt/theory_seq.h

@@ -399,7 +399,7 @@ namespace smt {
         void add_theory_assumptions(expr_ref_vector & assumptions) override;
         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"; }
-        bool include_func_interp(func_decl* f) override { return m_util.str.is_nth(f); }
+        bool include_func_interp(func_decl* f) override { return false; } // m_util.str.is_nth(f); }
         theory_var mk_var(enode* n) override;
         void apply_sort_cnstr(enode* n, sort* s) override;
         void display(std::ostream & out) const override;