z3/ast/
dynamic.rs

1use crate::ast::{Array, Ast, BV, Bool, Datatype, Float, Int, Real, Seq, Set};
2use crate::{Context, Sort, Symbol, ast};
3use std::ffi::CString;
4use z3_sys::*;
5
6/// A dynamically typed [`Ast`] node.
7pub struct Dynamic {
8    pub(crate) ctx: Context,
9    pub(crate) z3_ast: Z3_ast,
10}
11
12impl Dynamic {
13    pub fn from_ast(ast: &dyn Ast) -> Self {
14        unsafe { Self::wrap(ast.get_ctx(), ast.get_z3_ast()) }
15    }
16
17    pub fn new_const<S: Into<Symbol>>(name: S, sort: &Sort) -> Self {
18        let ctx = &Context::thread_local();
19        unsafe {
20            Self::wrap(
21                ctx,
22                Z3_mk_const(ctx.z3_ctx.0, name.into().as_z3_symbol(), sort.z3_sort).unwrap(),
23            )
24        }
25    }
26
27    pub fn fresh_const(prefix: &str, sort: &Sort) -> Self {
28        let ctx = sort.ctx.clone();
29        unsafe {
30            Self::wrap(&ctx, {
31                let pp = CString::new(prefix).unwrap();
32                let p = pp.as_ptr();
33                Z3_mk_fresh_const(ctx.z3_ctx.0, p, sort.z3_sort).unwrap()
34            })
35        }
36    }
37
38    pub fn sort_kind(&self) -> SortKind {
39        unsafe {
40            Z3_get_sort_kind(
41                self.ctx.z3_ctx.0,
42                Z3_get_sort(self.ctx.z3_ctx.0, self.z3_ast).unwrap(),
43            )
44        }
45    }
46
47    /// Returns `None` if the `Dynamic` is not actually a `Bool`
48    pub fn as_bool(&self) -> Option<Bool> {
49        match self.sort_kind() {
50            SortKind::Bool => Some(unsafe { Bool::wrap(&self.ctx, self.z3_ast) }),
51            _ => None,
52        }
53    }
54
55    /// Returns `None` if the `Dynamic` is not actually an `Int`
56    pub fn as_int(&self) -> Option<Int> {
57        match self.sort_kind() {
58            SortKind::Int => Some(unsafe { Int::wrap(&self.ctx, self.z3_ast) }),
59            _ => None,
60        }
61    }
62
63    /// Returns `None` if the `Dynamic` is not actually a `Real`
64    pub fn as_real(&self) -> Option<Real> {
65        match self.sort_kind() {
66            SortKind::Real => Some(unsafe { Real::wrap(&self.ctx, self.z3_ast) }),
67            _ => None,
68        }
69    }
70
71    /// Returns `None` if the `Dynamic` is not actually a `Float`
72    pub fn as_float(&self) -> Option<Float> {
73        match self.sort_kind() {
74            SortKind::FloatingPoint => Some(unsafe { Float::wrap(&self.ctx, self.z3_ast) }),
75            _ => None,
76        }
77    }
78
79    /// Returns `None` if the `Dynamic` is not actually a `String`
80    pub fn as_string(&self) -> Option<ast::String> {
81        unsafe {
82            if Z3_is_string_sort(
83                self.ctx.z3_ctx.0,
84                Z3_get_sort(self.ctx.z3_ctx.0, self.z3_ast)?,
85            ) {
86                Some(ast::String::wrap(&self.ctx, self.z3_ast))
87            } else {
88                None
89            }
90        }
91    }
92
93    /// Returns `None` if the `Dynamic` is not actually a `BV`
94    pub fn as_bv(&self) -> Option<BV> {
95        match self.sort_kind() {
96            SortKind::BV => Some(unsafe { BV::wrap(&self.ctx, self.z3_ast) }),
97            _ => None,
98        }
99    }
100
101    /// Returns `None` if the `Dynamic` is not actually an `Array`
102    pub fn as_array(&self) -> Option<Array> {
103        match self.sort_kind() {
104            SortKind::Array => Some(unsafe { Array::wrap(&self.ctx, self.z3_ast) }),
105            _ => None,
106        }
107    }
108
109    /// Returns `None` if the `Dynamic` is not actually a `Set`
110    pub fn as_set(&self) -> Option<Set> {
111        unsafe {
112            match self.sort_kind() {
113                SortKind::Array => {
114                    match Z3_get_sort_kind(
115                        self.ctx.z3_ctx.0,
116                        Z3_get_array_sort_range(
117                            self.ctx.z3_ctx.0,
118                            Z3_get_sort(self.ctx.z3_ctx.0, self.z3_ast)?,
119                        )?,
120                    ) {
121                        SortKind::Bool => Some(Set::wrap(&self.ctx, self.z3_ast)),
122                        _ => None,
123                    }
124                }
125                _ => None,
126            }
127        }
128    }
129
130    /// Returns `None` if the `Dynamic` is not actually a `Seq`.
131    pub fn as_seq(&self) -> Option<Seq> {
132        match self.sort_kind() {
133            SortKind::Seq => Some(unsafe { Seq::wrap(&self.ctx, self.z3_ast) }),
134            _ => None,
135        }
136    }
137
138    /// Returns `None` if the `Dynamic` is not actually a `Datatype`
139    pub fn as_datatype(&self) -> Option<Datatype> {
140        match self.sort_kind() {
141            SortKind::Datatype => Some(unsafe { Datatype::wrap(&self.ctx, self.z3_ast) }),
142            _ => None,
143        }
144    }
145}
z3/ast/dynamic.rs

z3/ast/
dynamic.rs
