add diagnostics option to new arithmetic solver

Author: NikolajBjorner

src/sat/smt/arith_diagnostics.cpp

@@ -15,6 +15,8 @@ Module Name:
 
 --*/
 
+#include "util/cancel_eh.h"
+#include "util/scoped_timer.h"
 #include "ast/ast_util.h"
 #include "ast/scoped_proof.h"
 #include "sat/smt/euf_solver.h"
@@ -242,4 +244,21 @@ namespace arith {
 
         return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
     }
+
+    bool solver::validate_conflict() {
+        scoped_ptr<::solver> vs = mk_smt2_solver(m, ctx.s().params(), symbol::null);
+        for (auto lit : m_core)
+            vs->assert_expr(ctx.literal2expr(lit));
+
+        for (auto [a, b] : m_eqs)
+            vs->assert_expr(m.mk_eq(a->get_expr(), b->get_expr()));
+
+        cancel_eh<reslimit> eh(m.limit());
+        scoped_timer timer(1000, &eh);
+        bool result = l_true != vs->check_sat();
+        CTRACE("arith", !result, vs->display(tout));
+        CTRACE("arith", !result, s().display(tout));
+        SASSERT(result);
+        return result;
+    }
 }

src/sat/smt/arith_internalize.cpp

@@ -472,7 +472,7 @@ namespace arith {
         bool _has_var = has_var(t);
         mk_enode(t);
         theory_var v = mk_evar(t);
-
+                                      
         if (!_has_var) {
             svector<lpvar> vars;
             for (expr* n : *t) {

src/sat/smt/arith_solver.cpp

@@ -1251,6 +1251,9 @@ namespace arith {
             for (literal c : m_core) tout << c << ": " << literal2expr(c) << "\n";
             for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
 
+        if (ctx.get_config().m_arith_validate)
+            VERIFY(validate_conflict());
+
         if (is_conflict) {
             DEBUG_CODE(
                 for (literal c : m_core) VERIFY(s().value(c) == l_true);

src/sat/smt/arith_solver.h

@@ -483,6 +483,7 @@ namespace arith {
         arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
         void explain_assumptions(lp::explanation const& e);
 
+        bool validate_conflict();
 
     public:
         solver(euf::solver& ctx, theory_id id);