z3-src 501.0.1

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8

def_module_params('nnf', 
                  description='negation normal form',
                  export=True,
                  params=(max_memory_param(),
                          ('sk_hack', BOOL, False, 'hack for VCC'),
                          ('mode', SYMBOL, 'skolem', 
                           'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'),
                          ('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled')))