smtlib/
logics.rs

1//! Generated by `cargo xtask logics`, do not edit by hand.
2
3use std::borrow::Cow;
4/// Logics allow specifictation of which (sub-)logic should be used by a
5/// solver.
6///
7/// > [A more detailed description of logics can be found on the
8/// SMT-LIB website.](https://smtlib.cs.uiowa.edu/logics.shtml)
9///
10/// ![This is a graph :)](https://smtlib.cs.uiowa.edu/Logics/logics.png)
11#[allow(nonstandard_style)]
12pub enum Logic {
13    /**Closed formulas built over arbitrary expansions of the Ints and ArraysEx
14  signatures with free sort and function symbols, but with the following
15  restrictions:
16  - all terms of sort Int are linear, that is, have no occurrences of the
17    function symbols *, /, div, mod, and abs, except as specified in the
18    :extensions attributes;
19  - all array terms have sort (Array Int Int).
20 */
21    AUFLIA,
22    /**Closed formulas built over arbitrary expansions of the Reals_Ints and
23  ArraysEx signatures with free sort and function symbols, but with the
24  following restrictions:
25  - all terms of sort Int are linear, that is, have no occurrences of the
26    function symbols *, /, div, mod, and abs, except as specified in the
27    :extensions attributes;
28  - all terms of sort Real are linear, that is, have no occurrences of the
29    function symbols * and /, except as specified in the
30    :extensions attribute;
31  - all array terms have sort
32    (Array Int Real) or
33    (Array Int (Array Int Real)).
34 */
35    AUFLIRA,
36    /**Closed formulas built over arbitrary expansions of the Reals_Ints and
37  ArraysEx signatures with free sort and function symbols.
38 */
39    AUFNIRA,
40    /**Closed formulas built over an arbitrary expansion of the
41  Ints signature with free constant symbols, but whose terms of sort Int
42  are all linear, that is, have no occurrences of the function symbols
43  *, /, div, mod, and abs, except as specified the :extensions attribute.
44 */
45    LIA,
46    /**Closed formulas built over arbitrary expansions of the Reals signature
47  with free constant symbols, but containing only linear atoms, that is,
48  atoms with no occurrences of the function symbols * and /, except as
49  specified the :extensions attribute.
50 */
51    LRA,
52    /**Closed quantifier-free formulas built over the FixedSizeBitVectors and
53  ArraysEx signatures, with the restriction that all array terms have sort of
54  the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
55 */
56    QF_ABV,
57    /**Closed quantifier-free formulas built over an arbitrary expansion of the
58  FixedSizeBitVectors and ArraysEx signatures with free sort and function
59  symbols, but with the restriction that all array terms have sort of the
60  form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
61 */
62    QF_AUFBV,
63    /**Closed quantifier-free formulas built over arbitrary expansions of the
64  Ints and ArraysEx signatures with free sort and function symbols, but
65  with the following restrictions:
66  - all terms of sort Int are linear, that is, have no occurrences of the
67    function symbols *, /, div, mod, and abs, except as specified in the
68    :extensions attributes;
69  - all array terms have sort (Array Int Int).
70 */
71    QF_AUFLIA,
72    /**Closed quantifier-free formulas built over an arbitrary expansion of
73  the ArraysEx signature with free sort and constant symbols.
74 */
75    QF_AX,
76    /**Closed quantifier-free formulas built over an arbitrary expansion of the
77  FixedSizeBitVectors signature with free constant symbols over the sorts
78  (_ BitVec m) for 0 < m.  Formulas in ite terms must satisfy the same
79  restriction as well, with the exception that they need not be closed
80  (because they may be in the scope of a let binder).
81 */
82    QF_BV,
83    /**Closed quantifier-free formulas with atoms of the form:
84  - q
85  - (op (- x y) n),
86  - (op (- x y) (- n)), or
87  - (op x y)
88  where
89    - q is a variable or free constant symbol of sort Bool,
90    - op is <, <=, >, >=, =, or distinct,
91    - x, y are free constant symbols of sort Int,
92    - n is a numeral.
93 */
94    QF_IDL,
95    /**Closed quantifier-free formulas built over an arbitrary expansion of the
96  Ints signature with free constant symbols, but whose terms of sort Int
97  are all linear, that is, have no occurrences of the function symbols
98  /, div, mod, and abs, and no occurrences of the function symbol *,
99  except as specified in the :extensions attribute.
100 */
101    QF_LIA,
102    /**Closed quantifier-free formulas built over arbitrary expansions of
103  the Reals signature with free constant symbols, but containing only
104  linear atoms, that is, atoms with no occurrences of the function
105  symbols * and /, except as specified the :extensions attribute.
106 */
107    QF_LRA,
108    /**Closed quantifier-free formulas built over an arbitrary expansion of the
109  Ints signature with free constant symbols.
110 */
111    QF_NIA,
112    /**Closed quantifier-free formulas built over arbitrary expansions of
113  the Reals signature with free constant symbols.*/
114    QF_NRA,
115    /**Closed quantifier-free formulas with atoms of the form:
116  - p
117  - (op (- x y) c),
118  - (op x y),
119  - (op (- (+ x ... x) (+ y ... y)) c) with n > 1 occurrences of x and of y,
120  where
121    - p is a variable or free constant symbol of sort Bool,
122    - c is an expression of the form m or (- m) for some numeral m,
123    - op is <, <=, >, >=, =, or distinct,
124    - x, y are free constant symbols of sort Real.
125 */
126    QF_RDL,
127    /**Closed quantifier-free formulas built over an arbitrary expansion of
128  the Core signature with free sort and function symbols.
129 */
130    QF_UF,
131    /**Closed quantifier-free formulas built over arbitrary expansions of
132  the FixedSizeBitVectors signature with free sort and function
133  symbols.
134 */
135    QF_UFBV,
136    /**Closed quantifier-free formulas built over an arbitrary expansion with
137  free sort and function symbols of the signature consisting of
138  - all the sort and function symbols of Core and
139  - the following symbols of Int:
140
141    :sorts ((Int 0))
142    :funs ((NUMERAL Int)
143           (- Int Int Int)
144           (+ Int Int Int)
145           (<= Int Int Bool)
146           (< Int Int Bool)
147           (>= Int Int Bool)
148           (> Int Int Bool)
149          )
150
151  Additionally, for every term of the form (op t1 t2) with op in {+, -},
152  at least one of t1 and t2 is a numeral.
153 */
154    QF_UFIDL,
155    /**Closed quantifier-free formulas built over arbitrary expansions of the
156  Ints signatures with free sort and function symbols, but with the
157  following restrictions:
158  - all terms of sort Int are linear, that is, have no occurrences of the
159    function symbols *, /, div, mod, and abs, except as specified in the
160    :extensions attributes;
161 */
162    QF_UFLIA,
163    /**Closed quantifier-free formulas built over arbitrary expansions of the
164  Reals signature with free sort and function symbols, but containing
165  only linear atoms, that is, atoms with no occurrences of the function
166  symbols * and /, except as specified the :extensions attribute.
167 */
168    QF_UFLRA,
169    /**Closed quantifier-free formulas built over arbitrary expansions of
170  the Reals signature with free sort and function symbols.
171 */
172    QF_UFNRA,
173    /**Closed formulas built over arbitrary expansions of the Reals signature
174  with free sort and function symbols, but containing only linear atoms,
175  that is, atoms with no occurrences of the function symbols * and /,
176  except as specified the :extensions attribute.
177 */
178    UFLRA,
179    /**Closed formulas built over an arbitrary expansion of the Ints signature
180  with free sort and function symbols.*/
181    UFNIA,
182    /// A fallback variant in case the user wants to specify
183    /// some logic which is not part of the predefined
184    /// collection.
185    Custom(String),
186}
187impl Logic {
188    /// Returns the name of the logic.
189    pub fn name(&self) -> Cow<'static, str> {
190        match self {
191            Self::AUFLIA => Cow::Borrowed("AUFLIA"),
192            Self::AUFLIRA => Cow::Borrowed("AUFLIRA"),
193            Self::AUFNIRA => Cow::Borrowed("AUFNIRA"),
194            Self::LIA => Cow::Borrowed("LIA"),
195            Self::LRA => Cow::Borrowed("LRA"),
196            Self::QF_ABV => Cow::Borrowed("QF_ABV"),
197            Self::QF_AUFBV => Cow::Borrowed("QF_AUFBV"),
198            Self::QF_AUFLIA => Cow::Borrowed("QF_AUFLIA"),
199            Self::QF_AX => Cow::Borrowed("QF_AX"),
200            Self::QF_BV => Cow::Borrowed("QF_BV"),
201            Self::QF_IDL => Cow::Borrowed("QF_IDL"),
202            Self::QF_LIA => Cow::Borrowed("QF_LIA"),
203            Self::QF_LRA => Cow::Borrowed("QF_LRA"),
204            Self::QF_NIA => Cow::Borrowed("QF_NIA"),
205            Self::QF_NRA => Cow::Borrowed("QF_NRA"),
206            Self::QF_RDL => Cow::Borrowed("QF_RDL"),
207            Self::QF_UF => Cow::Borrowed("QF_UF"),
208            Self::QF_UFBV => Cow::Borrowed("QF_UFBV"),
209            Self::QF_UFIDL => Cow::Borrowed("QF_UFIDL"),
210            Self::QF_UFLIA => Cow::Borrowed("QF_UFLIA"),
211            Self::QF_UFLRA => Cow::Borrowed("QF_UFLRA"),
212            Self::QF_UFNRA => Cow::Borrowed("QF_UFNRA"),
213            Self::UFLRA => Cow::Borrowed("UFLRA"),
214            Self::UFNIA => Cow::Borrowed("UFNIA"),
215            Self::Custom(s) => Cow::Owned(s.to_string()),
216        }
217    }
218}
219impl std::fmt::Display for Logic {
220    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
221        self.name().fmt(f)
222    }
223}
smtlib/logics.rs

smtlib/
logics.rs
