From db24cb8087dd997f79de229d67fcc398b666d646 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Aug 2015 10:56:07 +0200
Subject: [PATCH] add core validation option to directly validate cores using
 the context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/params/smt_params.cpp        |  1 +
 src/smt/params/smt_params.h          |  2 ++
 src/smt/params/smt_params_helper.pyg |  3 ++-
 src/smt/smt_context.cpp              |  1 +
 src/smt/smt_context.h                |  2 ++
 src/smt/smt_context_inv.cpp          | 28 ++++++++++++++++++++++++++++
 6 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 14f67bb5e..6028bbb24 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -35,6 +35,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_timeout = p.timeout();
+    m_core_validate = p.core_validate();
     model_params mp(_p);
     m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 7b54bcfb7..e67591d0e 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -195,6 +195,7 @@ struct smt_params : public preprocessor_params,
     //
     // -----------------------------------
     bool             m_display_installed_theories;
+    bool             m_core_validate;
 
     // -----------------------------------
     //
@@ -269,6 +270,7 @@ struct smt_params : public preprocessor_params,
         m_model_on_final_check(false),
         m_progress_sampling_freq(0),
         m_display_installed_theories(false),
+        m_core_validate(false),
         m_preprocess(true), // temporary hack for disabling all preprocessing..
         m_user_theory_preprocess_axioms(false),
         m_user_theory_persist_axioms(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 8be6110d5..5cd9cdcdc 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -57,5 +57,6 @@ def_module_params(module_name='smt',
                           ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
                           ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
-                          ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
+                          ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
+                          ('core.validate', BOOL, False, 'validate unsat core produced by SMT context')
                           ))
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e63fc148d..55e750980 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2928,6 +2928,7 @@ namespace smt {
               for (unsigned i = 0; i < sz; i++) {
                   tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
               });
+        validate_unsat_core();        
     }
 
     /**
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d8c0eb838..fb20a81c6 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1046,6 +1046,8 @@ namespace smt {
 
         void mk_unsat_core();
 
+        void validate_unsat_core();
+
         void init_search();
 
         void end_search();
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index a1f4bdd16..01641e166 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -399,5 +399,33 @@ namespace smt {
 
 #endif
 
+    /**
+       \brief validate unsat core returned by 
+     */
+    void context::validate_unsat_core() {
+        if (!get_fparams().m_core_validate) {
+            return;
+        }
+        context ctx(get_manager(), get_fparams(), get_params());
+        ptr_vector<expr> assertions;
+        get_assertions(assertions);
+        unsigned sz = assertions.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            ctx.assert_expr(assertions[i]);
+        }
+        sz = m_unsat_core.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            ctx.assert_expr(m_unsat_core.get(i));
+        }
+        lbool res = ctx.check();
+        switch (res) {
+        case l_false:
+            break;
+        default: 
+            UNREACHABLE();
+            throw default_exception("Core could not be validated");
+        }
+    }
+
 };