Skip to content

Commit

Permalink
Allow creating constants in Dynamic.
Browse files Browse the repository at this point in the history
  • Loading branch information
wsx-ucb committed May 1, 2023
1 parent 5c0c18f commit f9766a7
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 @@ -1673,6 +1673,25 @@ impl<'ctx> Dynamic<'ctx> {
_ => None,
}
}

pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sort: &Sort<'ctx>) -> Self {
assert_eq!(ctx, sort.ctx);

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 {
assert_eq!(ctx, sort.ctx);

let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
unsafe { Self::wrap(ctx, Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)) }
}
}

impl<'ctx> Datatype<'ctx> {
Expand Down

0 comments on commit f9766a7

Please sign in to comment.