Skip to content

Commit

Permalink
add new_const and fresh_const functions to Dynamic
Browse files Browse the repository at this point in the history
  • Loading branch information
Philipp15b authored and waywardmonkeys committed Dec 18, 2023
1 parent ad6273f commit ab67534
Showing 1 changed file with 19 additions and 0 deletions.
19 changes: 19 additions & 0 deletions z3/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1647,6 +1647,25 @@ impl<'ctx> Dynamic<'ctx> {
unsafe { Self::wrap(ast.get_ctx(), ast.get_z3_ast()) }
}

pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sort: &Sort<'ctx>) -> Self {
unsafe {
Self::wrap(
ctx,
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort),
)
}
}

pub fn fresh_const(ctx: &'ctx Context, prefix: &str, sort: &Sort<'ctx>) -> Self {
unsafe {
Self::wrap(ctx, {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
}

pub fn sort_kind(&self) -> SortKind {
unsafe { Z3_get_sort_kind(self.ctx.z3_ctx, Z3_get_sort(self.ctx.z3_ctx, self.z3_ast)) }
}
Expand Down

0 comments on commit ab67534

Please sign in to comment.