From 7c0ec21af894597bf84598a16fa7c89098b3cac4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Jul 2022 12:21:25 -0700
Subject: [PATCH] try to add basic expression simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/js/src/high-level/high-level.ts | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index c4f315de9..897cd01f7 100644
--- 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 //
     /////////////