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

move parameter sat.smt.proof to solver.proof.log

Browse source 
this update breaks use cases that set sat.smt.proof to True.
As it is such a new feature and the change affects possibly at most the tutorial it is made without compatibility layers.
This commit is contained in:
Nikolaj Bjorner 2022-11-23 07:59:04 +07:00
parent cd0d52acec
commit c7781f346d
4 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/params/solver_params.pyg
View file

@ -8,6 +8,7 @@ def_module_params('solver',
('lemmas2console', BOOL, False, 'print lemmas during search'), ('lemmas2console', BOOL, False, 'print lemmas during search'),
('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'), ('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'),
('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'), ('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', BOOL, True, 'check proof logs'),
('proof.save', BOOL, False, 'save proof log into a proof object that can be extracted using (get-proof)'), ('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)'), ('proof.trim', BOOL, False, 'trim and save proof into a proof object that an be extracted using (get-proof)'),

3
src/sat/sat_config.cpp
View file

@ -197,7 +197,6 @@ namespace sat {
m_drat_check_unsat = p.drat_check_unsat(); m_drat_check_unsat = p.drat_check_unsat();
m_drat_check_sat = p.drat_check_sat(); m_drat_check_sat = p.drat_check_sat();
m_drat_file = p.drat_file(); m_drat_file = p.drat_file();
m_smt_proof = p.smt_proof();
m_smt_proof_check = p.smt_proof_check(); m_smt_proof_check = p.smt_proof_check();
m_smt_proof_check_rup = p.smt_proof_check_rup(); m_smt_proof_check_rup = p.smt_proof_check_rup();
m_drat_disable = p.drat_disable(); m_drat_disable = p.drat_disable();
@ -206,7 +205,7 @@ namespace sat {
(sp.lemmas2console() || (sp.lemmas2console() ||
m_drat_check_unsat || m_drat_check_unsat ||
m_drat_file.is_non_empty_string() || m_drat_file.is_non_empty_string() ||
m_smt_proof.is_non_empty_string() || sp.proof_log().is_non_empty_string() ||
m_smt_proof_check || m_smt_proof_check ||
m_drat_check_sat); m_drat_check_sat);
m_drat_binary = p.drat_binary(); m_drat_binary = p.drat_binary();

1
src/sat/sat_config.h
View file

@ -178,7 +178,6 @@ namespace sat {
bool m_drat_disable; bool m_drat_disable;
bool m_drat_binary; bool m_drat_binary;
symbol m_drat_file; symbol m_drat_file;
symbol m_smt_proof;
bool m_smt_proof_check; bool m_smt_proof_check;
bool m_smt_proof_check_rup; bool m_smt_proof_check_rup;
bool m_drat_check_unsat; bool m_drat_check_unsat;

1
src/sat/sat_params.pyg
View file

@ -47,7 +47,6 @@ def_module_params('sat',
('threads', UINT, 1, 'number of parallel threads to use'), ('threads', UINT, 1, 'number of parallel threads to use'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.disable', BOOL, False, 'override anything that enables DRAT'), ('drat.disable', BOOL, False, 'override anything that enables DRAT'),
('smt.proof', SYMBOL, '', 'add SMT proof log to file'),
('smt.proof.check', BOOL, False, 'check SMT proof while it is created'), ('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_rup', BOOL, True, 'apply forward RUP proof checking'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),