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

@@ -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))

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),

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')
                           ))

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();        
     }
 
     /**

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();

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");
+        }
+    }
+
 };