From fd97be0e3e3f20270ff5968414c184b9894d45c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Mar 2023 21:03:27 -0800 Subject: [PATCH] move sat.smt.proof.check_rup into solver.proof.check_rup #6616 --- src/params/solver_params.pyg | 1 + src/sat/sat_config.cpp | 1 - src/sat/sat_config.h | 1 - src/sat/sat_params.pyg | 3 +-- src/sat/smt/euf_proof_checker.cpp | 6 +++--- 5 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/params/solver_params.pyg b/src/params/solver_params.pyg index 1c2be3213..0912b4c7f 100644 --- a/src/params/solver_params.pyg +++ b/src/params/solver_params.pyg @@ -10,6 +10,7 @@ def_module_params('solver', ('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'), ('proof.log', SYMBOL, '', 'log clause proof trail into a file'), ('proof.check', BOOL, True, 'check proof logs'), + ('proof.check_rup', BOOL, True, 'check proof RUP inference in proof logs'), ('proof.save', BOOL, False, 'save proof log into a proof object that can be extracted using (get-proof)'), ('proof.trim', BOOL, False, 'trim and save proof into a proof object that an be extracted using (get-proof)'), )) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 0a9e803a9..73516f66d 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -200,7 +200,6 @@ namespace sat { m_drat_check_sat = p.drat_check_sat(); m_drat_file = p.drat_file(); m_smt_proof_check = p.smt_proof_check(); - m_smt_proof_check_rup = p.smt_proof_check_rup(); m_drat_disable = p.drat_disable(); m_drat = !m_drat_disable && p.threads() == 1 && diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f8c0775b1..a47f041b0 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -180,7 +180,6 @@ namespace sat { bool m_drat_binary; symbol m_drat_file; bool m_smt_proof_check; - bool m_smt_proof_check_rup; bool m_drat_check_unsat; bool m_drat_check_sat; bool m_drat_activity; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 6aedf1c89..d40d606d1 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -48,8 +48,7 @@ def_module_params('sat', ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.disable', BOOL, False, 'override anything that enables DRAT'), ('smt', BOOL, False, 'use the SAT solver based incremental SMT core'), - ('smt.proof.check', BOOL, False, 'check SMT proof while it is created'), - ('smt.proof.check_rup', BOOL, True, 'apply forward RUP proof checking'), + ('smt.proof.check', BOOL, False, 'check proofs on the fly during SMT search'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.binary', BOOL, False, 'use Binary DRAT output format'), ('drat.check_unsat', BOOL, False, 'build up internal proof and check'), diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 2d4f67cd2..a538b2a80 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -28,7 +28,7 @@ Author: #include "sat/smt/bv_theory_checker.h" #include "sat/smt/distinct_theory_checker.h" #include "sat/smt/tseitin_theory_checker.h" - +#include "params/solver_params.hpp" namespace euf { @@ -388,8 +388,8 @@ namespace euf { m_sat_solver.updt_params(m_params); m_drat.updt_config(); m_rup = symbol("rup"); - sat_params sp(m_params); - m_check_rup = sp.smt_proof_check_rup(); + solver_params sp(m_params); + m_check_rup = sp.proof_check_rup(); } void smt_proof_checker::ensure_solver() {