update model validate to include arithmetic

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

src/smt/proto_model/proto_model.h

@@ -63,6 +63,9 @@ public:
     void register_factory(value_factory * f) { m_factories.register_plugin(f); }
 
     bool eval(expr * e, expr_ref & result, bool model_completion = false);
+    bool are_equal(expr* a, expr* b) { return m_eval.are_equal(a, b); }
+    bool is_false(expr* e) { return m_eval.are_equal(e, m.mk_false()); }
+    expr_ref operator()(expr* e) { expr_ref result(e, m); eval(e, result, false); return result; }
 
     
     value_factory * get_factory(family_id fid);

src/smt/smt_context.cpp

@@ -3470,13 +3470,9 @@ namespace smt {
         }
         if (r == l_true && gparams::get_value("model_validate") == "true") {
             recfun::util u(m);
-            model_ref mdl;
+            if (u.get_rec_funs().empty() && m_proto_model) {
-            get_model(mdl);            
+                for (theory* t : m_theory_set) {
-            if (u.get_rec_funs().empty()) {
+                    t->validate_model(*m_proto_model);
-                if (mdl.get()) {
-                    for (theory* t : m_theory_set) {
-                        t->validate_model(*mdl);
-                    }
                 }
             }
 #if 0

src/smt/smt_theory.h

@@ -368,7 +368,8 @@ namespace smt {
         //
         // ----------------------------------------------------
 
-        virtual void validate_model(model& mdl) {}
+        virtual void validate_model(proto_model& mdl) {}
+
 
         // ----------------------------------------------------
         //

src/smt/theory_lra.cpp

@@ -3882,6 +3882,30 @@ public:
     }
 
 
+    void validate_model(proto_model& mdl) {
+
+        rational r1, r2;
+        expr_ref res(m);
+        if (!m_model_is_initialized)
+            return;
+        for (unsigned v = 0; v < th.get_num_vars(); ++v) {
+            if (!is_registered_var(v))
+                continue;
+            enode* n = get_enode(v);
+            if (!n)
+                continue;
+            if (!th.is_relevant_and_shared(n))
+                continue;
+            rational r1 = get_value(v);
+            if (!mdl.eval(n->get_expr(), res, false))
+                continue;
+            if (!a.is_numeral(res, r2))
+                continue;
+            if (r1 != r2)
+                IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n"); 
+        }
+    }
+
 };
     
 theory_lra::theory_lra(context& ctx):
@@ -4009,6 +4033,10 @@ void theory_lra::setup() {
     m_imp->setup();
 }
 
+void theory_lra::validate_model(proto_model& mdl) {
+    m_imp->validate_model(mdl);
+}
+
 }
 template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
 template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);

src/smt/theory_lra.h

@@ -82,6 +82,7 @@ namespace smt {
         void init_model(model_generator & m) override;
         
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
+        void validate_model(proto_model& mdl) override;
 
         bool get_value(enode* n, expr_ref& r) override;
         bool include_func_interp(func_decl* f) override;

src/smt/theory_seq.cpp

@@ -2160,7 +2160,7 @@ app* theory_seq::mk_value(app* e) {
 }
 
 
-void theory_seq::validate_model(model& mdl) {
+void theory_seq::validate_model(proto_model& mdl) {
     return;
     for (auto const& eq : m_eqs) {
         sort* srt = eq.ls[0]->get_sort();

src/smt/theory_seq.h

@@ -407,7 +407,7 @@ namespace smt {
         void init_model(model_generator & mg) override;
         void finalize_model(model_generator & mg) override;
         void init_search_eh() override;
-        void validate_model(model& mdl) override;
+        void validate_model(proto_model& mdl) override;
         bool is_beta_redex(enode* p, enode* n) const override;
 
         void init_model(expr_ref_vector const& es);