deal with model construction, issue #684. fix model construction for ite #678. WIth this version, issue #686 does not repro

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

src/cmd_context/cmd_context.cpp

@@ -1634,6 +1634,7 @@ void cmd_context::validate_model() {
         scoped_ctrl_c ctrlc(eh);
         ptr_vector<expr>::const_iterator it  = begin_assertions();
         ptr_vector<expr>::const_iterator end = end_assertions();
+        bool invalid_model = false;
         for (; it != end; ++it) {
             expr * a = *it;
             if (is_ground(a)) {
@@ -1654,9 +1655,10 @@ void cmd_context::validate_model() {
                     continue;
                 }
                 TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
-                throw cmd_exception("an invalid model was generated");
+                invalid_model = true;
             }
         }
+        throw cmd_exception("an invalid model was generated");
     }
 }
 

src/smt/theory_seq.cpp

@@ -196,6 +196,7 @@ theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")),
     m(m),
     m_rep(m, m_dm),
+    m_reset_cache(false),
     m_eq_id(0),
     m_find(*this),
     m_factory(0),
@@ -242,6 +243,10 @@ void theory_seq::init(context* ctx) {
 }
 
 final_check_status theory_seq::final_check_eh() {
+    if (m_reset_cache) {
+        m_rep.reset_cache(); 
+        m_reset_cache = false;
+    }
     m_new_propagation = false;
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
     if (simplify_and_solve_eqs()) {
@@ -1366,7 +1371,7 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
 
 bool theory_seq::occurs(expr* a, expr_ref_vector const& b) {
     for (unsigned i = 0; i < b.size(); ++i) {
-        if (a == b[i]) return true;
+        if (a == b[i] || m.is_ite(b[i])) return true;
     }
     return false;
 }
@@ -1379,7 +1384,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
     m_todo.push_back(b);
     while (!m_todo.empty()) {
         b = m_todo.back();
-        if (a == b) {
+        if (a == b || m.is_ite(b)) {
             m_todo.reset();
             return true;
         }
@@ -2421,6 +2426,11 @@ void theory_seq::init_model(expr_ref_vector const& es) {
 void theory_seq::init_model(model_generator & mg) {
     m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
     mg.register_factory(m_factory);
+    for (unsigned j = 0; j < m_nqs.size(); ++j) {
+        ne const& n = m_nqs[j];
+        m_factory->register_value(n.l());
+        m_factory->register_value(n.r());  
+    }
     for (unsigned j = 0; j < m_nqs.size(); ++j) {
         ne const& n = m_nqs[j];
         for (unsigned i = 0; i < n.ls().size(); ++i) {
@@ -2452,6 +2462,13 @@ public:
     virtual void get_dependencies(buffer<model_value_dependency> & result) {
         result.append(m_dependencies.size(), m_dependencies.c_ptr());
     }
+
+    void add_buffer(svector<unsigned>& sbuffer, zstring const& zs) {
+        for (unsigned l = 0; l < zs.length(); ++l) {
+            sbuffer.push_back(zs[l]);
+        }        
+    }
+
     virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == m_dependencies.size());
         expr_ref_vector args(th.m);
@@ -2470,12 +2487,16 @@ public:
                     sbuffer.push_back(val.get_unsigned());
                 }
                 else {
+                    dependency* deps = 0;
+                    expr_ref tmp = th.canonize(m_strings[k], deps);
                     zstring zs;
-                    if (th.m_util.str.is_string(m_strings[k++], zs)) {
-                        for (unsigned l = 0; l < zs.length(); ++l) {
-                            sbuffer.push_back(zs[l]);
-                        }
+                    if (th.m_util.str.is_string(tmp, zs)) {
+                        add_buffer(sbuffer, zs);
                     }
+                    else {
+                        TRACE("seq", tout << "Not a string: " << tmp << "\n";);
+                    }
+                    ++k;
                 }
             }
             result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
@@ -2657,7 +2678,10 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
             result = expand(e3, deps);
             break;
         case l_undef:
-            result = e;
+            result = e;            
+            m_reset_cache = true;
+            TRACE("seq", tout << "undef: " << result << "\n";
+                  tout << lit << "@ level: " << ctx.get_scope_level() << "\n";);
             break;
         }
     }

src/smt/theory_seq.h

@@ -294,6 +294,7 @@ namespace smt {
         ast_manager&               m;
         dependency_manager         m_dm;
         solution_map               m_rep;        // unification representative.
+        bool                       m_reset_cache; // invalidate cache.
         scoped_vector<eq>          m_eqs;        // set of current equations.
         scoped_vector<ne>          m_nqs;        // set of current disequalities.
         scoped_vector<nc>          m_ncs;        // set of non-contains constraints.

src/smt/theory_seq_empty.h

@@ -126,6 +126,22 @@ namespace smt {
             symbol sym;
             if (u.str.is_string(n, sym)) {
                 m_strings.insert(sym);
+                if (sym.str().find(m_unique_delim) != std::string::npos) {
+                    add_new_delim();
+                }
+            }
+        }
+    private:
+
+        void add_new_delim() {
+            bool found = true;
+            while (found) {
+                found = false;
+                m_unique_delim += "!";
+                symbol_set::iterator it = m_strings.begin(), end = m_strings.end();
+                for (; it != end && !found; ++it) {
+                    found = it->str().find(m_unique_delim) != std::string::npos;                    
+                }
             }
         }
     };