smtlib/theories/
ints.rs

1#![doc = concat!("```ignore\n", include_str!("./Ints.smt2"), "```")]
2
3use smtlib_lowlevel::{
4    ast::{self, SpecConstant, Term},
5    lexicon::Numeral,
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 i64 {
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_usize(
73                    self.unsigned_abs() as _,
74                ))),
75            )
76        } else {
77            STerm::new(
78                st,
79                Term::SpecConstant(SpecConstant::Numeral(Numeral::from_usize(self as _))),
80            )
81        };
82        term.into()
83    }
84}
85impl<'st> Int<'st> {
86    /// Returns the sort of ints.
87    pub fn sort() -> Sort<'st> {
88        Self::AST_SORT.into()
89    }
90    /// Construct a new integer.
91    pub fn new(st: &'st Storage, value: impl IntoWithStorage<'st, Int<'st>>) -> Int<'st> {
92        value.into_with_storage(st)
93    }
94    fn binop<T: From<STerm<'st>>>(self, op: &'st str, other: Int<'st>) -> T {
95        app(self.static_st(), op, (self.term(), other.term())).into()
96    }
97    /// Construct the term expressing `(> self other)`
98    pub fn gt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
99        self.binop(">", other.into_with_storage(self.st()))
100    }
101    /// Construct the term expressing `(>= self other)`
102    pub fn ge(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
103        self.binop(">=", other.into_with_storage(self.st()))
104    }
105    /// Construct the term expressing `(< self other)`
106    pub fn lt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
107        self.binop("<", other.into_with_storage(self.st()))
108    }
109    /// Construct the term expressing `(<= self other)`
110    pub fn le(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
111        self.binop("<=", other.into_with_storage(self.st()))
112    }
113    // TODO: This seems to not be supported by z3?
114    /// Construct the term expressing `(abs self)`
115    pub fn abs(self) -> Int<'st> {
116        app(self.st(), "abs", self.term()).into()
117    }
118}
119
120impl std::ops::Neg for Int<'_> {
121    type Output = Self;
122    fn neg(self) -> Self::Output {
123        app(self.st(), "-", self.term()).into()
124    }
125}
126
127impl_op!(Int<'st>, i64, Add, add, "+", AddAssign, add_assign, +);
128impl_op!(Int<'st>, i64, Sub, sub, "-", SubAssign, sub_assign, -);
129impl_op!(Int<'st>, i64, Mul, mul, "*", MulAssign, mul_assign, *);
130impl_op!(Int<'st>, i64, Div, div, "div", DivAssign, div_assign, /);
131impl_op!(Int<'st>, i64, Rem, rem, "rem", RemAssign, rem_assign, %);
132impl_op!(Int<'st>, i64, Shl, shl, "hsl", ShlAssign, shl_assign, <<);
133impl_op!(Int<'st>, i64, Shr, shr, "hsr", ShrAssign, shr_assign, >>);
smtlib/theories/ints.rs

smtlib/theories/
ints.rs
