z3-src 415.4.3

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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    defined_names.h

Abstract:

    In some transformations, we need to name expressions.
    These expressions are stored in a table.

Author:

    Leonardo de Moura (leonardo) 2008-01-14.

Revision History:

--*/
#pragma once

#include "ast/ast.h"

/**
   \brief Mapping from expressions to skolem functions that are used to name them.

   The mapping supports backtracking using the methods #push_scope and #pop_scope.
*/
class defined_names {
    struct impl;
    struct pos_impl;
    impl      * m_impl;
    pos_impl  * m_pos_impl;
public:
    defined_names(ast_manager & m, char const * fresh_prefix = "z3name");
    ~defined_names();

    // -----------------------------------
    //
    // High-level API
    //
    // -----------------------------------

    /**
       \brief Create a name for expression \c e if it doesn't already exists. 
       
       Return true if a new name was created, and false if a name already exists for \c e.

       The resultant new name is stored in n, and a [apply-def] proof
       that (= e n) is stored into pr.

       If true is returned, then the definition of the new name is
       stored into new_def, and a [def-intro] proof into new_def_pr.

       The proofs are not produced when proof generation is disabled.

       The definition of an expression e with name n is:

       - (and (or (not e) n) (or e (not n)))  if e is an formula.
       - (and (or (not c) (= n t1)) (or c (= n t2))) if e is an if-then-else term of the form (ite c t1 t2)
       - (= n e) if e is a term.

       Remark: the definitions are closed with an universal quantifier if e contains free variables.
    */
    bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);

    /**
       \brief Create a name for a positive occurrence of the expression \c e.
       
       Return true if a new pos-name was created, and false if a pos-name already exists for \c e.

       If true is returned, then the definition of the new name is stored into new_def.
       It has the form:  (or (not n) e)

       Remark: the definitions are closed with an universal quantifier if e contains free variables.
    */
    bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);

    /**
       \brief Create a definition for 'n' using 'e'.
     */
    expr_ref mk_definition(expr * e, app * n);

    void push();
    void pop(unsigned num_scopes);
    void reset();

    unsigned get_num_names() const;
    func_decl * get_name_decl(unsigned i) const;
};