Add a binding for Z3_simplify()

BackdoorRE · Jul 2, 2019 · bea28c9 · bea28c9
1 parent a8f4f4c
commit bea28c9
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/z3/src/ast.rs b/z3/src/ast.rs
@@ -160,6 +160,15 @@ pub trait Ast<'ctx>: Sized {
             Z3_get_sort(self.get_ctx().z3_ctx, self.get_z3_ast())
         })
     }
+
+    /// Simplify the `Ast`. Returns a new `Ast` which is equivalent,
+    /// but simplified using algebraic simplification rules, such as
+    /// constant propagation.
+    fn simplify(&self) -> Self {
+        Self::new(self.get_ctx(), unsafe {
+            Z3_simplify(self.get_ctx().z3_ctx, self.get_z3_ast())
+        })
+    }
 }
 
 macro_rules! impl_ast {