Add high level bindings for js (Z3Prover#6048)

* [Draft] Added unfinished code for high level bindings for js

* * Rewrote structure of js api files
* Added more high level apis

* Minor fixes

* Fixed wasm github action

* Fix JS test

* Removed ContextOptions type

* * Added Ints to JS Api
* Added tests to JS Api

* Added run-time checks for contexts

* Removed default contexts

* Merged Context and createContext so that the api behaves the sames as in other constructors

* Added a test for Solver

* Added Reals

* Added classes for IntVals and RealVals

* Added abillity to specify logic for solver

* Try to make CI tests not fail

* Changed APIs after a round of review

* Fix test

* Added BitVectors

* Made sort into getter

* Added initial JS docs

* Added more coercible types

* Removed done TODOs

Author: ritave

.github/workflows/wasm-release.yml

@@ -23,8 +23,8 @@ jobs:
       - name: Setup node
         uses: actions/setup-node@v3
         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@v3
         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/**
@@ -92,3 +90,4 @@ examples/**/obj
 CMakeSettings.json
 # Editor temp files
 *.swp
+.DS_Store

doc/mk_api_doc.py

@@ -14,11 +14,13 @@
 
 ML_ENABLED=False
 MLD_ENABLED=False
+JS_ENABLED=False
 BUILD_DIR='../build'
 DOXYGEN_EXE='doxygen'
 TEMP_DIR=os.path.join(os.getcwd(), 'tmp')
 OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api')
 Z3PY_PACKAGE_PATH='../src/api/python/z3'
+JS_API_PATH='../src/api/js'
 Z3PY_ENABLED=True
 DOTNET_ENABLED=True
 JAVA_ENABLED=True
@@ -28,8 +30,8 @@
 
 def parse_options():
     global ML_ENABLED, MLD_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY
-    global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED
-    global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS
+    global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED, JS_ENABLED
+    global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS, JS_API_PATH
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument('-b',
         '--build',
@@ -46,6 +48,11 @@ def parse_options():
         default=False,
         help='Include ML/OCaml API documentation'
     )
+    parser.add_argument('--js',
+        action='store_true',
+        default=False,
+        help='Include JS/TS API documentation'
+    )
     parser.add_argument('--doxygen-executable',
         dest='doxygen_executable',
         default=DOXYGEN_EXE,
@@ -104,6 +111,7 @@ def parse_options():
     pargs = parser.parse_args()
     ML_ENABLED = pargs.ml
     MLD_ENABLED = pargs.mld
+    JS_ENABLED = pargs.js
     BUILD_DIR = pargs.build
     DOXYGEN_EXE = pargs.doxygen_executable
     TEMP_DIR = pargs.temp_dir
@@ -224,6 +232,10 @@ def doc_path(path):
         print("Java documentation disabled")
         doxygen_config_substitutions['JAVA_API_FILES'] = ''
         doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = ''
+    if JS_ENABLED:
+        print('Javascript documentation enabled')
+    else:
+        print('Javascript documentation disabled')
 
     doxygen_config_file = temp_path('z3api.cfg')
     configure_file(
@@ -241,7 +253,7 @@ def doc_path(path):
             '{prefix}<a class="el" href="z3__api_8h.html">C API</a> '
             ).format(
                 prefix=bullet_point_prefix)
-    
+
     if Z3PY_ENABLED:
         print("Python documentation enabled")
         website_dox_substitutions['PYTHON_API'] = (
@@ -274,6 +286,13 @@ def doc_path(path):
                 prefix=bullet_point_prefix)
     else:
         website_dox_substitutions['OCAML_API'] = ''
+    if JS_ENABLED:
+        website_dox_substitutions['JS_API'] = (
+            '{prefix}<a class="el" href="js/index.html">Javascript/Typescript API</a>'
+            ).format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['JS_API'] = ''
     configure_file(
         doc_path('website.dox.in'),
         temp_path('website.dox'),
@@ -339,6 +358,18 @@ def doc_path(path):
             exit(1)
         print("Generated ML/OCaml documentation.")
 
+    if JS_ENABLED:
+        try:
+            subprocess.check_output(['npm', 'run', '--prefix=%s' % JS_API_PATH, 'check-engine'])
+        except subprocess.CalledProcessError as e:
+            print("ERROR: node version check failed.")
+            print(e.output)
+            exit(1)
+        if subprocess.call(['npm', 'run', '--prefix=%s' % JS_API_PATH, 'docs']) != 0:
+            print("ERROR: npm run docs failed.")
+            exit(1)
+        print("Generated Javascript documentation.")
+
     print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY))
 except Exception:
     exctype, value = sys.exc_info()[:2]

doc/website.dox.in

@@ -1,13 +1,13 @@
 /**
    \mainpage An Efficient Theorem Prover
-    
+
    Z3 is a high-performance theorem prover being developed at <a class="el"
-   href="http://research.microsoft.com">Microsoft Research</a>. 
-   
+   href="http://research.microsoft.com">Microsoft Research</a>.
+
    <b>The Z3 website is at <a class="el" href="http://github.com/z3prover">http://github.com/z3prover</a>.</b>
 
    This website hosts the automatically generated documentation for the Z3 APIs.
 
    - \ref @C_API@
-   - \ref @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@
+   - \ref @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
 */

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"
+}