mirror of
https://github.com/Z3Prover/z3
synced 2025-08-07 19:51:22 +00:00
b9cba82531
- add outline of trim routine - streamline how proof terms are checked and how residue units are extracted.
15 lines
1.1 KiB
Text
15 lines
1.1 KiB
Text
|
|
def_module_params('solver',
|
|
description='solver parameters',
|
|
export=True,
|
|
params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
|
|
('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
|
|
('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
|
|
('lemmas2console', BOOL, False, 'print lemmas during search'),
|
|
('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'),
|
|
('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'),
|
|
('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.trim', BOOL, False, 'trim and save proof into a proof object that an be extracted using (get-proof)'),
|
|
))
|
|
|