mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Formatting: move q3 parameters closer together

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-28 15:37:18 -04:00
parent bd63458778
commit 5e87d7c4a3
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/fp_params.pyg
View file

@ -150,6 +150,8 @@ def_module_params('fp',
('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'), ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'),
('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'), ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'),
('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
('spacer.iuc', UINT, 1, ('spacer.iuc', UINT, 1,
'0 = use old implementation of unsat-core-generation, ' + '0 = use old implementation of unsat-core-generation, ' +
'1 = use new implementation of IUC generation, ' + '1 = use new implementation of IUC generation, ' +
@ -164,8 +166,6 @@ def_module_params('fp',
('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'),
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'),
('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'), ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'),
('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'), ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"), ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
('spacer.min_level', UINT, 0, 'Minimal level to explore'), ('spacer.min_level', UINT, 0, 'Minimal level to explore'),