try to add basic expression simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 22, 2022 · 7c0ec21 · 7c0ec21
1 parent 4368ec9
commit 7c0ec21
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
@@ -498,6 +498,14 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return result;
     }
 
+    ///////////////////////////////
+    // expression simplification //
+    ///////////////////////////////
+
+    async function simplify(e : Expr<Name>) {
+       return _toExpr(check(Z3.simplify(contextPtr, e)));
+    }
+
     /////////////
     // Objects //
     /////////////