add validation option for debugging regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 9, 2024 · 75005d9 · 75005d9
1 parent 2934618
commit 75005d9
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 6 deletions.
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
@@ -99,6 +99,7 @@ def_module_params(module_name='smt',
                           ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
                           ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
                           ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
+			  ('arith.validate', BOOL, False, 'validate lemmas generated by arithmetic solver'),
                           ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                           ('array.weak', BOOL, False, 'weak array theory'),

diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
@@ -36,6 +36,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
     m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
     m_arith_auto_config_simplex = p.arith_auto_config_simplex();
+    m_arith_validate = p.arith_validate();
     m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
     m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
     m_nl_arith_cross_nested = p.arith_nl_cross_nested();
@@ -95,4 +96,5 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials);
     DISPLAY_PARAM(m_nl_arith_optimize_bounds);
     DISPLAY_PARAM(m_nl_arith_cross_nested);
+    DISPLAY_PARAM(m_arith_validate);
 }
diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h
@@ -82,6 +82,7 @@ struct theory_arith_params {
     bool                    m_arith_adaptive_gcd = false;
     unsigned                m_arith_propagation_threshold = UINT_MAX;
 
+    bool                    m_arith_validate = false;
     arith_pivot_strategy    m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_SMALLEST;
 
     // used in diff-logic

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2389,7 +2389,9 @@ class theory_lra::imp {
 
     literal_vector m_core2;
 
-    void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {
+    void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& ps) {
+        if (params().m_arith_validate)
+            VERIFY(validate_assign(lit, core, eqs));
         if (core.size() < small_lemma_size() && eqs.empty()) {
             m_core2.reset();
             for (auto const& c : core) {
@@ -2399,7 +2401,7 @@ class theory_lra::imp {
             justification * js = nullptr;
             if (proofs_enabled()) {
                 js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(),
-                           params.size(), params.data());
+                           ps.size(), ps.data());
             }
             ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr);
         }
@@ -2408,7 +2410,7 @@ class theory_lra::imp {
                 lit, ctx().mk_justification(
                     ext_theory_propagation_justification(
                         get_id(), ctx(), core.size(), core.data(), 
-                        eqs.size(), eqs.data(), lit, params.size(), params.data())));            
+                        eqs.size(), eqs.data(), lit, ps.size(), ps.data())));            
         }
     }
 
@@ -3138,7 +3140,8 @@ class theory_lra::imp {
         std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
         scoped_trace_stream _sts(th, fn);
 
-        // VERIFY(validate_eq(x, y));
+        if (params().m_arith_validate)
+            VERIFY(validate_eq(x, y));
         ctx().assign_eq(x, y, eq_justification(js));
     }
 
@@ -3252,8 +3255,9 @@ class theory_lra::imp {
         for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
 
-
-        // VERIFY(validate_conflict(m_core, m_eqs));
+
+        if (params().m_arith_validate)
+            VERIFY(validate_conflict(m_core, m_eqs));
         if (is_conflict) {
             ctx().set_conflict(
                 ctx().mk_justification(