mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

move sat.smt.proof.check_rup into solver.proof.check_rup #6616

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-01 21:03:27 -08:00
parent 94b79eefea
commit fd97be0e3e
5 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/params/solver_params.pyg
View file

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

1
src/sat/sat_config.cpp
View file

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

1
src/sat/sat_config.h
View file

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

3
src/sat/sat_params.pyg
View file

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

6
src/sat/smt/euf_proof_checker.cpp
View file

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