fix bug reported in issue #193: MBQI needs to avoid instantiating data-types that contain model values in nested positions

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

src/sat/sat_bceq.cpp

@@ -45,6 +45,7 @@ namespace sat {
         m_R.reset();
         m_L_blits.reset();
         m_R_blits.reset();
+        m_bce_use_list.finalize();
         clause * const* it = m_solver.begin_clauses();
         clause * const* end = m_solver.end_clauses();
         for (; it != end; ++it) {
@@ -140,7 +141,6 @@ namespace sat {
         for (unsigned i = 0; i < m_L.size(); ++i) {
             ul.insert(*m_L[i]);
         }
-#define MOVE_R_TO_L                             \
 
         // cheap pass: add clauses from R in order
         // such that they are blocked with respect to
@@ -161,6 +161,10 @@ namespace sat {
         }
         // expensive pass: add clauses from R as long
         // as BCE produces the empty set of clauses.
+        m_bce_use_list.init(m_solver.num_vars());
+        for (unsigned i = 0; i < m_L.size(); ++i) {
+            m_bce_use_list.insert(*m_L[i]);
+        }
         for (unsigned i = 0; i < m_R.size(); ++i) {
             if (bce(*m_R[i])) {
                 m_R[i] = m_R.back();
@@ -173,29 +177,29 @@ namespace sat {
         m_use_list = save;
     }
 
-    bool bceq::bce(clause& cls) {
+    bool bceq::bce(clause& cls0) {
+        IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";);
         svector<bool> live_clauses;
-        use_list ul;
+        m_use_list = &m_bce_use_list;
-        m_use_list = &ul;
+        m_bce_use_list.insert(cls0);
-        ul.init(m_solver.num_vars());
-        for (unsigned i = 0; i < m_L.size(); ++i) {
-            ul.insert(*m_L[i]);
-        }
-        ul.insert(cls);
         svector<clause*> clauses(m_L), new_clauses;
         literal_vector blits(m_L_blits), new_blits;
-        clauses.push_back(&cls);
+        clauses.push_back(&cls0);
         blits.push_back(null_literal);
         bool removed = false;
         m_removed.reset();
         do {
             removed = false;
             for (unsigned i = 0; i < clauses.size(); ++i) {
-                clause& cls = *clauses[i];
+                clause& cls1 = *clauses[i];
-                literal lit = find_blocked(cls);
+                literal lit = find_blocked(cls1);
-                if (lit != null_literal) {
+                if (lit == null_literal) {
-                    m_removed.setx(cls.id(), true, false);
+                    m_bce_use_list.erase(cls1);
-                    new_clauses.push_back(&cls);
+                }
+                else {
+                    IF_VERBOSE(2, verbose_stream() << "; remove " << cls1 << "\n";);
+                    m_removed.setx(cls1.id(), true, false);
+                    new_clauses.push_back(&cls1);
                     new_blits.push_back(lit);
                     removed = true;
                     clauses[i] = clauses.back();
@@ -215,7 +219,7 @@ namespace sat {
             m_L.append(new_clauses);
             m_L_blits.append(new_blits);
         }
-        if (!clauses.empty()) std::cout << "Number left after BCE: " << clauses.size() << "\n";
+        IF_VERBOSE(1, if (!clauses.empty()) verbose_stream() << "; clauses left after BCE: " << clauses.size() << "\n";);
         return clauses.empty();
     }
 
@@ -442,9 +446,10 @@ namespace sat {
         roots[l2.var()] = l1;
         vars.push_back(l2.var());
         elim_eqs elim(m_solver);
-        for (unsigned i = 0; i < vars.size(); ++i) {
+        IF_VERBOSE(1, 
-            std::cout << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n";
+                   for (unsigned i = 0; i < vars.size(); ++i) {
-        }
+                       verbose_stream() << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n";
+                   });
         elim(roots, vars);
     }
 
@@ -473,7 +478,7 @@ namespace sat {
         init();
         pure_decompose();
         post_decompose();
-        std::cout << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n";
+        IF_VERBOSE(1, verbose_stream() << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n";);
 
         TRACE("sat",
               tout << "Decomposed set " << m_L.size() << "\n";

src/sat/sat_bceq.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include"sat_types.h"
 #include "union_find.h"
+#include "sat_simplifier.h"
 
 
 namespace sat {
@@ -33,6 +34,7 @@ namespace sat {
         typedef svector<bin_clause> bin_clauses;        
         solver &          m_solver;
         use_list*         m_use_list;
+        use_list          m_bce_use_list;
         solver*           m_s;
         random_gen        m_rand;
         svector<clause*>  m_clauses;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -100,6 +100,7 @@ public:
     virtual void set_progress_callback(progress_callback * callback) {}
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {        
+
         m_solver.pop_to_base_level();
         dep2asm_t dep2asm;
         m_model = 0;
@@ -112,6 +113,7 @@ public:
         r = initialize_soft_constraints();
         if (r != l_true) return r;
 
+        m_solver.display_dimacs(std::cout);
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         switch (r) {
         case l_true:

src/smt/smt_model_checker.cpp

@@ -171,7 +171,7 @@ namespace smt {
                     sk_value = sk_term;
                 }
             }
-            if (m_manager.is_model_value(sk_value))
+            if (contains_model_value(sk_value))
                 return false;
             bindings.set(num_decls - i - 1, sk_value);
         }
@@ -190,6 +190,30 @@ namespace smt {
         return true;
     }
 
+    void model_checker::operator()(expr *n) {
+        if (m_manager.is_model_value(n)) {
+            throw is_model_value();
+        }
+    }
+
+    bool model_checker::contains_model_value(expr* n) {
+        if (m_manager.is_model_value(n)) {
+            return true;
+        }
+        if (is_app(n) && to_app(n)->get_num_args() == 0) {
+            return false;
+        }
+        m_visited.reset();
+        try {
+            for_each_expr(*this, m_visited, n);
+        }
+        catch (is_model_value) {
+            return true;
+        }
+        return false;
+    }
+
+
     bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
         SASSERT(cex != 0);
         unsigned num_sks  = sks.size();

src/smt/smt_model_checker.h

@@ -80,6 +80,10 @@ namespace smt {
 
         quantifier * get_flat_quantifier(quantifier * q);
 
+        struct is_model_value {};
+        expr_mark m_visited;
+        bool contains_model_value(expr* e);
+
     public:
         model_checker(ast_manager & m, qi_params const & p, model_finder & mf);
         ~model_checker();
@@ -95,6 +99,9 @@ namespace smt {
         void reset();
 
         void set_cancel(bool f) { m_cancel = f; }
+
+        void operator()(expr* e);
+
     };
 };
 

src/smt/smt_model_finder.cpp

@@ -83,6 +83,7 @@ namespace smt {
             ast_manager &           m_manager;
             obj_map<expr, unsigned> m_elems; // and the associated generation
             obj_map<expr, expr *>   m_inv;
+            expr_mark               m_visited;
         public:
             instantiation_set(ast_manager & m):m_manager(m) {}
             
@@ -98,11 +99,11 @@ namespace smt {
             obj_map<expr, unsigned> const & get_elems() const { return m_elems; }
 
             void insert(expr * n, unsigned generation) {
-                if (m_elems.contains(n))
+                if (m_elems.contains(n) || contains_model_value(n))
                     return;
+                TRACE("model_finder", tout << mk_pp(n, m_manager) << "\n";);
                 m_manager.inc_ref(n);
                 m_elems.insert(n, generation);
-                CTRACE("model_finder", m_manager.is_model_value(n), tout << mk_pp(n, m_manager) << "\n";);
                 SASSERT(!m_manager.is_model_value(n));
             }
 
@@ -145,9 +146,10 @@ namespace smt {
                 obj_map<expr, unsigned>::iterator end = m_elems.end();
                 for (; it != end; ++it) {
                     expr *     t = (*it).m_key;
-                    SASSERT(!m_manager.is_model_value(t));
+                    SASSERT(!contains_model_value(t));
                     unsigned gen = (*it).m_value;
                     expr * t_val = ev.eval(t, true);
+                    TRACE("model_finder", tout << mk_pp(t, m_manager) << "\n";);
 
                     expr * old_t = 0;
                     if (m_inv.find(t_val, old_t)) {
@@ -167,6 +169,30 @@ namespace smt {
             obj_map<expr, expr *> const & get_inv_map() const {
                 return m_inv;
             }
+
+            struct is_model_value {};
+            void operator()(expr *n) {
+                if (m_manager.is_model_value(n)) {
+                    throw is_model_value();
+                }
+            }
+
+            bool contains_model_value(expr* n) {
+                if (m_manager.is_model_value(n)) {
+                    return true;
+                }
+                if (is_app(n) && to_app(n)->get_num_args() == 0) {
+                    return false;
+                }
+                m_visited.reset();
+                try {
+                    for_each_expr(*this, m_visited, n);
+                }
+                catch (is_model_value) {
+                    return true;
+                }
+                return false;
+            }
         };
 
         /**
@@ -286,7 +312,7 @@ namespace smt {
                 return get_root()->m_signed_proj;
             }
 
-            void mk_instatiation_set(ast_manager & m) {
+            void mk_instantiation_set(ast_manager & m) {
                 SASSERT(is_root());
                 m_set = alloc(instantiation_set, m);
             }
@@ -527,13 +553,13 @@ namespace smt {
                 return 0;
             }
             
-            void mk_instatiation_sets() {
+            void mk_instantiation_sets() {
                 ptr_vector<node>::const_iterator it  = m_nodes.begin();
                 ptr_vector<node>::const_iterator end = m_nodes.end();
                 for (; it != end; ++it) {
                     node * curr = *it;
                     if (curr->is_root()) {
-                        curr->mk_instatiation_set(m_manager);
+                        curr->mk_instantiation_set(m_manager);
                     }
                 }
             }
@@ -695,6 +721,7 @@ namespace smt {
                     return 0;
                 m_model->register_decl(k_decl, r);
                 SASSERT(m_model->get_const_interp(k_decl) == r);
+                TRACE("model_finder", tout << mk_pp(r, m_manager) << "\n";);
                 return r;
             }
 
@@ -1204,7 +1231,7 @@ namespace smt {
                         // a necessary instantiation.
                         enode * e_arg = n->get_arg(m_arg_i);
                         expr * arg    = e_arg->get_owner();
-                        A_f_i->insert(arg, e_arg->get_generation());
+                        A_f_i->insert(arg, e_arg->get_generation());                        
                     }
                 }
             }
@@ -1225,7 +1252,7 @@ namespace smt {
                     if (ctx->is_relevant(n)) {
                         enode * e_arg = n->get_arg(m_arg_i);
                         expr * arg    = e_arg->get_owner();
-                        s->insert(arg, e_arg->get_generation());
+                        s->insert(arg, e_arg->get_generation());                        
                     }
                 }
             }
@@ -3378,7 +3405,7 @@ namespace smt {
             quantifier_info * qi = get_quantifier_info(q);
             qi->process_auf(*(m_auf_solver.get()), m_context);
         }
-        m_auf_solver->mk_instatiation_sets();
+        m_auf_solver->mk_instantiation_sets();
         it  = qs.begin();
         for (; it != end; ++it) {
             quantifier * q       = *it;

src/smt/theory_opt.cpp

@@ -68,17 +68,10 @@ namespace smt {
 
     
     bool theory_opt::is_numeral(arith_util& a, expr* term) {
-        while (true) {
+        while (a.is_uminus(term) || a.is_to_real(term) || a.is_to_int(term)) {
-            if (a.is_uminus(term) || a.is_to_real(term) || a.is_to_int(term)) {
+            term = to_app(term)->get_arg(0);
-                term = to_app(term)->get_arg(0);
-            }
-            else if (a.is_numeral(term)) {
-                return true;
-            }
-            else {
-                return false;
-            }
         }
+        return a.is_numeral(term);
     }
 
 };