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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
//! Generated by `cargo xtask logics`, do not edit by hand.
use std::borrow::Cow;
/// Logics allow specifictation of which (sub-)logic should be used by a
/// solver.
///
/// > [A more detailed description of logics can be found on the
/// SMT-LIB website.](https://smtlib.cs.uiowa.edu/logics.shtml)
///
/// 
#[allow(nonstandard_style)]
pub enum Logic {
/**Closed formulas built over arbitrary expansions of the Ints and ArraysEx
signatures with free sort and function symbols, but with the following
restrictions:
- all terms of sort Int are linear, that is, have no occurrences of the
function symbols *, /, div, mod, and abs, except as specified in the
:extensions attributes;
- all array terms have sort (Array Int Int).
*/
AUFLIA,
/**Closed formulas built over arbitrary expansions of the Reals_Ints and
ArraysEx signatures with free sort and function symbols, but with the
following restrictions:
- all terms of sort Int are linear, that is, have no occurrences of the
function symbols *, /, div, mod, and abs, except as specified in the
:extensions attributes;
- all terms of sort Real are linear, that is, have no occurrences of the
function symbols * and /, except as specified in the
:extensions attribute;
- all array terms have sort
(Array Int Real) or
(Array Int (Array Int Real)).
*/
AUFLIRA,
/**Closed formulas built over arbitrary expansions of the Reals_Ints and
ArraysEx signatures with free sort and function symbols.
*/
AUFNIRA,
/**Closed formulas built over an arbitrary expansion of the
Ints signature with free constant symbols, but whose terms of sort Int
are all linear, that is, have no occurrences of the function symbols
*, /, div, mod, and abs, except as specified the :extensions attribute.
*/
LIA,
/**Closed formulas built over arbitrary expansions of the Reals signature
with free constant symbols, but containing only linear atoms, that is,
atoms with no occurrences of the function symbols * and /, except as
specified the :extensions attribute.
*/
LRA,
/**Closed quantifier-free formulas built over the FixedSizeBitVectors and
ArraysEx signatures, with the restriction that all array terms have sort of
the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
*/
QF_ABV,
/**Closed quantifier-free formulas built over an arbitrary expansion of the
FixedSizeBitVectors and ArraysEx signatures with free sort and function
symbols, but with the restriction that all array terms have sort of the
form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
*/
QF_AUFBV,
/**Closed quantifier-free formulas built over arbitrary expansions of the
Ints and ArraysEx signatures with free sort and function symbols, but
with the following restrictions:
- all terms of sort Int are linear, that is, have no occurrences of the
function symbols *, /, div, mod, and abs, except as specified in the
:extensions attributes;
- all array terms have sort (Array Int Int).
*/
QF_AUFLIA,
/**Closed quantifier-free formulas built over an arbitrary expansion of
the ArraysEx signature with free sort and constant symbols.
*/
QF_AX,
/**Closed quantifier-free formulas built over an arbitrary expansion of the
FixedSizeBitVectors signature with free constant symbols over the sorts
(_ BitVec m) for 0 < m. Formulas in ite terms must satisfy the same
restriction as well, with the exception that they need not be closed
(because they may be in the scope of a let binder).
*/
QF_BV,
/**Closed quantifier-free formulas with atoms of the form:
- q
- (op (- x y) n),
- (op (- x y) (- n)), or
- (op x y)
where
- q is a variable or free constant symbol of sort Bool,
- op is <, <=, >, >=, =, or distinct,
- x, y are free constant symbols of sort Int,
- n is a numeral.
*/
QF_IDL,
/**Closed quantifier-free formulas built over an arbitrary expansion of the
Ints signature with free constant symbols, but whose terms of sort Int
are all linear, that is, have no occurrences of the function symbols
/, div, mod, and abs, and no occurrences of the function symbol *,
except as specified in the :extensions attribute.
*/
QF_LIA,
/**Closed quantifier-free formulas built over arbitrary expansions of
the Reals signature with free constant symbols, but containing only
linear atoms, that is, atoms with no occurrences of the function
symbols * and /, except as specified the :extensions attribute.
*/
QF_LRA,
/**Closed quantifier-free formulas built over an arbitrary expansion of the
Ints signature with free constant symbols.
*/
QF_NIA,
/**Closed quantifier-free formulas built over arbitrary expansions of
the Reals signature with free constant symbols.*/
QF_NRA,
/**Closed quantifier-free formulas with atoms of the form:
- p
- (op (- x y) c),
- (op x y),
- (op (- (+ x ... x) (+ y ... y)) c) with n > 1 occurrences of x and of y,
where
- p is a variable or free constant symbol of sort Bool,
- c is an expression of the form m or (- m) for some numeral m,
- op is <, <=, >, >=, =, or distinct,
- x, y are free constant symbols of sort Real.
*/
QF_RDL,
/**Closed quantifier-free formulas built over an arbitrary expansion of
the Core signature with free sort and function symbols.
*/
QF_UF,
/**Closed quantifier-free formulas built over arbitrary expansions of
the FixedSizeBitVectors signature with free sort and function
symbols.
*/
QF_UFBV,
/**Closed quantifier-free formulas built over an arbitrary expansion with
free sort and function symbols of the signature consisting of
- all the sort and function symbols of Core and
- the following symbols of Int:
:sorts ((Int 0))
:funs ((NUMERAL Int)
(- Int Int Int)
(+ Int Int Int)
(<= Int Int Bool)
(< Int Int Bool)
(>= Int Int Bool)
(> Int Int Bool)
)
Additionally, for every term of the form (op t1 t2) with op in {+, -},
at least one of t1 and t2 is a numeral.
*/
QF_UFIDL,
/**Closed quantifier-free formulas built over arbitrary expansions of the
Ints signatures with free sort and function symbols, but with the
following restrictions:
- all terms of sort Int are linear, that is, have no occurrences of the
function symbols *, /, div, mod, and abs, except as specified in the
:extensions attributes;
*/
QF_UFLIA,
/**Closed quantifier-free formulas built over arbitrary expansions of the
Reals signature with free sort and function symbols, but containing
only linear atoms, that is, atoms with no occurrences of the function
symbols * and /, except as specified the :extensions attribute.
*/
QF_UFLRA,
/**Closed quantifier-free formulas built over arbitrary expansions of
the Reals signature with free sort and function symbols.
*/
QF_UFNRA,
/**Closed formulas built over arbitrary expansions of the Reals signature
with free sort and function symbols, but containing only linear atoms,
that is, atoms with no occurrences of the function symbols * and /,
except as specified the :extensions attribute.
*/
UFLRA,
/**Closed formulas built over an arbitrary expansion of the Ints signature
with free sort and function symbols.*/
UFNIA,
/// A fallback variant in case the user wants to specify
/// some logic which is not part of the predefined
/// collection.
Custom(String),
}
impl Logic {
/// Returns the name of the logic.
pub fn name(&self) -> Cow<'static, str> {
match self {
Self::AUFLIA => Cow::Borrowed("AUFLIA"),
Self::AUFLIRA => Cow::Borrowed("AUFLIRA"),
Self::AUFNIRA => Cow::Borrowed("AUFNIRA"),
Self::LIA => Cow::Borrowed("LIA"),
Self::LRA => Cow::Borrowed("LRA"),
Self::QF_ABV => Cow::Borrowed("QF_ABV"),
Self::QF_AUFBV => Cow::Borrowed("QF_AUFBV"),
Self::QF_AUFLIA => Cow::Borrowed("QF_AUFLIA"),
Self::QF_AX => Cow::Borrowed("QF_AX"),
Self::QF_BV => Cow::Borrowed("QF_BV"),
Self::QF_IDL => Cow::Borrowed("QF_IDL"),
Self::QF_LIA => Cow::Borrowed("QF_LIA"),
Self::QF_LRA => Cow::Borrowed("QF_LRA"),
Self::QF_NIA => Cow::Borrowed("QF_NIA"),
Self::QF_NRA => Cow::Borrowed("QF_NRA"),
Self::QF_RDL => Cow::Borrowed("QF_RDL"),
Self::QF_UF => Cow::Borrowed("QF_UF"),
Self::QF_UFBV => Cow::Borrowed("QF_UFBV"),
Self::QF_UFIDL => Cow::Borrowed("QF_UFIDL"),
Self::QF_UFLIA => Cow::Borrowed("QF_UFLIA"),
Self::QF_UFLRA => Cow::Borrowed("QF_UFLRA"),
Self::QF_UFNRA => Cow::Borrowed("QF_UFNRA"),
Self::UFLRA => Cow::Borrowed("UFLRA"),
Self::UFNIA => Cow::Borrowed("UFNIA"),
Self::Custom(s) => Cow::Owned(s.to_string()),
}
}
}
impl std::fmt::Display for Logic {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
self.name().fmt(f)
}
}