mirror of
https://github.com/Z3Prover/z3
synced 2025-12-31 00:09:51 +00:00
8a95dd4d65
A slice solver prunes the set of active assertions based on symbol occurrences in a goal that is tracked as a @query. Ground assertions that have symbols intersecting with the query are included in the solver state, and quantifiers that with patterns that intersect with the slice are included. The slice is the fixedpoint of including symbols from all included assertions. Enable the functionality for command-line use by setting solver.slice=true
18 lines
1.5 KiB
Text
18 lines
1.5 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'),
|
|
('slice', BOOL, False, 'use slice solver that filters assertions to use symbols occuring in @query formulas'),
|
|
('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)'),
|
|
))
|
|
|