Expose underlying Z3_context and Z3_sort (#298)

Closes #290
prove-rs · May 29, 2024 · 1252af7 · 1252af7
1 parent d134bb3
commit 1252af7
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/z3/src/context.rs b/z3/src/context.rs
@@ -17,6 +17,10 @@ impl Context {
         }
     }
 
+    pub fn get_z3_context(&self) -> Z3_context {
+        self.z3_ctx
+    }
+
     /// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
     pub fn interrupt(&self) {
         self.handle().interrupt();

diff --git a/z3/src/sort.rs b/z3/src/sort.rs
@@ -12,6 +12,10 @@ impl<'ctx> Sort<'ctx> {
         Sort { ctx, z3_sort }
     }
 
+    pub fn get_z3_sort(&self) -> Z3_sort {
+        self.z3_sort
+    }
+
     pub fn uninterpreted(ctx: &'ctx Context, name: Symbol) -> Sort<'ctx> {
         unsafe {
             Self::wrap(