z3-src 503.3.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
50
51
52
53
54
55
56
57
58
59
60
61

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    name_exprs.h

Abstract:

    Goodies for naming nested expressions.

Author:

    Leonardo (leonardo) 2011-10-06

Notes:

--*/
#pragma once

#include "ast/ast.h"
#include "ast/normal_forms/defined_names.h"

class expr_predicate {
public:
    virtual ~expr_predicate() = default;
    virtual bool operator()(expr * t) = 0;
};

class name_exprs {
public:
    virtual ~name_exprs() = default;
    virtual void operator()(expr * n,                          // [IN] expression that contain the sub-expressions to be named
                            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 (iff n p)
                            ) = 0;
    
    virtual void reset() = 0;
};

/**
   \brief Create an expression "namer" that will create replace nested expressions that satisfy pred with new
   fresh declarations.
*/
name_exprs * mk_expr_namer(ast_manager & m, defined_names & n, expr_predicate & pred);

/**
   \brief Create an expression "namer" that will replace quantifiers and labels with new fresh declarations.
*/
name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n);

/**
   \brief Create an expression "namer" that will replace all nested formulas and term if-then-elses with 
   fresh declarations.
*/
name_exprs * mk_nested_formula_namer(ast_manager & m, defined_names & n);

void del_name_exprs(name_exprs * functor);