fix #2531

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

src/ast/for_each_expr.cpp

@@ -63,3 +63,49 @@ bool has_skolem_functions(expr * n) {
     }
     return false;
 }
+
+subterms::subterms(expr_ref_vector const& es): m_es(es) {}
+subterms::subterms(expr_ref& e) : m_es(e.m()) { m_es.push_back(e); }
+subterms::iterator subterms::begin() { return iterator(*this, true); }
+subterms::iterator subterms::end() { return iterator(*this, false); }
+subterms::iterator::iterator(subterms& f, bool start): m_es(f.m_es) {
+    if (!start) m_es.reset();
+}
+expr* subterms::iterator::operator*() {
+    return m_es.back();
+}
+subterms::iterator subterms::iterator::operator++(int) {
+    iterator tmp = *this;
+    ++*this;
+    return tmp;
+}
+subterms::iterator& subterms::iterator::operator++() {
+    expr* e = m_es.back();
+    m_visited.mark(e, true);
+    if (is_app(e)) {
+        for (expr* arg : *to_app(e)) {
+            m_es.push_back(arg);
+        }
+    }
+    while (m_visited.is_marked(m_es.back())) {
+        m_es.pop_back();
+    }
+    return *this;
+}
+
+bool subterms::iterator::operator==(iterator const& other) const {
+    // ignore state of visited
+    if (other.m_es.size() != m_es.size()) {
+        return false;
+    }
+    for (unsigned i = m_es.size(); i-- > 0; ) {
+        if (m_es.get(i) != other.m_es.get(i))
+            return false;
+    }
+    return true;
+}
+
+bool subterms::iterator::operator!=(iterator const& other) const {
+    return !(*this == other);
+}
+

src/ast/for_each_expr.h

@@ -167,5 +167,25 @@ unsigned get_num_exprs(expr * n, expr_fast_mark1 & visited);
 
 bool has_skolem_functions(expr * n);
 
+class subterms {
+    expr_ref_vector m_es;
+public:
+    class iterator {
+        expr_ref_vector m_es;
+        expr_mark       m_visited;        
+    public:
+        iterator(subterms& f, bool start);
+        expr* operator*();
+        iterator operator++(int);
+        iterator& operator++();
+        bool operator==(iterator const& other) const;
+        bool operator!=(iterator const& other) const;
+    };
+    subterms(expr_ref_vector const& es);
+    subterms(expr_ref& e);
+    iterator begin();
+    iterator end();
+};
+
 #endif /* FOR_EACH_EXPR_H_ */
 

src/qe/nlqsat.cpp

@@ -666,7 +666,7 @@ namespace qe {
 
         // expr -> nlsat::solver
 
-        void hoist(expr_ref& fml) {
+        bool hoist(expr_ref& fml) {
             expr_ref_vector paxioms(m);
             ackermanize_div(fml, paxioms);
             quantifier_hoister hoist(m);
@@ -674,7 +674,6 @@ namespace qe {
             app_ref_vector vars(m);
             bool is_forall = false;   
             pred_abs abs(m);
-
             expr_ref fml_a(m.mk_and(fml, mk_and(paxioms)), m);
             abs.get_free_vars(fml_a, vars);
             insert_set(m_free_vars, vars);
@@ -752,6 +751,7 @@ namespace qe {
                 }
             }
             TRACE("qe", tout << fml << "\n";);
+            return true;
         }
 
 
@@ -836,7 +836,10 @@ namespace qe {
             }                         
             reset();
             TRACE("qe", tout << fml << "\n";);
-            hoist(fml);
+            if (!hoist(fml)) {
+                result.push_back(in.get());
+                return;
+            }
             TRACE("qe", tout << "ex: " << fml << "\n";);
             lbool is_sat = check_sat();
             

src/qe/qsat.cpp

@@ -511,14 +511,14 @@ namespace qe {
 
     bool pred_abs::validate_defs(model& model) const {
         bool valid = true;
-        obj_map<expr, expr*>::iterator it = m_pred2lit.begin(), end = m_pred2lit.end();
-        for (; it != end; ++it) {
+        for (auto& kv : m_pred2lit) {
             expr_ref val_a(m), val_b(m);
-            expr* a = it->m_key;
-            expr* b = it->m_value;
+            expr* a = kv.m_key;
+            expr* b = kv.m_value;
             val_a = model(a);
             val_b = model(b);
-            if (val_a != val_b) {
+            if ((m.is_true(val_a) && m.is_false(val_b)) || 
+                (m.is_false(val_a) && m.is_true(val_b))) {
                 TRACE("qe", 
                       tout << mk_pp(a, m) << " := " << val_a << "\n";
                       tout << mk_pp(b, m) << " := " << val_b << "\n";

src/smt/theory_seq.cpp

@@ -339,6 +339,7 @@ final_check_status theory_seq::final_check_eh() {
         m_rep.reset_cache(); 
         m_reset_cache = false;
     }
+
     m_new_propagation = false;
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
     TRACE("seq_verbose", get_context().display(tout););
@@ -3320,7 +3321,7 @@ bool theory_seq::solve_nc(unsigned idx) {
     expr_ref c = canonize(n.contains(), deps);
     expr* a = nullptr, *b = nullptr;
 
-    CTRACE("seq", c != n.contains(), tout << n.contains() << " => " << c << "\n";);
+    CTRACE("seq", c != n.contains(), tout << n.contains() << " =>\n" << c << "\n";);
 
     
     if (m.is_true(c)) {
@@ -3334,6 +3335,9 @@ bool theory_seq::solve_nc(unsigned idx) {
     }
 
     if (ctx.get_assignment(len_gt) == l_true) {
+        VERIFY(m_util.str.is_contains(n.contains(), a, b));
+        enforce_length(a);
+        enforce_length(b);
         TRACE("seq", tout << len_gt << " is true\n";);
         return true;
     }
@@ -3605,6 +3609,7 @@ bool theory_seq::internalize_term(app* term) {
 }
 
 void theory_seq::add_length(expr* e, expr* l) {
+    TRACE("seq", tout << get_context().get_scope_level() << " " << mk_pp(e, m) << "\n";);
     SASSERT(!m_length.contains(l));
     m_length.push_back(l);
     m_has_length.insert(e);
@@ -4278,9 +4283,9 @@ bool theory_seq::can_propagate() {
 
 expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
     expr_ref result = expand(e, eqs);
-    TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " expands to\n" << result << "\n";);
     m_rewrite(result);
-    TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " rewrites to\n" << result << "\n";);
     return result;
 }