formally_smt/theories/mod.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
25//! Declaration and usage of SMT-LIBv2 theories.
26//!
27//! This module contains everything regarding the declaration and usage of *theories* understood as
28//! in the terminology of SMT-LIBv2.
29//!
30//! Most of the types declared in this module, except [CombinedTheory], are theories declared
31//! through the [theories!] macro, so one may want to look at its documentation as well.
32//!
33//! Each theory type is a unit struct (e.g. declared as `pub struct Ints;`, so it is instantiated as
34//! `Ints`, not `Ints {}`) and exposes a set of associated functions, one for each symbol provided
35//! by the theory. Function and constant symbols (e.g. [Ints::plus()] or [Core::True()] are
36//! represented by returning a [Primitive] object. Sorts (e.g. [Ints::Int()]) return a [Sort].
37//!
38//! For parametric sorts (e.g. `(Array X Y)`) the corresponding functions accept a suitable number
39//! of [sort arguments](SortArgument), so `(Array Int Int)` would be represented by
40//! `Arrays::Array(Ints::Int(), Ints::Int())`.
41//!
42//! Theories are usually combined in a [Logic](logics::Logic), and the logic is what is set when
43//! instantiating a [Solver]. When a logic is set to a solver, its symbols become in scope when
44//! the solver applies [name resolution](Term::resolve()) to terms (e.g. those constructed with the
45//! [term] macro). Therefore, in common usage of the framework, elements in this module should
46//! rarely need to be mentioned directly.
47//!
48//! Instead, people implementing new *backends* will need to access this module quite
49//! often. We refer to the documentation on [how to write a new backend](crate::backends) for
50//! details.
51
52use crate::*;
53use formally::support::*;
54
55mod standard;
56
57pub use standard::*;
58
59/// A trait for types representing SMT-LIBv2 theories.
60///
61/// The purpose of a theory object is that of providing an [environment](Env) providing the symbols
62/// that the theory has to provide. Therefore, the trait expose two methods
63/// ([functions()](Theory::functions()) and [sorts()](crate::theories::Theory::sorts()) to return
64/// the corresponding function and sort scopes.
65///
66/// Implementing this trait directly is quite rare, since theories are usually better declared
67/// using the [theories!] macro.
68pub trait Theory {
69 fn functions(&self) -> Scope<Function>;
70
71 fn sorts(&self) -> Scope<Function>;
72
73 fn env(&self) -> Env {
74 Env {
75 functions: self.functions(),
76 sorts: self.sorts(),
77 }
78 }
79}
80
81pub trait TheoryEx: Theory {
82 type Atom<'t>: Into<Atom> + TryFrom<&'t Atom, Error = &'t Atom>;
83 type Sort<'t>: Into<Sort> + TryFrom<&'t Sort, Error = &'t Sort>;
84}
85
86/// An instance of [Theory] combining multiple theories together.
87pub struct CombinedTheory {
88 functions: Scope<Function>,
89 sorts: Scope<Function>,
90}
91
92impl CombinedTheory {
93 /// Create a theory combining the given theories.
94 pub fn new(theories: &[&dyn Theory]) -> CombinedTheory {
95 let mut functions = Scope::new();
96 let mut sorts = Scope::new();
97
98 for theory in theories {
99 functions.merge(&theory.functions());
100 sorts.merge(&theory.sorts());
101 }
102
103 CombinedTheory { functions, sorts }
104 }
105}
106
107impl Theory for CombinedTheory {
108 fn functions(&self) -> Scope<Function> {
109 self.functions.clone()
110 }
111 fn sorts(&self) -> Scope<Function> {
112 self.sorts.clone()
113 }
114}
115
116static SORT_DECL: PrimitiveData = PrimitiveData {
117 name: Identifier::new("Sort"),
118 parameters: Vec::new(),
119 domain: Vec::new(),
120 range: Sort::sort(),
121 associativity: None,
122};
123
124impl Sort {
125 /// The sort of sorts.
126 ///
127 /// [Sort::sort()] returns a special sort, not provided by any theory, which is the sort of
128 /// terms representing sorts. In other words, a sort term such as `(Array Int Real)` has
129 /// sort [Sort::sort()].
130 /// ```
131 /// # mod formally {
132 /// # pub extern crate formally_support as support;
133 /// # pub extern crate formally_smt as smt;
134 /// # }
135 /// # use formally::{smt::*, support::*};
136 /// # fn main() -> Result<()> {
137 /// let mut solver = Solver::new(&Config::default().logic("ALIA"))?;
138 ///
139 /// // construct and resolve the term
140 /// let array = solver.lookup(term!(Array Int Int), Role::Sort)?;
141 /// let sort = Sort::of(&array)?; // deduce the sort of the term
142 ///
143 /// assert_eq!(sort, Sort::sort()); // the resulting sort is `Sort::sort()`
144 /// # Ok(())
145 /// # }
146 /// ```
147 #[allow(clippy::self_named_constructors)]
148 pub const fn sort() -> Sort {
149 Sort {
150 head: SortHead::Bound(Function::Primitive(Primitive(Nominal(SArc::Static(
151 &SORT_DECL,
152 ))))),
153 arguments: SArc::Static(&[]),
154 }
155 }
156}