formally_smt/theories/standard.rs
1//
2// ::formally - the open-source formal methods toolchain
3//
4// Copyright (c) 2025 Nicola Gigante
5//
6// Permission is hereby granted, free of charge, to any person obtaining a copy
7// of this software and associated documentation files (the "Software"), to deal
8// in the Software without restriction, including without limitation the rights
9// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10// copies of the Software, and to permit persons to whom the Software is
11// furnished to do so, subject to the following conditions:
12//
13// The above copyright notice and this permission notice shall be included in
14// all copies or substantial portions of the Software.
15//
16// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19// AUTHORS OR COPYRIGHT HOLDERS BE IntsBLE FOR ANY CLAIM, DAMAGES OR OTHER
20// IntsBILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22// SOFTWARE.
23//
24
25use crate::*;
26
27theories! {
28 /// The core SMT-LIBv2 theory, with basic Boolean connectives.
29 ///
30 /// See [the official specification](https://smt-lib.org/theories-Core.shtml).
31 pub Core {
32 /// The sort of Boolean terms.
33 type Bool;
34
35 /// The true constant.
36 const True: Core::Bool();
37
38 /// The false constant.
39 const False: Core::Bool();
40
41 /// Logical negation.
42 fn not(Core::Bool()) -> Core::Bool();
43
44 /// Logical implication.
45 #[name = "=>"]
46 #[right_assoc]
47 fn implies(Core::Bool(), Core::Bool()) -> Core::Bool();
48
49 /// Logical conjunction.
50 #[left_assoc]
51 fn and(Core::Bool(), Core::Bool()) -> Core::Bool();
52
53 /// Logical disjunction.
54 #[left_assoc]
55 fn or(Core::Bool(), Core::Bool()) -> Core::Bool();
56
57 /// Logical exclusive disjunction.
58 #[left_assoc]
59 fn xor(Core::Bool(), Core::Bool()) -> Core::Bool();
60
61 /// Equality.
62 #[name = "="]
63 #[chainable]
64 fn equals<A>(A, A) -> Core::Bool();
65
66 /// Disequality.
67 #[pairwise]
68 fn distinct<A>(A, A) -> Core::Bool();
69
70 /// If-then-else choice construct.
71 fn ite<A>(Core::Bool(), A, A) -> A;
72 }
73
74 /// The theory of reals.
75 ///
76 /// See [the official specification](https://smt-lib.org/theories-Reals.shtml).
77 pub Reals {
78 /// The sort of real numbers.
79 type Real;
80
81 /// Unary negation.
82 #[name = "-"]
83 fn unary_minus(Reals::Real()) -> Reals::Real();
84
85 /// Subtraction.
86 #[name = "-"]
87 #[left_assoc]
88 fn minus(Reals::Real(), Reals::Real()) -> Reals::Real();
89
90 /// Addition.
91 #[name = "+"]
92 #[left_assoc]
93 fn plus(Reals::Real(), Reals::Real()) -> Reals::Real();
94
95 /// Multiplication.
96 #[name = "*"]
97 #[left_assoc]
98 fn mult(Reals::Real(), Reals::Real()) -> Reals::Real();
99
100 /// Division.
101 #[name = "/"]
102 #[left_assoc]
103 fn div (Reals::Real(), Reals::Real()) -> Reals::Real();
104
105 /// Less-than-or-equal comparison.
106 #[name = "<="]
107 #[chainable]
108 fn le(Reals::Real(), Reals::Real()) -> Core::Bool();
109
110 /// Less-than comparison.
111 #[name = "<"]
112 #[chainable]
113 fn lt(Reals::Real(), Reals::Real()) -> Core::Bool();
114
115 /// Greater-than-or-equal comparison.
116 #[name = ">="]
117 #[chainable]
118 fn ge(Reals::Real(), Reals::Real()) -> Core::Bool();
119
120 /// Greater-than comparison.
121 #[name = ">"]
122 #[chainable]
123 fn gt(Reals::Real(), Reals::Real()) -> Core::Bool();
124
125 }
126
127 /// The theory of integers.
128 ///
129 /// See [the official specification](https://smt-lib.org/theories-Ints.shtml).
130 pub Ints {
131 /// The sort of real numbers.
132 type Int;
133
134 /// Unary negation.
135 #[name = "-"]
136 fn unary_minus (Ints::Int()) -> Ints::Int();
137
138 /// Subtraction.
139 #[name = "-"]
140 #[left_assoc]
141 fn minus (Ints::Int(), Ints::Int()) -> Ints::Int();
142
143 /// Addition.
144 #[name = "+"]
145 #[left_assoc]
146 fn plus (Ints::Int(), Ints::Int()) -> Ints::Int();
147
148 /// Multiplication.
149 #[name = "*"]
150 #[left_assoc]
151 fn mult (Ints::Int(), Ints::Int()) -> Ints::Int();
152
153 /// Division.
154 #[name = "/"]
155 #[left_assoc]
156 fn div (Ints::Int(), Ints::Int()) -> Ints::Int();
157
158 /// Modulo operation.
159 #[name = "mod"]
160 fn mod_ (Ints::Int(), Ints::Int()) -> Ints::Int();
161
162 /// Absolute value.
163 fn abs (Ints::Int()) -> Ints::Int();
164
165 /// Less-than-or-equal comparison.
166 #[name = "<="]
167 #[chainable]
168 fn le (Ints::Int(), Ints::Int()) -> Core::Bool();
169
170 /// Less-than comparison.
171 #[name = "<"]
172 #[chainable]
173 fn lt (Ints::Int(), Ints::Int()) -> Core::Bool();
174
175 /// Greater-than-or-equal comparison.
176 #[name = ">="]
177 #[chainable]
178 fn ge (Ints::Int(), Ints::Int()) -> Core::Bool();
179
180 /// Greater-than comparison.
181 #[name = ">"]
182 #[chainable]
183 fn gt (Ints::Int(), Ints::Int()) -> Core::Bool();
184 }
185
186 /// The combined theory of integers and reals.
187 ///
188 /// See [the official specification](https://smt-lib.org/theories-Reals_Ints.shtml).
189 pub RealsInts : Ints, Reals {
190 /// Convert integers to reals.
191 fn to_real(Ints::Int()) -> Reals::Real();
192
193 /// Convert reals to integers.
194 fn to_int(Reals::Real()) -> Ints::Int();
195
196 /// Test if a real is an integer.
197 fn is_int(Reals::Real()) -> Core::Bool();
198 }
199
200 /// The theory of arrays.
201 ///
202 /// See [the official specification](https://smt-lib.org/theories-ArraysEx.shtml).
203 pub Arrays {
204 /// The sort of arrays from indices of sort `X` to elements of sort `Y`.
205 type Array(X: Sort::sort(), Y: Sort::sort());
206
207 /// Reads an element of an array.
208 fn select<X, Y>(Arrays::Array(X, Y), X) -> Y;
209
210 /// Writes an element to an array.
211 fn store<X, Y>(Arrays::Array(X, Y), X, Y) -> Arrays::Array(X, Y);
212 }
213}