fixing build break, addressing #935

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

src/cmd_context/cmd_context.cpp

@@ -1551,6 +1551,7 @@ void cmd_context::validate_model() {
     p.set_uint("sort_store", true);
     p.set_bool("completion", true);
     model_evaluator evaluator(*(md.get()), p);
+    evaluator.set_expand_array_equalities(false);
     contains_array_op_proc contains_array(m());
     {
         scoped_rlimit _rlimit(m().limit(), 0);

src/smt/mam.cpp

@@ -3942,7 +3942,7 @@ namespace smt {
 #endif
         
         virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) {
-            TRACE("trigger_bug", tout << "found match\n";);
+            TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
 #ifdef Z3DEBUG
             if (m_check_missing_instances) {
                 if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) {

src/smt/smt_context.cpp

@@ -304,7 +304,6 @@ namespace smt {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";              
               display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
               display(tout, j););
-        SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
         m_assigned_literals.push_back(l);
         m_assignment[l.index()]    = l_true;
         m_assignment[(~l).index()] = l_false;
@@ -319,14 +318,23 @@ namespace smt {
         d.m_phase_available        = true;
         d.m_phase                  = !l.sign();
         TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
+
         TRACE("relevancy", 
-              tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";);
+              tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
-        if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
+        if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
             m_atom_propagation_queue.push_back(l);
 
         if (m_manager.has_trace_stream())
             trace_assign(l, j, decision);
         m_case_split_queue->assign_lit_eh(l);
+
+        // a unit is asserted at search level. Mark it as relevant.
+        // this addresses bug... where a literal becomes fixed to true (false)
+        // as a conflict gets assigned misses relevancy (and quantifier instantiation).
+        // 
+        if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) {
+            mark_as_relevant(l);
+        }
     }
     
     bool context::bcp() {
@@ -1634,7 +1642,7 @@ namespace smt {
                     m_atom_propagation_queue.push_back(literal(v, val == l_false));
             }
         }
-        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << "\n";);
+        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";);
 #ifndef SMTCOMP
         m_case_split_queue->relevant_eh(n);
 #endif
@@ -3737,7 +3745,9 @@ namespace smt {
             // I invoke pop_scope_core instead of pop_scope because I don't want
             // to reset cached generations... I need them to rebuild the literals
             // of the new conflict clause.
+            if (relevancy()) record_relevancy(num_lits, lits);
             unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl);
+            if (relevancy()) restore_relevancy(num_lits, lits);
             SASSERT(m_scope_lvl == new_lvl);
             // the logical context may still be in conflict after
             // clauses are reinitialized in pop_scope.
@@ -3850,6 +3860,28 @@ namespace smt {
         }
         return false;
     }
+    
+    /*
+      \brief we record and restore relevancy information for literals in conflict clauses.
+      A literal may have been marked relevant within the scope that gets popped during
+      conflict resolution. In this case, the literal is no longer marked as relevant after
+      the pop. This can cause quantifier instantiation to miss relevant triggers and thereby
+      cause incmpleteness.
+     */
+    void context::record_relevancy(unsigned n, literal const* lits) {
+        m_relevant_conflict_literals.reset();
+        for (unsigned i = 0; i < n; ++i) {
+            m_relevant_conflict_literals.push_back(is_relevant(lits[i]));
+        }
+    }
+
+    void context::restore_relevancy(unsigned n, literal const* lits) {
+        for (unsigned i = 0; i < n; ++i) {
+            if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) {
+                mark_as_relevant(lits[i]);
+            }
+        }
+    }
 
     void context::get_relevant_labels(expr* cnstr, buffer<symbol> & result) {
         if (m_fparams.m_check_at_labels) {

src/smt/smt_context.h

@@ -1103,6 +1103,10 @@ namespace smt {
 
         bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); }
 
+        svector<bool>  m_relevant_conflict_literals;
+        void record_relevancy(unsigned n, literal const* lits);
+        void restore_relevancy(unsigned n, literal const* lits);
+
     public:
         // event handler for relevancy_propagator class
         void relevant_eh(expr * n);
@@ -1124,6 +1128,10 @@ namespace smt {
             return is_relevant(l.var());
         }
 
+        bool is_relevant_core(literal l) const {
+            return is_relevant_core(bool_var2expr(l.var()));
+        }
+
         void mark_as_relevant(expr * n) { m_relevancy_propagator->mark_as_relevant(n); m_relevancy_propagator->propagate(); }
 
         void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); }

src/smt/smt_quantifier.cpp

@@ -52,8 +52,9 @@ namespace smt {
             m_qi_queue.setup();
         }
 
-        bool has_trace_stream() const { return m_context.get_manager().has_trace_stream(); }
+        ast_manager& m() const { return m_context.get_manager(); }
-        std::ostream & trace_stream() { return m_context.get_manager().trace_stream(); }
+        bool has_trace_stream() const { return m().has_trace_stream(); }
+        std::ostream & trace_stream() { return m().trace_stream(); }
 
         quantifier_stat * get_stat(quantifier * q) const {
             return m_quantifier_stat.find(q);
@@ -110,8 +111,9 @@ namespace smt {
                           unsigned max_top_generation,
                           ptr_vector<enode> & used_enodes) {
             max_generation = std::max(max_generation, get_generation(q));
-            if (m_num_instances > m_params.m_qi_max_instances)
+            if (m_num_instances > m_params.m_qi_max_instances) {
                 return false;
+            }
             get_stat(q)->update_max_generation(max_generation);
             fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
             if (f) {
@@ -132,9 +134,17 @@ namespace smt {
                 }
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
                 m_num_instances++;
-                return true;
             }
-            return false;
+            TRACE("quantifier", 
+                  tout << mk_pp(q, m()) << " ";
+                  for (unsigned i = 0; i < num_bindings; ++i) {
+                      tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
+                  }
+                  tout << "\n";
+                  tout << "inserted: " << (f != 0) << "\n";
+                  );
+
+            return f != 0;
         }
 
         void init_search_eh() {
@@ -186,7 +196,7 @@ namespace smt {
         }
 
         bool check_quantifier(quantifier* q) {
-            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m_context.get_manager().is_rec_fun_def(q);
+            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m().is_rec_fun_def(q);
         }
 
         bool quick_check_quantifiers() {
@@ -501,13 +511,13 @@ namespace smt {
                 SASSERT(m_context->get_manager().is_pattern(mp));
                 bool unary = (mp->get_num_args() == 1);
                 if (!unary && j >= num_eager_multi_patterns) {
-                    TRACE("assign_quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
+                    TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
                           << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns
                           << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";);
                     m_lazy_mam->add_pattern(q, mp);
                 }
                 else {
-                    TRACE("assign_quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";);
+                    TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";);
                     m_mam->add_pattern(q, mp);
                 }
                 if (!unary)