formally_smt_macros/
lib.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 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
25//! Procedural macros exported by the `formally::smt` subcrate.
26#![doc = ""]
27#![cfg_attr(
28    not(feature = "__subcratedoc"),
29    doc = "**WARNING: This crate is not supposed to be used directly.**"
30)]
31#![doc = ""]
32#![cfg_attr(
33    not(feature = "__subcratedoc"),
34    doc = "**Use instead the `formally::smt` module of the main `formally` crate by enabling the `\"smt\"` feature.**"
35)]
36#![doc = ""]
37
38mod term;
39
40use proc_macro::TokenStream;
41use quote::quote;
42use syn::parse_macro_input;
43
44use term::*;
45
46/// Construct a term from a subset of the SMT-LIBv2 syntax for terms.
47///
48/// This macro provides a convenient way of constructing terms by implementing a subset of the
49/// SMT-LIBv2 syntax.
50///
51/// Example:
52/// ```
53/// # mod formally {
54/// #     pub extern crate formally_support as support;
55/// #     pub extern crate formally_smt as smt;
56/// # }
57/// # use formally::{smt::*, support::*};
58/// # fn main() -> Result<()> {
59/// let mut solver = Solver::new(&Config::default())?;
60///
61/// solver.declare(Declaration::boolean("p"))?;
62/// solver.declare(Declaration::boolean("q"))?;
63///
64/// let ponens = term!(=> (and (=> p q) p) q);
65/// solver.require(term!(not #ponens))?;
66///
67/// assert_eq!(solver.check()?, Answer::No);
68/// # Ok(())
69/// # }
70/// ```
71///
72/// In the above example we can note two features of the `term` macro combined with `Solver`.
73/// 1. names of the symbols can be used directly, in which case the resulting term will contain
74///    *unbound atoms* that the solver will resolve when needed (in this case, in the call to
75///    `require()`. This is the case of the `"and"`, `"p"`, `"q"`, and `"not"` symbols in the
76///    example above.
77/// 2. entities declared in the surrounding Rust code, including other terms, can be expanded by
78///    using the `#identifier` syntax, inspired by the `quote` macro of the `syn` crate. This is the
79///    case of the `#ponens` expansion in the example above.
80///
81/// When an entity is expanded it is used in the resulting term appropriately. In particular, one
82/// can expand `Declared` or `Defined` objects to obtain *bound atoms* that do not need
83/// further name resolution.
84///
85/// Expansion of repetitions from iterators, as in the `quote` macro, is not supported *yet*.
86#[proc_macro]
87pub fn term(input: TokenStream) -> TokenStream {
88    let term = parse_macro_input!(input as Root);
89
90    quote!(#term).into()
91}
formally_smt_macros/lib.rs

formally_smt_macros/
lib.rs
