z3-src 503.0.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

/*++
Copyright (c) 2007 Microsoft Corporation

Module Name:

    nnf.h

Abstract:

    Negation Normal Form & Skolemization

Author:

    Leonardo (leonardo) 2008-01-11

Notes:
    Major revision on 2011-10-06

--*/
#pragma once

#include "ast/ast.h"
#include "util/params.h"
#include "util/gparams.h"
#include "ast/normal_forms/defined_names.h"

class nnf {
    struct imp;
    imp *  m_imp;
public:
    nnf(ast_manager & m, defined_names & n, params_ref const & p = params_ref());
    ~nnf();

    void operator()(expr * n,                          // [IN] expression that should be put into NNF
                    expr_ref_vector & new_defs,        // [OUT] new definitions
                    proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
                    expr_ref & r,                      // [OUT] resultant expression
                    proof_ref & p                      // [OUT] proof for (~ n r)
                    );

    void updt_params(params_ref const & p);
    static void get_param_descrs(param_descrs & r);

    void reset();
    void reset_cache();
};

Z3_REGISTER_MODULE_PARAMS(nnf, "nnf", nnf::get_param_descrs, nullptr);