Add high level bindings for js

.github/workflows/wasm-release.yml

@@ -23,8 +23,8 @@ jobs:
       - name: Setup node
         uses: actions/setup-node@v2
         with:
-          node-version: 'lts/*'
-          registry-url: 'https://registry.npmjs.org'
+          node-version: "lts/*"
+          registry-url: "https://registry.npmjs.org"
 
       - name: Prepare for publish
         run: |
@@ -37,13 +37,13 @@ jobs:
         with:
           no-install: true
           version: ${{env.EM_VERSION}}
-          actions-cache-folder: 'emsdk-cache'
+          actions-cache-folder: "emsdk-cache"
 
       - name: Install dependencies
         run: npm ci
 
       - name: Build TypeScript
-        run: npm run build-ts
+        run: npm run build:ts
 
       - name: Build wasm
         run: |
@@ -52,7 +52,7 @@ jobs:
           source $(dirname $(which emsdk))/emsdk_env.sh
           which node
           which clang++
-          npm run build-wasm
+          npm run build:wasm
 
       - name: Test
         run: npm test

.github/workflows/wasm.yml

@@ -2,7 +2,7 @@ name: WebAssembly Build
 
 on:
   push:
-    branches: [ master ]
+    branches: [master]
   pull_request:
 
 defaults:
@@ -23,20 +23,20 @@ jobs:
       - name: Setup node
         uses: actions/setup-node@v2
         with:
-          node-version: 'lts/*'
+          node-version: "lts/*"
 
       - name: Setup emscripten
         uses: mymindstorm/setup-emsdk@v11
         with:
           no-install: true
           version: ${{env.EM_VERSION}}
-          actions-cache-folder: 'emsdk-cache'
+          actions-cache-folder: "emsdk-cache"
 
       - name: Install dependencies
         run: npm ci
 
       - name: Build TypeScript
-        run: npm run build-ts
+        run: npm run build:ts
 
       - name: Build wasm
         run: |
@@ -45,7 +45,7 @@ jobs:
           source $(dirname $(which emsdk))/emsdk_env.sh
           which node
           which clang++
-          npm run build-wasm
+          npm run build:wasm
 
       - name: Test
         run: npm test

.gitignore

@@ -66,6 +66,7 @@ src/api/python/z3/z3consts.py
 src/api/python/z3/z3core.py
 src/ast/pattern/database.h
 src/util/version.h
+src/util/z3_version.h
 src/api/java/Native.cpp
 src/api/java/Native.java
 src/api/java/enumerations/*.java
@@ -76,11 +77,8 @@ src/api/ml/z3native.mli
 src/api/ml/z3enums.mli
 src/api/ml/z3.mllib
 src/api/js/node_modules/
-src/api/js/*.js
 src/api/js/build/
-src/api/js/**/*.d.ts
-!src/api/js/scripts/*.js
-!src/api/js/src/*.js
+src/api/js/**/*.__GENERATED__.*
 debug/*
 
 out/**

scripts/mk_util.py

@@ -246,10 +246,13 @@ def rmf(fname):
 
 def exec_compiler_cmd(cmd):
     r = exec_cmd(cmd)
-    if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
-        rmf('a.exe')
-    else:
-        rmf('a.out')
+    # Windows
+    rmf('a.exe')
+    # Unix
+    rmf('a.out')
+    # Emscripten
+    rmf('a.wasm')
+    rmf('a.worker.js')
     return r
 
 def test_cxx_compiler(cc):
@@ -293,6 +296,10 @@ def test_fpmath(cc):
     t.commit()
     # -Werror is needed because some versions of clang warn about unrecognized
     # -m flags.
+    # TODO(ritave): Safari doesn't allow SIMD WebAssembly extension, add a flag to build script
+    if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2 -msimd128']) == 0:
+        FPMATH_FLAGS='-msse -msse2 -msimd128'
+        return 'SSE2-EMSCRIPTEN'
     if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
         FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
         return "SSE2-GCC"
@@ -499,7 +506,7 @@ def find_ml_lib():
 
 def is64():
     global LINUX_X64
-    if is_sunos() and sys.version_info.major < 3: 
+    if is_sunos() and sys.version_info.major < 3:
         return LINUX_X64
     else:
         return LINUX_X64 and sys.maxsize >= 2**32
@@ -625,11 +632,11 @@ def check_eol():
         else:
             LINUX_X64=False
 
-            
+
 if os.name == 'posix' and os.uname()[4] == 'arm64':
     IS_ARCH_ARM64 = True
 
-            
+
 def display_help(exit_code):
     print("mk_make.py: Z3 Makefile generator\n")
     print("This script generates the Makefile for the Z3 theorem prover.")
@@ -792,7 +799,7 @@ def extract_c_includes(fname):
     linenum = 1
     for line in f:
         m1 = std_inc_pat.match(line)
-        if m1: 
+        if m1:
             root_file_name = m1.group(1)
             slash_pos =  root_file_name.rfind('/')
             if slash_pos >= 0  and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src"
@@ -1650,7 +1657,7 @@ def set_key_file(self):
        else:
            print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
            self.key_file = None
-    
+
 
 # build for dotnet core
 class DotNetDLLComponent(Component):
@@ -1664,7 +1671,7 @@ def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_fi
         self.assembly_info_dir = assembly_info_dir
         self.key_file = default_key_file
 
-    
+
     def mk_makefile(self, out):
         if not is_dotnet_core_enabled():
             return
@@ -1680,7 +1687,7 @@ def mk_makefile(self, out):
             out.write(' ')
             out.write(cs_file)
         out.write('\n')
-        
+
         set_key_file(self)
         key = ""
         if not self.key_file is None:
@@ -1724,7 +1731,7 @@ def mk_makefile(self, out):
             ous.write(core_csproj_str)
 
         dotnetCmdLine = [DOTNET, "build", csproj]
-        
+
         dotnetCmdLine.extend(['-c'])
         if DEBUG_MODE:
             dotnetCmdLine.extend(['Debug'])
@@ -1733,19 +1740,19 @@ def mk_makefile(self, out):
 
         path = os.path.join(os.path.abspath(BUILD_DIR), ".")
         dotnetCmdLine.extend(['-o', "\"%s\"" % path])
-            
+
         MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
-        out.write('\n')        
+        out.write('\n')
         out.write('%s: %s\n\n' % (self.name, dllfile))
 
     def main_component(self):
         return is_dotnet_core_enabled()
-    
+
     def has_assembly_info(self):
         # TBD: is this required for dotnet core given that version numbers are in z3.csproj file?
         return False
 
-    
+
     def mk_win_dist(self, build_path, dist_path):
         if is_dotnet_core_enabled():
             mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
@@ -2038,7 +2045,7 @@ def mk_makefile(self, out):
             out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
             if IS_OSX:
                 out.write('\tinstall_name_tool -id %s/libz3.dylib libz3.dylib\n' % (stubs_install_path))
-                out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path))                
+                out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path))
             out.write('\n')
 
             if IS_WINDOWS:
@@ -3117,7 +3124,7 @@ def get_platform_toolset_str():
     if len(tokens) < 2:
         return default
     else:
-        if tokens[0] == "15": 
+        if tokens[0] == "15":
             # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
             return "v141"
         else:

src/api/js/.nvmrc

@@ -0,0 +1 @@
+v16.15.0

src/api/js/.prettierrc.json

@@ -0,0 +1,6 @@
+{
+  "singleQuote": true,
+  "arrowParens": "avoid",
+  "printWidth": 120,
+  "trailingComma": "all"
+}

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

@@ -1,4 +1,5 @@
-import { init, Z3_error_code } from './build/node-wrapper';
+import process from 'process';
+import { init, Z3_error_code } from '../../build/node';
 
 // demonstrates use of the raw API
 

src/api/js/test-ts-api.ts → src/api/js/examples/low-level/test-ts-api.ts

@@ -3,24 +3,24 @@
 // TypeScript can infer all of them.
 // They're just here so readers can see what types things are.
 
+// @ts-ignore we're not going to bother with types for this
+import process from 'process';
+import { sprintf } from 'sprintf-js';
 import type {
+  Z3_app,
+  Z3_ast,
+  Z3_ast_vector,
   Z3_config,
   Z3_context,
+  Z3_func_decl,
+  Z3_func_entry,
+  Z3_func_interp,
+  Z3_model,
   Z3_solver,
   Z3_sort,
-  Z3_ast,
-  Z3_app,
-  Z3_model,
   Z3_symbol,
-  Z3_ast_vector,
-  Z3_func_decl,
-  Z3_func_interp,
-  Z3_func_entry,
-} from './build/node-wrapper';
-import { init, Z3_lbool, Z3_ast_kind, Z3_sort_kind, Z3_symbol_kind } from './build/node-wrapper';
-
-// @ts-ignore we're not going to bother with types for this
-import { sprintf } from 'sprintf-js';
+} from '../../build/node';
+import { init, Z3_ast_kind, Z3_lbool, Z3_sort_kind, Z3_symbol_kind } from '../../build/node';
 
 let printf = (str: string, ...args: unknown[]) => console.log(sprintf(str.replace(/\n$/, ''), ...args));
 

src/api/js/jest.config.js

@@ -0,0 +1,7 @@
+/** @type {import('ts-jest/dist/types').InitialOptionsTsJest} */
+module.exports = {
+  preset: 'ts-jest',
+  testEnvironment: 'node',
+  roots: ['<rootDir>/src'],
+  verbose: true,
+};