3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00

missing file

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 15:54:53 -08:00
parent 589f096e6e
commit 823dd6ca47

View file

@ -0,0 +1,9 @@
def_module_params('model',
export=True,
params=(('validate', BOOL, False, 'validate models produced by Z3'),
('partial', BOOL, False, 'enable/disable partial function interpretations'),
('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model')))