mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

Merge branch 'master' into jfleisher/devIntellitest

Browse source
This commit is contained in:
jofleish 2022-06-22 13:06:19 -04:00
parent e7d897bba5 8dad9a29c2
commit ed3f3a1a00
407 changed files with 24473 additions and 4926 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
.github/dependabot.yml vendored Normal file
View file

@ -0,0 +1,6 @@
version: 2
updates:
- package-ecosystem: "github-actions"
directory: "/"
schedule:
interval: "weekly"

7
.github/workflows/android-build.yml vendored
View file

@ -7,6 +7,9 @@ on:
env:
BUILD_TYPE: Release
permissions:
contents: read
jobs:
build:
runs-on: ubuntu-latest
@ -18,7 +21,7 @@ jobs:
steps:
- name: Checkout code
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Configure CMake and build
run: |
@ -29,7 +32,7 @@ jobs:
tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so
- name: Archive production artifacts
uses: actions/upload-artifact@v2
uses: actions/upload-artifact@v3
with:
name: android-build-${{ matrix.android-abi }}
path: build/z3-build-${{ matrix.android-abi }}.tar

13
.github/workflows/coverage.yml vendored
View file

@ -6,6 +6,9 @@ on:
schedule:
- cron: "0 11 * * *"
permissions:
contents: read
jobs:
build:
runs-on: ubuntu-latest
@ -18,7 +21,7 @@ jobs:
COV_DETAILS_PATH: ${{github.workspace}}/cov-details
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
- name: Setup
run: |
@ -73,27 +76,27 @@ jobs:
- name: Gather coverage
run: |
cd ${{github.workspace}}
gcovr --html coverage.html --gcov-executable "llvm-cov gcov" .
gcovr --html coverage.html --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .
cd -
- name: Gather detailed coverage
run: |
cd ${{github.workspace}}
mkdir cov-details
gcovr --html-details ${{env.COV_DETAILS_PATH}}/coverage.html --gcov-executable "llvm-cov gcov" -r `pwd`/src --object-directory `pwd`/build
gcovr --html-details ${{env.COV_DETAILS_PATH}}/coverage.html --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" -r `pwd`/src --object-directory `pwd`/build
cd -
- name: Get date
id: date
run: echo "::set-output name=date::$(date +'%Y-%m-%d')"
- uses: actions/upload-artifact@v2
- uses: actions/upload-artifact@v3
with:
name: coverage-${{steps.date.outputs.date}}
path: ${{github.workspace}}/coverage.html
retention-days: 4
- uses: actions/upload-artifact@v2
- uses: actions/upload-artifact@v3
with:
name: coverage-details-${{steps.date.outputs.date}}
path: ${{env.COV_DETAILS_PATH}}

5
.github/workflows/cross-build.yml vendored
View file

@ -4,6 +4,9 @@ on:
push:
pull_request:
permissions:
contents: read
jobs:
build:
runs-on: ubuntu-latest
@ -16,7 +19,7 @@ jobs:
steps:
- name: Checkout code
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Install cross build tools
run: apt update && apt install -y ninja-build cmake python3 g++-11-${{ matrix.arch }}-linux-gnu

11
.github/workflows/docker-image.yml vendored
View file

@ -5,6 +5,9 @@ on:
- cron: "0 1 * * 0" # every Sunday at 1 am
workflow_dispatch: # on button click
permissions:
contents: read
jobs:
push_to_registry:
name: Push Docker image to GitHub Docker registry
@ -12,10 +15,10 @@ jobs:
steps:
- name: Check out the repo
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Log in to GitHub Docker registry
uses: docker/login-action@v1
uses: docker/login-action@v2
with:
registry: ghcr.io
username: ${{ secrets.DOCKER_USERNAME }}
@ -26,7 +29,7 @@ jobs:
# -------
- name: Extract metadata (tags, labels) for Bare Z3 Docker Image
id: meta
uses: docker/metadata-action@v3
uses: docker/metadata-action@v4
with:
images: ghcr.io/z3prover/z3
flavor: |
@ -38,7 +41,7 @@ jobs:
type=edge
type=sha,prefix=ubuntu-20.04-bare-z3-sha-
- name: Build and push Bare Z3 Docker Image
uses: docker/build-push-action@v2.7.0
uses: docker/build-push-action@v3.0.0
with:
context: .
push: true

16
.github/workflows/wasm-release.yml vendored
View file

@ -2,6 +2,8 @@ name: WebAssembly Publish
on:
workflow_dispatch:
release:
types: [published]
defaults:
run:
@ -16,13 +18,13 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Setup node
uses: actions/setup-node@v2
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: |
@ -35,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: |
@ -50,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

14
.github/workflows/wasm.yml vendored
View file

@ -2,7 +2,7 @@ name: WebAssembly Build
on:
push:
branches: [ master ]
branches: [master]
pull_request:
defaults:
@ -18,25 +18,25 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Setup node
uses: actions/setup-node@v2
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

5
.github/workflows/wip.yml vendored
View file

@ -7,12 +7,15 @@ on:
env:
BUILD_TYPE: Debug
permissions:
contents: read
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
- name: Configure CMake
run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}}

7
.gitignore vendored
View file

@ -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

2
CMakeLists.txt
View file

@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.4)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
project(Z3 VERSION 4.8.16.0 LANGUAGES CXX)
project(Z3 VERSION 4.8.18.0 LANGUAGES CXX)
################################################################################
# Project version

22
RELEASE_NOTES
View file

@ -10,6 +10,28 @@ Version 4.8.next
- native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
Version 4.8.17
==============
- fix breaking bug in python interface for user propagator pop
- integrate fixes to z3str3
- initial support for nested algebraic datatypes with sequences
- initiate map/fold operators on sequences - full integration for next releases
- initiate maxdiff/mindiff on arrays - full integration for next releases
Version 4.8.16
==============
- initial support for Darwin Arm64 (for M1, M2, .. users) thanks to zwimer and Anja Petkovi'c
Komel for updates.
Java is not yet supported, pypi native arm64 distributions are not yet supported.
cmake dependency added to enable users to build for not-yet-supported platforms directly;
specifically M1 seems to come up.
- added functionality to user propagator decisions. Thanks to Clemens Eisenhofer.
- added options for rc2 and maxres-bin to maxsat (note that there was no real difference measured
from maxres on MaxSAT unweighted so default option is unchanged)
- improved search for mutex constraints (at-most-1 constraints) among soft
constraints for maxsat derived from approach used in rc2 sample.
- multiple merges
Version 4.8.15
==============
- elaborate user propagator API. Change id based scheme to expressions

42
doc/mk_api_doc.py
View file

@ -11,15 +11,16 @@ import getopt
import pydoc
import sys
import subprocess
import shutil
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
@ -29,8 +30,8 @@ SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__))
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',
@ -47,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,
@ -105,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
@ -133,10 +140,12 @@ def cleanup_API(inf, outf):
pat1 = re.compile(".*def_API.*")
pat2 = re.compile(".*extra_API.*")
pat3 = re.compile(r".*def_Type\(.*")
pat4 = re.compile("Z3_DECLARE_CLOSURE.*")
pat5 = re.compile("DEFINE_TYPE.*")
_inf = open(inf, 'r')
_outf = open(outf, 'w')
for line in _inf:
if not pat1.match(line) and not pat2.match(line) and not pat3.match(line):
if not pat1.match(line) and not pat2.match(line) and not pat3.match(line) and not pat4.match(line) and not pat5.match(line):
_outf.write(line)
def configure_file(template_file_path, output_file_path, substitutions):
@ -223,6 +232,10 @@ try:
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(
@ -240,7 +253,7 @@ try:
'{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'] = (
@ -273,6 +286,13 @@ try:
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'),
@ -338,6 +358,18 @@ try:
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]

8
doc/website.dox.in
View file

@ -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@
*/

3
examples/c++/example.cpp
View file

@ -4,6 +4,7 @@ Copyright (c) 2015 Microsoft Corporation
--*/
#include <iostream>
#include<vector>
#include"z3++.h"
@ -737,7 +738,7 @@ void tactic_example8() {
try {
t(g);
}
catch (exception) {
catch (exception&) {
std::cout << "tactic failed...\n";
}
std::cout << "trying again...\n";

2
examples/python/tutorial/jupyter/guide.ipynb
View file

@ -1395,7 +1395,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.1"
"version": "3.8.8"
}
},
"nbformat": 4,

2
scripts/mk_project.py
View file

@ -8,7 +8,7 @@
from mk_util import *
def init_version():
set_version(4, 8, 16, 0)
set_version(4, 8, 18, 0)
# Z3 Project definition
def init_project_def():

9
scripts/mk_unix_dist.py
View file

@ -28,6 +28,7 @@ JAVA_ENABLED=True
GIT_HASH=False
PYTHON_ENABLED=True
MAKEJOBS=getenv("MAKEJOBS", '8')
OS_NAME=None
def set_verbose(flag):
global VERBOSE
@ -58,13 +59,14 @@ def display_help():
print(" --dotnet-key=<file> sign the .NET assembly with the private key in <file>.")
print(" --arch=<arch> set architecture (to arm64) to force arm64 build")
print(" --nojava do not include Java bindings in the binary distribution files.")
print(" --os=<os> set OS version.")
print(" --nopython do not include Python bindings in the binary distribution files.")
print(" --githash include git hash in the Zip file.")
exit(0)
# Parse configuration option for mk_make script
def parse_options():
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, OS_NAME
path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help',
@ -74,6 +76,7 @@ def parse_options():
'nodotnet',
'dotnet-key=',
'arch=',
'os=',
'githash',
'nopython'
])
@ -103,6 +106,8 @@ def parse_options():
mk_util.IS_ARCH_ARM64 = True
else:
raise MKException("Invalid architecture directive '%s'. Legal directives: arm64" % arg)
elif opt == '--os':
OS_NAME = arg
else:
raise MKException("Invalid command line option '%s'" % opt)
set_build_dir(path)
@ -154,6 +159,8 @@ def mk_z3():
return 1
def get_os_name():
if OS_NAME is not None:
return OS_NAME
import platform
basic = os.uname()[0].lower()
if basic == 'linux':

51
scripts/mk_util.py
View file

@ -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 @@ elif os.name == 'posix':
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 @@ class DotNetDLLComponent(Component):
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 @@ class DotNetDLLComponent(Component):
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 @@ class DotNetDLLComponent(Component):
ous.write(core_csproj_str)
dotnetCmdLine = [DOTNET, "build", csproj]
dotnetCmdLine.extend(['-c'])
if DEBUG_MODE:
dotnetCmdLine.extend(['Debug'])
@ -1733,19 +1740,19 @@ class DotNetDLLComponent(Component):
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 @@ class MLComponent(Component):
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:
@ -2599,6 +2606,7 @@ def mk_config():
OS_DEFINES = '-D_FREEBSD_'
SO_EXT = '.so'
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
elif sysname == 'NetBSD':
CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS
OS_DEFINES = '-D_NETBSD_'
@ -2632,7 +2640,7 @@ def mk_config():
if is64():
if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
CXXFLAGS = '%s -fPIC' % CXXFLAGS
if sysname == 'Linux':
if sysname == 'Linux' or sysname == 'FreeBSD':
CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
elif not LINUX_X64:
CXXFLAGS = '%s -m32' % CXXFLAGS
@ -3019,10 +3027,12 @@ def mk_bindings(api_files):
if is_dotnet_core_enabled():
dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet')
mk_dir(dotnet_output_dir)
java_input_dir = None
java_output_dir = None
java_package_name = None
if is_java_enabled():
java_output_dir = get_component('java').src_dir
java_input_dir = get_component('java').src_dir
java_package_name = get_component('java').package_name
ml_output_dir = None
if is_ml_enabled():
@ -3033,7 +3043,8 @@ def mk_bindings(api_files):
api_output_dir=get_component('api').src_dir,
z3py_output_dir=get_z3py_dir(),
dotnet_output_dir=dotnet_output_dir,
java_output_dir=java_output_dir,
java_input_dir=java_input_dir,
java_output_dir=java_output_dir,
java_package_name=java_package_name,
ml_output_dir=ml_output_dir,
ml_src_dir=ml_output_dir
@ -3116,7 +3127,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:

48
scripts/nightly.yaml
View file

@ -2,7 +2,7 @@ variables:
Major: '4'
Minor: '8'
Patch: '16'
Patch: '18'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
stages:
@ -29,7 +29,7 @@ stages:
pool:
vmImage: "macOS-latest"
steps:
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0
- script: git clone https://github.com/z3prover/z3test z3test
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
- task: PublishPipelineArtifact@1
@ -86,13 +86,14 @@ stages:
artifactName: 'UbuntuDoc'
targetPath: $(Build.ArtifactStagingDirectory)
- job: Manylinux
displayName: "Manylinux build"
- job: ManyLinuxBuild
variables:
python: "/opt/python/cp37-cp37m/bin/python"
name: ManyLinux
displayName: "ManyLinux build"
pool:
vmImage: "Ubuntu-18.04"
container: "quay.io/pypa/manylinux2010_x86_64:latest"
variables:
python: "/opt/python/cp37-cp37m/bin/python"
steps:
- script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
- script: git clone https://github.com/z3prover/z3test z3test
@ -100,9 +101,29 @@ stages:
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'Manylinux'
artifactName: '$(name)Build'
targetPath: $(Build.ArtifactStagingDirectory)
# - job: MuslLinuxBuild
# condition: eq(0,1)
# variables:
# python: "/opt/python/cp310-cp310/bin/python"
# name: MuslLinux
# displayName: "MuslLinux build"
# pool:
# vmImage: "Ubuntu-18.04"
# container: "quay.io/pypa/musllinux_1_1_x86_64:latest"
# steps:
# - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
# - script: git clone https://github.com/z3prover/z3test z3test
# - script: $(python) z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2
# - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/
# - task: PublishPipelineArtifact@0
# inputs:
# artifactName: '$(name)Build'
# targetPath: $(Build.ArtifactStagingDirectory)
- job: Windows32
displayName: "Windows 32-bit build"
pool:
@ -393,8 +414,13 @@ stages:
targetPath: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
inputs:
artifactName: 'Manylinux'
artifactName: 'ManyLinuxBuild'
targetPath: $(Agent.TempDirectory)
# - task: DownloadPipelineArtifact@2
# displayName: 'Download MuslLinux Build'
# inputs:
# artifact: 'MuslLinuxBuild'
# path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
inputs:
artifactName: 'Mac'
@ -405,13 +431,15 @@ stages:
targetPath: $(Agent.TempDirectory)
- script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir libc-bin; cd libc-bin; unzip ../*glibc*.zip
# - script: cd $(Agent.TempDirectory); mkdir musl-bin; cd musl-bin; unzip ../*-linux.zip
- script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
- script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
- script: python3 -m pip install --user -U setuptools wheel
- script: cd src/api/python; python3 setup.py sdist
# take a look at this PREMIUM HACK I came up with to get around the fact that the azure variable syntax overloads the bash syntax for subshells
- script: cd src/api/python; echo $(Agent.TempDirectory)/linux-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/libc-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
# - script: cd src/api/python; echo $(Agent.TempDirectory)/musl-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel

64
scripts/release.yml
View file

@ -6,7 +6,7 @@
trigger: none
variables:
ReleaseVersion: '4.8.16'
ReleaseVersion: '4.8.18'
stages:
@ -43,6 +43,28 @@ stages:
artifactName: 'macOSBuild'
targetPath: $(Build.ArtifactStagingDirectory)
- job: MacBuildArm64
displayName: "macOS Build"
pool:
vmImage: "macOS-latest"
steps:
- task: PythonScript@0
displayName: Build
inputs:
scriptSource: 'filepath'
scriptPath: scripts/mk_unix_dist.py
arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --nojava --arch=arm64 --os=osx-11.0
- task: CopyFiles@2
inputs:
sourceFolder: dist
contents: '*.zip'
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'macOSBuildArm64'
targetPath: $(Build.ArtifactStagingDirectory)
- job: UbuntuBuild
displayName: "Ubuntu build"
pool:
@ -107,13 +129,23 @@ stages:
artifactName: 'UbuntuDoc'
targetPath: $(Build.ArtifactStagingDirectory)
- job: ManyLinuxBuild
displayName: "ManyLinux build"
- job: LinuxBuilds
strategy:
matrix:
manyLinux:
name: ManyLinux
image: "quay.io/pypa/manylinux2010_x86_64:latest"
python: "/opt/python/cp37-cp37m/bin/python"
muslLinux:
name: MuslLinux
image: "quay.io/pypa/musllinux_1_1_x86_64:latest"
python: "/opt/python/cp310-cp310/bin/python"
displayName: "$(name) build"
pool:
vmImage: "ubuntu-latest"
container: "quay.io/pypa/manylinux2010_x86_64:latest"
container: $(image)
variables:
python: "/opt/python/cp37-cp37m/bin/python"
python: $(python)
steps:
- task: PythonScript@0
displayName: Build
@ -138,7 +170,7 @@ stages:
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'ManyLinuxBuild'
artifactName: '$(name)Build'
targetPath: $(Build.ArtifactStagingDirectory)
- template: build-win-signed.yml
@ -378,6 +410,11 @@ stages:
inputs:
artifact: 'ManyLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download MuslLinux Build'
inputs:
artifact: 'MuslLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
inputs:
@ -389,14 +426,18 @@ stages:
artifact: 'WindowsBuild-x64'
path: $(Agent.TempDirectory)
- script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip
- script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir libc-bin; cd libc-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir musl-bin; cd musl-bin; unzip ../*-linux.zip
- script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
- script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
- script: python3 -m pip install --user -U setuptools wheel
- script: cd src/api/python; python3 setup.py sdist
# take a look at this PREMIUM HACK I came up with to get around the fact that the azure variable syntax overloads the bash syntax for subshells
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/linux-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/libc-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/musl-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- task: PublishPipelineArtifact@0
@ -429,6 +470,11 @@ stages:
inputs:
artifact: 'macOSBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download macOSArm64 Build'
inputs:
artifact: 'macOSBuildArm64'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
inputs:
@ -507,4 +553,4 @@ stages:
secureFile: 'pypircs'
- script: python3 -m pip install --upgrade pip
- script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine
- script: python3 -m twine upload --config-file $(pypircs.secureFilePath) -r $(pypiReleaseServer) dist/*
- script: python3 -m twine upload --config-file $(pypircs.secureFilePath) -r $(pypiReleaseServer) dist/*

240
scripts/update_api.py
View file

@ -42,6 +42,7 @@ IN_ARRAY = 3
OUT_ARRAY = 4
INOUT_ARRAY = 5
OUT_MANAGED_ARRAY = 6
FN_PTR = 7
# Primitive Types
VOID = 0
@ -60,37 +61,46 @@ DOUBLE = 12
FLOAT = 13
CHAR = 14
CHAR_PTR = 15
LBOOL = 16
FIRST_FN_ID = 50
FIRST_OBJ_ID = 100
def is_obj(ty):
return ty >= FIRST_OBJ_ID
def is_fn(ty):
return FIRST_FN_ID <= ty and ty < FIRST_OBJ_ID
Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double',
FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'bool', SYMBOL : 'Z3_symbol',
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char', CHAR_PTR: 'Z3_char_ptr'
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char', CHAR_PTR: 'Z3_char_ptr', LBOOL : 'Z3_lbool'
}
Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong',
UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float',
STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol',
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.POINTER(ctypes.c_char)'
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.POINTER(ctypes.c_char)', LBOOL : 'ctypes.c_int'
}
# Mapping to .NET types
Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr' }
PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr', LBOOL : 'int' }
# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string' }
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' }
Closures = []
class APITypes:
def __init__(self):
self.next_type_id = FIRST_OBJ_ID
self.next_fntype_id = FIRST_FN_ID
def def_Type(self, var, c_type, py_type):
"""Process type definitions of the form def_Type(var, c_type, py_type)
@ -103,24 +113,42 @@ class APITypes:
Type2Str[id] = c_type
Type2PyStr[id] = py_type
self.next_type_id += 1
def def_Types(self, api_files):
global Closures
pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
for api_file in api_files:
with open(api_file, 'r') as api:
for line in api:
m = pat1.match(line)
if m:
self.def_Type(m.group(1), m.group(2), m.group(3))
continue
m = pat2.match(line)
if m:
self.fun_Type(m.group(1))
Closures += [(m.group(1), m.group(2), m.group(3))]
continue
#
# Populate object type entries in dotnet and ML bindings.
#
for k in Type2Str:
v = Type2Str[k]
if is_obj(k):
if is_obj(k) or is_fn(k):
Type2Dotnet[k] = v
Type2ML[k] = v.lower()
def fun_Type(self, var):
"""Process function type definitions"""
id = self.next_fntype_id
exec('%s = %s' % (var, id), globals())
Type2Str[id] = var
Type2PyStr[id] = var
self.next_fntype_id += 1
def type2str(ty):
global Type2Str
return Type2Str[ty]
@ -147,6 +175,9 @@ def _in(ty):
def _in_array(sz, ty):
return (IN_ARRAY, ty, sz)
def _fnptr(ty):
return (FN_PTR, ty)
def _out(ty):
return (OUT, ty)
@ -179,11 +210,13 @@ def param_array_size_pos(p):
def param2str(p):
if param_kind(p) == IN_ARRAY:
return "%s const *" % type2str(param_type(p))
return "%s const *" % (type2str(param_type(p)))
elif param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY:
return "%s*" % type2str(param_type(p))
return "%s*" % (type2str(param_type(p)))
elif param_kind(p) == OUT:
return "%s*" % type2str(param_type(p))
return "%s*" % (type2str(param_type(p)))
elif param_kind(p) == FN_PTR:
return "%s*" % (type2str(param_type(p)))
else:
return type2str(param_type(p))
@ -276,6 +309,13 @@ def display_args_to_z3(params):
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
Unchecked = frozenset([ 'Z3_dec_ref', 'Z3_params_dec_ref', 'Z3_model_dec_ref',
'Z3_func_interp_dec_ref', 'Z3_func_entry_dec_ref',
'Z3_goal_dec_ref', 'Z3_tactic_dec_ref', 'Z3_probe_dec_ref',
'Z3_fixedpoint_dec_ref', 'Z3_param_descrs_dec_ref',
'Z3_ast_vector_dec_ref', 'Z3_ast_map_dec_ref',
'Z3_apply_result_dec_ref', 'Z3_solver_dec_ref',
'Z3_stats_dec_ref', 'Z3_optimize_dec_ref'])
def mk_py_wrappers():
core_py.write("""
@ -345,7 +385,7 @@ def mk_py_wrapper_single(sig, decode_string=True):
core_py.write(" %s_elems.f(" % lval)
display_args_to_z3(params)
core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped:
if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped and not name in Unchecked:
core_py.write(" _elems.Check(a0)\n")
if result == STRING and decode_string:
core_py.write(" return _to_pystr(r)\n")
@ -374,11 +414,21 @@ def mk_dotnet(dotnet):
v = Type2Str[k]
if is_obj(k):
dotnet.write(' using %s = System.IntPtr;\n' % v)
dotnet.write(' using voidp = System.IntPtr;\n')
dotnet.write('\n')
dotnet.write(' public class Native\n')
dotnet.write(' {\n\n')
dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
for name, ret, sig in Closures:
sig = sig.replace("void*","voidp").replace("unsigned","uint")
sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
ret = ret.replace("void*","voidp").replace("unsigned","uint")
if "*" in sig or "*" in ret:
continue
dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
dotnet.write(' public delegate %s %s(%s);\n' % (ret,name,sig))
dotnet.write(' public class LIB\n')
dotnet.write(' {\n')
dotnet.write(' const string Z3_DLL_NAME = \"libz3\";\n'
@ -456,7 +506,7 @@ def mk_dotnet_wrappers(dotnet):
dotnet.write(" if (r == IntPtr.Zero)\n")
dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
@ -473,22 +523,22 @@ def mk_dotnet_wrappers(dotnet):
Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' }
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long', LBOOL : 'int' }
Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'}
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong', LBOOL : 'jint'}
def type2java(ty):
global Type2Java
if (ty >= FIRST_OBJ_ID):
if (ty >= FIRST_FN_ID):
return 'long'
else:
return Type2Java[ty]
def type2javaw(ty):
global Type2JavaW
if (ty >= FIRST_OBJ_ID):
if (ty >= FIRST_FN_ID):
return 'jlong'
else:
return Type2JavaW[ty]
@ -513,6 +563,8 @@ def param2java(p):
return "UIntArrayPtr"
else:
return "ObjArrayPtr"
elif k == FN_PTR:
return "LongPtr"
else:
return type2java(param_type(p))
@ -552,7 +604,7 @@ def java_array_element_type(p):
else:
return 'jlong'
def mk_java(java_dir, package_name):
def mk_java(java_src, java_dir, package_name):
java_nativef = os.path.join(java_dir, 'Native.java')
java_wrapperf = os.path.join(java_dir, 'Native.cpp')
java_native = open(java_nativef, 'w')
@ -627,7 +679,7 @@ def mk_java(java_dir, package_name):
java_native.write(" if (res == 0)\n")
java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n')
@ -637,65 +689,9 @@ def mk_java(java_dir, package_name):
java_native.write('}\n')
java_wrapper = open(java_wrapperf, 'w')
pkg_str = package_name.replace('.', '_')
java_wrapper.write('// Automatically generated file\n')
java_wrapper.write('#include<jni.h>\n')
java_wrapper.write('#include<stdlib.h>\n')
java_wrapper.write('#include"z3.h"\n')
java_wrapper.write('#ifdef __cplusplus\n')
java_wrapper.write('extern "C" {\n')
java_wrapper.write('#endif\n\n')
java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n')
java_wrapper.write('#if defined(__LP64__) || defined(_WIN64)\n\n')
java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n')
java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); \n')
java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) \n\n')
java_wrapper.write('#else\n\n')
java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n')
java_wrapper.write(' T * NEW = 0; { \\\n')
java_wrapper.write(' jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \\\n')
java_wrapper.write(' unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \\\n')
java_wrapper.write(' if (OLD != 0) { \\\n')
java_wrapper.write(' NEW = (T*) (new int[size]); \\\n')
java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n')
java_wrapper.write(' NEW[i] = reinterpret_cast<T>(temp[i]); \\\n')
java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n')
java_wrapper.write(' } \\\n')
java_wrapper.write(' } \n\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' delete [] NEW; \n\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n')
java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n')
java_wrapper.write(' NEW[i] = reinterpret_cast<T>(temp[i]); \\\n')
java_wrapper.write(' delete [] temp; \\\n')
java_wrapper.write(' }\n\n')
java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n')
java_wrapper.write(' temp[i] = reinterpret_cast<jlong>(NEW[i]); \\\n')
java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \\\n')
java_wrapper.write(' delete [] temp; \\\n')
java_wrapper.write(' }\n\n')
java_wrapper.write('#endif\n\n')
java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n')
java_wrapper.write('{\n')
java_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n')
java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
java_wrapper.write(' // wrappers below.\n')
java_wrapper.write('}\n\n')
java_wrapper.write('DLL_VIS JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str)
java_wrapper.write('{\n')
java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n')
java_wrapper.write('}\n\n')
java_wrapper.write('')
with open(java_src + "/NativeStatic.txt") as ins:
for line in ins:
java_wrapper.write(line)
for name, result, params in _dotnet_decls:
java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
i = 0
@ -973,6 +969,9 @@ def def_API(name, result, params):
elif ty == VOID_PTR:
log_c.write(" P(0);\n")
exe_c.write("in.get_obj_addr(%s)" % i)
elif ty == LBOOL:
log_c.write(" I(static_cast<signed>(a%s));\n" % i)
exe_c.write("static_cast<%s>(in.get_int(%s))" % (type2str(ty), i))
elif ty == PRINT_MODE or ty == ERROR_CODE:
log_c.write(" U(static_cast<unsigned>(a%s));\n" % i)
exe_c.write("static_cast<%s>(in.get_uint(%s))" % (type2str(ty), i))
@ -1070,6 +1069,9 @@ def def_API(name, result, params):
log_c.write(" }\n")
log_c.write(" Ap(%s);\n" % sz_e)
exe_c.write("reinterpret_cast<%s**>(in.get_obj_array(%s))" % (tstr, i))
elif kind == FN_PTR:
log_c.write("// P(a%s);\n" % i)
exe_c.write("reinterpret_cast<%s>(in.get_obj(%s))" % (param2str(p), i))
else:
error ("unsupported parameter for %s, %s" % (name, p))
i = i + 1
@ -1244,7 +1246,7 @@ def ml_unwrap(t, ts, s):
return '(' + ts + ') String_val(' + s + ')'
elif t == BOOL or (type2str(t) == 'bool'):
return '(' + ts + ') Bool_val(' + s + ')'
elif t == INT or t == PRINT_MODE or t == ERROR_CODE:
elif t == INT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return '(' + ts + ') Int_val(' + s + ')'
elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')'
@ -1265,7 +1267,7 @@ def ml_set_wrap(t, d, n):
return d + ' = Val_unit;'
elif t == BOOL or (type2str(t) == 'bool'):
return d + ' = Val_bool(' + n + ');'
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
@ -1278,7 +1280,7 @@ def ml_set_wrap(t, d, n):
return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';'
def ml_alloc_and_store(t, lhs, rhs):
if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or (type2str(t) == 'bool'):
if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or t == LBOOL or (type2str(t) == 'bool'):
return ml_set_wrap(t, lhs, rhs)
else:
pts = ml_plus_type(type2str(t))
@ -1286,6 +1288,27 @@ def ml_alloc_and_store(t, lhs, rhs):
alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts)
return alloc_str + ml_set_wrap(t, lhs, rhs)
z3_long_funs = frozenset([
'Z3_solver_check',
'Z3_solver_check_assumptions',
'Z3_simplify',
'Z3_simplify_ex',
])
z3_ml_overrides = frozenset([
'Z3_mk_config'])
z3_ml_callbacks = frozenset([
'Z3_solver_propagate_init',
'Z3_solver_propagate_fixed',
'Z3_solver_propagate_final',
'Z3_solver_propagate_eq',
'Z3_solver_propagate_diseq',
'Z3_solver_propagate_created',
'Z3_solver_propagate_decide'
])
def mk_ml(ml_src_dir, ml_output_dir):
global Type2Str
ml_nativef = os.path.join(ml_output_dir, 'z3native.ml')
@ -1299,6 +1322,8 @@ def mk_ml(ml_src_dir, ml_output_dir):
ml_native.write('\n')
for name, result, params in _dotnet_decls:
if name in z3_ml_callbacks:
continue
ml_native.write('external %s : ' % ml_method_name(name))
ip = inparams(params)
op = outparams(params)
@ -1343,17 +1368,6 @@ def mk_ml(ml_src_dir, ml_output_dir):
mk_z3native_stubs_c(ml_src_dir, ml_output_dir)
z3_long_funs = frozenset([
'Z3_solver_check',
'Z3_solver_check_assumptions',
'Z3_simplify',
'Z3_simplify_ex',
])
z3_ml_overrides = frozenset([
'Z3_mk_config'
])
def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w')
@ -1368,6 +1382,8 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
if name in z3_ml_overrides:
continue
if name in z3_ml_callbacks:
continue
ip = inparams(params)
op = outparams(params)
@ -1433,7 +1449,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
# determine if the function has a context as parameter.
have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT)
if have_context and name not in Unwrapped:
if have_context and name not in Unwrapped and name not in Unchecked:
ml_wrapper.write(' Z3_error_code ec;\n')
if result != VOID:
@ -1559,7 +1575,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
if release_caml_gc:
ml_wrapper.write('\n caml_acquire_runtime_system();\n')
if have_context and name not in Unwrapped:
if have_context and name not in Unwrapped and name not in Unchecked:
ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n')
ml_wrapper.write(' if (ec != Z3_OK) {\n')
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
@ -1703,7 +1719,6 @@ def write_log_h_preamble(log_h):
def write_log_c_preamble(log_c):
log_c.write('// Automatically generated file\n')
log_c.write('#include<iostream>\n')
log_c.write('#include\"api/z3.h\"\n')
log_c.write('#include\"api/api_log_macros.h\"\n')
log_c.write('#include\"api/z3_logger.h\"\n')
@ -1820,28 +1835,22 @@ _error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
_lib.Z3_set_error_handler.restype = None
_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_push_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
Z3_pop_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
final_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
eq_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_fixed_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_final_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
Z3_eq_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
_lib.Z3_solver_propagate_init.restype = None
_lib.Z3_solver_propagate_init.argtypes = [ContextObj, SolverObj, ctypes.c_void_p, push_eh_type, pop_eh_type, fresh_eh_type]
_lib.Z3_solver_propagate_final.restype = None
_lib.Z3_solver_propagate_final.argtypes = [ContextObj, SolverObj, final_eh_type]
_lib.Z3_solver_propagate_fixed.restype = None
_lib.Z3_solver_propagate_fixed.argtypes = [ContextObj, SolverObj, fixed_eh_type]
_lib.Z3_solver_propagate_eq.restype = None
_lib.Z3_solver_propagate_eq.argtypes = [ContextObj, SolverObj, eq_eh_type]
_lib.Z3_solver_propagate_diseq.restype = None
_lib.Z3_solver_propagate_diseq.argtypes = [ContextObj, SolverObj, eq_eh_type]
on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
_lib.Z3_optimize_register_model_eh.restype = None
@ -1861,6 +1870,7 @@ def generate_files(api_files,
api_output_dir=None,
z3py_output_dir=None,
dotnet_output_dir=None,
java_input_dir=None,
java_output_dir=None,
java_package_name=None,
ml_output_dir=None,
@ -1938,7 +1948,7 @@ def generate_files(api_files,
print("Generated '{}'".format(dotnet_file.name))
if java_output_dir:
mk_java(java_output_dir, java_package_name)
mk_java(java_input_dir, java_output_dir, java_package_name)
if ml_output_dir:
assert not ml_src_dir is None
@ -1962,6 +1972,10 @@ def main(args):
dest="dotnet_output_dir",
default=None,
help="Directory to emit dotnet files. If not specified no files are emitted.")
parser.add_argument("--java-input-dir",
dest="java_input_dir",
default=None,
help="Directory where Java sources reside.")
parser.add_argument("--java-output-dir",
dest="java_output_dir",
default=None,
@ -1984,6 +1998,9 @@ def main(args):
if pargs.java_package_name == None:
logging.error('--java-package-name must be specified')
return 1
if pargs.java_input_dir is None:
logging.error('--java-input-dir must be specified')
return 1
if pargs.ml_output_dir:
if pargs.ml_src_dir is None:
@ -1999,6 +2016,7 @@ def main(args):
api_output_dir=pargs.api_output_dir,
z3py_output_dir=pargs.z3py_output_dir,
dotnet_output_dir=pargs.dotnet_output_dir,
java_input_dir=pargs.java_input_dir,
java_output_dir=pargs.java_output_dir,
java_package_name=pargs.java_package_name,
ml_output_dir=pargs.ml_output_dir,

86
src/api/api_ast.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
@ -874,6 +873,91 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_substitute_funs(Z3_context c,
Z3_ast _a,
unsigned num_funs,
Z3_func_decl const _from[],
Z3_ast const _to[]) {
Z3_TRY;
LOG_Z3_substitute_funs(c, _a, num_funs, _from, _to);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * a = to_expr(_a);
func_decl * const * from = to_func_decls(_from);
expr * const * to = to_exprs(num_funs, _to);
expr * r = nullptr, *v, *w;
expr_ref_vector trail(m), args(m);
ptr_vector<expr> todo;
obj_map<func_decl, expr*> rep;
obj_map<expr, expr*> cache;
for (unsigned i = 0; i < num_funs; i++) {
if (from[i]->get_range() != to[i]->get_sort()) {
SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
RETURN_Z3(of_expr(nullptr));
}
rep.insert(from[i], to[i]);
}
var_subst subst(m, false);
todo.push_back(a);
while (!todo.empty()) {
r = todo.back();
if (cache.contains(r))
todo.pop_back();
else if (is_app(r)) {
args.reset();
unsigned sz = todo.size();
bool change = false;
for (expr* arg : *to_app(r)) {
if (cache.find(arg, v)) {
args.push_back(v);
change |= v != arg;
}
else {
todo.push_back(arg);
}
}
if (todo.size() == sz) {
if (rep.find(to_app(r)->get_decl(), w)) {
expr_ref new_v = subst(w, args);
v = new_v;
trail.push_back(v);
}
else if (change) {
v = m.mk_app(to_app(r)->get_decl(), args);
trail.push_back(v);
}
else
v = r;
cache.insert(r, v);
todo.pop_back();
}
}
else if (is_var(r)) {
cache.insert(r, r);
todo.pop_back();
}
else if (is_quantifier(r)) {
if (cache.find(to_quantifier(r)->get_expr(), v)) {
v = m.update_quantifier(to_quantifier(r), v);
trail.push_back(v);
cache.insert(r, v);
todo.pop_back();
}
else
todo.push_back(to_quantifier(r)->get_expr());
}
else
UNREACHABLE();
}
r = cache[a];
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
Z3_ast _a,
unsigned num_exprs,

2
src/api/api_ast_map.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
@ -52,7 +51,6 @@ extern "C" {
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m) {
Z3_TRY;
LOG_Z3_ast_map_dec_ref(c, m);
RESET_ERROR_CODE();
if (m)
to_ast_map(m)->dec_ref();
Z3_CATCH;

2
src/api/api_ast_vector.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
@ -47,7 +46,6 @@ extern "C" {
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v) {
Z3_TRY;
LOG_Z3_ast_vector_dec_ref(c, v);
RESET_ERROR_CODE();
if (v)
to_ast_vector(v)->dec_ref();
Z3_CATCH;

1
src/api/api_bv.cpp
View file

@ -102,6 +102,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
MK_BV_PUNARY(Z3_mk_sign_ext, OP_SIGN_EXT);
MK_BV_PUNARY(Z3_mk_zero_ext, OP_ZERO_EXT);
MK_BV_PUNARY(Z3_mk_repeat, OP_REPEAT);
MK_BV_PUNARY(Z3_mk_bit2bool, OP_BIT2BOOL);
MK_BV_PUNARY(Z3_mk_rotate_left, OP_ROTATE_LEFT);
MK_BV_PUNARY(Z3_mk_rotate_right, OP_ROTATE_RIGHT);
MK_BV_PUNARY(Z3_mk_int2bv, OP_INT2BV);

11
src/api/api_config_params.cpp
View file

@ -64,6 +64,17 @@ extern "C" {
}
}
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c) {
Z3_TRY;
LOG_Z3_get_global_param_descrs(c);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
d->m_descrs = gparams::get_global_param_descrs();
auto r = of_param_descrs(d);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
Z3_config Z3_API Z3_mk_config(void) {
try {
memory::initialize(UINT_MAX);

4
src/api/api_context.cpp
View file

@ -113,6 +113,7 @@ namespace api {
}
if (m_params.owns_manager())
m_manager.detach();
}
context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
@ -371,8 +372,9 @@ extern "C" {
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_dec_ref(c, a);
RESET_ERROR_CODE();
if (a && to_ast(a)->get_ref_count() == 0) {
// the error is unchecked (but should not happen) in GC'ed wrappers
RESET_ERROR_CODE();
SET_ERROR_CODE(Z3_DEC_REF_ERROR, nullptr);
return;
}

14
src/api/api_datatype.cpp
View file

@ -365,6 +365,20 @@ extern "C" {
Z3_CATCH;
}
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) {
Z3_TRY;
LOG_Z3_mk_datatype_sort(c, name);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
datatype_util adt_util(m);
parameter p(to_symbol(name));
sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p);
mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_mk_datatypes(Z3_context c,
unsigned num_sorts,
Z3_symbol const sort_names[],

1
src/api/api_fpa.cpp
View file

@ -16,7 +16,6 @@ Author:
Notes:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

2
src/api/api_goal.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
@ -52,7 +51,6 @@ extern "C" {
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g) {
Z3_TRY;
LOG_Z3_goal_dec_ref(c, g);
RESET_ERROR_CODE();
if (g)
to_goal(g)->dec_ref();
Z3_CATCH;

1
src/api/api_model.cpp
View file

@ -53,7 +53,6 @@ extern "C" {
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m) {
Z3_TRY;
LOG_Z3_model_dec_ref(c, m);
RESET_ERROR_CODE();
if (m) {
to_model(m)->dec_ref();
}

1
src/api/api_numeral.cpp
View file

@ -16,7 +16,6 @@ Revision History:
--*/
#include<cmath>
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

2
src/api/api_opt.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "util/scoped_ctrl_c.h"
@ -67,7 +66,6 @@ extern "C" {
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) {
Z3_TRY;
LOG_Z3_optimize_dec_ref(c, o);
RESET_ERROR_CODE();
if (o)
to_optimize(o)->dec_ref();
Z3_CATCH;

6
src/api/api_params.cpp
View file

@ -17,7 +17,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
@ -54,7 +53,6 @@ extern "C" {
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p) {
Z3_TRY;
LOG_Z3_params_dec_ref(c, p);
RESET_ERROR_CODE();
if (p)
to_params(p)->dec_ref();
Z3_CATCH;
@ -141,8 +139,8 @@ extern "C" {
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p) {
Z3_TRY;
LOG_Z3_param_descrs_dec_ref(c, p);
RESET_ERROR_CODE();
to_param_descrs(p)->dec_ref();
if (p)
to_param_descrs(p)->dec_ref();
Z3_CATCH;
}

1
src/api/api_parsers.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

1
src/api/api_qe.cpp
View file

@ -17,7 +17,6 @@ Notes:
--*/
#include <iostream>
#include "ast/expr_map.h"
#include "api/z3.h"
#include "api/api_log_macros.h"

1
src/api/api_rcf.cpp
View file

@ -19,7 +19,6 @@ Author:
Notes:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

26
src/api/api_solver.cpp
View file

@ -16,7 +16,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include<thread>
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
@ -207,7 +206,7 @@ extern "C" {
if (!smt_logics::supported_logic(to_symbol(logic))) {
std::ostringstream strm;
strm << "logic '" << to_symbol(logic) << "' is not recognized";
throw default_exception(strm.str());
SET_ERROR_CODE(Z3_INVALID_ARG, strm.str());
RETURN_Z3(nullptr);
}
else {
@ -412,9 +411,8 @@ extern "C" {
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_dec_ref(c, s);
RESET_ERROR_CODE();
if (s)
to_solver(s)->dec_ref();
if (s)
to_solver(s)->dec_ref();
Z3_CATCH;
}
@ -564,7 +562,7 @@ extern "C" {
init_solver(c, s);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
expr_ref_vector trail = to_solver_ref(s)->get_trail();
expr_ref_vector trail = to_solver_ref(s)->get_trail(UINT_MAX);
for (expr* f : trail) {
v->m_ast_vector.push_back(f);
}
@ -975,6 +973,22 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr**, unsigned*, lbool*))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(c);
Z3_CATCH;
}
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase) {
Z3_TRY;
LOG_Z3_solver_next_split(c, cb, t, idx, phase);
RESET_ERROR_CODE();
reinterpret_cast<user_propagator::callback*>(cb)->next_split_cb(to_expr(t), idx, (lbool)phase);
Z3_CATCH;
}
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) {
Z3_TRY;
LOG_Z3_solver_propagate_declare(c, name, n, domain, range);

1
src/api/api_special_relations.cpp
View file

@ -17,7 +17,6 @@ Revision History:
--*/
#include <iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

1
src/api/api_stats.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"

4
src/api/api_tactic.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
@ -73,7 +72,6 @@ extern "C" {
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic t) {
Z3_TRY;
LOG_Z3_tactic_dec_ref(c, t);
RESET_ERROR_CODE();
if (t)
to_tactic(t)->dec_ref();
Z3_CATCH;
@ -104,7 +102,6 @@ extern "C" {
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p) {
Z3_TRY;
LOG_Z3_probe_dec_ref(c, p);
RESET_ERROR_CODE();
if (p)
to_probe(p)->dec_ref();
Z3_CATCH;
@ -477,7 +474,6 @@ extern "C" {
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r) {
Z3_TRY;
LOG_Z3_apply_result_dec_ref(c, r);
RESET_ERROR_CODE();
if (r)
to_apply_result(r)->dec_ref();
Z3_CATCH;

41
src/api/c++/z3++.h
View file

@ -21,7 +21,7 @@ Notes:
#pragma once
#include<cassert>
#include<iostream>
#include<ostream>
#include<string>
#include<sstream>
#include<memory>
@ -459,6 +459,7 @@ namespace z3 {
}
~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); }
static param_descrs global_param_descrs(context& c) { return param_descrs(c, Z3_get_global_param_descrs(c)); }
unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
@ -1359,6 +1360,7 @@ namespace z3 {
friend expr operator~(expr const & a);
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
expr bit2bool(unsigned i) const { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
@ -3943,11 +3945,13 @@ namespace z3 {
typedef std::function<void(void)> final_eh_t;
typedef std::function<void(expr const&, expr const&)> eq_eh_t;
typedef std::function<void(expr const&)> created_eh_t;
typedef std::function<void(expr&, unsigned&, Z3_lbool&)> decide_eh_t;
final_eh_t m_final_eh;
eq_eh_t m_eq_eh;
fixed_eh_t m_fixed_eh;
created_eh_t m_created_eh;
decide_eh_t m_decide_eh;
solver* s;
context* c;
std::vector<z3::context*> subcontexts;
@ -4009,8 +4013,16 @@ namespace z3 {
expr e(p->ctx(), _e);
p->m_created_eh(e);
}
static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast* _val, unsigned* bit, Z3_lbool* is_pos) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
expr val(p->ctx(), *_val);
p->m_decide_eh(val, *bit, *is_pos);
// TBD: life time of val is within the scope of this callback.
*_val = val;
}
public:
user_propagator_base(context& c) : s(nullptr), c(&c) {}
@ -4119,6 +4131,22 @@ namespace z3 {
Z3_solver_propagate_created(ctx(), *s, created_eh);
}
}
void register_decide(decide_eh_t& c) {
m_decide_eh = c;
if (s) {
Z3_solver_propagate_decide(ctx(), *s, decide_eh);
}
}
void register_decide() {
m_decide_eh = [this](expr& val, unsigned& bit, Z3_lbool& is_pos) {
decide(val, bit, is_pos);
};
if (s) {
Z3_solver_propagate_decide(ctx(), *s, decide_eh);
}
}
virtual void fixed(expr const& /*id*/, expr const& /*e*/) { }
@ -4127,6 +4155,13 @@ namespace z3 {
virtual void final() { }
virtual void created(expr const& /*e*/) {}
virtual void decide(expr& /*val*/, unsigned& /*bit*/, Z3_lbool& /*is_pos*/) {}
void next_split(expr const & e, unsigned idx, Z3_lbool phase) {
assert(cb);
Z3_solver_next_split(ctx(), cb, e, idx, phase);
}
/**
\brief tracks \c e by a unique identifier that is returned by the call.

1
src/api/dotnet/CMakeLists.txt
View file

@ -113,6 +113,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
Tactic.cs
TupleSort.cs
UninterpretedSort.cs
UserPropagator.cs
Version.cs
Z3Exception.cs
Z3Object.cs

34
src/api/dotnet/Context.cs
View file

@ -25,6 +25,8 @@ using System.Runtime.InteropServices;
namespace Microsoft.Z3
{
using Z3_context = System.IntPtr;
/// <summary>
/// The main interaction with Z3 happens via the Context.
/// </summary>
@ -77,6 +79,23 @@ namespace Microsoft.Z3
InitContext();
}
}
/// <summary>
/// Internal Constructor. It is used from UserPropagator
/// </summary>
internal Context(Z3_context ctx)
: base()
{
lock (creation_lock)
{
is_external = true;
m_ctx = ctx;
InitContext();
}
}
bool is_external = false;
#endregion
#region Symbols
@ -669,6 +688,16 @@ namespace Microsoft.Z3
CheckContextMatch(range);
return new FuncDecl(this, prefix, null, range);
}
/// <summary>
/// Declare a function to be processed by the user propagator plugin.
/// </summary>
public FuncDecl MkUserPropagatorFuncDecl(string name, Sort[] domain, Sort range)
{
using var _name = MkSymbol(name);
var fn = Native.Z3_solver_propagate_declare(nCtx, _name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject);
return new FuncDecl(this, fn);
}
#endregion
#region Bound Variables
@ -4978,11 +5007,14 @@ namespace Microsoft.Z3
m_n_err_handler = null;
IntPtr ctx = m_ctx;
m_ctx = IntPtr.Zero;
Native.Z3_del_context(ctx);
if (!is_external)
Native.Z3_del_context(ctx);
}
else
GC.ReRegisterForFinalize(this);
}
#endregion
}
}

10
src/api/dotnet/NativeContext.cs
View file

@ -1341,13 +1341,13 @@ namespace Microsoft.Z3
#region Tracing
/// <summary>
/// Enable tracint to file
/// Enable trace to file
/// </summary>
/// <param name="file"></param>
public void TraceToFile(string file)
/// <param name="tag">Tag to trace</param>
public static void EnableTrace(string tag)
{
Debug.Assert(!string.IsNullOrEmpty(file));
Native.Z3_enable_trace(file);
Debug.Assert(!string.IsNullOrEmpty(tag));
Native.Z3_enable_trace(tag);
}
#endregion

313
src/api/dotnet/UserPropagator.cs Normal file
View file

@ -0,0 +1,313 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
UserPropagator.cs
Abstract:
User Propagator plugin
Author:
Nikolaj Bjorner (nbjorner) 2022-05-07
Notes:
--*/
using System;
using System.Diagnostics;
using System.Linq;
using System.Collections.Generic;
using System.Runtime.InteropServices;
namespace Microsoft.Z3
{
using Z3_solver_callback = System.IntPtr;
using Z3_context = System.IntPtr;
using Z3_solver = System.IntPtr;
using voidp = System.IntPtr;
using Z3_ast = System.IntPtr;
/// <summary>
/// Propagator context for .Net
/// </summary>
public class UserPropagator
{
/// <summary>
/// Delegate type for fixed callback
/// </summary>
public delegate void FixedEh(Expr term, Expr value);
/// <summary>
/// Delegate type for equality or disequality callback
/// </summary>
public delegate void EqEh(Expr term, Expr value);
/// <summary>
/// Delegate type for when a new term using a registered function symbol is created internally
/// </summary>
public delegate void CreatedEh(Expr term);
/// <summary>
/// Delegate type for callback into solver's branching
/// <param name="term">A bit-vector or Boolean used for branching</param>
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
/// </summary>
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
Solver solver;
Context ctx;
GCHandle gch;
Z3_solver_callback callback = IntPtr.Zero;
FixedEh fixed_eh;
Action final_eh;
EqEh eq_eh;
EqEh diseq_eh;
CreatedEh created_eh;
DecideEh decide_eh;
void Callback(Action fn, Z3_solver_callback cb) {
this.callback = cb;
try {
fn();
}
catch {
// TBD: add debug log or exception handler
}
finally {
this.callback = IntPtr.Zero;
}
}
static void _push(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Push(), cb);
}
static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Pop(num_scopes), cb);
}
static voidp _fresh(voidp _ctx, Z3_context new_context) {
var gch = GCHandle.FromIntPtr(_ctx);
var prop = (UserPropagator)gch.Target;
var ctx = new Context(new_context);
var prop1 = prop.Fresh(ctx);
return GCHandle.ToIntPtr(prop1.gch);
}
static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var term = Expr.Create(prop.ctx, _term);
using var value = Expr.Create(prop.ctx, _value);
prop.Callback(() => prop.fixed_eh(term, value), cb);
}
static void _final(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.final_eh(), cb);
}
static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.eq_eh(s, t), cb);
}
static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.diseq_eh(s, t), cb);
}
static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var t = Expr.Create(prop.ctx, a);
prop.Callback(() => prop.created_eh(t), cb);
}
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
var t = Expr.Create(prop.ctx, a);
var u = t;
prop.callback = cb;
prop.decide_eh(ref t, ref idx, ref phase);
prop.callback = IntPtr.Zero;
if (u != t)
a = t.NativeObject;
}
/// <summary>
/// Propagator constructor from a solver class.
/// </summary>
public UserPropagator(Solver s)
{
gch = GCHandle.Alloc(this);
solver = s;
ctx = solver.Context;
var cb = GCHandle.ToIntPtr(gch);
Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, cb, _push, _pop, _fresh);
}
/// <summary>
/// Propagator constructor from a context. It is used from inside of Fresh.
/// </summary>
public UserPropagator(Context _ctx)
{
gch = GCHandle.Alloc(this);
solver = null;
ctx = _ctx;
}
/// <summary>
/// Release provate memory.
/// </summary>
~UserPropagator()
{
if (gch != null)
gch.Free();
if (solver == null)
ctx.Dispose();
}
/// <summary>
/// Virtual method for push. It must be overwritten by inherited class.
/// </summary>
public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
/// <summary>
/// Virtual method for pop. It must be overwritten by inherited class.
/// </summary>
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
/// <summary>
/// Virtual method for fresh. It can be overwritten by inherited class.
/// </summary>
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
/// <summary>
/// Declare combination of assigned expressions a conflict
/// </summary>
void Conflict(params Expr[] terms) {
Propagate(terms, ctx.MkFalse());
}
/// <summary>
/// Propagate consequence
/// </summary>
void Propagate(Expr[] terms, Expr conseq) {
var nTerms = Z3Object.ArrayToNative(terms);
Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
}
/// <summary>
/// Set fixed callback
/// </summary>
public FixedEh Fixed
{
set
{
this.fixed_eh = value;
if (solver != null)
Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed);
}
}
/// <summary>
/// Set final callback
/// </summary>
public Action Final
{
set
{
this.final_eh = value;
if (solver != null)
Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
}
}
/// <summary>
/// Set equality event callback
/// </summary>
public EqEh Eq
{
set
{
this.eq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
}
}
/// <summary>
/// Set disequality event callback
/// </summary>
public EqEh Diseq
{
set
{
this.diseq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
}
}
/// <summary>
/// Set created callback
/// </summary>
public CreatedEh Created
{
set
{
this.created_eh = value;
if (solver != null)
Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
}
}
/// <summary>
/// Set decision callback
/// </summary>
public DecideEh Decide
{
set
{
this.decide_eh = value;
if (solver != null)
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
}
}
/// <summary>
/// Track assignments to a term
/// </summary>
public void Register(Expr term) {
if (this.callback != IntPtr.Zero) {
Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
}
else {
Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);
}
}
}
}

2
src/api/dotnet/Z3Object.cs
View file

@ -113,7 +113,7 @@ namespace Microsoft.Z3
return s.NativeObject;
}
internal Context Context
public Context Context
{
get
{

2
src/api/java/CMakeLists.txt
View file

@ -19,6 +19,8 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
COMMAND "${PYTHON_EXECUTABLE}"
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-input-dir"
"${CMAKE_CURRENT_SOURCE_DIR}"
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"

78
src/api/java/NativeStatic.txt Normal file
View file

@ -0,0 +1,78 @@
// Automatically generated file
#include<jni.h>
#include<stdlib.h>
#include"z3.h"
#ifdef __cplusplus
extern "C" {
#endif
#ifdef __GNUC__
#if __GNUC__ >= 4
#define DLL_VIS __attribute__ ((visibility ("default")))
#else
#define DLL_VIS
#endif
#else
#define DLL_VIS
#endif
#if defined(__LP64__) || defined(_WIN64)
#define GETLONGAELEMS(T,OLD,NEW) \
T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);
#define RELEASELONGAELEMS(OLD,NEW) \
if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT);
#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \
jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW);
#define SETLONGAREGION(OLD,Z,SZ,NEW) \
jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW)
#else
#define GETLONGAELEMS(T,OLD,NEW) \
T * NEW = 0; { \
jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \
unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \
if (OLD != 0) { \
NEW = (T*) (new int[size]); \
for (unsigned i=0; i < size; i++) \
NEW[i] = reinterpret_cast<T>(temp[i]); \
jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \
} \
}
#define RELEASELONGAELEMS(OLD,NEW) \
delete [] NEW;
#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \
{ \
jlong * temp = new jlong[SZ]; \
jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \
for (int i = 0; i < (SZ); i++) \
NEW[i] = reinterpret_cast<T>(temp[i]); \
delete [] temp; \
}
#define SETLONGAREGION(OLD,Z,SZ,NEW) \
{ \
jlong * temp = new jlong[SZ]; \
for (int i = 0; i < (SZ); i++) \
temp[i] = reinterpret_cast<jlong>(NEW[i]); \
jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \
delete [] temp; \
}
#endif
void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)
{
// Internal do-nothing error handler. This is required to avoid that Z3 calls exit()
// upon errors, but the actual error handling is done by throwing exceptions in the
// wrappers below.
}
DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)
{
Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);
}

1
src/api/js/.nvmrc Normal file
View file

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

6
src/api/js/.prettierrc.json Normal file
View file

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

91
src/api/js/PUBLISHED_README.md
View file

@ -1,30 +1,86 @@
# Z3 TypeScript Bindings
This project provides low-level TypeScript bindings for the [Z3 theorem prover](https://github.com/Z3Prover/z3). It is available on npm as [z3-solver](https://www.npmjs.com/package/z3-solver).
Z3 itself is distributed as a wasm artifact as part of this package. You can find the documentation for the Z3 API [here](https://z3prover.github.io/api/html/z3__api_8h.html), though note the differences below.
This project provides high-level and low-level TypeScript bindings for the [Z3 theorem prover](https://github.com/Z3Prover/z3). It is available on npm as [z3-solver](https://www.npmjs.com/package/z3-solver).
Z3 itself is distributed as a wasm artifact as part of this package.
## Using
This requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications.
```javascript
const { init } = require('z3-solver');
const {
Z3, // Low-level C-like API
Context, // High-level Z3Py-like API
} = await init();
```
Other than the differences below, the bindings can be used exactly as you'd use the C library. Because this is a wrapper around a C library, most of the values you'll use are just numbers representing pointers. For this reason you are strongly encouraged to make use of the TypeScript types to differentiate among the different kinds of value.
This package has different initialization for browser and node. Your bundler and node should choose good version automatically, but you can import the one you need manually - `const { init } = require('z3-solver/node');` or `const { init } = require('z3-solver/browser');`.
The module exports an `init` function, is an async function which initializes the library and returns `{ em, Z3 }` - `em` contains the underlying emscripten module, which you can use to e.g. kill stray threads, and `Z3` contains the actual bindings. The other module exports are the enums defined in the Z3 API.
### Limitations
[`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c).
The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications.
The Emscripten worker model will spawn multiple instances of `z3-built.js` for long-running operations. When building for the web, you should include that file as its own script on the page - using a bundler like webpack will prevent it from loading correctly.
## Differences from the C API
## High-level
### Integers
You can find the documentation for the high-level Z3 API [here](https://z3prover.github.io/api/html/js/index.html). There are some usage examples in `src/high-level/high-level.test.ts`
Most of the API requires a context to run, and so you need to initialize one to access most functionality.
```javascript
const { init } = require('z3-solver');
const { Context } = await init();
const { Solver, Int, And } = new Context('main');
const x = Int.const('x');
const solver = new Solver();
solver.add(And(x.ge(0), x.le(9)));
console.log(await solver.check());
// sat
```
Typescript types try to catch errors concerning mixing of Contexts during compile time. Objects returned from `new Context('name')` have a type narrowed by the provided Context name and will fail to compile if you try to mix them.
```typescript
const { Int: Int1 } = new Context('context1');
const { Int: Int2 } = new Context('context2');
const x = Int1.const('x');
const y = Int2.const('y');
// The below will fail to compile in Typescript
x.ge(y);
```
```typescript
// Use templated functions to propagate narrowed types
function add<Name extends string>(a: Arith<Name>, b: Arith<Name>): Arith<Name> {
return a.add(b).add(5);
}
```
Some long-running functions are promises and will run in a separate thread.
Currently Z3-solver is not thread safe, and so, high-level APIs ensures that only one long-running function can run at a time, and all other long-running requests will queue up and be run one after another.
## Low-level
You can find the documentation for the low-level Z3 API [here](https://z3prover.github.io/api/html/z3__api_8h.html), though note the differences below. `examples/low-level/` contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c).
The bindings can be used exactly as you'd use the C library. Because this is a wrapper around a C library, most of the values you'll use are just numbers representing pointers. For this reason you are strongly encouraged to make use of the TypeScript types to differentiate among the different kinds of value.
The module exports an `init` function, which is an async function which initializes the library and returns `{ em, Z3 }` - `em` contains the underlying emscripten module, which you can use to e.g. kill stray threads, and `Z3` contains the actual bindings. The other module exports are the enums defined in the Z3 API.
### Differences from the C API
#### Integers
JavaScript numbers are IEEE double-precisions floats. These can be used wherever the C API expects an `int`, `unsigned int`, `float`, or `double`.
`int64_t` and `uint64_t` cannot be precisely represented by JS numbers, so in the TS bindings they are represented by [BigInts](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Data_structures#bigint_type).
### Out parameters
#### Out parameters
In C, to return multiple values a function will take an address to write to, conventionally referred to as an "out parameter". Sometimes the function returns a boolean to indicate success; other times it may return nothing or some other value.
@ -54,7 +110,7 @@ is represented in the TS bindings as
```ts
function model_eval(c: Z3_context, m: Z3_model, t: Z3_ast, model_completion: boolean): Z3_ast | null {
// ...
// ...
}
```
@ -62,12 +118,12 @@ Note that the boolean return type of the C function is translated into a nullabl
When the return value is of interest it is included in the returned record under the key `rv`.
### Arrays
#### Arrays
The when the C API takes an array as an argument it will also require a parameter which specifies the length of the array (since arrays do not carry their own lengths in C). In the TS bindings this is automatically inferred.
For example, the C declaration
```js
unsigned Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
```
@ -82,8 +138,7 @@ function rcf_mk_roots(c: Z3_context, a: Z3_rcf_num[]): { rv: number; roots: Z3_r
When there are multiple arrays which the C API expects to be of the same length, the TS bindings will enforce that this is the case.
### Null pointers
#### Null pointers
Some of the C APIs accept or return null pointers (represented by types whose name end in `_opt`). These are represented in the TS bindings as `| null`. For example, the C declaration
@ -99,8 +154,7 @@ function model_get_const_interp(c: Z3_context, m: Z3_model, a: Z3_func_decl): Z3
}
```
### Async functions
#### Async functions
Certain long-running APIs are not appropriate to call on the main thread. In the TS bindings those APIs are marked as `async` and are automatically called on a different thread. This includes the following APIs:
@ -120,5 +174,4 @@ Certain long-running APIs are not appropriate to call on the main thread. In the
- `Z3_fixedpoint_query_from_lvl`
- `Z3_polynomial_subresultants`
Note that these are not thread-safe, and so only one call can be running at a time. Trying to call a second async API before the first completes will throw.
Note that these are not thread-safe, and so only one call can be running at a time. In contrast to high-level APIs, trying to call a second async API before the first completes will throw.

23
src/api/js/build-wasm.sh
View file

@ -1,23 +0,0 @@
#!/bin/bash
set -euxo pipefail
export ROOT=$PWD
cd ../../..
export CXXFLAGS="-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0"
export LDFLAGS="-s WASM_BIGINT -s -pthread -s USE_PTHREADS=1"
if [ ! -f "build/Makefile" ]; then
emconfigure python scripts/mk_make.py --staticlib --single-threaded
fi
cd build
emmake make -j$(nproc) libz3.a
cd $ROOT
export EM_CACHE=$HOME/.emscripten/
export FNS=$(node scripts/list-exports.js)
export METHODS='["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]'
emcc build/async-fns.cc ../../../build/libz3.a --std=c++20 --pre-js src/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=$METHODS -s EXPORTED_FUNCTIONS=$FNS -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js

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

@ -1,4 +1,5 @@
import { init } from './build/wrapper';
import process from 'process';
import { init, Z3_error_code } from '../../build/node';
// demonstrates use of the raw API
@ -47,6 +48,15 @@ import { init } from './build/wrapper';
console.log(Z3.query_constructor(ctx, nil_con, 0));
console.log(Z3.query_constructor(ctx, cons_con, 2));
if (Z3.get_error_code(ctx) !== Z3_error_code.Z3_OK) {
throw new Error('something failed: ' + Z3.get_error_msg(ctx, Z3.get_error_code(ctx)));
}
await Z3.eval_smtlib2_string(ctx, '(simplify)');
if (Z3.get_error_code(ctx) === Z3_error_code.Z3_OK) {
throw new Error('expected call to eval_smtlib2_string with invalid argument to fail');
}
console.log('confirming error messages work:', Z3.get_error_msg(ctx, Z3.get_error_code(ctx)));
Z3.dec_ref(ctx, strAst);
Z3.del_context(ctx);

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

@ -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/wrapper';
import { init, Z3_lbool, Z3_ast_kind, Z3_sort_kind, Z3_symbol_kind } from './build/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));

7
src/api/js/jest.config.js Normal file
View file

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

11342
src/api/js/package-lock.json generated
View file

File diff suppressed because it is too large Load diff

52
src/api/js/package.json
View file

@ -1,27 +1,61 @@
{
"name": "z3-solver",
"keywords": ["Z3", "theorem", "prover", "solver", "satisfiability", "smt", "satisfiability modulo theories"],
"keywords": [
"Z3",
"theorem",
"prover",
"solver",
"satisfiability",
"smt",
"satisfiability modulo theories"
],
"homepage": "https://github.com/Z3Prover/z3/tree/master/src/api/js",
"repository": "github:Z3Prover/z3",
"engines": {
"node": ">=16"
"node": ">=16 <18"
},
"main": "build/wrapper.js",
"types": "build/wrapper.d.ts",
"browser": "build/browser.js",
"main": "build/node.js",
"types": "build/node.d.ts",
"files": [
"build/*.{js,d.ts,wasm}"
],
"scripts": {
"build-ts": "mkdir -p build && node scripts/make-ts-wrapper.js > build/wrapper.ts && tsc",
"build-wasm": "mkdir -p build && node scripts/make-cc-wrapper.js > build/async-fns.cc && ./build-wasm.sh",
"format": "prettier --write --single-quote --arrow-parens avoid --print-width 120 --trailing-comma all '{,src/,scripts/}*.{js,ts}'",
"test": "node test-ts-api.js"
"build:ts": "run-s -l build:ts:generate build:ts:tsc",
"build:ts:tsc": "tsc --pretty --project tsconfig.build.json ",
"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}'",
"test": "jest",
"docs": "typedoc",
"check-engine": "check-engine"
},
"contributors": [
"Kevin Gibbons <bakkot@gmail.com>",
"Nikolaj Bjorner",
"Olaf Tomalka <olaf@tomalka.me>"
],
"devDependencies": {
"@types/jest": "^27.5.1",
"@types/node": "^17.0.8",
"@types/prettier": "^2.6.1",
"@types/sprintf-js": "^1.1.2",
"check-engine": "^1.10.1",
"iter-tools": "^7.3.1",
"jest": "^28.1.0",
"npm-run-all": "^4.1.5",
"prettier": "^2.5.1",
"rimraf": "^3.0.2",
"sprintf-js": "^1.1.2",
"ts-jest": "^28.0.3",
"ts-node": "^10.8.0",
"typedoc": "^0.22.17",
"typescript": "^4.5.4"
},
"license": "MIT"
"license": "MIT",
"dependencies": {
"async-mutex": "^0.3.2"
}
}

4
src/api/js/scripts/async-fns.js → src/api/js/scripts/async-fns.ts
View file

@ -1,8 +1,6 @@
'use strict';
// things which you probably want to do off-thread
// from https://github.com/Z3Prover/z3/issues/5746#issuecomment-1006289146
module.exports = [
export const asyncFuncs = [
'Z3_eval_smtlib2_string',
'Z3_simplify',
'Z3_simplify_ex',

77
src/api/js/scripts/build-wasm.ts Normal file
View file

@ -0,0 +1,77 @@
import assert from 'assert';
import { SpawnOptions, spawnSync as originalSpawnSync } from 'child_process';
import fs, { existsSync } from 'fs';
import os from 'os';
import path from 'path';
import process from 'process';
import { asyncFuncs } from './async-fns';
import { makeCCWrapper } from './make-cc-wrapper';
import { functions } from './parse-api';
console.log('--- Building WASM');
const SWAP_OPTS: SpawnOptions = {
shell: true,
stdio: 'inherit',
env: {
...process.env,
CXXFLAGS: '-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0',
LDFLAGS: '-s WASM_BIGINT -s -pthread -s USE_PTHREADS=1',
FPMATH_ENABLED: 'False', // Until Safari supports WASM SSE, we have to disable fast FP support
// TODO(ritave): Setting EM_CACHE breaks compiling on M1 MacBook
//EM_CACHE: path.join(os.homedir(), '.emscripten/'),
},
};
function spawnSync(command: string, opts: SpawnOptions = {}) {
console.log(`- ${command}`);
// TODO(ritave): Create a splitter that keeps track of quoted strings
const [cmd, ...args] = command.split(' ');
const { error, ...rest } = originalSpawnSync(cmd, args, { ...SWAP_OPTS, ...opts });
if (error !== undefined || rest.status !== 0) {
if (error !== undefined) {
console.error(error.message);
} else {
console.error(`Process exited with status ${rest.status}`);
}
process.exit(1);
}
return rest;
}
function exportedFuncs(): string[] {
const extras = ['_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFuncs.map(f => '_async_' + f)];
// TODO(ritave): This variable is unused in original script, find out if it's important
const fns: any[] = (functions as any[]).filter(f => !asyncFuncs.includes(f.name));
return [...extras, ...(functions as any[]).map(f => '_' + f.name)];
}
assert(fs.existsSync('./package.json'), 'Not in the root directory of js api');
const z3RootDir = path.join(process.cwd(), '../../../');
// TODO(ritave): Detect if it's in the configuration we need
if (!existsSync(path.join(z3RootDir, 'build/Makefile'))) {
spawnSync('emconfigure python scripts/mk_make.py --staticlib --single-threaded --arm64=false', {
cwd: z3RootDir,
});
}
spawnSync(`emmake make -j${os.cpus().length} libz3.a`, { cwd: path.join(z3RootDir, 'build') });
const ccWrapperPath = 'build/async-fns.cc';
console.log(`- Building ${ccWrapperPath}`);
fs.mkdirSync(path.dirname(ccWrapperPath), { recursive: true });
fs.writeFileSync(ccWrapperPath, makeCCWrapper());
const fns = JSON.stringify(exportedFuncs());
const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
const libz3a = path.normalize('../../../build/libz3.a');
spawnSync(
`emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js`,
);
fs.rmSync(ccWrapperPath);
console.log('--- WASM build finished');

11
src/api/js/scripts/list-exports.js
View file

@ -1,11 +0,0 @@
'use strict';
// this is called by build.sh to generate the names of the bindings to export
let { functions } = require('./parse-api.js');
let asyncFns = require('./async-fns.js');
let extras = asyncFns.map(f => '_async_' + f);
let fns = functions.filter(f => !asyncFns.includes(f.name));
console.log(JSON.stringify([...extras, ...functions.map(f => '_' + f.name)]));

82
src/api/js/scripts/make-cc-wrapper.js
View file

@ -1,82 +0,0 @@
'use strict';
// generates c wrappers with off-thread versions of specified functions
let path = require('path');
let { functions } = require('./parse-api.js');
let asyncFns = require('./async-fns.js');
let wrappers = [];
for (let fnName of asyncFns) {
let fn = functions.find(f => f.name === fnName);
if (fn == null) {
throw new Error(`could not find definition for ${fnName}`);
}
let wrapper;
if (fn.cRet === 'Z3_string') {
wrapper = `wrapper_str`;
} else if (['int', 'unsigned', 'void'].includes(fn.cRet) || fn.cRet.startsWith('Z3_')) {
wrapper = `wrapper`;
} else {
throw new Error(`async function with unknown return type ${fn.cRet}`);
}
wrappers.push(
`
extern "C" void async_${fn.name}(${fn.params
.map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
.join(', ')}) {
${wrapper}<decltype(&${fn.name}), &${fn.name}>(${fn.params.map(p => `${p.name}`).join(', ')});
}
`.trim(),
);
}
console.log(`// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
// DO NOT EDIT IT BY HAND
#include <thread>
#include <emscripten.h>
#include "../../z3.h"
template<typename Fn, Fn fn, typename... Args>
void wrapper(Args&&... args) {
std::thread t([...args = std::forward<Args>(args)] {
try {
auto result = fn(args...);
MAIN_THREAD_ASYNC_EM_ASM({
resolve_async($0);
}, result);
} catch (...) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async('failed with unknown exception');
});
throw;
}
});
t.detach();
}
template<typename Fn, Fn fn, typename... Args>
void wrapper_str(Args&&... args) {
std::thread t([...args = std::forward<Args>(args)] {
try {
auto result = fn(args...);
MAIN_THREAD_ASYNC_EM_ASM({
resolve_async(UTF8ToString($0));
}, result);
} catch (...) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async('failed with unknown exception');
});
throw;
}
});
t.detach();
}
${wrappers.join('\n\n')}`);

119
src/api/js/scripts/make-cc-wrapper.ts Normal file
View file

@ -0,0 +1,119 @@
// generates c wrappers with off-thread versions of specified functions
import path from 'path';
import { asyncFuncs } from './async-fns';
import { functions } from './parse-api';
export function makeCCWrapper() {
let wrappers = [];
for (let fnName of asyncFuncs) {
let fn = functions.find(f => f.name === fnName);
if (fn == null) {
throw new Error(`could not find definition for ${fnName}`);
}
let wrapper;
if (fn.cRet === 'Z3_string') {
wrapper = `wrapper_str`;
} else if (['int', 'unsigned', 'void'].includes(fn.cRet) || fn.cRet.startsWith('Z3_')) {
wrapper = `wrapper`;
} else {
throw new Error(`async function with unknown return type ${fn.cRet}`);
}
wrappers.push(
`
extern "C" void async_${fn.name}(${fn.params
.map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
.join(', ')}) {
${wrapper}<decltype(&${fn.name}), &${fn.name}>(${fn.params.map(p => `${p.name}`).join(', ')});
}
`.trim(),
);
}
return `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
// DO NOT EDIT IT BY HAND
#include <thread>
#include <emscripten.h>
#include "../../z3.h"
template<typename Fn, Fn fn, typename... Args>
void wrapper(Args&&... args) {
std::thread t([...args = std::forward<Args>(args)] {
try {
auto result = fn(args...);
MAIN_THREAD_ASYNC_EM_ASM({
resolve_async($0);
}, result);
} catch (std::exception& e) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async(new Error(UTF8ToString($0)));
}, e.what());
} catch (...) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async('failed with unknown exception');
});
}
});
t.detach();
}
template<typename Fn, Fn fn, typename... Args>
void wrapper_str(Args&&... args) {
std::thread t([...args = std::forward<Args>(args)] {
try {
auto result = fn(args...);
MAIN_THREAD_ASYNC_EM_ASM({
resolve_async(UTF8ToString($0));
}, result);
} catch (std::exception& e) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async(new Error(UTF8ToString($0)));
}, e.what());
} catch (...) {
MAIN_THREAD_ASYNC_EM_ASM({
reject_async(new Error('failed with unknown exception'));
});
}
});
t.detach();
}
class Z3Exception : public std::exception {
public:
const std::string m_msg;
Z3Exception(const std::string& msg) : m_msg(msg) {}
virtual const char* what() const throw () {
return m_msg.c_str();
}
};
void throwy_error_handler(Z3_context ctx, Z3_error_code c) {
throw Z3Exception(Z3_get_error_msg(ctx, c));
}
void noop_error_handler(Z3_context ctx, Z3_error_code c) {
// pass
}
extern "C" void set_throwy_error_handler(Z3_context ctx) {
Z3_set_error_handler(ctx, throwy_error_handler);
}
extern "C" void set_noop_error_handler(Z3_context ctx) {
Z3_set_error_handler(ctx, noop_error_handler);
}
${wrappers.join('\n\n')}
`;
}
if (require.main === module) {
console.log(makeCCWrapper());
}

422
src/api/js/scripts/make-ts-wrapper.js
View file

@ -1,422 +0,0 @@
'use strict';
let path = require('path');
let prettier = require('prettier');
let { primitiveTypes, types, enums, functions } = require('./parse-api.js');
let asyncFns = require('./async-fns.js');
let subtypes = {
__proto__: null,
Z3_sort: 'Z3_ast',
Z3_func_decl: 'Z3_ast',
};
let makePointerType = t =>
`export type ${t} = ` + (t in subtypes ? `Subpointer<'${t}', '${subtypes[t]}'>;` : `Pointer<'${t}'>;`);
// this supports a up to 6 out intergers/pointers
// or up to 3 out int64s
const BYTES_TO_ALLOCATE_FOR_OUT_PARAMS = 24;
function toEmType(type) {
if (type in primitiveTypes) {
type = primitiveTypes[type];
}
if (['boolean', 'number', 'string', 'bigint', 'void'].includes(type)) {
return type;
}
if (type.startsWith('Z3_')) {
return 'number';
}
throw new Error(`unknown parameter type ${type}`);
}
function isZ3PointerType(type) {
return type.startsWith('Z3_');
}
function toEm(p) {
if (typeof p === 'string') {
// we've already set this, e.g. by replacing it with an expression
return p;
}
let { type } = p;
if (p.kind === 'out') {
throw new Error(`unknown out parameter type ${JSON.stringify(p)}`);
}
if (p.isArray) {
if (isZ3PointerType(type) || type === 'unsigned' || type === 'int') {
// this works for nullables also because null coerces to 0
return `intArrayToByteArr(${p.name} as unknown as number[])`;
} else if (type === 'boolean') {
return `boolArrayToByteArr(${p.name})`;
} else {
throw new Error(`only know how to deal with arrays of int/bool (got ${type})`);
}
}
if (type in primitiveTypes) {
type = primitiveTypes[type];
}
if (['boolean', 'number', 'bigint', 'string'].includes(type)) {
return p.name;
}
if (type.startsWith('Z3_')) {
return p.name;
}
throw new Error(`unknown parameter type ${JSON.stringify(p)}`);
}
let isInParam = p => ['in', 'in_array'].includes(p.kind);
function wrapFunction(fn) {
let inParams = fn.params.filter(isInParam);
let outParams = fn.params.map((p, idx) => ({ ...p, idx })).filter(p => !isInParam(p));
// we'll figure out how to deal with these cases later
let unknownInParam = inParams.find(
p =>
p.isPtr ||
p.type === 'Z3_char_ptr' ||
(p.isArray && !(isZ3PointerType(p.type) || p.type === 'unsigned' || p.type === 'int' || p.type === 'boolean')),
);
if (unknownInParam) {
console.error(`skipping ${fn.name} - unknown in parameter ${JSON.stringify(unknownInParam)}`);
return null;
}
if (fn.ret === 'Z3_char_ptr') {
console.error(`skipping ${fn.name} - returns a string or char pointer`);
return null;
}
// console.error(fn.name);
let isAsync = asyncFns.includes(fn.name);
let trivial =
!['string', 'boolean'].includes(fn.ret) &&
!fn.nullableRet &&
outParams.length === 0 &&
!inParams.some(p => p.type === 'string' || p.isArray || p.nullable);
let name = fn.name.startsWith('Z3_') ? fn.name.substring(3) : fn.name;
let params = inParams.map(p => {
let type = p.type;
if (p.isArray && p.nullable) {
type = `(${type} | null)[]`;
} else if (p.isArray) {
type = `${type}[]`;
} else if (p.nullable) {
type = `${type} | null`;
}
return `${p.name}: ${type}`;
});
if (trivial && isAsync) {
// i.e. and async
return `${name}: function (${params.join(', ')}): Promise<${fn.ret}> {
return Mod.async_call(Mod._async_${fn.name}, ${fn.params.map(toEm).join(', ')});
}`;
}
if (trivial) {
return `${name}: Mod._${fn.name} as ((${params.join(', ')}) => ${fn.ret})`;
}
// otherwise fall back to ccall
let ctypes = fn.params.map(p =>
p.kind === 'in_array' ? 'array' : p.kind === 'out_array' ? 'number' : p.isPtr ? 'number' : toEmType(p.type),
);
let prefix = '';
let infix = '';
let rv = 'ret';
let suffix = '';
let args = fn.params;
let arrayLengthParams = new Map();
for (let p of inParams) {
if (p.nullable && !p.isArray) {
// this would be easy to implement - just map null to 0 - but nothing actually uses nullable non-array input parameters, so we can't ensure we've done it right
console.error(`skipping ${fn.name} - nullable input parameter`);
return null;
}
if (!p.isArray) {
continue;
}
let { sizeIndex } = p;
if (arrayLengthParams.has(sizeIndex)) {
let otherParam = arrayLengthParams.get(sizeIndex);
prefix += `
if (${otherParam}.length !== ${p.name}.length) {
throw new TypeError(\`${otherParam} and ${p.name} must be the same length (got \${${otherParam}.length} and \{${p.name}.length})\`);
}
`.trim();
continue;
}
arrayLengthParams.set(sizeIndex, p.name);
let sizeParam = fn.params[sizeIndex];
if (!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)) {
throw new Error(
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
);
}
args[sizeIndex] = `${p.name}.length`;
params[sizeIndex] = null;
}
let returnType = fn.ret;
let cReturnType = toEmType(fn.ret);
if (outParams.length > 0) {
let mapped = [];
let memIdx = 0; // offset from `outAddress` where the data should get written, in units of 4 bytes
for (let outParam of outParams) {
if (outParam.isArray) {
if (isZ3PointerType(outParam.type) || outParam.type === 'unsigned') {
let { sizeIndex } = outParam;
let count;
if (arrayLengthParams.has(sizeIndex)) {
// i.e. this is also the length of an input array
count = args[sizeIndex];
} else {
let sizeParam = fn.params[sizeIndex];
if (!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)) {
throw new Error(
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
);
}
count = sizeParam.name;
}
let outArrayAddress = `outArray_${outParam.name}`;
prefix += `
let ${outArrayAddress} = Mod._malloc(4 * ${count});
try {
`.trim();
suffix =
`
} finally {
Mod._free(${outArrayAddress});
}
`.trim() + suffix;
args[outParam.idx] = outArrayAddress;
mapped.push({
name: outParam.name,
read:
`readUintArray(${outArrayAddress}, ${count})` +
(outParam.type === 'unsigned' ? '' : `as unknown as ${outParam.type}[]`),
type: `${outParam.type}[]`,
});
} else {
console.error(`skipping ${fn.name} - out array of ${outParam.type}`);
return null;
}
} else if (outParam.isPtr) {
function setArg() {
args[outParam.idx] = memIdx === 0 ? 'outAddress' : `outAddress + ${memIdx * 4}`;
}
let read, type;
if (outParam.type === 'string') {
read = `Mod.UTF8ToString(getOutUint(${memIdx}))`;
setArg();
++memIdx;
} else if (isZ3PointerType(outParam.type)) {
read = `getOutUint(${memIdx}) as unknown as ${outParam.type}`;
setArg();
++memIdx;
} else if (outParam.type === 'unsigned') {
read = `getOutUint(${memIdx})`;
setArg();
++memIdx;
} else if (outParam.type === 'int') {
read = `getOutInt(${memIdx})`;
setArg();
++memIdx;
} else if (outParam.type === 'uint64_t') {
if (memIdx % 2 === 1) {
++memIdx;
}
read = `getOutUint64(${memIdx / 2})`;
setArg();
memIdx += 2;
} else if (outParam.type === 'int64_t') {
if (memIdx % 2 === 1) {
++memIdx;
}
read = `getOutInt64(${memIdx / 2})`;
setArg();
memIdx += 2;
} else {
console.error(`skipping ${fn.name} - unknown out parameter type ${outParam.type}`);
return null;
}
if (memIdx > Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / 4)) {
// prettier-ignore
console.error(`skipping ${fn.name} - out parameter sizes sum to ${memIdx * 4}, which is > ${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS}`);
return null;
}
mapped.push({
name: outParam.name,
read,
type: outParam.type,
});
} else {
console.error(`skipping ${fn.name} - out param is neither pointer nor array`);
return null;
}
}
let ignoreReturn = fn.ret === 'boolean' || fn.ret === 'void';
if (outParams.length === 1) {
let outParam = mapped[0];
if (ignoreReturn) {
returnType = outParam.type;
rv = outParam.read;
} else {
returnType = `{ rv: ${fn.ret}, ${outParam.name} : ${outParam.type} }`;
rv = `{ rv: ret, ${outParam.name} : ${outParam.read} }`;
}
} else {
if (ignoreReturn) {
returnType = `{ ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
rv = `{ ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
} else {
returnType = `{ rv: ${fn.ret}, ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
rv = `{ rv: ret, ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
}
}
if (fn.ret === 'boolean') {
// assume the boolean indicates success
infix += `
if (!ret) {
return null;
}
`.trim();
cReturnType = 'boolean';
returnType += ' | null';
} else if (fn.ret === 'void') {
cReturnType = 'void';
} else if (isZ3PointerType(fn.ret) || fn.ret === 'unsigned') {
cReturnType = 'number';
} else {
console.error(`skipping ${fn.name} - out parameter for function which returns non-boolean`);
return null;
}
}
if (fn.nullableRet) {
returnType += ' | null';
infix += `
if (ret === 0) {
return null;
}
`.trim();
}
if (isAsync) {
}
// prettier-ignore
let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`;
if (isAsync) {
invocation = `await Mod.async_call(() => ${invocation})`;
returnType = `Promise<${returnType}>`;
}
let out = `${name}: ${isAsync ? 'async' : ''} function(${params.filter(p => p != null).join(', ')}): ${returnType} {
${prefix}`;
if (infix === '' && suffix === '' && rv === 'ret') {
out += `return ${invocation};`;
} else {
out += `
let ret = ${invocation};
${infix}return ${rv};${suffix}
`.trim();
}
out += '}';
return out;
}
function wrapEnum(name, values) {
let enumEntries = Object.entries(values);
return `export enum ${name} {
${enumEntries.map(([k, v], i) => k + (v === (enumEntries[i - 1]?.[1] ?? -1) + 1 ? '' : ` = ${v}`) + ',').join('\n')}
};`;
}
function getValidOutArrayIndexes(size) {
return Array.from({ length: Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / size) }, (_, i) => i).join(' | ');
}
let out = `
// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
// DO NOT EDIT IT BY HAND
// @ts-ignore no-implicit-any
import initModule = require('./z3-built.js');
interface Pointer<T extends string> extends Number {
readonly __typeName: T;
}
interface Subpointer<T extends string, S extends string> extends Pointer<S> {
readonly __typeName2: T;
}
${Object.entries(primitiveTypes)
.filter(e => e[0] !== 'void')
.map(e => `type ${e[0]} = ${e[1]};`)
.join('\n')}
${Object.keys(types)
.filter(k => k.startsWith('Z3'))
.map(makePointerType)
.join('\n')}
${Object.entries(enums)
.map(e => wrapEnum(e[0], e[1]))
.join('\n\n')}
export async function init() {
let Mod = await initModule();
// this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array
function intArrayToByteArr(ints: number[]) {
return new Uint8Array((new Uint32Array(ints)).buffer);
}
function boolArrayToByteArr(bools: boolean[]) {
return bools.map(b => b ? 1 : 0);
}
function readUintArray(address: number, count: number) {
return Array.from(new Uint32Array(Mod.HEAPU32.buffer, address, count));
}
let outAddress = Mod._malloc(${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS});
let outUintArray = (new Uint32Array(Mod.HEAPU32.buffer, outAddress, 4));
let getOutUint = (i: ${getValidOutArrayIndexes(4)}) => outUintArray[i];
let outIntArray = (new Int32Array(Mod.HEAPU32.buffer, outAddress, 4));
let getOutInt = (i: ${getValidOutArrayIndexes(4)}) => outIntArray[i];
let outUint64Array = (new BigUint64Array(Mod.HEAPU32.buffer, outAddress, 2));
let getOutUint64 = (i: ${getValidOutArrayIndexes(8)}) => outUint64Array[i];
let outInt64Array = (new BigInt64Array(Mod.HEAPU32.buffer, outAddress, 2));
let getOutInt64 = (i: ${getValidOutArrayIndexes(8)}) => outInt64Array[i];
return {
em: Mod,
Z3: {
${functions
.map(wrapFunction)
.filter(f => f != null)
.join(',\n')}
}
};
}
`;
console.log(prettier.format(out, { singleQuote: true, parser: 'typescript' }));

468
src/api/js/scripts/make-ts-wrapper.ts Normal file
View file

@ -0,0 +1,468 @@
import assert from 'assert';
import fs from 'fs';
import path from 'path';
import prettier from 'prettier';
import { asyncFuncs } from './async-fns';
import { enums, Func, FuncParam, functions, primitiveTypes, types } from './parse-api';
assert(process.argv.length === 4, `Usage: ${process.argv[0]} ${process.argv[1]} wrapperFilePath typesFilePath`);
const wrapperFilePath = process.argv[2];
const typesFilePath = process.argv[3];
function makeTsWrapper() {
const subtypes = {
__proto__: null,
Z3_sort: 'Z3_ast',
Z3_func_decl: 'Z3_ast',
} as unknown as Record<string, string>;
const makePointerType = (t: string) =>
`export type ${t} = ` + (t in subtypes ? `Subpointer<'${t}', '${subtypes[t]}'>;` : `Pointer<'${t}'>;`);
// this supports a up to 6 out integers/pointers
// or up to 3 out int64s
const BYTES_TO_ALLOCATE_FOR_OUT_PARAMS = 24;
const CUSTOM_IMPLEMENTATIONS = ['Z3_mk_context', 'Z3_mk_context_rc'];
function toEmType(type: string) {
if (type in primitiveTypes) {
type = primitiveTypes[type];
}
if (['boolean', 'number', 'string', 'bigint', 'void'].includes(type)) {
return type;
}
if (type.startsWith('Z3_')) {
return 'number';
}
throw new Error(`unknown parameter type ${type}`);
}
function isZ3PointerType(type: string) {
return type.startsWith('Z3_');
}
function toEm(p: string | FuncParam) {
if (typeof p === 'string') {
// we've already set this, e.g. by replacing it with an expression
return p;
}
let { type } = p;
if (p.kind === 'out') {
throw new Error(`unknown out parameter type ${JSON.stringify(p)}`);
}
if (p.isArray) {
if (isZ3PointerType(type) || type === 'unsigned' || type === 'int') {
// this works for nullables also because null coerces to 0
return `intArrayToByteArr(${p.name} as unknown as number[])`;
} else if (type === 'boolean') {
return `boolArrayToByteArr(${p.name})`;
} else {
throw new Error(`only know how to deal with arrays of int/bool (got ${type})`);
}
}
if (type in primitiveTypes) {
type = primitiveTypes[type];
}
if (['boolean', 'number', 'bigint', 'string'].includes(type)) {
return p.name;
}
if (type.startsWith('Z3_')) {
return p.name;
}
throw new Error(`unknown parameter type ${JSON.stringify(p)}`);
}
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;
}
let inParams = fn.params.filter(isInParam);
let outParams = fn.params.map((p, idx) => ({ ...p, idx })).filter(p => !isInParam(p));
// we'll figure out how to deal with these cases later
let unknownInParam = inParams.find(
p =>
p.isPtr ||
p.type === 'Z3_char_ptr' ||
(p.isArray && !(isZ3PointerType(p.type) || p.type === 'unsigned' || p.type === 'int' || p.type === 'boolean')),
);
if (unknownInParam) {
console.error(`skipping ${fn.name} - unknown in parameter ${JSON.stringify(unknownInParam)}`);
return null;
}
if (fn.ret === 'Z3_char_ptr') {
console.error(`skipping ${fn.name} - returns a string or char pointer`);
return null;
}
// console.error(fn.name);
let isAsync = asyncFuncs.includes(fn.name);
let trivial =
!['string', 'boolean'].includes(fn.ret) &&
!fn.nullableRet &&
outParams.length === 0 &&
!inParams.some(p => p.type === 'string' || p.isArray || p.nullable);
let name = fn.name.startsWith('Z3_') ? fn.name.substring(3) : fn.name;
const params: (string | null)[] = inParams.map(p => {
let type = p.type;
if (p.isArray && p.nullable) {
type = `(${type} | null)[]`;
} else if (p.isArray) {
type = `${type}[]`;
} else if (p.nullable) {
type = `${type} | null`;
}
return `${p.name}: ${type}`;
});
if (trivial && isAsync) {
// i.e. and async
return `${name}: function (${params.join(', ')}): Promise<${fn.ret}> {
return Mod.async_call(Mod._async_${fn.name}, ${fn.params.map(toEm).join(', ')});
}`;
}
if (trivial) {
return `${name}: Mod._${fn.name} as ((${params.join(', ')}) => ${fn.ret})`;
}
// otherwise fall back to ccall
const ctypes = fn.params.map(p =>
p.kind === 'in_array' ? 'array' : p.kind === 'out_array' ? 'number' : p.isPtr ? 'number' : toEmType(p.type),
);
let prefix = '';
let infix = '';
let rv = 'ret';
let suffix = '';
const args: (string | FuncParam)[] = fn.params;
let arrayLengthParams = new Map();
for (let p of inParams) {
if (p.nullable && !p.isArray) {
// this would be easy to implement - just map null to 0 - but nothing actually uses nullable non-array input parameters, so we can't ensure we've done it right
console.error(`skipping ${fn.name} - nullable input parameter`);
return null;
}
if (!p.isArray) {
continue;
}
let { sizeIndex } = p;
assert(sizeIndex !== undefined);
if (arrayLengthParams.has(sizeIndex)) {
let otherParam = arrayLengthParams.get(sizeIndex);
prefix += `
if (${otherParam}.length !== ${p.name}.length) {
throw new TypeError(\`${otherParam} and ${p.name} must be the same length (got \${${otherParam}.length} and \{${p.name}.length})\`);
}
`.trim();
continue;
}
arrayLengthParams.set(sizeIndex, p.name);
const sizeParam = fn.params[sizeIndex];
if (!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)) {
throw new Error(
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
);
}
args[sizeIndex] = `${p.name}.length`;
params[sizeIndex] = null;
}
let returnType = fn.ret;
let cReturnType = toEmType(fn.ret);
if (outParams.length > 0) {
let mapped = [];
let memIdx = 0; // offset from `outAddress` where the data should get written, in units of 4 bytes
for (let outParam of outParams) {
if (outParam.isArray) {
if (isZ3PointerType(outParam.type) || outParam.type === 'unsigned') {
let { sizeIndex } = outParam;
assert(sizeIndex !== undefined);
let count;
if (arrayLengthParams.has(sizeIndex)) {
// i.e. this is also the length of an input array
count = args[sizeIndex];
} else {
let sizeParam = fn.params[sizeIndex];
if (
!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)
) {
throw new Error(
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
);
}
count = sizeParam.name;
}
let outArrayAddress = `outArray_${outParam.name}`;
prefix += `
let ${outArrayAddress} = Mod._malloc(4 * ${count});
try {
`.trim();
suffix =
`
} finally {
Mod._free(${outArrayAddress});
}
`.trim() + suffix;
args[outParam.idx] = outArrayAddress;
mapped.push({
name: outParam.name,
read:
`readUintArray(${outArrayAddress}, ${count})` +
(outParam.type === 'unsigned' ? '' : `as unknown as ${outParam.type}[]`),
type: `${outParam.type}[]`,
});
} else {
console.error(`skipping ${fn.name} - out array of ${outParam.type}`);
return null;
}
} else if (outParam.isPtr) {
function setArg() {
args[outParam.idx] = memIdx === 0 ? 'outAddress' : `outAddress + ${memIdx * 4}`;
}
let read, type;
if (outParam.type === 'string') {
read = `Mod.UTF8ToString(getOutUint(${memIdx}))`;
setArg();
++memIdx;
} else if (isZ3PointerType(outParam.type)) {
read = `getOutUint(${memIdx}) as unknown as ${outParam.type}`;
setArg();
++memIdx;
} else if (outParam.type === 'unsigned') {
read = `getOutUint(${memIdx})`;
setArg();
++memIdx;
} else if (outParam.type === 'int') {
read = `getOutInt(${memIdx})`;
setArg();
++memIdx;
} else if (outParam.type === 'uint64_t') {
if (memIdx % 2 === 1) {
++memIdx;
}
read = `getOutUint64(${memIdx / 2})`;
setArg();
memIdx += 2;
} else if (outParam.type === 'int64_t') {
if (memIdx % 2 === 1) {
++memIdx;
}
read = `getOutInt64(${memIdx / 2})`;
setArg();
memIdx += 2;
} else {
console.error(`skipping ${fn.name} - unknown out parameter type ${outParam.type}`);
return null;
}
if (memIdx > Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / 4)) {
// prettier-ignore
console.error(`skipping ${fn.name} - out parameter sizes sum to ${memIdx * 4}, which is > ${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS}`);
return null;
}
mapped.push({
name: outParam.name,
read,
type: outParam.type,
});
} else {
console.error(`skipping ${fn.name} - out param is neither pointer nor array`);
return null;
}
}
let ignoreReturn = fn.ret === 'boolean' || fn.ret === 'void';
if (outParams.length === 1) {
let outParam = mapped[0];
if (ignoreReturn) {
returnType = outParam.type;
rv = outParam.read;
} else {
returnType = `{ rv: ${fn.ret}, ${outParam.name} : ${outParam.type} }`;
rv = `{ rv: ret, ${outParam.name} : ${outParam.read} }`;
}
} else {
if (ignoreReturn) {
returnType = `{ ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
rv = `{ ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
} else {
returnType = `{ rv: ${fn.ret}, ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
rv = `{ rv: ret, ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
}
}
if (fn.ret === 'boolean') {
// assume the boolean indicates success
infix += `
if (!ret) {
return null;
}
`.trim();
cReturnType = 'boolean';
returnType += ' | null';
} else if (fn.ret === 'void') {
cReturnType = 'void';
} else if (isZ3PointerType(fn.ret) || fn.ret === 'unsigned') {
cReturnType = 'number';
} else {
console.error(`skipping ${fn.name} - out parameter for function which returns non-boolean`);
return null;
}
}
if (fn.nullableRet) {
returnType += ' | null';
infix += `
if (ret === 0) {
return null;
}
`.trim();
}
// prettier-ignore
let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`;
if (isAsync) {
invocation = `await Mod.async_call(() => ${invocation})`;
returnType = `Promise<${returnType}>`;
}
let out = `${name}: ${isAsync ? 'async' : ''} function(${params.filter(p => p != null).join(', ')}): ${returnType} {
${prefix}`;
if (infix === '' && suffix === '' && rv === 'ret') {
out += `return ${invocation};`;
} else {
out += `
let ret = ${invocation};
${infix}return ${rv};${suffix}
`.trim();
}
out += '}';
return out;
}
function wrapEnum(name: string, values: Record<string, number>) {
let enumEntries = Object.entries(values);
return `export enum ${name} {
${enumEntries.map(([k, v], i) => k + (v === (enumEntries[i - 1]?.[1] ?? -1) + 1 ? '' : ` = ${v}`) + ',').join('\n')}
};`;
}
function getValidOutArrayIndexes(size: number) {
return Array.from({ length: Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / size) }, (_, i) => i).join(' | ');
}
const typesDocument = `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
// DO NOT EDIT IT BY HAND
interface Pointer<T extends string> extends Number {
readonly __typeName: T;
}
interface Subpointer<T extends string, S extends string> extends Pointer<S> {
readonly __typeName2: T;
}
${Object.keys(types)
.filter(k => k.startsWith('Z3'))
.map(makePointerType)
.join('\n')}
${Object.entries(enums)
.map(e => wrapEnum(e[0], e[1]))
.join('\n\n')}
`;
const relativePath: string = path.relative(path.dirname(wrapperFilePath), path.dirname(typesFilePath)) || './';
const ext: string = path.extname(typesFilePath);
const basename: string = path.basename(typesFilePath);
const importPath = relativePath + basename.slice(0, -ext.length);
const wrapperDocument = `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
// DO NOT EDIT IT BY HAND
import {
${Object.keys(types)
.filter(k => k.startsWith('Z3'))
.join(',\n')},
${Object.keys(enums).join(',\n')},
} from '${importPath}';
${Object.entries(primitiveTypes)
.filter(e => e[0] !== 'void')
.map(e => `type ${e[0]} = ${e[1]};`)
.join('\n')}
export async function init(initModule: any) {
let Mod = await initModule();
// this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array
function intArrayToByteArr(ints: number[]) {
return new Uint8Array((new Uint32Array(ints)).buffer);
}
function boolArrayToByteArr(bools: boolean[]) {
return bools.map(b => b ? 1 : 0);
}
function readUintArray(address: number, count: number) {
return Array.from(new Uint32Array(Mod.HEAPU32.buffer, address, count));
}
let outAddress = Mod._malloc(${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS});
let outUintArray = (new Uint32Array(Mod.HEAPU32.buffer, outAddress, 4));
let getOutUint = (i: ${getValidOutArrayIndexes(4)}) => outUintArray[i];
let outIntArray = (new Int32Array(Mod.HEAPU32.buffer, outAddress, 4));
let getOutInt = (i: ${getValidOutArrayIndexes(4)}) => outIntArray[i];
let outUint64Array = (new BigUint64Array(Mod.HEAPU32.buffer, outAddress, 2));
let getOutUint64 = (i: ${getValidOutArrayIndexes(8)}) => outUint64Array[i];
let outInt64Array = (new BigInt64Array(Mod.HEAPU32.buffer, outAddress, 2));
let getOutInt64 = (i: ${getValidOutArrayIndexes(8)}) => outInt64Array[i];
return {
em: Mod,
Z3: {
mk_context: function(c: Z3_config): Z3_context {
let ctx = Mod._Z3_mk_context(c);
Mod._set_noop_error_handler(ctx);
return ctx;
},
mk_context_rc: function(c: Z3_config): Z3_context {
let ctx = Mod._Z3_mk_context_rc(c);
Mod._set_noop_error_handler(ctx);
return ctx;
},
${functions
.map(wrapFunction)
.filter(f => f != null)
.join(',\n')}
}
};
}
`;
return {
wrapperDocument: prettier.format(wrapperDocument, { singleQuote: true, parser: 'typescript' }),
typesDocument: prettier.format(typesDocument, { singleQuote: true, parser: 'typescript' }),
};
}
const { wrapperDocument, typesDocument } = makeTsWrapper();
fs.mkdirSync(path.dirname(wrapperFilePath), { recursive: true });
fs.writeFileSync(wrapperFilePath, wrapperDocument);
fs.mkdirSync(path.dirname(typesFilePath), { recursive: true });
fs.writeFileSync(typesFilePath, typesDocument);

93
src/api/js/scripts/parse-api.js → src/api/js/scripts/parse-api.ts
View file

@ -1,9 +1,8 @@
'use strict';
import assert from 'assert';
import fs from 'fs';
import path from 'path';
let fs = require('fs');
let path = require('path');
let files = [
const files = [
'z3_api.h',
'z3_algebraic.h',
'z3_ast_containers.h',
@ -15,15 +14,15 @@ let files = [
'z3_spacer.h',
];
let aliases = {
const aliases = {
__proto__: null,
Z3_bool: 'boolean',
Z3_string: 'string',
bool: 'boolean',
signed: 'int',
};
} as unknown as Record<string, string>;
let primitiveTypes = {
const primitiveTypes = {
__proto__: null,
Z3_char_ptr: 'string',
unsigned: 'number',
@ -32,18 +31,18 @@ let primitiveTypes = {
int64_t: 'bigint',
double: 'number',
float: 'number',
};
} as unknown as Record<string, string>;
let optTypes = {
const optTypes = {
__proto__: null,
Z3_sort_opt: 'Z3_sort',
Z3_ast_opt: 'Z3_ast',
Z3_func_interp_opt: 'Z3_func_interp',
};
} as unknown as Record<string, string>;
// parse type declarations
let types = {
const types = {
__proto__: null,
// these are function types I can't be bothered to parse
@ -55,11 +54,26 @@ let types = {
Z3_eq_eh: 'Z3_eq_eh',
Z3_final_eh: 'Z3_final_eh',
Z3_created_eh: 'Z3_created_eh',
};
Z3_decide_eh: 'Z3_decide_eh',
} as unknown as Record<string, string>;
let defApis = Object.create(null);
let functions = [];
let enums = Object.create(null);
export type ApiParam = { kind: string; sizeIndex?: number; type: string };
export type Api = { params: ApiParam[]; ret: string; extra: boolean };
const defApis: Record<string, Api> = Object.create(null);
export type FuncParam = {
type: string;
cType: string;
name: string;
isConst: boolean;
isPtr: boolean;
isArray: boolean;
nullable: boolean;
kind?: string;
sizeIndex?: number;
};
export type Func = { ret: string; cRet: string; name: string; params: FuncParam[]; nullableRet: boolean };
const functions: Func[] = [];
let enums: Record<string, Record<string, number>> = Object.create(null);
for (let file of files) {
let contents = fs.readFileSync(path.join(__dirname, '..', '..', file), 'utf8');
@ -79,31 +93,40 @@ for (let file of files) {
/def_Type\(\s*'(?<name>[A-Za-z0-9_]+)',\s*'(?<cname>[A-Za-z0-9_]+)',\s*'(?<pname>[A-Za-z0-9_]+)'\)/g,
);
for (let { groups } of typeMatches) {
assert(groups !== undefined);
pytypes[groups.name] = groups.cname;
}
// we don't have to pre-populate the types map with closure types
// use the Z3_DECLARE_CLOSURE to identify closure types
// for (let match of contents.matchAll(/Z3_DECLARE_CLOSURE\((?<type>[A-Za-z0-9_]+),/g)) {
// types[match.groups.type] = match.groups.type
// }
// we filter first to ensure our regex isn't too strict
let apiLines = contents.split('\n').filter(l => /def_API|extra_API/.test(l));
for (let line of apiLines) {
let match = line.match(
/^\s*(?<def>def_API|extra_API) *\(\s*'(?<name>[A-Za-z0-9_]+)'\s*,\s*(?<ret>[A-Za-z0-9_]+)\s*,\s*\((?<params>((_in|_out|_in_array|_out_array|_inout_array)\([^)]+\)\s*,?\s*)*)\)\s*\)\s*$/,
/^\s*(?<def>def_API|extra_API) *\(\s*'(?<name>[A-Za-z0-9_]+)'\s*,\s*(?<ret>[A-Za-z0-9_]+)\s*,\s*\((?<params>((_in|_out|_in_array|_out_array|_fnptr|_inout_array)\([^)]+\)\s*,?\s*)*)\)\s*\)\s*$/,
);
if (match == null) {
if (match === null) {
throw new Error(`failed to match def_API call ${JSON.stringify(line)}`);
}
assert(match.groups !== undefined);
let { name, ret, def } = match.groups;
let params = match.groups.params.trim();
let text = params;
let parsedParams = [];
while (true) {
text = eatWs(text);
({ text, match } = eat(text, /^_(?<kind>in|out|in_array|out_array|inout_array)\(/));
({ text, match } = eat(text, /^_(?<kind>in|out|in_array|out_array|inout_array|fnptr)\(/));
if (match == null) {
break;
}
assert(match.groups !== undefined);
let kind = match.groups.kind;
if (kind === 'inout_array') kind = 'in_array'; // https://github.com/Z3Prover/z3/discussions/5761
if (kind === 'in' || kind === 'out') {
if (kind === 'in' || kind === 'out' || kind == 'fnptr') {
({ text, match } = expect(text, /^[A-Za-z0-9_]+/));
parsedParams.push({ kind, type: match[0] });
} else {
@ -121,7 +144,6 @@ for (let file of files) {
throw new Error(`extra text in parameter list ${JSON.stringify(text)}`);
}
if (name in defApis) {
throw new Error(`multiple defApi calls for ${name}`);
}
@ -129,15 +151,10 @@ for (let file of files) {
}
for (let match of contents.matchAll(/DEFINE_TYPE\((?<type>[A-Za-z0-9_]+)\)/g)) {
assert(match.groups !== undefined);
types[match.groups.type] = match.groups.type;
}
// we don't have to pre-populate the types map with closure types
// use the Z3_DECLARE_CLOSURE to identify closure types
// for (let match of contents.matchAll(/Z3_DECLARE_CLOSURE\((?<type>[A-Za-z0-9_]+),/g)) {
// types[match.groups.type] = match.groups.type
// }
// parse enum declarations
for (let idx = 0; idx < contents.length; ) {
let nextIdx = contents.indexOf('typedef enum', idx);
@ -155,12 +172,13 @@ for (let file of files) {
if (match === null) {
throw new Error(`could not parse enum ${JSON.stringify(slice)}`);
}
let vals = Object.create(null);
let vals: Record<string, number> = Object.create(null);
let next = 0;
while (true) {
let blank = true;
while (blank) {
({ match, text } = eat(text, /^\s*(\/\/[^\n]*\n)?/));
assert(match !== null);
blank = match[0].length > 0;
}
({ match, text } = eat(text, /^[A-Za-z0-9_]+/));
@ -172,6 +190,7 @@ for (let file of files) {
({ match, text } = eat(text, /^= *(?<val>[^\n,\s]+)/));
if (match !== null) {
assert(match.groups !== undefined);
let parsedVal = Number(match.groups.val);
if (Object.is(parsedVal, NaN)) {
throw new Error('unknown value ' + match.groups.val);
@ -221,12 +240,14 @@ for (let file of files) {
if (match == null) {
throw new Error(`failed to match c definition: ${JSON.stringify(slice)}`);
}
assert(match.groups !== undefined);
let { ret, name, params } = match.groups;
let parsedParams = [];
if (params.trim() !== 'void') {
for (let param of params.split(',')) {
let paramType, paramName, isConst, isPtr, isArray;
let paramType: string, paramName: string, isConst: boolean, isPtr: boolean, isArray: boolean;
let { match, text } = eat(param, /^\s*/);
({ match, text } = eat(text, /^[A-Za-z0-9_]+/));
@ -302,7 +323,7 @@ for (let file of files) {
}
}
function isKnownType(t) {
function isKnownType(t: string) {
return t in enums || t in types || t in primitiveTypes || ['string', 'boolean', 'void'].includes(t);
}
@ -339,19 +360,19 @@ for (let fn of functions) {
}
}
function eat(str, regex) {
const match = str.match(regex);
if (match == null) {
function eat(str: string, regex: string | RegExp) {
const match: RegExpMatchArray | null = str.match(regex);
if (match === null) {
return { match, text: str };
}
return { match, text: str.substring(match[0].length) };
}
function eatWs(text) {
function eatWs(text: string) {
return eat(text, /^\s*/).text;
}
function expect(str, regex) {
function expect(str: string, regex: string | RegExp) {
let { text, match } = eat(str, regex);
if (match === null) {
throw new Error(`expected ${regex}, got ${JSON.stringify(text)}`);
@ -359,4 +380,4 @@ function expect(str, regex) {
return { text, match };
}
module.exports = { primitiveTypes, types, enums, functions };
export { primitiveTypes, types, enums, functions };

16
src/api/js/src/browser.ts Normal file
View file

@ -0,0 +1,16 @@
import { createApi, Z3HighLevel } from './high-level';
import { init as initWrapper, Z3LowLevel } from './low-level';
export * from './high-level/types';
export { Z3Core, Z3LowLevel } from './low-level';
export * from './low-level/types.__GENERATED__';
export async function init(): Promise<Z3LowLevel & Z3HighLevel> {
const initZ3 = (global as any).initZ3;
if (initZ3 === undefined) {
throw new Error('initZ3 was not imported correctly. Please consult documentation on how to load Z3 in browser');
}
const lowLevel = await initWrapper(initZ3);
const highLevel = createApi(lowLevel.Z3);
return { ...lowLevel, ...highLevel };
}

450
src/api/js/src/high-level/high-level.test.ts Normal file
View file

@ -0,0 +1,450 @@
import assert from 'assert';
import asyncToArray from 'iter-tools/methods/async-to-array';
import { init, killThreads } from '../jest';
import { Arith, Bool, Model, sat, unsat, Z3AssertionError, Z3HighLevel } from './types';
/**
* Generate all possible solutions from given assumptions.
*
* **NOTE**: The set of solutions might be infinite.
* Always ensure to limit amount generated, either by knowing that the
* solution space is constrainted, or by taking only a specified
* amount of solutions
* ```typescript
* import { sliceAsync } from 'iter-tools';
* // ...
* for await (const model of sliceAsync(10, solver.solutions())) {
* console.log(model.sexpr());
* }
* ```
* @see http://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations
* @returns Models with solutions. Nothing if no constants provided
*/
// TODO(ritave): Use faster solution https://stackoverflow.com/a/70656700
// TODO(ritave): Move to high-level.ts
async function* allSolutions<Name extends string>(...assertions: Bool<Name>[]): AsyncIterable<Model<Name>> {
if (assertions.length === 0) {
return;
}
const { Or } = assertions[0].ctx;
const solver = new assertions[0].ctx.Solver();
solver.add(...assertions);
while ((await solver.check()) === sat) {
const model = solver.model();
const decls = model.decls();
if (decls.length === 0) {
return;
}
yield model;
solver.add(
Or(
...decls
// TODO(ritave): Assert on arity > 0
.filter(decl => decl.arity() === 0)
.map(decl => {
const term = decl.call();
// TODO(ritave): Assert not an array / uinterpeted sort
const value = model.eval(term, true);
return term.neq(value);
}),
),
);
}
}
async function prove(conjecture: Bool): Promise<void> {
const solver = new conjecture.ctx.Solver();
const { Not } = solver.ctx;
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(unsat);
}
async function solve(conjecture: Bool): Promise<Model> {
const solver = new conjecture.ctx.Solver();
solver.add(conjecture);
expect(await solver.check()).toStrictEqual(sat);
return solver.model();
}
describe('high-level', () => {
let api: { em: any } & Z3HighLevel;
beforeAll(async () => {
api = await init();
});
afterAll(async () => {
await killThreads(api.em);
});
it('can set params', () => {
const { setParam, getParam, resetParams } = api;
expect(getParam('pp.decimal')).toStrictEqual('false');
setParam('pp.decimal', 'true');
expect(getParam('pp.decimal')).toStrictEqual('true');
setParam({ 'pp.decimal': 'false', timeout: 4 });
expect(getParam('pp.decimal')).toStrictEqual('false');
expect(getParam('timeout')).toStrictEqual('4');
resetParams();
expect(getParam('pp.decimal')).toStrictEqual('false');
expect(getParam('timeout')).toStrictEqual('4294967295');
});
it('proves x = y implies g(x) = g(y)', async () => {
const { Solver, Int, Function, Implies, Not } = new api.Context('main');
const solver = new Solver();
const sort = Int.sort();
const x = Int.const('x');
const y = Int.const('y');
const g = Function.declare('g', sort, sort);
const conjecture = Implies(x.eq(y), g.call(x).eq(g.call(y)));
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(unsat);
});
it('disproves x = y implies g(g(x)) = g(y)', async () => {
const { Solver, Int, Function, Implies, Not } = new api.Context('main');
const solver = new Solver();
const sort = Int.sort();
const x = Int.const('x');
const y = Int.const('y');
const g = Function.declare('g', sort, sort);
const conjecture = Implies(x.eq(y), g.call(g.call(x)).eq(g.call(y)));
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(sat);
});
it('checks that Context matches', () => {
const c1 = new api.Context('context');
const c2 = new api.Context('context');
const c3 = new api.Context('foo');
const c4 = new api.Context('bar');
// Contexts with the same name don't do type checking during compile time.
// We need to check for different context dynamically
expect(() => c1.Or(c2.Int.val(5).eq(2))).toThrowError(Z3AssertionError);
// On the other hand, this won't compile due to automatic generics
// @ts-expect-error
expect(() => c3.Or(c4.Int.val(5).eq(2))).toThrowError(Z3AssertionError);
const allUniqueContexes = new Set([c1, c2, c3, c4]).size === 4;
expect(allUniqueContexes).toStrictEqual(true);
expect(() => c1.Or(c1.Int.val(5).eq(2))).not.toThrowError();
});
describe('booleans', () => {
it("proves De Morgan's Law", async () => {
const { Bool, Not, And, Eq, Or } = new api.Context('main');
const [x, y] = [Bool.const('x'), Bool.const('y')];
const conjecture = Eq(Not(And(x, y)), Or(Not(x), Not(y)));
await prove(conjecture);
});
});
describe('ints', () => {
it('finds a model', async () => {
const { Solver, Int, isIntVal } = new api.Context('main');
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
solver.add(x.ge(1)); // x >= 1
solver.add(y.lt(x.add(3))); // y < x + 3
expect(await solver.check()).toStrictEqual(sat);
const model = solver.model();
expect(model.length).toStrictEqual(2);
for (const decl of model) {
expect(decl.arity()).toStrictEqual(0);
}
const xValueExpr = model.get(x);
const yValueExpr = model.get(y);
assert(isIntVal(xValueExpr));
assert(isIntVal(yValueExpr));
const xValue = xValueExpr.value;
const yValue = yValueExpr.value;
assert(typeof xValue === 'bigint');
assert(typeof yValue === 'bigint');
expect(xValue).toBeGreaterThanOrEqual(1n);
expect(yValue).toBeLessThanOrEqual(xValue + 3n);
});
// TODO(ritave): After changes made since last commit (a332187c746c23450860deb210d94e6e042dd424),
// this test takes twice as long (from 5s to 10s). Figure out why
it('solves sudoku', async () => {
function toSudoku(data: string): (number | null)[][] {
const cells: (number | null)[][] = Array.from({ length: 9 }, () => Array.from({ length: 9 }, () => null));
const lines = data.trim().split('\n');
for (let row = 0; row < 9; row++) {
const line = lines[row].trim();
for (let col = 0; col < 9; col++) {
const char = line[col];
if (char !== '.') {
cells[row][col] = Number.parseInt(char);
}
}
}
return cells;
}
const INSTANCE = toSudoku(`
....94.3.
...51...7
.89....4.
......2.8
.6.2.1.5.
1.2......
.7....52.
9...65...
.4.97....
`);
const EXPECTED = toSudoku(`
715894632
234516897
689723145
493657218
867231954
152489763
376148529
928365471
541972386
`);
const { Solver, Int, Distinct, isIntVal } = new api.Context('main');
const cells: Arith[][] = [];
// 9x9 matrix of integer variables
for (let i = 0; i < 9; i++) {
const row = [];
for (let j = 0; j < 9; j++) {
row.push(Int.const(`x_${i}_${j}`));
}
cells.push(row);
}
const solver = new Solver();
// each cell contains a value 1<=x<=9
for (let i = 0; i < 9; i++) {
for (let j = 0; j < 9; j++) {
solver.add(cells[i][j].ge(1), cells[i][j].le(9));
}
}
// each row contains a digit only once
for (let i = 0; i < 9; i++) {
solver.add(Distinct(...cells[i]));
}
// each column contains a digit only once
for (let j = 0; j < 9; j++) {
const column = [];
for (let i = 0; i < 9; i++) {
column.push(cells[i][j]);
}
solver.add(Distinct(...column));
}
// each 3x3 contains a digit at most once
for (let iSquare = 0; iSquare < 3; iSquare++) {
for (let jSquare = 0; jSquare < 3; jSquare++) {
const square = [];
for (let i = iSquare * 3; i < iSquare * 3 + 3; i++) {
for (let j = jSquare * 3; j < jSquare * 3 + 3; j++) {
square.push(cells[i][j]);
}
}
solver.add(Distinct(...square));
}
}
for (let i = 0; i < 9; i++) {
for (let j = 0; j < 9; j++) {
const digit = INSTANCE[i][j];
if (digit !== null) {
solver.add(cells[i][j].eq(digit));
}
}
}
expect(await solver.check()).toStrictEqual(sat);
const model = solver.model();
const result = [];
for (let i = 0; i < 9; i++) {
let row = [];
for (let j = 0; j < 9; j++) {
const cell = model.eval(cells[i][j]);
assert(isIntVal(cell));
const value = cell.value;
assert(typeof value === 'bigint');
expect(value).toBeGreaterThanOrEqual(0n);
expect(value).toBeLessThanOrEqual(9n);
// JSON.stringify doesn't handle bigints
row.push(Number(value));
}
result.push(row);
}
expect(JSON.stringify(result)).toStrictEqual(JSON.stringify(EXPECTED));
}, 120_000);
});
describe('reals', () => {
it('can work with numerals', async () => {
const { Real, And } = new api.Context('main');
const n1 = Real.val('1/2');
const n2 = Real.val('0.5');
const n3 = Real.val(0.5);
await prove(And(n1.eq(n2), n1.eq(n3)));
const n4 = Real.val('-1/3');
const n5 = Real.val('-0.3333333333333333333333333333333333');
await prove(n4.neq(n5));
});
it('can do non-linear arithmetic', async () => {
api.setParam('pp.decimal', true);
api.setParam('pp.decimal_precision', 20);
const { Real, Solver, isReal, isRealVal } = new api.Context('main');
const x = Real.const('x');
const y = Real.const('y');
const z = Real.const('z');
const solver = new Solver();
solver.add(x.mul(x).add(y.mul(y)).eq(1)); // x^2 + y^2 == 1
solver.add(x.mul(x).mul(x).add(z.mul(z).mul(z)).lt('1/2')); // x^3 + z^3 < 1/2
expect(await solver.check()).toStrictEqual(sat);
const model = solver.model();
expect(isRealVal(model.get(x))).toStrictEqual(true);
// solution of y is a polynomial
// https://stackoverflow.com/a/69740906
expect(isReal(model.get(y))).toStrictEqual(true);
expect(isRealVal(model.get(z))).toStrictEqual(true);
});
});
describe('bitvectors', () => {
it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = new api.Context('main');
const x = BitVec.const('x', 32);
const sSol = (await solve(x.sub(10).sle(0).eq(x.sle(10)))).get(x); // signed: (x - 10 <= 0) == (x <= 10)
const uSol = (await solve(x.sub(10).ule(0).eq(x.ule(10)))).get(x); // unsigned: (x - 10 <= 0) == (x <= 10)
assert(isBitVecVal(sSol) && isBitVecVal(uSol));
let v = sSol.asSignedValue();
expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true);
v = uSol.value;
expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true);
const y = BitVec.const('y', 32);
await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y)));
});
it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = new api.Context('main');
const x = BitVec.const('x', 32);
const y = BitVec.const('y', 32);
const model = await solve(x.xor(y).sub(103).eq(x.mul(y)));
const xSol = model.get(x);
const ySol = model.get(y);
assert(isBitVecVal(xSol) && isBitVecVal(ySol));
const xv = xSol.asSignedValue();
const yv = ySol.asSignedValue();
// this solutions wraps around so we need to check using modulo
expect((xv ^ yv) - 103n === (xv * yv) % 2n ** 32n).toStrictEqual(true);
});
});
describe('Solver', () => {
it('can use push and pop', async () => {
const { Solver, Int } = new api.Context('main');
const solver = new Solver();
const x = Int.const('x');
solver.add(x.gt(0));
expect(await solver.check()).toStrictEqual(sat);
solver.push();
solver.add(x.lt(0));
expect(solver.numScopes()).toStrictEqual(1);
expect(await solver.check()).toStrictEqual(unsat);
solver.pop();
expect(solver.numScopes()).toStrictEqual(0);
expect(await solver.check()).toStrictEqual(sat);
});
it('can find multiple solutions', async () => {
const { Int, isIntVal } = new api.Context('main');
const x = Int.const('x');
const solutions = await asyncToArray(allSolutions(x.ge(1), x.le(5)));
expect(solutions.length).toStrictEqual(5);
const results = solutions
.map(solution => {
const expr = solution.eval(x);
assert(isIntVal(expr));
return expr.value;
})
.sort((a, b) => {
assert(a !== null && b !== null && typeof a === 'bigint' && typeof b === 'bigint');
if (a < b) {
return -1;
} else if (a == b) {
return 0;
} else {
return 1;
}
});
expect(results).toStrictEqual([1n, 2n, 3n, 4n, 5n]);
});
});
describe('AstVector', () => {
it('can use basic methods', async () => {
const { Solver, AstVector, Int } = new api.Context('main');
const solver = new Solver();
const vector = new AstVector<Arith>();
for (let i = 0; i < 5; i++) {
vector.push(Int.const(`int__${i}`));
}
const length = vector.length;
for (let i = 0; i < length; i++) {
solver.add(vector.get(i).gt(1));
}
expect(await solver.check()).toStrictEqual(sat);
});
});
});

1888
src/api/js/src/high-level/high-level.ts Normal file
View file

File diff suppressed because it is too large Load diff

2
src/api/js/src/high-level/index.ts Normal file
View file

@ -0,0 +1,2 @@
export * from './high-level';
export * from './types';

1132
src/api/js/src/high-level/types.ts Normal file
View file

File diff suppressed because it is too large Load diff

90
src/api/js/src/high-level/utils.test.ts Normal file
View file

@ -0,0 +1,90 @@
import { Z3AssertionError } from './types';
import { allSatisfy, assert, assertExhaustive, autoBind } from './utils';
describe('allSatisfy', () => {
it('returns null on empty array', () => {
expect(allSatisfy([], () => true)).toBeNull();
});
it('returns true if all satisfy', () => {
expect(allSatisfy([2, 4, 6, 8], arg => arg % 2 === 0)).toStrictEqual(true);
});
it('returns false if any element fails', () => {
expect(allSatisfy([2, 4, 1, 8], arg => arg % 2 === 0)).toStrictEqual(false);
});
});
describe('assertExhaustive', () => {
enum MyEnum {
A,
B,
}
it('stops compilation', () => {
const result: MyEnum = MyEnum.A as any;
switch (result) {
case MyEnum.A:
break;
default:
// @ts-expect-error
assertExhaustive(result);
}
});
it('allows compilation', () => {
const result: MyEnum = MyEnum.A as any;
switch (result) {
case MyEnum.A:
break;
case MyEnum.B:
break;
default:
assertExhaustive(result);
}
});
it('throws', () => {
const result: MyEnum = undefined as any;
switch (result) {
case MyEnum.A:
throw new Error();
case MyEnum.B:
throw new Error();
default:
expect(() => assertExhaustive(result)).toThrowError();
}
});
});
describe('autoBind', () => {
class Binded {
readonly name = 'Richard';
constructor(shouldBind: boolean) {
if (shouldBind === true) {
autoBind(this);
}
}
test(): string {
return `Hello ${this.name}`;
}
}
it('binds this', () => {
const { test: withoutBind } = new Binded(false);
const { test: withBind } = new Binded(true);
expect(() => withoutBind()).toThrowError(TypeError);
expect(withBind()).toStrictEqual('Hello Richard');
});
});
describe('assert', () => {
it('throws on failure', () => {
expect(() => assert(false)).toThrowError(Z3AssertionError);
expect(() => assert(false, 'foobar')).toThrowError(new Z3AssertionError('foobar'));
});
it('does nothing on sucess', () => {
expect(() => assert(true, 'hello')).not.toThrow();
});
});

85
src/api/js/src/high-level/utils.ts Normal file
View file

@ -0,0 +1,85 @@
import { Z3AssertionError } from './types';
function getAllProperties(obj: Record<string, any>) {
const properties = new Set<[any, string | symbol]>();
do {
for (const key of Reflect.ownKeys(obj)) {
properties.add([obj, key]);
}
} while ((obj = Reflect.getPrototypeOf(obj)!) && obj !== Object.prototype);
return properties;
}
// https://github.com/sindresorhus/auto-bind
// We modify it to use CommonJS instead of ESM
/*
MIT License
Copyright (c) Sindre Sorhus <sindresorhus@gmail.com> (https://sindresorhus.com)
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
export function autoBind<Self extends Record<string | symbol, any>>(self: Self): Self {
for (const [obj, key] of getAllProperties(self.constructor.prototype)) {
if (key === 'constructor') {
continue;
}
const descriptor = Reflect.getOwnPropertyDescriptor(obj, key);
if (descriptor && typeof descriptor.value === 'function') {
(self[key] as any) = self[key].bind(self);
}
}
return self;
}
/**
* Use to ensure that switches are checked to be exhaustive at compile time
*
* @example Basic usage
* ```typescript
* enum Something {
* left,
* right,
* };
* const something = getSomething();
* switch (something) {
* case Something.left:
* ...
* case Something.right:
* ...
* default:
* assertExhaustive(something);
* }
* ```
*
* @param x - The param on which the switch operates
*/
export function assertExhaustive(x: never): never {
throw new Error('Unexpected code execution detected, should be caught at compile time');
}
export function assert(condition: boolean, reason?: string): asserts condition {
if (!condition) {
throw new Z3AssertionError(reason ?? 'Assertion failed');
}
}
/**
* Check the all elements of a `collection` satisfy the `premise`.
* If any of the items fail the `premise`, returns false;
* @returns null if the `collection` is empty, boolean otherwise
*/
export function allSatisfy<T>(collection: Iterable<T>, premise: (arg: T) => boolean): boolean | null {
let hasItems = false;
for (const arg of collection) {
hasItems = true;
if (!premise(arg)) {
return false;
}
}
return hasItems === true ? true : null;
}

62
src/api/js/src/jest.ts Normal file
View file

@ -0,0 +1,62 @@
// This file is not included in the build
// @ts-ignore no-implicit-any
import { createApi, Z3HighLevel } from './high-level';
import { init as initWrapper, Z3LowLevel } from './low-level';
import initModule = require('../build/z3-built');
export * from './high-level/types';
export { Z3Core, Z3LowLevel } from './low-level';
export * from './low-level/types.__GENERATED__';
export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
const lowLevel = await initWrapper(initModule);
const highLevel = createApi(lowLevel.Z3);
return { ...lowLevel, ...highLevel };
}
function delay(ms: number): Promise<void> & { cancel(): void };
function delay(ms: number, result: Error): Promise<never> & { cancel(): void };
function delay<T>(ms: number, result: T): Promise<T> & { cancel(): void };
function delay<T>(ms: number, result?: T | Error): Promise<T | void> & { cancel(): void } {
let handle: any;
const promise = new Promise<void | T>(
(resolve, reject) =>
(handle = setTimeout(() => {
if (result instanceof Error) {
reject(result);
} else if (result !== undefined) {
resolve(result);
}
resolve();
}, ms)),
);
return { ...promise, cancel: () => clearTimeout(handle) };
}
function waitWhile(premise: () => boolean, pollMs: number = 100): Promise<void> & { cancel(): void } {
let handle: any;
const promise = new Promise<void>(resolve => {
handle = setInterval(() => {
if (premise()) {
clearTimeout(handle);
resolve();
}
}, pollMs);
});
return { ...promise, cancel: () => clearInterval(handle) };
}
export function killThreads(em: any): Promise<void> {
em.PThread.terminateAllThreads();
// Create a polling lock to wait for threads to return
// TODO(ritave): Threads should be killed automatically, or there should be a better way to wait for them
const lockPromise = waitWhile(() => !em.PThread.unusedWorkers.length && !em.PThread.runningWorkers.length);
const delayPromise = delay(5000, new Error('Waiting for threads to be killed timed out'));
return Promise.race([lockPromise, delayPromise]).finally(() => {
lockPromise.cancel();
delayPromise.cancel();
});
}

1
src/api/js/src/async-wrapper.js → src/api/js/src/low-level/async-wrapper.js
View file

@ -1,4 +1,5 @@
// this wrapper works with async-fns to provide promise-based off-thread versions of some functions
// It's prepended directly by emscripten to the resulting z3-built.js
let capability = null;
function resolve_async(val) {

4
src/api/js/src/low-level/index.ts Normal file
View file

@ -0,0 +1,4 @@
export * from './types.__GENERATED__';
export * from './wrapper.__GENERATED__';
export type Z3Core = Awaited<ReturnType<typeof import('./wrapper.__GENERATED__')['init']>>['Z3'];
export type Z3LowLevel = Awaited<ReturnType<typeof import('./wrapper.__GENERATED__')['init']>>;

38
src/api/js/src/node.ts Normal file
View file

@ -0,0 +1,38 @@
// @ts-ignore no-implicit-any
import initModule = require('./z3-built');
import { createApi, Z3HighLevel } from './high-level';
import { init as initWrapper, Z3LowLevel } from './low-level';
export * from './high-level/types';
export { Z3Core, Z3LowLevel } from './low-level';
export * from './low-level/types.__GENERATED__';
/**
* The main entry point to the Z3 API
*
* ```typescript
* import { init, sat } from 'z3-solver';
*
* const { Context } = await init();
* const { Solver, Int } = new Context('main');
*
* const x = Int.const('x');
* const y = Int.const('y');
*
* const solver = new Solver();
* solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10
*
* if (await solver.check() !== sat) {
* throw new Error("couldn't find a solution")
* }
* const model = solver.model();
*
* console.log(`x=${model.get(x)}, y=${model.get(y)}`);
* // x=0, y=12
* ```
* @category Global */
export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
const lowLevel = await initWrapper(initModule);
const highLevel = createApi(lowLevel.Z3);
return { ...lowLevel, ...highLevel };
}

4
src/api/js/tsconfig.build.json Normal file
View file

@ -0,0 +1,4 @@
{
"extends": "./tsconfig.json",
"exclude": ["src/**/*.test.ts", "src/jest.ts"]
}

10
src/api/js/tsconfig.json
View file

@ -6,9 +6,11 @@
"declaration": true,
"forceConsistentCasingInFileNames": true,
"strict": true,
"skipLibCheck": true
"skipLibCheck": true,
"outDir": "build/",
"allowJs": true,
"checkJs": false
},
"exclude": [
"src"
]
"include": ["src/**/*.ts"],
"exclude": ["node_modules"]
}

8
src/api/js/typedoc.json Normal file
View file

@ -0,0 +1,8 @@
{
"$schema": "https://typedoc.org/schema.json",
"entryPoints": ["./src/node.ts"],
"out": "../../../doc/api/html/js",
"exclude": ["./src/low-level/**/*"],
"readme": "./PUBLISHED_README.md",
"categorizeByGroup": false
}

14
src/api/ml/z3.ml
View file

@ -119,6 +119,7 @@ sig
val get_ast_kind : ast -> Z3enums.ast_kind
val is_expr : ast -> bool
val is_app : ast -> bool
val is_numeral : ast -> bool
val is_var : ast -> bool
val is_quantifier : ast -> bool
val is_sort : ast -> bool
@ -191,6 +192,7 @@ end = struct
| _ -> false
let is_app (x:ast) = get_ast_kind x = APP_AST
let is_numeral (x:ast) = get_ast_kind x = NUMERAL_AST
let is_var (x:ast) = get_ast_kind x = VAR_AST
let is_quantifier (x:ast) = get_ast_kind x = QUANTIFIER_AST
let is_sort (x:ast) = get_ast_kind x = SORT_AST
@ -914,6 +916,12 @@ struct
let mk_sort_s (ctx:context) (name:string) (constructors:Constructor.constructor list) =
mk_sort ctx (Symbol.mk_string ctx name) constructors
let mk_sort_ref (ctx: context) (name:Symbol.symbol) =
Z3native.mk_datatype_sort ctx name
let mk_sort_ref_s (ctx: context) (name: string) =
mk_sort_ref ctx (Symbol.mk_string ctx name)
let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) =
let n = List.length names in
@ -1018,7 +1026,7 @@ struct
let is_int (x:expr) =
((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = INT_SORT)
let is_arithmetic_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ANUM)
let is_arithmetic_numeral (x:expr) = (AST.is_numeral x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ANUM)
let is_le (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LE)
let is_ge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_GE)
let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LT)
@ -1129,7 +1137,7 @@ struct
let mk_sort (ctx:context) size = Z3native.mk_bv_sort ctx size
let is_bv (x:expr) =
((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = BV_SORT)
let is_bv_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNUM)
let is_bv_numeral (x:expr) = (AST.is_numeral x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNUM)
let is_bv_bit1 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT1)
let is_bv_bit0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT0)
let is_bv_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNEG)
@ -1258,7 +1266,9 @@ struct
let mk_seq_replace = Z3native.mk_seq_replace
let mk_seq_at = Z3native.mk_seq_at
let mk_seq_length = Z3native.mk_seq_length
let mk_seq_nth = Z3native.mk_seq_nth
let mk_seq_index = Z3native.mk_seq_index
let mk_seq_last_index = Z3native.mk_seq_last_index
let mk_str_to_int = Z3native.mk_str_to_int
let mk_str_le = Z3native.mk_str_le
let mk_str_lt = Z3native.mk_str_lt

18
src/api/ml/z3.mli
View file

@ -1061,6 +1061,15 @@ sig
if the corresponding sort reference is 0, then the value in sort_refs should be an index
referring to one of the recursive datatypes that is declared. *)
val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
(* Create a forward reference to a recursive datatype being declared.
The forward reference can be used in a nested occurrence: the range of an array
or as element sort of a sequence. The forward reference should only be used when
used in an accessor for a recursive datatype that gets declared. *)
val mk_sort_ref : context -> Symbol.symbol -> Sort.sort
(* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *)
val mk_sort_ref_s : context -> string -> Sort.sort
(** Create a new datatype sort. *)
val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort
@ -1858,7 +1867,7 @@ sig
(** create regular expression sorts over sequences of the argument sort *)
val mk_re_sort : context -> Sort.sort -> Sort.sort
(** test if sort is a regular expression sort *)
val is_re_sort : context -> Sort.sort -> bool
@ -1906,10 +1915,17 @@ sig
(** length of a sequence *)
val mk_seq_length : context -> Expr.expr -> Expr.expr
(** [mk_seq_nth ctx s index] retrieves from [s] the element at position [index].
The function is under-specified if the index is out of bounds. *)
val mk_seq_nth : context -> Expr.expr -> Expr.expr -> Expr.expr
(** index of the first occurrence of the second argument in the first *)
val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(** [mk_seq_last_index ctx s substr] occurence of [substr] in the sequence [s] *)
val mk_seq_last_index : context -> Expr.expr -> Expr.expr -> Expr.expr
(** retrieve integer expression encoded in string *)
val mk_str_to_int : context -> Expr.expr -> Expr.expr

42
src/api/ml/z3native_stubs.c.pre
View file

@ -294,7 +294,8 @@ static struct custom_operations Z3_ast_plus_custom_ops = {
Z3_ast_compare_ext
};
MK_CTX_OF(ast, 16) // let's say 16 bytes per ast
// FUDGE
MK_CTX_OF(ast, 8) // let's say 16 bytes per ast
#define MK_PLUS_OBJ_NO_REF(X, USED) \
typedef struct { \
@ -410,25 +411,26 @@ MK_CTX_OF(ast, 16) // let's say 16 bytes per ast
\
MK_CTX_OF(X, USED)
MK_PLUS_OBJ_NO_REF(symbol, 32)
MK_PLUS_OBJ_NO_REF(constructor, 32)
MK_PLUS_OBJ_NO_REF(constructor_list, 32)
MK_PLUS_OBJ_NO_REF(rcf_num, 32)
MK_PLUS_OBJ(params, 128)
MK_PLUS_OBJ(param_descrs, 128)
MK_PLUS_OBJ(model, 512)
MK_PLUS_OBJ(func_interp, 128)
MK_PLUS_OBJ(func_entry, 128)
MK_PLUS_OBJ(goal, 128)
MK_PLUS_OBJ(tactic, 128)
MK_PLUS_OBJ(probe, 128)
MK_PLUS_OBJ(apply_result, 128)
MK_PLUS_OBJ(solver, 20 * 1000 * 1000) // pretend a solver is 20MB
MK_PLUS_OBJ(stats, 128)
MK_PLUS_OBJ(ast_map, 1024 * 2)
MK_PLUS_OBJ(ast_vector, 128)
MK_PLUS_OBJ(fixedpoint, 20 * 1000 * 1000)
MK_PLUS_OBJ(optimize, 20 * 1000 * 1000)
// FUDGE
MK_PLUS_OBJ_NO_REF(symbol, 16)
MK_PLUS_OBJ_NO_REF(constructor, 16)
MK_PLUS_OBJ_NO_REF(constructor_list, 16)
MK_PLUS_OBJ_NO_REF(rcf_num, 16)
MK_PLUS_OBJ(params, 64)
MK_PLUS_OBJ(param_descrs, 64)
MK_PLUS_OBJ(model, 64)
MK_PLUS_OBJ(func_interp, 32)
MK_PLUS_OBJ(func_entry, 32)
MK_PLUS_OBJ(goal, 64)
MK_PLUS_OBJ(tactic, 64)
MK_PLUS_OBJ(probe, 64)
MK_PLUS_OBJ(apply_result, 32)
MK_PLUS_OBJ(solver, 20 * 1000)
MK_PLUS_OBJ(stats, 32)
MK_PLUS_OBJ(ast_map, 32)
MK_PLUS_OBJ(ast_vector, 32)
MK_PLUS_OBJ(fixedpoint, 20 * 1000)
MK_PLUS_OBJ(optimize, 20 * 1000)
#ifdef __cplusplus
extern "C" {

1
src/api/python/MANIFEST.in
View file

@ -5,3 +5,4 @@ recursive-include core *.cmake
recursive-include core/src *
recursive-include core/cmake *
recursive-include core/scripts *
include pyproject.toml

40
src/api/python/setup.py
View file

@ -178,6 +178,20 @@ def _copy_bins():
continue
shutil.copy(os.path.join(header_dir, fname), os.path.join(HEADERS_DIR, fname))
# This hack lets z3 installed libs link on M1 macs; it is a hack, not a proper fix
# @TODO: Linked issue: https://github.com/Z3Prover/z3/issues/5926
major_minor = '.'.join(_z3_version().split('.')[:2])
link_name = None
if BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
pass # TODO: When windows VMs work on M1, fill this in
elif BUILD_PLATFORM in ('darwin', 'osx'):
split = LIBRARY_FILE.split('.')
link_name = split[0] + '.' + major_minor + '.' + split[1]
else:
link_name = LIBRARY_FILE + '.' + major_minor
if link_name:
os.symlink(LIBRARY_FILE, os.path.join(LIBS_DIR, link_name), True)
def _copy_sources():
"""
Prepare for a source distribution by assembling a minimal set of source files needed
@ -236,6 +250,16 @@ class clean(_clean):
#try: os.makedirs(os.path.join(ROOT_DIR, 'build'))
#except OSError: pass
# platform.freedesktop_os_release was added in 3.10
os_id = ''
if hasattr(platform, 'freedesktop_os_release'):
try:
osr = platform.freedesktop_os_release()
print(osr)
os_id = osr['ID']
except OSError:
pass
if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
if RELEASE_DIR is None:
name = get_platform()
@ -257,13 +281,20 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
# extract the architecture of the release from the directory name
arch = RELEASE_METADATA[1]
distos = RELEASE_METADATA[2]
if distos in ('debian', 'ubuntu') or 'linux' in distos:
raise Exception("Linux binary distributions must be built on centos to conform to PEP 513")
if distos in ('debian', 'ubuntu'):
raise Exception(
"Linux binary distributions must be built on centos to conform to PEP 513 or alpine if targetting musl"
)
elif distos == 'glibc':
if arch == 'x64':
plat_name = 'manylinux1_x86_64'
else:
plat_name = 'manylinux1_i686'
elif distos == 'linux' and os_id == 'alpine':
if arch == 'x64':
plat_name = 'musllinux_1_1_x86_64'
else:
plat_name = 'musllinux_1_1_i686'
elif distos == 'win':
if arch == 'x64':
plat_name = 'win_amd64'
@ -273,10 +304,10 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
osver = RELEASE_METADATA[3]
if osver.count('.') > 1:
osver = '.'.join(osver.split('.')[:2])
if arch == 'x64':
if arch == 'x64':
plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
elif arch == 'arm64':
plat_name ='macosx_%s_arm64' % osver.replace('.', '_')
plat_name ='macosx_%s_arm64' % osver.replace('.', '_')
else:
raise Exception(f"idk how os {distos} {osver} works. what goes here?")
else:
@ -287,7 +318,6 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
sys.argv.insert(idx + 1, plat_name)
sys.argv.insert(idx + 2, '--universal') # supports py2+py3. if --plat-name is not specified this will also mean that the package can be installed on any machine regardless of architecture, so watch out!
setup(
name='z3-solver',
version=_z3_version(),

145
src/api/python/z3/z3.py
View file

@ -209,7 +209,8 @@ class Context:
Z3_del_config(conf)
def __del__(self):
Z3_del_context(self.ctx)
if Z3_del_context is not None:
Z3_del_context(self.ctx)
self.ctx = None
self.eh = None
@ -225,6 +226,10 @@ class Context:
"""
Z3_interrupt(self.ref())
def param_descrs(self):
"""Return the global parameter description set."""
return ParamDescrsRef(Z3_get_global_param_descrs(self.ref()), self)
# Global Z3 context
_main_ctx = None
@ -342,7 +347,7 @@ class AstRef(Z3PPObject):
Z3_inc_ref(self.ctx.ref(), self.as_ast())
def __del__(self):
if self.ctx.ref() is not None and self.ast is not None:
if self.ctx.ref() is not None and self.ast is not None and Z3_dec_ref is not None:
Z3_dec_ref(self.ctx.ref(), self.as_ast())
self.ast = None
@ -1101,6 +1106,28 @@ class ExprRef(AstRef):
else:
return []
def from_string(self, s):
pass
def serialize(self):
s = Solver()
f = Function('F', self.sort(), BoolSort(self.ctx))
s.add(f(self))
return s.sexpr()
def deserialize(st):
"""inverse function to the serialize method on ExprRef.
It is made available to make it easier for users to serialize expressions back and forth between
strings. Solvers can be serialized using the 'sexpr()' method.
"""
s = Solver()
s.from_string(st)
if len(s.assertions()) != 1:
raise Z3Exception("single assertion expected")
fml = s.assertions()[0]
if fml.num_args() != 1:
raise Z3Exception("dummy function 'F' expected")
return fml.arg(0)
def _to_expr_ref(a, ctx):
if isinstance(a, Pattern):
@ -5102,7 +5129,7 @@ class ScopedConstructor:
self.ctx = ctx
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_del_constructor is not None:
Z3_del_constructor(self.ctx.ref(), self.c)
@ -5114,7 +5141,7 @@ class ScopedConstructorList:
self.ctx = ctx
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_del_constructor_list is not None:
Z3_del_constructor_list(self.ctx.ref(), self.c)
@ -5394,7 +5421,7 @@ class ParamsRef:
return ParamsRef(self.ctx, self.params)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_params_dec_ref is not None:
Z3_params_dec_ref(self.ctx.ref(), self.params)
def set(self, name, val):
@ -5459,7 +5486,7 @@ class ParamDescrsRef:
return ParamsDescrsRef(self.descr, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_param_descrs_dec_ref is not None:
Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
def size(self):
@ -5522,7 +5549,7 @@ class Goal(Z3PPObject):
Z3_goal_inc_ref(self.ctx.ref(), self.goal)
def __del__(self):
if self.goal is not None and self.ctx.ref() is not None:
if self.goal is not None and self.ctx.ref() is not None and Z3_goal_dec_ref is not None:
Z3_goal_dec_ref(self.ctx.ref(), self.goal)
def depth(self):
@ -5826,7 +5853,7 @@ class AstVector(Z3PPObject):
Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
def __del__(self):
if self.vector is not None and self.ctx.ref() is not None:
if self.vector is not None and self.ctx.ref() is not None and Z3_ast_vector_dec_ref is not None:
Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
def __len__(self):
@ -5989,7 +6016,7 @@ class AstMap:
return AstMap(self.map, self.ctx)
def __del__(self):
if self.map is not None and self.ctx.ref() is not None:
if self.map is not None and self.ctx.ref() is not None and Z3_ast_map_dec_ref is not None:
Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
def __len__(self):
@ -6108,7 +6135,7 @@ class FuncEntry:
return FuncEntry(self.entry, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_func_entry_dec_ref is not None:
Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
def num_args(self):
@ -6215,7 +6242,7 @@ class FuncInterp(Z3PPObject):
Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
def __del__(self):
if self.f is not None and self.ctx.ref() is not None:
if self.f is not None and self.ctx.ref() is not None and Z3_func_interp_dec_ref is not None:
Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
def else_value(self):
@ -6333,7 +6360,7 @@ class ModelRef(Z3PPObject):
Z3_model_inc_ref(self.ctx.ref(), self.model)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_model_dec_ref is not None:
Z3_model_dec_ref(self.ctx.ref(), self.model)
def __repr__(self):
@ -6443,7 +6470,25 @@ class ModelRef(Z3PPObject):
return None
r = _to_expr_ref(_r, self.ctx)
if is_as_array(r):
return self.get_interp(get_as_array_func(r))
fi = self.get_interp(get_as_array_func(r))
if fi is None:
return fi
e = fi.else_value()
if e is None:
return fi
if fi.arity() != 1:
return fi
srt = decl.range()
dom = srt.domain()
e = K(dom, e)
i = 0
sz = fi.num_entries()
n = fi.arity()
while i < sz:
fe = fi.entry(i)
e = Store(e, fe.arg_value(0), fe.value())
i += 1
return e
else:
return r
else:
@ -6594,6 +6639,19 @@ class ModelRef(Z3PPObject):
"""Update the interpretation of a constant"""
if is_expr(x):
x = x.decl()
if is_func_decl(x) and x.arity() != 0 and isinstance(value, FuncInterp):
fi1 = value.f
fi2 = Z3_add_func_interp(x.ctx_ref(), self.model, x.ast, value.else_value().ast);
fi2 = FuncInterp(fi2, x.ctx)
for i in range(value.num_entries()):
e = value.entry(i)
n = Z3_func_entry_get_num_args(x.ctx_ref(), e.entry)
v = AstVector()
for j in range(n):
v.push(entry.arg_value(j))
val = Z3_func_entry_get_value(x.ctx_ref(), e.entry)
Z3_func_interp_add_entry(x.ctx_ref(), fi2.f, v.vector, val)
return
if not is_func_decl(x) or x.arity() != 0:
raise Z3Exception("Expecting 0-ary function or constant expression")
value = _py2expr(value)
@ -6649,7 +6707,7 @@ class Statistics:
return Statistics(self.stats, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_stats_dec_ref is not None:
Z3_stats_dec_ref(self.ctx.ref(), self.stats)
def __repr__(self):
@ -6842,7 +6900,7 @@ class Solver(Z3PPObject):
self.set("smtlib2_log", logFile)
def __del__(self):
if self.solver is not None and self.ctx.ref() is not None:
if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
def set(self, *args, **keys):
@ -7365,7 +7423,7 @@ class Fixedpoint(Z3PPObject):
return FixedPoint(self.fixedpoint, self.ctx)
def __del__(self):
if self.fixedpoint is not None and self.ctx.ref() is not None:
if self.fixedpoint is not None and self.ctx.ref() is not None and Z3_fixedpoint_dec_ref is not None:
Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
def set(self, *args, **keys):
@ -7788,7 +7846,7 @@ class Optimize(Z3PPObject):
return Optimize(self.optimize, self.ctx)
def __del__(self):
if self.optimize is not None and self.ctx.ref() is not None:
if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
if self._on_models_id is not None:
del _on_models[self._on_models_id]
@ -8013,7 +8071,7 @@ class ApplyResult(Z3PPObject):
return ApplyResult(self.result, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
if self.ctx.ref() is not None and Z3_apply_result_dec_ref is not None:
Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
def __len__(self):
@ -8118,7 +8176,7 @@ class Tactic:
return Tactic(self.tactic, self.ctx)
def __del__(self):
if self.tactic is not None and self.ctx.ref() is not None:
if self.tactic is not None and self.ctx.ref() is not None and Z3_tactic_dec_ref is not None:
Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
def solver(self, logFile=None):
@ -8429,7 +8487,7 @@ class Probe:
return Probe(self.probe, self.ctx)
def __del__(self):
if self.probe is not None and self.ctx.ref() is not None:
if self.probe is not None and self.ctx.ref() is not None and Z3_probe_dec_ref is not None:
Z3_probe_dec_ref(self.ctx.ref(), self.probe)
def __lt__(self, other):
@ -8733,8 +8791,12 @@ def substitute(t, *m):
m = m1
if z3_debug():
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(
p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
_z3_assert(
all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) for p in m]),
"Z3 invalid substitution, expression pairs expected.")
_z3_assert(
all([p[0].sort().eq(p[1].sort()) for p in m]),
'Z3 invalid substitution, mismatching "from" and "to" sorts.')
num = len(m)
_from = (Ast * num)()
_to = (Ast * num)()
@ -8764,6 +8826,27 @@ def substitute_vars(t, *m):
_to[i] = m[i].as_ast()
return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
def substitute_funs(t, *m):
"""Apply subistitution m on t, m is a list of pairs of a function and expression (from, to)
Every occurrence in to of the function from is replaced with the expression to.
The expression to can have free variables, that refer to the arguments of from.
For examples, see
"""
if isinstance(m, tuple):
m1 = _get_args(m)
if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1):
m = m1
if z3_debug():
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, funcion pairs expected.")
num = len(m)
_from = (FuncDecl * num)()
_to = (Ast * num)()
for i in range(num):
_from[i] = m[i][0].as_func_decl()
_to[i] = m[i][1].as_ast()
return _to_expr_ref(Z3_substitute_funs(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
def Sum(*args):
"""Create the sum of the Z3 expressions.
@ -9150,7 +9233,7 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
# Global default rounding mode
_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
_dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
_dflt_fpsort_ebits = 11
_dflt_fpsort_sbits = 53
@ -11249,7 +11332,7 @@ def user_prop_push(ctx, cb):
def user_prop_pop(ctx, cb, num_scopes):
prop = _prop_closures.get(ctx)
prop.cb = cb
pop(num_scopes)
prop.pop(num_scopes)
def user_prop_fresh(id, ctx):
@ -11295,13 +11378,13 @@ def user_prop_diseq(ctx, cb, x, y):
prop.cb = None
_user_prop_push = push_eh_type(user_prop_push)
_user_prop_pop = pop_eh_type(user_prop_pop)
_user_prop_fresh = fresh_eh_type(user_prop_fresh)
_user_prop_fixed = fixed_eh_type(user_prop_fixed)
_user_prop_final = final_eh_type(user_prop_final)
_user_prop_eq = eq_eh_type(user_prop_eq)
_user_prop_diseq = eq_eh_type(user_prop_diseq)
_user_prop_push = Z3_push_eh(user_prop_push)
_user_prop_pop = Z3_pop_eh(user_prop_pop)
_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
_user_prop_final = Z3_final_eh(user_prop_final)
_user_prop_eq = Z3_eq_eh(user_prop_eq)
_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
class UserPropagateBase:

93
src/api/z3_api.h
View file

@ -1444,6 +1444,7 @@ Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_as
Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));
Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb));
Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
Z3_DECLARE_CLOSURE(Z3_decide_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast* t, unsigned* idx, Z3_lbool* phase));
/**
@ -1684,6 +1685,14 @@ extern "C" {
*/
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
/**
\brief Retrieve description of global parameters.
def_API('Z3_get_global_param_descrs', PARAM_DESCRS, (_in(CONTEXT),))
*/
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c);
/**
\brief Interrupt the execution of a Z3 procedure.
This procedure can be used to interrupt: solvers, simplifiers and tactics.
@ -2093,6 +2102,19 @@ extern "C" {
unsigned num_constructors,
Z3_constructor constructors[]);
/**
\brief create a forward reference to a recursive datatype being declared.
The forward reference can be used in a nested occurrence: the range of an array
or as element sort of a sequence. The forward reference should only be used when
used in an accessor for a recursive datatype that gets declared.
Forward references can replace the use sort references, that are unsigned integers
in the \c Z3_mk_constructor call
def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL)))
*/
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name);
/**
\brief Create list of constructors.
@ -2913,6 +2935,16 @@ extern "C" {
def_API('Z3_mk_repeat', AST, (_in(CONTEXT), _in(UINT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
/**
\brief Extracts the bit at position \ccode{i} of a bit-vector and
yields a boolean.
The node \c t1 must have a bit-vector sort.
def_API('Z3_mk_bit2bool', AST, (_in(CONTEXT), _in(UINT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1);
/**
\brief Shift left.
@ -3686,7 +3718,7 @@ extern "C" {
/**
\brief Return index of first occurrence of \c substr in \c s starting from offset \c offset.
\brief Return index of the first occurrence of \c substr in \c s starting from offset \c offset.
If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well.
The value is -1 if \c offset is negative or larger than the length of \c s.
@ -3695,7 +3727,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
/**
\brief Return the last occurrence of \c substr in \c s.
\brief Return index of the last occurrence of \c substr in \c s.
If \c s does not contain \c substr, then the value is -1,
def_API('Z3_mk_seq_last_index', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
@ -4839,7 +4871,7 @@ extern "C" {
/**
\brief Return \c Z3_L_TRUE if \c a is true, \c Z3_L_FALSE if it is false, and \c Z3_L_UNDEF otherwise.
def_API('Z3_get_bool_value', INT, (_in(CONTEXT), _in(AST)))
def_API('Z3_get_bool_value', LBOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
@ -5260,6 +5292,20 @@ extern "C" {
unsigned num_exprs,
Z3_ast const to[]);
/**
\brief Substitute funcions in \c from with new expressions in \c to.
The expressions in \c to can have free variables. The free variable in \c to at index 0
refers to the first argument of \c from, the free variable at index 1 corresponds to the second argument.
def_API('Z3_substitute_funs', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, FUNC_DECL), _in_array(2, AST)))
*/
Z3_ast Z3_API Z3_substitute_funs(Z3_context c,
Z3_ast a,
unsigned num_funs,
Z3_func_decl const from[],
Z3_ast const to[]);
/**
\brief Translate/Copy the AST \c a from context \c source to context \c target.
AST \c a must have been created using context \c source.
@ -6709,6 +6755,8 @@ extern "C" {
\param push_eh - a callback invoked when scopes are pushed
\param pop_eh - a callback invoked when scopes are poped
\param fresh_eh - a solver may spawn new solvers internally. This callback is used to produce a fresh user_context to be associated with fresh solvers.
def_API('Z3_solver_propagate_init', VOID, (_in(CONTEXT), _in(SOLVER), _in(VOID_PTR), _fnptr(Z3_push_eh), _fnptr(Z3_pop_eh), _fnptr(Z3_fresh_eh)))
*/
void Z3_API Z3_solver_propagate_init(
@ -6724,6 +6772,8 @@ extern "C" {
The supported expression types are
- Booleans
- Bit-vectors
def_API('Z3_solver_propagate_fixed', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_fixed_eh)))
*/
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh);
@ -6740,25 +6790,50 @@ extern "C" {
The callback context can only be accessed (for propagation and for dynamically registering expressions) within a callback.
If the callback context gets used for propagation or conflicts, those propagations take effect and
may trigger new decision variables to be set.
def_API('Z3_solver_propagate_final', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_final_eh)))
*/
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);
/**
\brief register a callback on expression equalities.
def_API('Z3_solver_propagate_eq', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_eq_eh)))
*/
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
/**
\brief register a callback on expression dis-equalities.
def_API('Z3_solver_propagate_diseq', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_eq_eh)))
*/
void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
/**
* \brief register a callback when a new expression with a registered function is used by the solver
* The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.
\brief register a callback when a new expression with a registered function is used by the solver
The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.
def_API('Z3_solver_propagate_created', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_created_eh)))
*/
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
/**
\brief register a callback when the solver decides to split on a registered expression.
The callback may set the passed expression to another registered expression which will be selected instead.
In case the expression is a bitvector the bit to split on is determined by the bit argument and the
truth-value to try first is given by is_pos. In case the truth value is undefined the solver will decide.
def_API('Z3_solver_propagate_decide', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_decide_eh)))
*/
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
/**
Sets the next expression to split on
def_API('Z3_solver_next_split', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(AST), _in(UINT), _in(LBOOL)))
*/
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase);
/**
Create uninterpreted function declaration for the user propagator.
When expressions using the function are created by the solver invoke a callback
@ -6817,7 +6892,7 @@ extern "C" {
\sa Z3_solver_check_assumptions
def_API('Z3_solver_check', INT, (_in(CONTEXT), _in(SOLVER)))
def_API('Z3_solver_check', LBOOL, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
@ -6830,7 +6905,7 @@ extern "C" {
\sa Z3_solver_check
def_API('Z3_solver_check_assumptions', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST)))
def_API('Z3_solver_check_assumptions', LBOOL, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST)))
*/
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
unsigned num_assumptions, Z3_ast const assumptions[]);
@ -6851,7 +6926,7 @@ extern "C" {
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
The function return \c Z3_L_FALSE if the current assertions are not satisfiable.
def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
def_API('Z3_get_implied_equalities', LBOOL, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*/
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
Z3_solver s,
@ -6862,7 +6937,7 @@ extern "C" {
/**
\brief retrieve consequences from solver that determine values of the supplied function symbols.
def_API('Z3_solver_get_consequences', INT, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))
def_API('Z3_solver_get_consequences', LBOOL, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))
*/
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,

4
src/api/z3_fixedpoint.h
View file

@ -109,7 +109,7 @@ extern "C" {
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
def_API('Z3_fixedpoint_query', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST)))
def_API('Z3_fixedpoint_query', LBOOL, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST)))
*/
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query);
@ -123,7 +123,7 @@ extern "C" {
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
def_API('Z3_fixedpoint_query_relations', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL)))
def_API('Z3_fixedpoint_query_relations', LBOOL, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL)))
*/
Z3_lbool Z3_API Z3_fixedpoint_query_relations(
Z3_context c, Z3_fixedpoint d,

2
src/api/z3_optimization.h
View file

@ -151,7 +151,7 @@ extern "C" {
\sa Z3_optimize_get_statistics
\sa Z3_optimize_get_unsat_core
def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
def_API('Z3_optimize_check', LBOOL, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
*/
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);

1
src/api/z3_private.h
View file

@ -18,7 +18,6 @@ Notes:
--*/
#include<iostream>
#include "util/rational.h"
#include "api/z3_macros.h"

1
src/api/z3_replayer.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include "util/stream_buffer.h"
#include "util/symbol.h"
#include "util/trace.h"
#include<iostream>
#include<sstream>
#include<vector>

1
src/api/z3_replayer.h
View file

@ -18,7 +18,6 @@ Notes:
--*/
#pragma once
#include<iostream>
#include "api/z3.h"
#include "util/z3_exception.h"

2
src/api/z3_spacer.h
View file

@ -40,7 +40,7 @@ extern "C" {
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
def_API('Z3_fixedpoint_query_from_lvl', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(UINT)))
def_API('Z3_fixedpoint_query_from_lvl', LBOOL, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(UINT)))
*/
Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c,Z3_fixedpoint d, Z3_ast query, unsigned lvl);

36
src/ast/array_decl_plugin.cpp
View file

@ -527,6 +527,19 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return nullptr;
}
return mk_array_ext(arity, domain, parameters[0].get_int());
case OP_ARRAY_MAXDIFF:
case OP_ARRAY_MINDIFF: {
if (num_parameters != 0)
m_manager->raise_exception("min/maxdiff don't take any parameters");
if (arity != 2 || domain[0] != domain[1] || !is_array_sort(domain[0]) || 1 != get_array_arity(domain[0]))
m_manager->raise_exception("min/maxdiff don't take two arrays of same sort and with integer index");
sort* idx = get_array_domain(domain[0], 0);
arith_util arith(*m_manager);
if (!arith.is_int(idx))
m_manager->raise_exception("min/maxdiff take integer index domain");
return m_manager->mk_func_decl(k == OP_ARRAY_MAXDIFF ? symbol("maxdiff") : symbol("mindiff"),
arity, domain, arith.mk_int(), func_decl_info(m_family_id, k));
}
case OP_ARRAY_DEFAULT:
return mk_default(arity, domain);
case OP_SET_UNION:
@ -587,6 +600,10 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF));
op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF));
#if 0
op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE));
op_names.push_back(builtin_name("card", OP_SET_CARD));
@ -613,6 +630,24 @@ bool array_decl_plugin::is_fully_interp(sort * s) const {
return m_manager->is_fully_interp(get_array_range(s));
}
bool array_decl_plugin::is_value(app * _e) const {
expr* e = _e;
array_util u(*m_manager);
while (true) {
if (u.is_const(e, e))
return m_manager->is_value(e);
if (u.is_store(e)) {
for (unsigned i = 1; i < to_app(e)->get_num_args(); ++i)
if (!m_manager->is_value(to_app(e)->get_arg(i)))
return false;
e = to_app(e)->get_arg(0);
continue;
}
return false;
}
}
func_decl * array_recognizers::get_as_array_func_decl(expr * n) const {
SASSERT(is_as_array(n));
return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast());
@ -687,3 +722,4 @@ func_decl* array_util::mk_array_ext(sort *domain, unsigned i) {
parameter p(i);
return m_manager.mk_func_decl(m_fid, OP_ARRAY_EXT, 1, &p, 2, domains);
}

11
src/ast/array_decl_plugin.h
View file

@ -45,6 +45,8 @@ enum array_op_kind {
OP_ARRAY_EXT,
OP_ARRAY_DEFAULT,
OP_ARRAY_MAP,
OP_ARRAY_MAXDIFF,
OP_ARRAY_MINDIFF,
OP_SET_UNION,
OP_SET_INTERSECT,
OP_SET_DIFFERENCE,
@ -135,6 +137,9 @@ class array_decl_plugin : public decl_plugin {
expr * get_some_value(sort * s) override;
bool is_fully_interp(sort * s) const override;
bool is_value(app * e) const override;
};
class array_recognizers {
@ -157,6 +162,8 @@ public:
bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
bool is_maxdiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAXDIFF); }
bool is_mindiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MINDIFF); }
bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); }
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
@ -182,6 +189,8 @@ public:
bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
MATCH_BINARY(is_subset);
MATCH_BINARY(is_maxdiff);
MATCH_BINARY(is_mindiff);
};
class array_util : public array_recognizers {
@ -272,6 +281,8 @@ public:
func_decl * mk_array_ext(sort* domain, unsigned i);
sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
sort * mk_array_sort(sort* a, sort* b, sort* range) { sort* dom[2] = { a, b }; return mk_array_sort(2, dom, range); }
sort * mk_array_sort(sort* a, sort* b, sort* c, sort* range) { sort* dom[3] = { a, b, c}; return mk_array_sort(3, dom, range); }
sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);

15
src/ast/ast.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include "ast/arith_decl_plugin.h"
#include "ast/ast_translation.h"
#include "util/z3_version.h"
#include <iostream>
// -----------------------------------
@ -498,9 +499,9 @@ bool compare_nodes(ast const * n1, ast const * n2) {
template<typename T>
inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_value) {
if (size == 0)
return init_value;
switch (size) {
case 0:
return init_value;
case 1:
return combine_hash(array[0]->hash(), init_value);
case 2:
@ -993,7 +994,7 @@ sort * basic_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
}
func_decl * basic_decl_plugin::mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache) {
unsigned id = s->get_decl_id();
unsigned id = s->get_small_id();
force_ptr_array_size(cache, id + 1);
if (cache[id] == 0) {
sort * domain[2] = { s, s};
@ -1009,7 +1010,7 @@ func_decl * basic_decl_plugin::mk_eq_decl_core(char const * name, decl_kind k, s
}
func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
unsigned id = s->get_decl_id();
unsigned id = s->get_small_id();
force_ptr_array_size(m_ite_decls, id + 1);
if (m_ite_decls[id] == 0) {
sort * domain[3] = { m_bool_sort, s, s};
@ -1672,12 +1673,12 @@ void ast_manager::add_lambda_def(func_decl* f, quantifier* q) {
}
quantifier* ast_manager::is_lambda_def(func_decl* f) {
if (f->get_info() && f->get_info()->is_lambda()) {
if (f->get_info() && f->get_info()->is_lambda())
return m_lambda_defs[f];
}
return nullptr;
}
void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
SASSERT(m_plugins.get(id, 0) == 0);
m_plugins.setx(id, plugin, 0);
@ -2413,7 +2414,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
static void trace_quant(std::ostream& strm, quantifier* q) {
strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
<< " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls();
<< " #" << q->get_id() << " " << ensure_quote(q->get_qid()) << " " << q->get_num_decls();
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
strm << " #" << q->get_pattern(i)->get_id();
}

18
src/ast/ast.h
View file

@ -272,6 +272,7 @@ public:
family_id get_family_id() const { return m_family_id; }
decl_kind get_decl_kind() const { return m_kind; }
bool is_decl_of(family_id fid, decl_kind k) const { return m_family_id == fid && k == m_kind; }
unsigned get_num_parameters() const { return m_parameters.size(); }
parameter const & get_parameter(unsigned idx) const { return m_parameters[idx]; }
parameter const * get_parameters() const { return m_parameters.begin(); }
@ -572,11 +573,12 @@ protected:
decl(ast_kind k, symbol const & name, decl_info * info):ast(k), m_name(name), m_info(info) {}
public:
unsigned get_decl_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; }
unsigned get_small_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; }
symbol const & get_name() const { return m_name; }
decl_info * get_info() const { return m_info; }
family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
decl_kind get_decl_kind() const { return m_info == nullptr ? null_decl_kind : m_info->get_decl_kind(); }
bool is_decl_of(family_id fid, decl_kind k) const { return m_info && m_info->is_decl_of(fid, k); }
unsigned get_num_parameters() const { return m_info == nullptr ? 0 : m_info->get_num_parameters(); }
parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
@ -671,6 +673,9 @@ protected:
public:
sort* get_sort() const;
unsigned get_small_id() const { return get_id(); }
};
// -----------------------------------
@ -715,7 +720,7 @@ public:
unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
parameter const* get_parameters() const { return get_decl()->get_parameters(); }
bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
bool is_app_of(family_id fid, decl_kind k) const { return m_decl->is_decl_of(fid, k); }
unsigned get_num_args() const { return m_num_args; }
expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
expr * const * get_args() const { return m_args; }
@ -1615,7 +1620,7 @@ public:
bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; }
void add_lambda_def(func_decl* f, quantifier* q);
quantifier* is_lambda_def(func_decl* f);
quantifier* is_lambda_def(app* e) { return is_lambda_def(e->get_decl()); }
symbol const& lambda_def_qid() const { return m_lambda_def; }
@ -1914,9 +1919,8 @@ public:
return mk_fresh_const(prefix.c_str(), s, skolem);
}
app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) {
auto str = prefix.str();
return mk_fresh_const(str.c_str(), s, skolem);
app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) {
return mk_const(mk_fresh_func_decl(prefix, symbol::null, 0, nullptr, s, skolem));
}
symbol mk_fresh_var_name(char const * prefix = nullptr);
@ -2574,7 +2578,7 @@ typedef ast_ref_fast_mark2 expr_ref_fast_mark2;
when N is deleted.
*/
class ast_mark {
struct decl2uint { unsigned operator()(decl const & d) const { return d.get_decl_id(); } };
struct decl2uint { unsigned operator()(decl const & d) const { return d.get_small_id(); } };
obj_mark<expr> m_expr_marks;
obj_mark<decl, bit_vector, decl2uint> m_decl_marks;
public:

2
src/ast/ast_ll_pp.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "ast/ast_ll_pp.h"
#include "ast/for_each_ast.h"
#include "ast/arith_decl_plugin.h"
#include "ast/datatype_decl_plugin.h"

2
src/ast/ast_ll_pp.h
View file

@ -19,7 +19,7 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include<iostream>
#include<ostream>
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs=true, bool compact=true);
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs=true, bool compact=true);

2
src/ast/ast_pp_dot.h
View file

@ -6,7 +6,7 @@ Abstract: Pretty-printer for proofs in Graphviz format
#pragma once
#include <iostream>
#include <ostream>
#include "ast/ast_pp.h"
class ast_pp_dot {

Some files were not shown because too many files have changed in this diff Show more