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> StaticSorted<'st> for Real<'st> {
53    type Inner = Self;
54    const AST_SORT: ast::Sort<'static> = ast::Sort::new_simple("Real");
55    fn static_st(&self) -> &'st Storage {
56        self.0.st()
57    }
58}
59impl<'st> IntoWithStorage<'st, Real<'st>> for i64 {
60    fn into_with_storage(self, st: &'st Storage) -> Real<'st> {
61        (self as f64).into_with_storage(st)
62    }
63}
64impl<'st> IntoWithStorage<'st, Real<'st>> for f64 {
65    fn into_with_storage(self, st: &'st Storage) -> Real<'st> {
66        let s = Term::Identifier(qual_ident(st.alloc_str(&format!("{:?}", self.abs())), None));
67        let term = if self.is_sign_negative() {
68            Term::Application(qual_ident("-", None), st.alloc_slice(&[st.alloc_term(s)]))
69        } else {
70            s
71        };
72        STerm::new(st, term).into()
73    }
74}
75impl<'st> Real<'st> {
76    /// Returns the sort of reals.
77    pub fn sort() -> Sort<'st> {
78        Self::AST_SORT.into()
79    }
80    fn binop<T: From<STerm<'st>>>(self, op: &'st str, other: Real<'st>) -> T {
81        app(self.st(), op, (self.term(), other.term())).into()
82    }
83    /// Construct the term expressing `(> self other)`
84    pub fn gt(self, other: impl Into<Self>) -> Bool<'st> {
85        self.binop(">", other.into())
86    }
87    /// Construct the term expressing `(>= self other)`
88    pub fn ge(self, other: impl Into<Self>) -> Bool<'st> {
89        self.binop(">=", other.into())
90    }
91    /// Construct the term expressing `(< self other)`
92    pub fn lt(self, other: impl Into<Self>) -> Bool<'st> {
93        self.binop("<", other.into())
94    }
95    /// Construct the term expressing `(<= self other)`
96    pub fn le(self, other: impl Into<Self>) -> Bool<'st> {
97        self.binop("<=", other.into())
98    }
99    /// Construct the term expressing `(abs self)`
100    pub fn abs(self) -> Real<'st> {
101        app(self.st(), "abs", self.term()).into()
102    }
103}
104
105impl std::ops::Neg for Real<'_> {
106    type Output = Self;
107    fn neg(self) -> Self::Output {
108        app(self.st(), "-", self.term()).into()
109    }
110}
111
112impl_op!(Real<'st>, f64, Add, add, "+", AddAssign, add_assign, +);
113impl_op!(Real<'st>, f64, Sub, sub, "-", SubAssign, sub_assign, -);
114impl_op!(Real<'st>, f64, Mul, mul, "*", MulAssign, mul_assign, *);
115impl_op!(Real<'st>, f64, Div, div, "div", DivAssign, div_assign, /);
smtlib/theories/reals.rs

smtlib/theories/
reals.rs
