#5641 - projection that skips interpreted functions can violate model evaluation.

src/qe/mbp/mbp_arith.cpp

@@ -249,8 +249,8 @@ namespace mbp {
         bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
             app_ref_vector vs(m);
             vs.push_back(v);
-            project(model, vs, lits, false);
+            vector<def> defs;
-            return vs.empty();
+            return project(model, vs, lits, defs, false) && vs.empty();            
         }
 
         typedef opt::model_based_opt::var var;
@@ -265,12 +265,12 @@ namespace mbp {
             return t;
         }
 
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, bool compute_def) {
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, vector<def>& result, bool compute_def) {
             bool has_arith = false;
             for (expr* v : vars) 
                 has_arith |= is_arith(v);            
             if (!has_arith) 
-                return vector<def>();            
+                return true;            
             model_evaluator eval(model);
             TRACE("qe", tout << model;);
             eval.set_model_completion(true);
@@ -294,7 +294,7 @@ namespace mbp {
             }
             fmls.shrink(j);
             TRACE("qe", tout << "formulas\n" << fmls << "\n";
-		                for (auto [e, id] : tids)
+		                for (auto const& [e, id] : tids)
 		                    tout << mk_pp(e, m) << " -> " << id << "\n";);
 
             // fmls holds residue,
@@ -312,7 +312,7 @@ namespace mbp {
                     rational r;
                     expr_ref val = eval(v);
                     if (!m.inc())
-                        return vector<def>();
+                        return false;
                     if (!a.is_numeral(val, r))
                         throw default_exception("evaluation did not produce a numeral");
                     TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
@@ -326,17 +326,15 @@ namespace mbp {
                 if (is_arith(e) && !var_mark.is_marked(e)) 
                     mark_rec(fmls_mark, e);                
             }
-
             if (m_check_purified) {
                 for (expr* fml : fmls) 
                     mark_rec(fmls_mark, fml);                
                 for (auto& kv : tids) {
                     expr* e = kv.m_key;
-                    if (!var_mark.is_marked(e)) {
+                    if (!var_mark.is_marked(e)) 
                         mark_rec(fmls_mark, e);                    
                 }
             }
-            }
 
             ptr_vector<expr> index2expr;
             for (auto& kv : tids) 
@@ -364,16 +362,18 @@ namespace mbp {
                   for (auto const& d : defs) tout << "def: " << d << "\n";
                   tout << fmls << "\n";);
             
-            vector<def> result;
             if (compute_def) 
                 optdefs2mbpdef(defs, index2expr, real_vars, result);     
-            if (m_apply_projection)
+            if (m_apply_projection && !apply_projection(eval, result, fmls))
-                apply_projection(result, fmls);
+                return false;
+
             TRACE("qe",
-                for (auto [v, t] : result)
+                for (auto const& [v, t] : result)
                     tout << v << " := " << t << "\n";
+                for (auto* f : fmls)
+                    tout << mk_pp(f, m) << " := " << eval(f) << "\n";
                 tout << "fmls:" << fmls << "\n";);
-            return result;
+            return true;
         }        
 
         void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
@@ -548,10 +548,11 @@ namespace mbp {
             }
         }
 
-        void apply_projection(vector<def>& defs, expr_ref_vector& fmls) {
+        bool apply_projection(model_evaluator& eval, vector<def> const& defs, expr_ref_vector& fmls) {
             if (fmls.empty() || defs.empty())
-                return;
+                return true;
             expr_safe_replace subst(m);
+            expr_ref_vector fmls_tmp(m);
             expr_ref tmp(m);
             for (unsigned i = defs.size(); i-- > 0; ) {
                 auto const& d = defs[i];
@@ -561,8 +562,11 @@ namespace mbp {
             unsigned j = 0;
             for (expr* fml : fmls) {
                 subst(fml, tmp);
+                if (m.is_false(eval(tmp)))
+                    return false;
                 fmls[j++] = tmp;
             }
+            return true;
         }
 
     };
@@ -579,12 +583,13 @@ namespace mbp {
         return (*m_imp)(model, var, vars, lits);
     }
 
-    void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-        m_imp->project(model, vars, lits, false);
+        vector<def> defs;
+        return m_imp->project(model, vars, lits, defs, false);
     }
 
-    vector<def> arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return m_imp->project(model, vars, lits, true);
+        return m_imp->project(model, vars, lits, defs, true);
     }
 
     void arith_project_plugin::set_check_purified(bool check_purified) {

src/qe/mbp/mbp_arith.h

@@ -29,8 +29,8 @@ namespace mbp {
         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
         family_id get_family_id() override;
-        void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }
 
         opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt);

src/qe/mbp/mbp_arrays.cpp

@@ -1624,8 +1624,8 @@ namespace mbp {
               );
     }
 
-    vector<def> array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return vector<def>();
+        return true;
     }
 
     void array_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {

src/qe/mbp/mbp_arrays.h

@@ -35,7 +35,7 @@ namespace mbp {
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects);
         family_id get_family_id() override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
 
     };

src/qe/mbp/mbp_datatypes.cpp

@@ -300,8 +300,8 @@ namespace mbp {
         return m_imp->solve(model, vars, lits);
     }
 
-    vector<def> datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return vector<def>();
+        return true;
     }
 
     void datatype_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {

src/qe/mbp/mbp_datatypes.h

@@ -34,7 +34,7 @@ namespace mbp {
         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         family_id get_family_id() override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
 
     };

src/qe/mbp/mbp_plugin.h

@@ -67,7 +67,7 @@ namespace mbp {
         virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
         virtual family_id get_family_id() { return null_family_id; }
 
-        virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
+        virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; };
 
         /**
            \brief project vars modulo model, return set of definitions for eliminated variables.
@@ -76,7 +76,7 @@ namespace mbp {
            - returns set of definitions
              (TBD: in triangular form, the last definition can be substituted into definitions that come before)
         */
-        virtual vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return vector<def>(); }
+        virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) { return true; }
 
         /**
            \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF,

src/qe/qe_mbi.cpp

@@ -266,7 +266,10 @@ namespace qe {
     vector<mbp::def> uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) {
         mbp::arith_project_plugin ap(m);
         ap.set_check_purified(false);
-        return ap.project(*mdl.get(), avars, lits);
+        vector<mbp::def> defs;
+        bool ok = ap.project(*mdl.get(), avars, lits, defs);
+        CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n");
+        return defs;
     }
 
     mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) {

src/sat/smt/q_mbi.cpp

@@ -67,7 +67,7 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto [qlit, fml, generation] : m_instantiations) {
+        for (auto const& [qlit, fml, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
             sat::literal lit = ctx.mk_literal(fml);
             m_qs.add_clause(~qlit, ~lit);
@@ -308,8 +308,10 @@ namespace q {
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;
             }
-            if (p)
+            if (!p)
-                (*p)(*m_model, vars, fmls);
+                continue;
+            if (!(*p)(*m_model, vars, fmls))
+                return expr_ref(nullptr, m);
         }
         for (app* v : vars) {
             expr_ref term(m);

src/sat/smt/q_model_fixer.cpp

@@ -256,7 +256,7 @@ namespace q {
               tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
               if (v2r.find(value, r)) 
                   tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
-              ctx.display(tout);              
+              /*ctx.display(tout); */
               );
         if (v2r.find(value, r)) 
             return r->get_expr();