smtlib/theories/
ints.rs

1#![doc = concat!("```ignore\n", include_str!("./Ints.smt2"), "```")]
2
3use smtlib_lowlevel::{
4    ast::{self, Identifier, QualIdentifier, SpecConstant, Term},
5    lexicon::{Numeral, Symbol},
6    Storage,
7};
8
9use crate::{
10    impl_op,
11    sorts::Sort,
12    terms::{app, Const, Dynamic, IntoWithStorage, STerm, Sorted, StaticSorted},
13    Bool,
14};
15
16/// A [`Int`] is a term containing a
17/// [integer](https://en.wikipedia.org/wiki/Integer). You can [read more
18/// here.](https://smtlib.cs.uiowa.edu/theories-Ints.shtml).
19#[derive(Debug, Clone, Copy)]
20pub struct Int<'st>(STerm<'st>);
21impl<'st> From<Const<'st, Int<'st>>> for Int<'st> {
22    fn from(c: Const<'st, Int<'st>>) -> Self {
23        c.1
24    }
25}
26impl<'st> IntoWithStorage<'st, Int<'st>> for Const<'st, Int<'st>> {
27    fn into_with_storage(self, _st: &'st Storage) -> Int<'st> {
28        self.1
29    }
30}
31impl std::fmt::Display for Int<'_> {
32    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
33        STerm::from(*self).term().fmt(f)
34    }
35}
36
37impl<'st> From<Int<'st>> for Dynamic<'st> {
38    fn from(i: Int<'st>) -> Self {
39        i.into_dynamic()
40    }
41}
42
43impl<'st> From<Int<'st>> for STerm<'st> {
44    fn from(i: Int<'st>) -> Self {
45        i.0
46    }
47}
48impl<'st> From<STerm<'st>> for Int<'st> {
49    fn from(t: STerm<'st>) -> Self {
50        Int(t)
51    }
52}
53impl<'st> From<(STerm<'st>, Sort<'st>)> for Int<'st> {
54    fn from((t, _): (STerm<'st>, Sort<'st>)) -> Self {
55        t.into()
56    }
57}
58impl<'st> StaticSorted<'st> for Int<'st> {
59    type Inner = Self;
60    const AST_SORT: ast::Sort<'static> = ast::Sort::new_simple("Int");
61
62    fn static_st(&self) -> &'st Storage {
63        self.0.st()
64    }
65}
66impl<'st> IntoWithStorage<'st, Int<'st>> for i128 {
67    fn into_with_storage(self, st: &'st Storage) -> Int<'st> {
68        let term = if self < 0 {
69            app(
70                st,
71                "-",
72                Term::SpecConstant(SpecConstant::Numeral(Numeral::from_u128(
73                    self.unsigned_abs() as _,
74                ))),
75            )
76        } else {
77            STerm::new(
78                st,
79                Term::SpecConstant(SpecConstant::Numeral(Numeral::from_u128(self as _))),
80            )
81        };
82        term.into()
83    }
84}
85/// Error returned when trying to convert an [`Int`] to a primitive type.
86#[derive(Debug, thiserror::Error, PartialEq, Eq, PartialOrd, Ord)]
87pub enum TryFromError {
88    #[error("numeral was a string. this happens when the numeral is too large to fit into u128")]
89    /// The numeral is too large to fit into a u128.
90    NumeralWasString,
91    #[error("out of range {}", if *neg { format!("-{abs}") } else { abs.to_string() })]
92    /// Too large to fit into the target type.
93    OutOfRange {
94        /// The number is negative.
95        neg: bool,
96        /// The absolute value of the number.
97        abs: u128,
98    },
99    #[error("numeral was not a spec constant or a negation of a numeral")]
100    /// The term was not a numeral or a negation of a numeral.
101    NotANumeral,
102}
103impl<'st> TryFrom<Int<'st>> for i128 {
104    type Error = TryFromError;
105    fn try_from(i: Int<'st>) -> Result<Self, Self::Error> {
106        match i.term() {
107            Term::SpecConstant(SpecConstant::Numeral(c)) => {
108                let n = c.into_u128().map_err(|_| TryFromError::NumeralWasString)?;
109                n.try_into()
110                    .map_err(|_| TryFromError::OutOfRange { abs: n, neg: false })
111            }
112            Term::Application(
113                QualIdentifier::Identifier(Identifier::Simple(Symbol("-"))),
114                [Term::SpecConstant(SpecConstant::Numeral(c))],
115            ) => {
116                let n = c.into_u128().map_err(|_| TryFromError::NumeralWasString)?;
117                if n == i128::MIN as u128 {
118                    // This is a special case, as i128::MIN cannot be
119                    // represented as a positive i128.
120                    return Ok(i128::MIN);
121                }
122                n.try_into()
123                    .map_err(|_| TryFromError::OutOfRange { abs: n, neg: true })
124                    .map(|n: i128| -n)
125            }
126            _ => Err(TryFromError::NotANumeral),
127        }
128    }
129}
130impl<'st> IntoWithStorage<'st, Int<'st>> for u128 {
131    fn into_with_storage(self, st: &'st Storage) -> Int<'st> {
132        STerm::new(
133            st,
134            Term::SpecConstant(SpecConstant::Numeral(Numeral::from_u128(self as _))),
135        )
136        .into()
137    }
138}
139impl<'st> TryFrom<Int<'st>> for u128 {
140    type Error = TryFromError;
141    fn try_from(i: Int<'st>) -> Result<Self, Self::Error> {
142        match i.term() {
143            Term::SpecConstant(SpecConstant::Numeral(c)) => {
144                c.into_u128().map_err(|_| TryFromError::NumeralWasString)
145            }
146            _ => Err(TryFromError::NotANumeral),
147        }
148    }
149}
150macro_rules! impl_int_conv {
151    (from $s:ty, into $t:ty) => {
152        impl<'st> IntoWithStorage<'st, Int<'st>> for $t {
153            fn into_with_storage(self, st: &'st Storage) -> Int<'st> {
154                IntoWithStorage::into_with_storage(self as $s, st)
155            }
156        }
157        impl<'st> TryFrom<Int<'st>> for $t {
158            type Error = TryFromError;
159            fn try_from(i: Int<'st>) -> Result<Self, Self::Error> {
160                let n = <$s>::try_from(i)?;
161                n.try_into().map_err(|_| TryFromError::OutOfRange {
162                    abs: n as u128,
163                    #[allow(unused_comparisons)]
164                    neg: n < 0,
165                })
166            }
167        }
168    };
169}
170impl_int_conv!(from i128, into i8);
171impl_int_conv!(from i128, into i16);
172impl_int_conv!(from i128, into i32);
173impl_int_conv!(from i128, into i64);
174impl_int_conv!(from i128, into isize);
175impl_int_conv!(from u128, into u8);
176impl_int_conv!(from u128, into u16);
177impl_int_conv!(from u128, into u32);
178impl_int_conv!(from u128, into u64);
179impl_int_conv!(from u128, into usize);
180
181impl<'st> Int<'st> {
182    /// Returns the sort of ints.
183    pub fn sort() -> Sort<'st> {
184        Self::AST_SORT.into()
185    }
186    /// Construct a new integer.
187    pub fn new(st: &'st Storage, value: impl IntoWithStorage<'st, Int<'st>>) -> Int<'st> {
188        value.into_with_storage(st)
189    }
190    fn binop<T: From<STerm<'st>>>(self, op: &'st str, other: Int<'st>) -> T {
191        app(self.static_st(), op, (self.term(), other.term())).into()
192    }
193    /// Construct the term expressing `(> self other)`
194    pub fn gt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
195        self.binop(">", other.into_with_storage(self.st()))
196    }
197    /// Construct the term expressing `(>= self other)`
198    pub fn ge(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
199        self.binop(">=", other.into_with_storage(self.st()))
200    }
201    /// Construct the term expressing `(< self other)`
202    pub fn lt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
203        self.binop("<", other.into_with_storage(self.st()))
204    }
205    /// Construct the term expressing `(<= self other)`
206    pub fn le(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
207        self.binop("<=", other.into_with_storage(self.st()))
208    }
209    // TODO: This seems to not be supported by z3?
210    /// Construct the term expressing `(abs self)`
211    pub fn abs(self) -> Int<'st> {
212        app(self.st(), "abs", self.term()).into()
213    }
214}
215
216impl std::ops::Neg for Int<'_> {
217    type Output = Self;
218    fn neg(self) -> Self::Output {
219        app(self.st(), "-", self.term()).into()
220    }
221}
222
223impl_op!(Int<'st>, i64, Add, add, "+", AddAssign, add_assign, +);
224impl_op!(Int<'st>, i64, Sub, sub, "-", SubAssign, sub_assign, -);
225impl_op!(Int<'st>, i64, Mul, mul, "*", MulAssign, mul_assign, *);
226impl_op!(Int<'st>, i64, Div, div, "div", DivAssign, div_assign, /);
227impl_op!(Int<'st>, i64, Rem, rem, "rem", RemAssign, rem_assign, %);
228impl_op!(Int<'st>, i64, Shl, shl, "hsl", ShlAssign, shl_assign, <<);
229impl_op!(Int<'st>, i64, Shr, shr, "hsr", ShrAssign, shr_assign, >>);
smtlib/theories/ints.rs

smtlib/theories/
ints.rs
