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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
/********************* */
/*! \file modes.h
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_public.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__MODES_H
#define __CVC4__THEORY__QUANTIFIERS__MODES_H
#include <iostream>
namespace CVC4 {
namespace theory {
namespace quantifiers {
typedef enum {
/** Apply instantiation round before full effort (possibly at standard effort) */
INST_WHEN_PRE_FULL,
/** Apply instantiation round at full effort or above */
INST_WHEN_FULL,
/** Apply instantiation round at full effort, after all other theories finish, or above */
INST_WHEN_FULL_DELAY,
/** Apply instantiation round at full effort half the time, and last call always */
INST_WHEN_FULL_LAST_CALL,
/** Apply instantiation round at full effort after all other theories finish half the time, and last call always */
INST_WHEN_FULL_DELAY_LAST_CALL,
/** Apply instantiation round at last call only */
INST_WHEN_LAST_CALL,
} InstWhenMode;
typedef enum {
/** Do not consider polarity of patterns */
LITERAL_MATCH_NONE,
/** Consider polarity of boolean predicates only */
LITERAL_MATCH_PREDICATE,
/** Consider polarity of boolean predicates, as well as equalities */
LITERAL_MATCH_EQUALITY,
} LiteralMatchMode;
typedef enum {
/** mbqi from CADE 24 paper */
MBQI_GEN_EVAL,
/** no mbqi */
MBQI_NONE,
/** default, mbqi from Section 5.4.2 of AJR thesis */
MBQI_FMC,
/** mbqi with integer intervals */
MBQI_FMC_INTERVAL,
/** abstract mbqi algorithm */
MBQI_ABS,
/** mbqi trust (produce no instantiations) */
MBQI_TRUST,
} MbqiMode;
typedef enum {
/** default, apply at full effort */
QCF_WHEN_MODE_DEFAULT,
/** apply at last call */
QCF_WHEN_MODE_LAST_CALL,
/** apply at standard effort */
QCF_WHEN_MODE_STD,
/** apply based on heuristics */
QCF_WHEN_MODE_STD_H,
} QcfWhenMode;
typedef enum {
/** default, use qcf for conflicts only */
QCF_CONFLICT_ONLY,
/** use qcf for conflicts and propagations */
QCF_PROP_EQ,
/** use qcf for conflicts, propagations and heuristic instantiations */
QCF_PARTIAL,
/** use qcf for model checking */
QCF_MC,
} QcfMode;
typedef enum {
/** use but do not trust */
USER_PAT_MODE_USE,
/** default, if patterns are supplied for a quantifier, use only those */
USER_PAT_MODE_TRUST,
/** resort to user patterns only when necessary */
USER_PAT_MODE_RESORT,
/** ignore user patterns */
USER_PAT_MODE_IGNORE,
/** interleave use/resort for user patterns */
USER_PAT_MODE_INTERLEAVE,
} UserPatMode;
typedef enum {
/** default for trigger selection */
TRIGGER_SEL_DEFAULT,
/** only consider minimal terms for triggers */
TRIGGER_SEL_MIN,
/** only consider maximal terms for triggers */
TRIGGER_SEL_MAX,
} TriggerSelMode;
typedef enum CVC4_PUBLIC {
/** default : prenex quantifiers without user patterns */
PRENEX_NO_USER_PAT,
/** prenex all */
PRENEX_ALL,
/** prenex none */
PRENEX_NONE,
} PrenexQuantMode;
typedef enum {
/** enforce fairness by UF corresponding to datatypes size */
CEGQI_FAIR_UF_DT_SIZE,
/** enforce fairness by datatypes size */
CEGQI_FAIR_DT_SIZE,
/** enforce fairness by datatypes height bound */
CEGQI_FAIR_DT_HEIGHT_PRED,
/** do not use fair strategy for CEGQI */
CEGQI_FAIR_NONE,
} CegqiFairMode;
typedef enum {
/** consider all terms in master equality engine */
TERM_DB_ALL,
/** consider only relevant terms */
TERM_DB_RELEVANT,
} TermDbMode;
typedef enum {
/** do not lift ITEs in quantified formulas */
ITE_LIFT_QUANT_MODE_NONE,
/** only lift ITEs in quantified formulas if reduces the term size */
ITE_LIFT_QUANT_MODE_SIMPLE,
/** lift ITEs */
ITE_LIFT_QUANT_MODE_ALL,
} IteLiftQuantMode;
typedef enum {
/** synthesize I( x ) */
SYGUS_INV_TEMPL_MODE_NONE,
/** synthesize ( pre( x ) V I( x ) ) */
SYGUS_INV_TEMPL_MODE_PRE,
/** synthesize ( post( x ) ^ I( x ) ) */
SYGUS_INV_TEMPL_MODE_POST,
} SygusInvTemplMode;
typedef enum {
/** infer all definitions */
MACROS_QUANT_MODE_ALL,
/** infer ground definitions */
MACROS_QUANT_MODE_GROUND,
/** infer ground uf definitions */
MACROS_QUANT_MODE_GROUND_UF,
} MacrosQuantMode;
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC;
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */
|
