smtlib/theories/
core.rs

1#![doc = concat!("```ignore\n", include_str!("./Core.smt2"), "```")]
2
3use smtlib_lowlevel::{
4    ast::{self, Term},
5    Storage,
6};
7
8use crate::{
9    impl_op,
10    sorts::Sort,
11    terms::{app, qual_ident, Const, Dynamic, IntoWithStorage, STerm, Sorted, StaticSorted},
12};
13
14/// A [`Bool`] is a term containing a
15/// [boolean](https://en.wikipedia.org/wiki/Boolean_data_type). You can [read more
16/// here.](https://smtlib.cs.uiowa.edu/theories-Core.shtml).
17#[derive(Clone, Copy)]
18pub struct Bool<'st>(STerm<'st>);
19
20impl<'st> Bool<'st> {
21    /// Construct a new bool.
22    pub fn new(st: &'st Storage, value: bool) -> Bool<'st> {
23        value.into_with_storage(st)
24    }
25}
26
27impl std::fmt::Debug for Bool<'_> {
28    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
29        self.0.fmt(f)
30    }
31}
32
33impl<'st> From<Const<'st, Bool<'st>>> for Bool<'st> {
34    fn from(c: Const<'st, Bool<'st>>) -> Self {
35        c.1
36    }
37}
38impl<'st> IntoWithStorage<'st, Bool<'st>> for Const<'st, Bool<'st>> {
39    fn into_with_storage(self, _st: &'st Storage) -> Bool<'st> {
40        self.1
41    }
42}
43impl std::fmt::Display for Bool<'_> {
44    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45        self.term().fmt(f)
46    }
47}
48impl<'st> From<Bool<'st>> for Dynamic<'st> {
49    fn from(b: Bool<'st>) -> Self {
50        b.into_dynamic()
51    }
52}
53impl<'st> IntoWithStorage<'st, Bool<'st>> for bool {
54    fn into_with_storage(self, st: &'st Storage) -> Bool<'st> {
55        let s = match self {
56            true => "true",
57            false => "false",
58        };
59
60        STerm::new(st, Term::Identifier(qual_ident(s, None))).into()
61    }
62}
63impl<'st> From<Bool<'st>> for STerm<'st> {
64    fn from(b: Bool<'st>) -> Self {
65        b.0
66    }
67}
68impl<'st> From<STerm<'st>> for Bool<'st> {
69    fn from(t: STerm<'st>) -> Self {
70        Bool(t)
71    }
72}
73impl<'st> From<(STerm<'st>, Sort<'st>)> for Bool<'st> {
74    fn from((t, _): (STerm<'st>, Sort<'st>)) -> Self {
75        t.into()
76    }
77}
78impl<'st> StaticSorted<'st> for Bool<'st> {
79    type Inner = Self;
80    const AST_SORT: ast::Sort<'static> = ast::Sort::new_simple("Bool");
81    fn static_st(&self) -> &'st Storage {
82        self.sterm().st()
83    }
84}
85impl<'st> Bool<'st> {
86    /// Returns the sort of bools.
87    pub fn sort() -> Sort<'st> {
88        Self::AST_SORT.into()
89    }
90    fn binop(self, op: &'st str, other: Bool<'st>) -> Self {
91        app(self.st(), op, (self.term(), other.term())).into()
92    }
93    /// Construct the term expressing `(==> self other)`.
94    ///
95    /// The value of the returned boolean is true if:
96    /// - `self` is false
97    /// - or `other` is true
98    pub fn implies(self, other: Bool<'st>) -> Bool<'st> {
99        self.binop("=>", other)
100    }
101    /// Construct the term expressing `(ite self then otherwise)`.
102    ///
103    /// This is similar to the [ternary condition
104    /// operator](https://en.wikipedia.org/wiki/Ternary_conditional_operator),
105    /// and an if statement:
106    /// - **C-style notation:** `self ? then : otherwise`
107    /// - **Rust notation:**  `if self { then } else { otherwise }`
108    pub fn ite<T: Sorted<'st> + From<(STerm<'st>, Sort<'st>)>>(self, then: T, otherwise: T) -> T {
109        let sort = then.sort();
110        let term = app(
111            self.st(),
112            "ite",
113            (self.term(), then.term(), otherwise.term()),
114        );
115        let dyn_term = Dynamic::from_term_sort(term, sort);
116        T::from_dynamic(dyn_term)
117    }
118}
119
120impl_op!(Bool<'st>, bool, BitAnd, bitand, "and", BitAndAssign, bitand_assign, &);
121impl_op!(Bool<'st>, bool, BitOr,  bitor,  "or", BitOrAssign,  bitor_assign,  |);
122impl_op!(Bool<'st>, bool, BitXor, bitxor, "xor",  BitXorAssign, bitxor_assign, ^);
123
124impl<'st> std::ops::Not for Bool<'st> {
125    type Output = Bool<'st>;
126
127    fn not(self) -> Self::Output {
128        app(self.st(), "not", self.term()).into()
129    }
130}
131
132/// Construct the term expressing `(and ...terms)` representing the conjunction
133/// of all of the terms. That is to say, the result is true iff all terms in
134/// `terms` is true.
135pub fn and<'st, const N: usize>(st: &'st Storage, terms: [Bool<'st>; N]) -> Bool<'st> {
136    app(st, "and", terms.map(Sorted::term)).into()
137}
138/// Construct the term expressing `(or ...terms)` representing the disjunction
139/// of all of the terms. That is to say, the result is true iff any of the terms
140/// in `terms` is true.
141pub fn or<'st, const N: usize>(st: &'st Storage, terms: [Bool<'st>; N]) -> Bool<'st> {
142    app(st, "or", terms.map(Sorted::term)).into()
143}
144/// Construct the term expressing `(xor ...terms)`.
145pub fn xor<'st, const N: usize>(st: &'st Storage, terms: [Bool<'st>; N]) -> Bool<'st> {
146    app(st, "xor", terms.map(Sorted::term)).into()
147}
148
149/// Construct the term expressing `(equal terms)` representing that all of the
150/// terms in `terms` are equal.
151pub fn equal<'st, T, const N: usize>(st: &'st Storage, terms: [T; N]) -> Bool<'st>
152where
153    T: Into<STerm<'st>>,
154{
155    app(st, "=", terms.map(Into::into).map(STerm::term)).into()
156}
157/// Construct the term expressing `(distinct terms)` representing that all of
158/// the terms in `terms` are distinct (or not-equal).
159pub fn distinct<'st, T, const N: usize>(st: &'st Storage, terms: [T; N]) -> Bool<'st>
160where
161    T: Into<STerm<'st>>,
162{
163    app(st, "distinct", terms.map(Into::into).map(STerm::term)).into()
164}
smtlib/theories/core.rs

smtlib/theories/
core.rs
