z3-src 503.2.1

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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    smt_setup.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-06-24.

Revision History:

--*/
#pragma once

#include "ast/ast.h"
#include "params/smt_params.h"

struct static_features;
namespace smt {
    
    enum config_mode {
        CFG_BASIC,   // install theories based on user options
        CFG_LOGIC,   // install theories and configure Z3 based on the value of the parameter set-logic.
        CFG_AUTO    // install theories based on static features of the input formula
    };

    class context;
    /**
       \brief Object used to setup a logical context.
       
       \warning In the current version, we can only setup a logical context at scope level 0,
       and before internalizing any formula. Auxiliary temporary contexts are used to avoid this
       limitation.
    */
    class setup {
        context &          m_context;
        ast_manager &      m_manager;
        smt_params &       m_params;
        symbol             m_logic;
        bool               m_already_configured;
        void setup_auto_config();
        void setup_default();
        //
        // setup_<logic>() methods do not depend on static features of the formula. So, they are safe to use
        // even in an incremental setting. 
        //
        // setup_<logic>(static_features & st) can only be used if the logical context will perform a single 
        // check.
        // 
        void setup_QF_DT();
        void setup_QF_UF();
        void setup_QF_UF(static_features const & st);
        void setup_QF_RDL();
        void setup_QF_RDL(static_features & st);
        void setup_QF_IDL();
        void setup_QF_IDL(static_features & st);
        void setup_QF_UFIDL();
        void setup_QF_UFIDL(static_features & st);
        void setup_QF_LRA();
        void setup_QF_LRA(static_features const & st);
        void setup_QF_LIA();
        void setup_QF_LIRA(static_features const& st);
        void setup_QF_LIA(static_features const & st);
        void setup_QF_UFLIA();
        void setup_QF_UFLIA(static_features & st);
        void setup_QF_UFLRA();
        void setup_QF_BV();
        void setup_QF_AUFBV();
        void setup_QF_AX();
        void setup_QF_AX(static_features const & st);
        void setup_QF_AUFLIA();
        void setup_QF_AUFLIA(static_features const & st);
        void setup_QF_FP();
        void setup_QF_FPBV();
        void setup_QF_S();
        void setup_LRA();
        void setup_CSP();
        void setup_special_relations();
        void setup_polymorphism();
        void setup_AUFLIA(bool simple_array = true);
        void setup_AUFLIA(static_features const & st);
        void setup_AUFLIRA(bool simple_array = true);
        void setup_UFNIA();
        void setup_UFLRA();
        void setup_AUFLIAp();
        void setup_AUFNIRA();
        void setup_QF_BVRE();
        void setup_unknown();
        void setup_unknown(static_features & st);
        void setup_arrays();
        void setup_datatypes();
        void setup_recfuns();
        void setup_bv();
        void setup_arith();
        void setup_dl();
        void setup_seq_str(static_features const & st);
        void setup_seq();
        void setup_char();
        void setup_finite_set();
        void setup_card();
        void setup_sls();
        void setup_i_arith();
        void setup_mi_arith();
        void setup_lra_arith();
        void setup_fpa();
        void setup_relevancy(static_features& st);

    public:
        setup(context & c, smt_params & params);
        void mark_already_configured() { m_already_configured = true; }
        bool already_configured() const { return m_already_configured; }
        bool set_logic(symbol logic) { 
            if (already_configured()) 
                return false;
            m_logic = logic; 
            return true;
        }
        symbol const & get_logic() const { return m_logic; }
        void operator()(config_mode cm);
        void setup_ff();
    };
}