formally_smt/
pool.rs

1//
2// ::formally - the open-source formal methods toolchain
3//
4// Copyright (c) 2026 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 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20// LIABILITY, 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::formally;
26use dashmap::DashSet;
27use formally::{
28    smt::*,
29    support::{Identifier, Nominal},
30};
31use std::{borrow::Borrow, cell::RefCell, collections::HashSet, fmt::Debug, sync::Arc};
32
33/// Trait for types that implement subterm sharing for [terms][Term].
34///
35/// [TermPool] instances provides the basic functionality for subterm sharing in the framework.
36/// The trait is currently implemented only by [HashPool] and [DashPool], with the latter usable in
37/// multithraeded contexts. Since [Term] cannot be publicly constructed, this trait is not designed
38/// to be implemented by downstream crates.
39///
40/// The main use of [TermPool] instances is to give them to [TermManager::with_pool()] in order to
41/// share the same pool among different term managers and solvers. This allows to share the same
42/// [Term] objects between different SMT backends, even among different threads when using
43/// [DashPool].
44///
45/// The [TermPool::shared()] method is rarely called directly. Prefer using [ToTerm::into_term_in()]
46/// to manually get a [Term] out of a [ToTerm] object (which, again, is rarely needed, because
47/// [ToTerm] is usually accepted directly throughout the framework).
48pub trait TermPool {
49    /// Return the unique [Term] whose underlying [TermKind] is equal to the argument.
50    fn shared(&self, kind: TermKind) -> Term;
51
52    /// Return the unique [Term] whose underlying [TermKind] is equal to the one referenced by the
53    /// argument.
54    fn shared_ref(&self, kind: &TermKind) -> Term;
55}
56
57#[derive(Debug, Hash, PartialEq, Eq)]
58struct Lookup<T>(T);
59
60impl Borrow<TermKind> for Lookup<Arc<TermInner>> {
61    fn borrow(&self) -> &TermKind {
62        &self.0.kind
63    }
64}
65
66/// Sequential, single-threaded implementation of [TermPool].
67///
68/// [HashPool] is based on the standard [HashSet] so its use is limited to a single thread, and
69/// consequently the type is not [Send] nor [Sync]. If the same [TermPool] has to be shared among
70/// different threads, look for [DashPool] instead.
71///
72/// [HashPool] is the default [TermPool] implementation used by [TermManager::with_backend()].
73#[derive(Debug, Default)]
74pub struct HashPool {
75    pool: RefCell<HashSet<Lookup<Arc<TermInner>>>>,
76}
77
78impl HashPool {
79    pub fn new() -> HashPool {
80        HashPool::default()
81    }
82}
83
84/// Concurrent, multithreaded implementation of [TermPool].
85///
86/// [DashPool] is based on [DashSet] from the [dashmap] crate. As such the type is both [Send] and
87/// [Sync] and can be shared and accessed freely by multiple threads without additional
88/// synchronization.
89///
90/// Give a [DashPool] instance to [TermManager::with_pool()] in order to share the same concurrent
91/// pool among different term managers used in different threads.
92#[derive(Debug, Default)]
93pub struct DashPool {
94    pool: DashSet<Lookup<Arc<TermInner>>>,
95}
96
97impl DashPool {
98    pub fn new() -> DashPool {
99        DashPool::default()
100    }
101}
102
103impl TermPool for DashPool {
104    fn shared(&self, kind: TermKind) -> Term {
105        if let Some(kind) = self.pool.get(&kind) {
106            Term(Nominal(kind.0.clone()))
107        } else {
108            let arc = Arc::new(TermInner::new(kind));
109            let term = Term(Nominal(arc.clone()));
110            self.pool.insert(Lookup(arc));
111
112            term
113        }
114    }
115
116    fn shared_ref(&self, kind: &TermKind) -> Term {
117        if let Some(kind) = self.pool.get(kind) {
118            Term(Nominal(kind.0.clone()))
119        } else {
120            let arc = Arc::new(TermInner::new(kind.clone()));
121            let term = Term(Nominal(arc.clone()));
122            self.pool.insert(Lookup(arc));
123
124            term
125        }
126    }
127}
128
129impl TermPool for HashPool {
130    fn shared(&self, kind: TermKind) -> Term {
131        if let Some(kind) = self.pool.borrow().get(&kind) {
132            Term(Nominal(kind.0.clone()))
133        } else {
134            let arc = Arc::new(TermInner::new(kind));
135            let term = Term(Nominal(arc.clone()));
136            self.pool.borrow_mut().insert(Lookup(arc));
137
138            term
139        }
140    }
141
142    fn shared_ref(&self, kind: &TermKind) -> Term {
143        if let Some(kind) = self.pool.borrow().get(kind) {
144            Term(Nominal(kind.0.clone()))
145        } else {
146            let arc = Arc::new(TermInner::new(kind.clone()));
147            let term = Term(Nominal(arc.clone()));
148            self.pool.borrow_mut().insert(Lookup(arc));
149
150            term
151        }
152    }
153}
154
155/// Trait for types that can be uniqued in [TermPools](TermPool) to obtain a [Term].
156///
157/// This trait represents types that can be converted to [Term] after being uniqued into a
158/// [TermPool]. This includes of course [Term] itself and [TermKind], but also many types
159/// convertible to [TermKind], the [Sort] type, and the result of the [term!] macro.
160///
161/// Most methods in the framework that would accept a [Term] (e.g. in [Solver]) accept a generic
162/// [ToTerm] argument instead, so e.g. an invocation of the [term!] macro can be passed directly to
163/// them. In the particular cases where a [Term] has to be manually obtained from a [ToTerm]
164/// instance, one passes a reference to a [TermPool] to [ToTerm::into_term_in()] or
165/// [ToTerm::to_term_in()].
166pub trait ToTerm: Debug {
167    /// Convert the object into a [Term] by uniquing in the given [TermPool].
168    fn into_term_in(self, pool: &dyn TermPool) -> Term;
169
170    /// Convert the object (by reference) into a [Term] by uniquing in the given [TermPool].
171    fn to_term_in(&self, pool: &dyn TermPool) -> Term;
172}
173
174impl<T: ToTerm> ToTerm for &T {
175    fn into_term_in(self, pool: &dyn TermPool) -> Term {
176        self.to_term_in(pool)
177    }
178
179    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
180        (*self).to_term_in(pool)
181    }
182}
183
184impl ToTerm for Term {
185    fn into_term_in(self, _pool: &dyn TermPool) -> Term {
186        self
187    }
188
189    fn to_term_in(&self, _pool: &dyn TermPool) -> Term {
190        self.clone()
191    }
192}
193
194impl ToTerm for TermKind {
195    fn into_term_in(self, pool: &dyn TermPool) -> Term {
196        pool.shared(self)
197    }
198
199    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
200        pool.shared_ref(self)
201    }
202}
203
204impl ToTerm for Constant {
205    fn into_term_in(self, pool: &dyn TermPool) -> Term {
206        TermKind::Constant(self).into_term_in(pool)
207    }
208
209    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
210        TermKind::Constant(self.clone()).into_term_in(pool)
211    }
212}
213
214impl ToTerm for Atom {
215    fn into_term_in(self, pool: &dyn TermPool) -> Term {
216        TermKind::Atom(self).into_term_in(pool)
217    }
218
219    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
220        TermKind::Atom(self.clone()).into_term_in(pool)
221    }
222}
223
224impl ToTerm for FunctionRef {
225    fn into_term_in(self, pool: &dyn TermPool) -> Term {
226        TermKind::Atom(Atom::from(self)).into_term_in(pool)
227    }
228
229    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
230        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
231    }
232}
233
234impl ToTerm for BoundRef {
235    fn into_term_in(self, pool: &dyn TermPool) -> Term {
236        TermKind::Atom(Atom::from(self)).into_term_in(pool)
237    }
238
239    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
240        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
241    }
242}
243
244impl ToTerm for Function {
245    fn into_term_in(self, pool: &dyn TermPool) -> Term {
246        TermKind::Atom(Atom::from(self)).into_term_in(pool)
247    }
248
249    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
250        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
251    }
252}
253
254impl ToTerm for Variable {
255    fn into_term_in(self, pool: &dyn TermPool) -> Term {
256        TermKind::Atom(Atom::from(self)).into_term_in(pool)
257    }
258
259    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
260        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
261    }
262}
263
264impl ToTerm for Primitive {
265    fn into_term_in(self, pool: &dyn TermPool) -> Term {
266        TermKind::Atom(Atom::from(self)).into_term_in(pool)
267    }
268
269    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
270        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
271    }
272}
273
274impl ToTerm for UserFunction {
275    fn into_term_in(self, pool: &dyn TermPool) -> Term {
276        TermKind::Atom(Atom::from(self)).into_term_in(pool)
277    }
278
279    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
280        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
281    }
282}
283
284impl ToTerm for Declared {
285    fn into_term_in(self, pool: &dyn TermPool) -> Term {
286        TermKind::Atom(Atom::from(self)).into_term_in(pool)
287    }
288
289    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
290        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
291    }
292}
293
294impl ToTerm for Defined {
295    fn into_term_in(self, pool: &dyn TermPool) -> Term {
296        TermKind::Atom(Atom::from(self)).into_term_in(pool)
297    }
298
299    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
300        TermKind::Atom(Atom::from(self.clone())).into_term_in(pool)
301    }
302}
303
304impl ToTerm for Identifier<'_> {
305    fn into_term_in(self, pool: &dyn TermPool) -> Term {
306        TermKind::Atom(Atom::from(self.into_owned())).into_term_in(pool)
307    }
308
309    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
310        TermKind::Atom(Atom::from(self.clone().into_owned())).into_term_in(pool)
311    }
312}
313
314impl ToTerm for Quantified {
315    fn into_term_in(self, pool: &dyn TermPool) -> Term {
316        TermKind::Quantified(self).into_term_in(pool)
317    }
318
319    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
320        TermKind::Quantified(self.clone()).into_term_in(pool)
321    }
322}
323
324impl ToTerm for Let {
325    fn into_term_in(self, pool: &dyn TermPool) -> Term {
326        TermKind::Let(self).into_term_in(pool)
327    }
328
329    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
330        TermKind::Let(self.clone()).into_term_in(pool)
331    }
332}
333
334impl ToTerm for Sort {
335    fn into_term_in(self, pool: &dyn TermPool) -> Term {
336        let mut arguments = Vec::with_capacity(self.arguments.len());
337        for arg in &*self.arguments {
338            match arg {
339                SortArgument::Value(c) => arguments.push(
340                    Constant::Integer {
341                        value: c.clone(),
342                        span: None,
343                    }
344                    .to_term_in(pool),
345                ),
346                SortArgument::Sort(s) => arguments.push(s.to_term_in(pool)),
347            }
348        }
349
350        Atom {
351            head: FunctionRef::from(self.head.clone()),
352            arguments: Arc::from(arguments.into_boxed_slice()),
353            span: None,
354        }
355        .into_term_in(pool)
356    }
357
358    fn to_term_in(&self, pool: &dyn TermPool) -> Term {
359        self.clone().into_term_in(pool)
360    }
361}
formally_smt/pool.rs

formally_smt/
pool.rs
