smtlib/
terms.rs

1//! Terms are the building blocks for constructing the mathematical expressions
2//! used in assertions with [`Solver`](crate::Solver).
3//!
4//! They are a statically-typed and ergonomic layer on top of
5//! [`smtlib_lowlevel::ast::Term`], which provides a more _Rust-like_ API.
6
7use std::marker::PhantomData;
8
9use itertools::Itertools;
10use smtlib_lowlevel::{
11    ast::{self, Attribute, AttributeValue, Identifier, QualIdentifier, SortedVar, Term},
12    lexicon::{Keyword, Symbol},
13    Storage,
14};
15
16use crate::{sorts::Sort, Bool};
17
18/// Construct a `STerm` with the presence of `Storage`
19pub trait IntoSTerm {
20    /// Construct a `STerm` with the presence of `Storage`
21    fn into_sterm(self, st: &'_ Storage) -> STerm<'_>;
22}
23
24/// Construct a `STerm` with the presence of `Storage`
25pub trait IntoWithStorage<'st, T> {
26    /// Construct a `STerm` with the presence of `Storage`
27    fn into_with_storage(self, st: &'st Storage) -> T;
28}
29
30impl<'st, T> IntoWithStorage<'st, T> for T {
31    fn into_with_storage(self, _st: &'st Storage) -> T {
32        self
33    }
34}
35
36impl<'st> IntoWithStorage<'st, &'st Term<'st>> for Term<'st> {
37    fn into_with_storage(self, st: &'st Storage) -> &'st Term<'st> {
38        st.alloc_term(self)
39    }
40}
41
42/// A smtlib term with its associated storage.
43///
44/// This is a wrapper around a [`Term`] which also carries a pointer to its
45/// [`Storage`]. Having a pointer to the storage allows new terms to be created
46/// more ergonomically without passing around the storage.
47#[derive(Clone, Copy)]
48#[cfg_attr(feature = "serde", derive(serde::Serialize))]
49pub struct STerm<'st> {
50    #[cfg_attr(feature = "serde", serde(skip))]
51    st: &'st Storage,
52    term: &'st Term<'st>,
53}
54
55impl std::fmt::Debug for STerm<'_> {
56    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
57        f.debug_struct("STerm")
58            .field("st", &"Storage { .. }")
59            .field("term", &self.term)
60            .finish()
61    }
62}
63impl<'st> STerm<'st> {
64    /// Construct a new [`STerm`] with the given term in the given [`Storage`].
65    pub fn new(st: &'st Storage, term: Term<'st>) -> Self {
66        Self {
67            st,
68            term: st.alloc_term(term),
69        }
70    }
71    /// Construct a new [`STerm`] with the given an already allocated term.
72    pub fn new_from_ref(st: &'st Storage, term: &'st Term<'st>) -> Self {
73        Self { st, term }
74    }
75    /// The [`Storage`] associated with the term.
76    pub fn st(self) -> &'st Storage {
77        self.st
78    }
79    /// The [`Term`] associated with the term.
80    pub fn term(self) -> &'st Term<'st> {
81        self.term
82    }
83}
84impl std::fmt::Display for STerm<'_> {
85    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
86        self.term().fmt(f)
87    }
88}
89impl<'st> From<STerm<'st>> for &'st Term<'st> {
90    fn from(sterm: STerm<'st>) -> Self {
91        sterm.term
92    }
93}
94
95pub(crate) fn app<'st>(
96    st: &'st Storage,
97    name: &'st str,
98    args: impl ApplicationArgs<'st>,
99) -> STerm<'st> {
100    STerm::new(
101        st,
102        Term::Application(qual_ident(name, None), args.into_args(st)),
103    )
104}
105
106pub(crate) trait ApplicationArgs<'st> {
107    fn into_args(self, st: &'st Storage) -> &'st [&'st Term<'st>];
108}
109
110impl<'st, A: IntoWithStorage<'st, &'st Term<'st>>> ApplicationArgs<'st> for A {
111    fn into_args(self, st: &'st Storage) -> &'st [&'st Term<'st>] {
112        st.alloc_slice(&[self.into_with_storage(st)])
113    }
114}
115impl<'st, A: IntoWithStorage<'st, &'st Term<'st>>, B: IntoWithStorage<'st, &'st Term<'st>>>
116    ApplicationArgs<'st> for (A, B)
117{
118    fn into_args(self, st: &'st Storage) -> &'st [&'st Term<'st>] {
119        st.alloc_slice(&[self.0.into_with_storage(st), self.1.into_with_storage(st)])
120    }
121}
122impl<
123        'st,
124        A: IntoWithStorage<'st, &'st Term<'st>>,
125        B: IntoWithStorage<'st, &'st Term<'st>>,
126        C: IntoWithStorage<'st, &'st Term<'st>>,
127    > ApplicationArgs<'st> for (A, B, C)
128{
129    fn into_args(self, st: &'st Storage) -> &'st [&'st Term<'st>] {
130        st.alloc_slice(&[
131            self.0.into_with_storage(st),
132            self.1.into_with_storage(st),
133            self.2.into_with_storage(st),
134        ])
135    }
136}
137impl<'st, A: IntoWithStorage<'st, &'st Term<'st>>, const N: usize> ApplicationArgs<'st> for [A; N] {
138    fn into_args(self, st: &'st Storage) -> &'st [&'st Term<'st>] {
139        st.alloc_slice(&self.map(|a| a.into_with_storage(st)))
140    }
141}
142
143pub(crate) fn qual_ident<'st>(s: &'st str, sort: Option<ast::Sort<'st>>) -> QualIdentifier<'st> {
144    if let Some(sort) = sort {
145        QualIdentifier::Sorted(Identifier::Simple(Symbol(s)), sort)
146    } else {
147        QualIdentifier::Identifier(Identifier::Simple(Symbol(s)))
148    }
149}
150
151/// This struct wraps specific instances of other terms to indicate that they
152/// are constant. Constants are named terms whose value can be extracted from a
153/// model using [`Model::eval`](crate::Model::eval).
154///
155/// To construct a `Const<'st, T>` call [`T::new_const`](Sort::new_const) where
156/// `T` implements [`Sort`].
157#[derive(Debug, Clone, Copy)]
158pub struct Const<'st, T>(pub(crate) &'st str, pub(crate) T);
159
160impl<T> Const<'_, T> {
161    /// The name of the constant
162    pub fn name(&self) -> &str {
163        self.0
164    }
165}
166impl<T> std::ops::Deref for Const<'_, T> {
167    type Target = T;
168
169    fn deref(&self) -> &Self::Target {
170        &self.1
171    }
172}
173
174/// This type wraps terms loosing all static type information. It is particular
175/// useful when constructing terms dynamically.
176#[derive(Debug, Clone, Copy)]
177pub struct Dynamic<'st>(STerm<'st>, Sort<'st>);
178impl std::fmt::Display for Dynamic<'_> {
179    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
180        STerm::from(*self).term.fmt(f)
181    }
182}
183
184/// A trait for statically typing STM-LIB terms.
185///
186/// Refer to the [`Sorted`] trait for a more general version of this trait.
187pub trait StaticSorted<'st>: Into<STerm<'st>> + From<STerm<'st>> {
188    /// The inner type of the term. This is used for [`Const<'st, T>`](Const)
189    /// where the inner type is `T`.
190    type Inner: StaticSorted<'st>;
191    /// The sort of this sort.
192    #[allow(clippy::declare_interior_mutable_const)]
193    const AST_SORT: ast::Sort<'static>;
194    /// The sort of this sort.
195    fn sort() -> Sort<'st> {
196        Self::AST_SORT.into()
197    }
198    /// Construct a new constante of this sort.
199    fn new_const(st: &'st Storage, name: &str) -> Const<'st, Self> {
200        let name = st.alloc_str(name);
201        let bv = Term::Identifier(qual_ident(name, Some(Self::AST_SORT)));
202        let bv = STerm::new(st, bv);
203        Const(name, bv.into())
204    }
205    /// The storage associated with the term.
206    fn static_st(&self) -> &'st Storage;
207}
208
209/// An trait for typing STM-LIB terms.
210///
211/// This trait indicates that a type can construct a [`Term`] which is the
212/// low-level primitive that is used to define expressions for the SMT solvers
213/// to evaluate.
214pub trait Sorted<'st>: Into<STerm<'st>> {
215    /// The inner type of the term. This is used for [`Const<'st, T>`](Const)
216    /// where the inner type is `T`.
217    type Inner: Sorted<'st>;
218    /// The sort of the term.
219    fn sort(&self) -> Sort<'st>;
220    /// Check if a sort is of this type.
221    fn is_sort(sort: Sort<'st>) -> bool;
222    /// The storage associated with any term of this sort.
223    fn st(&self) -> &'st Storage;
224    /// Constructy the smtlib AST representation of the term with associated
225    /// storage.
226    fn sterm(self) -> STerm<'st> {
227        self.into()
228    }
229    /// Construct the smtlib AST representation of term.
230    fn term(self) -> &'st Term<'st> {
231        self.sterm().term()
232    }
233    /// Casts a dynamically typed term into a concrete type
234    fn from_dynamic(d: Dynamic<'st>) -> Self
235    where
236        Self: From<(STerm<'st>, Sort<'st>)>,
237    {
238        (d.0, d.1).into()
239    }
240    /// Casts a dynamically typed term into a concrete type iff the dynamic sort
241    /// matches
242    fn try_from_dynamic(d: Dynamic<'st>) -> Option<Self>
243    where
244        Self: From<(STerm<'st>, Sort<'st>)>,
245    {
246        if Self::is_sort(d.sort()) {
247            Some((d.0, d.1).into())
248        } else {
249            None
250        }
251    }
252    /// Casts the term into a dynamic term which looses static types and stores
253    /// the sort dynamically.
254    fn into_dynamic(self) -> Dynamic<'st> {
255        let sort = self.sort();
256        Dynamic::from_term_sort(self.into(), sort)
257    }
258    /// Construct the term representing `(= self other)`
259    fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st> {
260        let other = other.into_with_storage(self.st()).term();
261        app(self.st(), "=", (self.term(), other)).into()
262    }
263    /// Construct the term representing `(distinct self other)`
264    fn _neq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st> {
265        let other = other.into_with_storage(self.st()).term();
266        app(self.st(), "distinct", (self.term(), other)).into()
267    }
268    /// Wraps the term in a a label, which can be used to extract information
269    /// from models at a later point.
270    fn labeled(self) -> (Label<Self>, Self::Inner)
271    where
272        Self::Inner: From<STerm<'st>>,
273    {
274        let label = Label::generate();
275        let name = label.name();
276        let name = self.st().alloc_str(&name);
277        let args = self.st().alloc_slice(&[Attribute::WithValue(
278            Keyword("named"),
279            AttributeValue::Symbol(Symbol(name)),
280        )]);
281
282        (
283            label,
284            STerm::new(self.st(), Term::Annotation(self.into().into(), args)).into(),
285        )
286    }
287}
288impl<'st, T: Into<STerm<'st>>> From<Const<'st, T>> for STerm<'st> {
289    fn from(c: Const<'st, T>) -> Self {
290        c.1.into()
291    }
292}
293impl<'st, T: Sorted<'st>> Sorted<'st> for Const<'st, T> {
294    type Inner = T;
295    fn sort(&self) -> Sort<'st> {
296        T::sort(self)
297    }
298    fn is_sort(sort: Sort<'st>) -> bool {
299        T::is_sort(sort)
300    }
301    fn st(&self) -> &'st Storage {
302        self.1.st()
303    }
304}
305
306impl<'st, T: StaticSorted<'st>> Sorted<'st> for T {
307    type Inner = T::Inner;
308
309    fn sort(&self) -> Sort<'st> {
310        Self::AST_SORT.into()
311    }
312
313    fn is_sort(sort: Sort<'st>) -> bool {
314        sort == Self::sort()
315    }
316
317    fn st(&self) -> &'st Storage {
318        self.static_st()
319    }
320}
321
322/// Labels are annotations that can be put on expressions to track their
323/// satisfiability.
324///
325/// > **NOTE:** API's for labels are yet to be part of the crate at the time of
326/// > writing.
327pub struct Label<T>(u64, PhantomData<T>);
328impl<T> Label<T> {
329    pub(crate) fn generate() -> Self {
330        use core::sync::atomic::{AtomicU64, Ordering};
331        static NAMED_LABEL_COUNT: AtomicU64 = AtomicU64::new(0);
332
333        let n = NAMED_LABEL_COUNT.fetch_add(1, Ordering::Relaxed);
334
335        Label(n, PhantomData)
336    }
337    pub(crate) fn name(&self) -> String {
338        format!("named-label-{}", self.0)
339    }
340}
341
342impl<'st, T> From<Const<'st, T>> for Dynamic<'st>
343where
344    T: Into<Dynamic<'st>>,
345{
346    fn from(c: Const<'st, T>) -> Self {
347        c.1.into()
348    }
349}
350impl<'st> From<Dynamic<'st>> for STerm<'st> {
351    fn from(d: Dynamic<'st>) -> Self {
352        d.0
353    }
354}
355impl<'st> From<(STerm<'st>, Sort<'st>)> for Dynamic<'st> {
356    fn from((t, sort): (STerm<'st>, Sort<'st>)) -> Self {
357        Dynamic::from_term_sort(t, sort)
358    }
359}
360impl<'st> Dynamic<'st> {
361    /// Construct a dynamic term from a term and a sort.
362    pub fn from_term_sort(t: STerm<'st>, sort: Sort<'st>) -> Self {
363        Dynamic(t, sort)
364    }
365
366    /// Returns the sort of the dynamic term.
367    pub fn sort(&self) -> Sort<'st> {
368        self.1
369    }
370
371    /// Attempt to cast the dynamic into an [`Int`](crate::Int) if the sort
372    /// matches.
373    pub fn as_int(&self) -> Result<crate::Int<'st>, crate::Error> {
374        crate::Int::try_from_dynamic(*self).ok_or_else(|| crate::Error::DynamicCastSortMismatch {
375            expected: crate::Int::AST_SORT.to_string(),
376            actual: self.1.to_string(),
377        })
378    }
379
380    /// Attempt to cast the dynamic into a [`Bool`] if the sort
381    /// matches.
382    pub fn as_bool(&self) -> Result<crate::Bool<'st>, crate::Error> {
383        crate::Bool::try_from_dynamic(*self).ok_or_else(|| crate::Error::DynamicCastSortMismatch {
384            expected: crate::Bool::AST_SORT.to_string(),
385            actual: self.1.to_string(),
386        })
387    }
388}
389impl<'st> Sorted<'st> for Dynamic<'st> {
390    type Inner = Self;
391    fn sort(&self) -> Sort<'st> {
392        self.1
393    }
394    fn is_sort(_sort: Sort<'st>) -> bool {
395        true
396    }
397    fn st(&self) -> &'st Storage {
398        self.0.st()
399    }
400}
401
402#[macro_export]
403#[doc(hidden)]
404macro_rules! impl_op {
405    ($ty:ty, $other:ty, $trait:tt, $fn:ident, $op:literal, $a_trait:tt, $a_fn:tt, $a_op:tt) => {
406        impl<'st, R> std::ops::$trait<R> for Const<'st, $ty>
407        where
408            R: IntoWithStorage<'st, $ty>,
409        {
410            type Output = $ty;
411            fn $fn(self, rhs: R) -> Self::Output {
412                self.1.binop($op, $crate::terms::IntoWithStorage::into_with_storage(rhs, self.st()))
413            }
414        }
415        impl<'st, R> std::ops::$trait<R> for $ty
416        where
417            R: IntoWithStorage<'st, $ty>,
418        {
419            type Output = Self;
420            fn $fn(self, rhs: R) -> Self::Output {
421                self.binop($op, $crate::terms::IntoWithStorage::into_with_storage(rhs, self.st()))
422            }
423        }
424        impl<'st> std::ops::$trait<Const<'st, $ty>> for $other {
425            type Output = $ty;
426            fn $fn(self, rhs: Const<'st, $ty>) -> Self::Output {
427                // $ty::from(self).binop($op, rhs.1)
428                <$other as $crate::terms::IntoWithStorage<'st, $ty>>::into_with_storage(self, rhs.st()).binop($op, rhs.1)
429            }
430        }
431        impl<'st> std::ops::$trait<$ty> for $other {
432            type Output = $ty;
433            fn $fn(self, rhs: $ty) -> Self::Output {
434                // <$ty>::from(self).binop($op, rhs)
435                <$other as $crate::terms::IntoWithStorage<'st, $ty>>::into_with_storage(self, rhs.st()).binop($op, rhs)
436            }
437        }
438        impl<'st, R> std::ops::$a_trait<R> for $ty
439        where
440            R: IntoWithStorage<'st, $ty>,
441        {
442            fn $a_fn(&mut self, rhs: R) {
443                *self = *self $a_op rhs;
444            }
445        }
446    };
447}
448
449/// This trait is implemented for types and sequences which can be used as
450/// quantified variables in [`forall`] and [`exists`].
451pub trait QuantifierVars<'st> {
452    /// The concrete sequence of variable declaration which should be quantified
453    /// over.
454    fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>];
455}
456
457impl<'st, A> QuantifierVars<'st> for Const<'st, A>
458where
459    A: StaticSorted<'st>,
460{
461    fn into_vars(self, _st: &'st Storage) -> &'st [SortedVar<'st>] {
462        let st = self.st();
463        st.alloc_slice(&[SortedVar(Symbol(self.0), A::AST_SORT)])
464    }
465}
466macro_rules! impl_quantifiers {
467    ($($x:ident $n:tt),+ $(,)?) => {
468        impl<'st, $($x,)+> QuantifierVars<'st> for ($(Const<'st, $x>),+)
469        where
470            $($x: StaticSorted<'st>),+
471        {
472            fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>] {
473                st.alloc_slice(&[
474                    $(SortedVar(Symbol((self.$n).0.into()), $x::AST_SORT)),+
475                ])
476            }
477        }
478    };
479}
480impl_quantifiers!(A 0, B 1);
481impl_quantifiers!(A 0, B 1, C 2);
482impl_quantifiers!(A 0, B 1, C 2, D 3);
483impl_quantifiers!(A 0, B 1, C 2, D 3, E 4);
484
485impl<'st> QuantifierVars<'st> for Vec<Const<'st, Dynamic<'st>>> {
486    fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>] {
487        st.alloc_slice(self.as_slice()).into_vars(st)
488    }
489}
490impl<'st> QuantifierVars<'st> for &'st [Const<'st, Dynamic<'st>>] {
491    fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>] {
492        if self.is_empty() {
493            &[]
494        } else {
495            st.alloc_slice(
496                &self
497                    .iter()
498                    .map(|v| SortedVar(Symbol(v.0), v.1 .1.ast()))
499                    .collect_vec(),
500            )
501        }
502    }
503}
504impl<'st> QuantifierVars<'st> for &'st [SortedVar<'st>] {
505    fn into_vars(self, _st: &'st Storage) -> &'st [SortedVar<'st>] {
506        self
507    }
508}
509
510/// Universally quantifies over `vars` in expression `term`.
511pub fn forall<'st>(st: &'st Storage, vars: impl QuantifierVars<'st>, term: Bool<'st>) -> Bool<'st> {
512    STerm::new(
513        st,
514        Term::Forall(vars.into_vars(st), STerm::from(term).into()),
515    )
516    .into()
517}
518/// Existentially quantifies over `vars` in expression `term`.
519pub fn exists<'st>(st: &'st Storage, vars: impl QuantifierVars<'st>, term: Bool<'st>) -> Bool<'st> {
520    STerm::new(
521        st,
522        Term::Exists(vars.into_vars(st), STerm::from(term).into()),
523    )
524    .into()
525}
smtlib/terms.rs

smtlib/
terms.rs
