[WIP] More TS Binding Features (Z3Prover#6412)

* feat: basic quantfier support

* feat: added isQuantifier

* feat: expanded functions

* wip: (lambda broken)

* temp fix to LambdaImpl typing issue

* feat: function type inference

* formatting with prettier

* fix: imported from invalid module

* fix isBool bug and dumping to smtlib

* substitution and model.updateValue

* api to add custom func interps to model

* fix: building

* properly handling uint32 -> number conversion in z3 TS wrapper

* added simplify

* remame Add->Sum and Mul->Product

* formatting

Author: walnutwaldo

src/api/js/examples/high-level/using_smtlib2.ts

@@ -0,0 +1,36 @@
+// @ts-ignore we're not going to bother with types for this
+import process from 'process';
+import { init } from '../../build/node';
+import assert from 'assert';
+
+(async () => {
+  let { Context, em } = await init();
+  let z3 = Context('main');
+
+  const x = z3.BitVec.const('x', 256);
+  const y = z3.BitVec.const('y', 256);
+  const z = z3.BitVec.const('z', 256);
+  const xPlusY = x.add(y);
+  const xPlusZ = x.add(z);
+  const expr = xPlusY.mul(xPlusZ);
+
+  const to_check = expr.eq(z3.Const('test', expr.sort));
+
+  const solver = new z3.Solver();
+  solver.add(to_check);
+  const cr = await solver.check();
+  console.log(cr);
+  assert(cr === 'sat');
+
+  const model = solver.model();
+  let modelStr = model.sexpr();
+  modelStr = modelStr.replace(/\n/g, ' ');
+  console.log("Model: ", modelStr);
+
+  const exprs = z3.ast_from_string(modelStr);
+  console.log(exprs);
+
+})().catch(e => {
+  console.error('error', e);
+  process.exit(1);
+});

src/api/js/examples/low-level/example-raw.ts

@@ -1,3 +1,4 @@
+// @ts-ignore we're not going to bother with types for this
 import process from 'process';
 import { init, Z3_error_code } from '../../build/node';
 

src/api/js/package-lock.json

@@ -1,5 +1,6 @@
 {
   "name": "z3-solver",
+  "version": "0.1.0",
   "keywords": [
     "Z3",
     "theorem",
@@ -26,8 +27,8 @@
     "build:ts:generate": "ts-node --transpileOnly scripts/make-ts-wrapper.ts src/low-level/wrapper.__GENERATED__.ts src/low-level/types.__GENERATED__.ts",
     "build:wasm": "ts-node --transpileOnly ./scripts/build-wasm.ts",
     "clean": "rimraf build 'src/**/*.__GENERATED__.*'",
-    "lint": "prettier -c '{,src/,scripts/,examples}*.{js,ts}'",
-    "format": "prettier --write '{,src/,scripts/}*.{js,ts}'",
+    "lint": "prettier -c '{./,src/,scripts/,examples/}**/*.{js,ts}'",
+    "format": "prettier --write '{./,src/,scripts/}**/*.{js,ts}'",
     "test": "jest",
     "docs": "typedoc",
     "check-engine": "check-engine"
@@ -53,8 +54,8 @@
     "ts-expect": "^1.3.0",
     "ts-jest": "^28.0.3",
     "ts-node": "^10.8.0",
-    "typedoc": "^0.22.17",
-    "typescript": "^4.5.4"
+    "typedoc": "^0.23.16",
+    "typescript": "^4.8.4"
   },
   "license": "MIT",
   "dependencies": {

src/api/js/package.json

@@ -76,6 +76,7 @@ function makeTsWrapper() {
   }
 
   const isInParam = (p: FuncParam) => p.kind !== undefined && ['in', 'in_array'].includes(p.kind);
+
   function wrapFunction(fn: Func) {
     if (CUSTOM_IMPLEMENTATIONS.includes(fn.name)) {
       return null;
@@ -104,7 +105,7 @@ function makeTsWrapper() {
 
     let isAsync = asyncFuncs.includes(fn.name);
     let trivial =
-      !['string', 'boolean'].includes(fn.ret) &&
+      !['string', 'boolean', 'unsigned'].includes(fn.ret) &&
       !fn.nullableRet &&
       outParams.length === 0 &&
       !inParams.some(p => p.type === 'string' || p.isArray || p.nullable);
@@ -234,6 +235,7 @@ function makeTsWrapper() {
           function setArg() {
             args[outParam.idx] = memIdx === 0 ? 'outAddress' : `outAddress + ${memIdx * 4}`;
           }
+
           let read, type;
           if (outParam.type === 'string') {
             read = `Mod.UTF8ToString(getOutUint(${memIdx}))`;
@@ -330,11 +332,15 @@ function makeTsWrapper() {
       if (ret === 0) {
         return null;
       }
-    `.trim();
+      `.trim();
+    } else if (fn.ret === 'unsigned') {
+      infix += `
+      ret = (new Uint32Array([ret]))[0];
+      `.trim();
     }
 
     // prettier-ignore
-    let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`;
+    let invocation = `Mod.ccall('${isAsync ? "async_" : ""}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(", ")}])`;
 
     if (isAsync) {
       invocation = `await Mod.async_call(() => ${invocation})`;

src/api/js/scripts/make-ts-wrapper.ts

@@ -45,7 +45,7 @@ const types = {
   __proto__: null,
 
   // these are function types I can't be bothered to parse
-  // NSB: They can be extracted automatically from z3_api.h thanks to the use 
+  // NSB: They can be extracted automatically from z3_api.h thanks to the use
   // of a macro.
   Z3_error_handler: 'Z3_error_handler',
   Z3_push_eh: 'Z3_push_eh',