smtlib/theories/
reals.rs

1#![doc = concat!("```ignore\n", include_str!("./Reals.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    Bool,
13};
14
15/// A [`Real`] is a term containing a
16/// [real](https://en.wikipedia.org/wiki/Real_number). You can [read more
17/// here.](https://smtlib.cs.uiowa.edu/theories-Reals.shtml).
18#[derive(Debug, Clone, Copy)]
19pub struct Real<'st>(STerm<'st>);
20impl<'st> From<Const<'st, Real<'st>>> for Real<'st> {
21    fn from(c: Const<'st, Real<'st>>) -> Self {
22        c.1
23    }
24}
25impl<'st> IntoWithStorage<'st, Real<'st>> for Const<'st, Real<'st>> {
26    fn into_with_storage(self, _st: &'st Storage) -> Real<'st> {
27        self.1
28    }
29}
30impl std::fmt::Display for Real<'_> {
31    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
32        self.term().fmt(f)
33    }
34}
35
36impl<'st> From<Real<'st>> for Dynamic<'st> {
37    fn from(i: Real<'st>) -> Self {
38        i.into_dynamic()
39    }
40}
41
42impl<'st> From<Real<'st>> for STerm<'st> {
43    fn from(i: Real<'st>) -> Self {
44        i.0
45    }
46}
47impl<'st> From<STerm<'st>> for Real<'st> {
48    fn from(t: STerm<'st>) -> Self {
49        Real(t)
50    }
51}
52impl<'st> From<(STerm<'st>, Sort<'st>)> for Real<'st> {
53    fn from((t, _): (STerm<'st>, Sort<'st>)) -> Self {
54        t.into()
55    }
56}
57impl<'st> StaticSorted<'st> for Real<'st> {
58    type Inner = Self;
59    const AST_SORT: ast::Sort<'static> = ast::Sort::new_simple("Real");
60    fn static_st(&self) -> &'st Storage {
61        self.0.st()
62    }
63}
64impl<'st> IntoWithStorage<'st, Real<'st>> for i64 {
65    fn into_with_storage(self, st: &'st Storage) -> Real<'st> {
66        (self as f64).into_with_storage(st)
67    }
68}
69impl<'st> IntoWithStorage<'st, Real<'st>> for f64 {
70    fn into_with_storage(self, st: &'st Storage) -> Real<'st> {
71        let s = Term::Identifier(qual_ident(
72            st.alloc_str(&format!("{:.10}", self.abs())),
73            None,
74        ));
75        let term = if self.is_sign_negative() {
76            Term::Application(qual_ident("-", None), st.alloc_slice(&[st.alloc_term(s)]))
77        } else {
78            s
79        };
80        STerm::new(st, term).into()
81    }
82}
83
84#[cfg(feature = "decimal")]
85impl<'st> IntoWithStorage<'st, Real<'st>> for rust_decimal::Decimal {
86    fn into_with_storage(self, st: &'st Storage) -> Real<'st> {
87        // Make sure to format as Real
88        let mut s = self.abs().to_string();
89        if !s.contains(".") {
90            s += ".0";
91        }
92        let id = Term::Identifier(qual_ident(st.alloc_str(&s), None));
93        let term = if self.is_sign_negative() {
94            Term::Application(qual_ident("-", None), st.alloc_slice(&[st.alloc_term(id)]))
95        } else {
96            id
97        };
98        STerm::new(st, term).into()
99    }
100}
101
102impl<'st> Real<'st> {
103    /// Construct a new real.
104    pub fn new(st: &'st Storage, value: impl IntoWithStorage<'st, Real<'st>>) -> Real<'st> {
105        value.into_with_storage(st)
106    }
107
108    /// Returns the sort of reals.
109    pub fn sort() -> Sort<'st> {
110        Self::AST_SORT.into()
111    }
112    fn binop<T: From<STerm<'st>>>(self, op: &'st str, other: Real<'st>) -> T {
113        app(self.st(), op, (self.term(), other.term())).into()
114    }
115    /// Construct the term expressing `(> self other)`
116    pub fn gt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
117        self.binop(">", other.into_with_storage(self.st()))
118    }
119    /// Construct the term expressing `(>= self other)`
120    pub fn ge(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
121        self.binop(">=", other.into_with_storage(self.st()))
122    }
123    /// Construct the term expressing `(< self other)`
124    pub fn lt(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
125        self.binop("<", other.into_with_storage(self.st()))
126    }
127    /// Construct the term expressing `(<= self other)`
128    pub fn le(self, other: impl IntoWithStorage<'st, Self>) -> Bool<'st> {
129        self.binop("<=", other.into_with_storage(self.st()))
130    }
131    /// Construct the term expressing `(abs self)`
132    pub fn abs(self) -> Real<'st> {
133        app(self.st(), "abs", self.term()).into()
134    }
135    /// Construct the term expressing floor division of two terms
136    pub fn floor_div<R>(self, rhs: impl IntoWithStorage<'st, Self>) -> Self {
137        self.binop("div", rhs.into_with_storage(self.st()))
138    }
139}
140
141impl std::ops::Neg for Real<'_> {
142    type Output = Self;
143    fn neg(self) -> Self::Output {
144        app(self.st(), "-", self.term()).into()
145    }
146}
147
148impl_op!(Real<'st>, f64, Add, add, "+", AddAssign, add_assign, +);
149impl_op!(Real<'st>, f64, Sub, sub, "-", SubAssign, sub_assign, -);
150impl_op!(Real<'st>, f64, Mul, mul, "*", MulAssign, mul_assign, *);
151impl_op!(Real<'st>, f64, Div, div, "/", DivAssign, div_assign, /);
smtlib/theories/reals.rs

smtlib/theories/
reals.rs
