From 66d0fb54775d8ce6d0e7d05e8923051fc6a7217d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Feb 2026 21:24:40 -0800 Subject: [PATCH] git bindings v1.0 --- README-CMake.md | 36 ++ README.md | 8 + build_z3.bat | 30 ++ doc/CMakeLists.txt | 24 + doc/README | 8 +- doc/mk_api_doc.py | 130 +++++- doc/mk_go_doc.py | 654 +++++++++++++++++++++++++++ doc/test_go_doc/README.html | 303 +++++++++++++ doc/test_go_doc/index.html | 164 +++++++ doc/website.dox.in | 2 +- doc/z3api.cfg.in | 6 +- examples/go/README.md | 145 ++++++ examples/go/advanced_example.go | 313 +++++++++++++ examples/go/basic_example.go | 98 ++++ examples/go/go.mod | 8 + scripts/mk_util.py | 9 +- src/CMakeLists.txt | 12 + src/api/go/CMakeLists.txt | 54 +++ src/api/go/README.md | 331 ++++++++++++++ src/api/go/add_godoc.py | 89 ++++ src/api/go/arith.go | 126 ++++++ src/api/go/array.go | 29 ++ src/api/go/bitvec.go | 160 +++++++ src/api/go/datatype.go | 293 ++++++++++++ src/api/go/fixedpoint.go | 282 ++++++++++++ src/api/go/fp.go | 139 ++++++ src/api/go/go.mod | 6 + src/api/go/log.go | 67 +++ src/api/go/optimize.go | 218 +++++++++ src/api/go/seq.go | 232 ++++++++++ src/api/go/solver.go | 263 +++++++++++ src/api/go/tactic.go | 294 ++++++++++++ src/api/go/z3.go | 763 ++++++++++++++++++++++++++++++++ 33 files changed, 5289 insertions(+), 7 deletions(-) create mode 100644 build_z3.bat create mode 100644 doc/mk_go_doc.py create mode 100644 doc/test_go_doc/README.html create mode 100644 doc/test_go_doc/index.html create mode 100644 examples/go/README.md create mode 100644 examples/go/advanced_example.go create mode 100644 examples/go/basic_example.go create mode 100644 examples/go/go.mod create mode 100644 src/api/go/CMakeLists.txt create mode 100644 src/api/go/README.md create mode 100644 src/api/go/add_godoc.py create mode 100644 src/api/go/arith.go create mode 100644 src/api/go/array.go create mode 100644 src/api/go/bitvec.go create mode 100644 src/api/go/datatype.go create mode 100644 src/api/go/fixedpoint.go create mode 100644 src/api/go/fp.go create mode 100644 src/api/go/go.mod create mode 100644 src/api/go/log.go create mode 100644 src/api/go/optimize.go create mode 100644 src/api/go/seq.go create mode 100644 src/api/go/solver.go create mode 100644 src/api/go/tactic.go create mode 100644 src/api/go/z3.go diff --git a/README-CMake.md b/README-CMake.md index 26bde8f37..c9edb9378 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -423,6 +423,7 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``Z3_BUILD_GO_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Go bindings will be built. Requires Go 1.20+ and ``Z3_BUILD_LIBZ3_SHARED=ON``. * ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built. * ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built. * ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings. @@ -523,6 +524,41 @@ where ``VERSION`` is the Z3 version. Under non Windows systems a symbolic link named ``com.microsoft.z3.jar`` is provided. This symbolic link is not created when building under Windows. +### Go bindings + +Go bindings can be built by setting ``Z3_BUILD_GO_BINDINGS=ON``. The Go bindings use CGO to wrap +the Z3 C API, so you'll need: + +* Go 1.20 or later installed on your system +* ``Z3_BUILD_LIBZ3_SHARED=ON`` (Go bindings require the shared library) + +Example: + +``` +mkdir build +cd build +cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ../ +make +``` + +If CMake detects a Go installation (via ``go`` executable in PATH), it will create two optional targets: + +* ``go-bindings`` - Builds the Go bindings +* ``test-go-examples`` - Runs the Go examples + +Note that the Go bindings are installed as source files (not compiled) since Go packages are +typically distributed as source and compiled by the user's Go toolchain. + +To use the installed Go bindings, set the appropriate CGO flags: + +``` +export CGO_CFLAGS="-I/path/to/z3/include" +export CGO_LDFLAGS="-L/path/to/z3/lib -lz3" +export LD_LIBRARY_PATH="/path/to/z3/lib:$LD_LIBRARY_PATH" # Linux/macOS +``` + +For detailed usage examples and API documentation, see ``src/api/go/README.md`` and ``examples/go/``. + ## Developer/packager notes These notes are help developers and packagers of Z3. diff --git a/README.md b/README.md index ddda3662c..04fe821ec 100644 --- a/README.md +++ b/README.md @@ -195,6 +195,14 @@ For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and trou See [``examples/java``](examples/java) for examples. +### ``Go`` + +Use the ``--go`` command line flag with ``mk_make.py`` to enable building these. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build. + +With CMake, use the ``-DZ3_BUILD_GO_BINDINGS=ON`` option. + +See [``examples/go``](examples/go) for examples and [``src/api/go/README.md``](src/api/go/README.md) for complete API documentation. + ### ``OCaml`` Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these. diff --git a/build_z3.bat b/build_z3.bat new file mode 100644 index 000000000..57b0c233b --- /dev/null +++ b/build_z3.bat @@ -0,0 +1,30 @@ +@echo off +REM Z3 Build Script + +echo Checking for build directory... +if not exist C:\z3\build ( + echo Creating build directory... + mkdir C:\z3\build +) else ( + echo Build directory already exists +) + +echo Changing to build directory... +cd /d C:\z3\build + +echo Running CMake configuration... +cmake .. +if errorlevel 1 ( + echo CMake configuration failed! + exit /b 1 +) + +echo Building Z3 with parallel 8... +cmake --build . --parallel 8 +if errorlevel 1 ( + echo Build failed! + exit /b 1 +) + +echo Build completed successfully! +exit /b 0 diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index 6f81edf0d..4b1de889b 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -9,6 +9,7 @@ set(MK_API_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_api_doc.py") set(PYTHON_API_OPTIONS "") set(DOTNET_API_OPTIONS "") set(JAVA_API_OPTIONS "") +set(GO_API_OPTIONS "") SET(DOC_EXTRA_DEPENDS "") if (Z3_BUILD_PYTHON_BINDINGS) @@ -41,6 +42,15 @@ else() list(APPEND JAVA_API_OPTIONS "--no-java") endif() +if (Z3_BUILD_GO_BINDINGS) + list(APPEND GO_API_OPTIONS "--go") + list(APPEND GO_API_OPTIONS "--go-search-paths" + "${PROJECT_SOURCE_DIR}/src/api/go" + ) +else() + # Go bindings don't have a --no-go option, just omit --go +endif() + option(Z3_ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON) if (Z3_ALWAYS_BUILD_DOCS) set(ALWAYS_BUILD_DOCS_ARG "ALL") @@ -66,12 +76,26 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG} ${PYTHON_API_OPTIONS} ${DOTNET_API_OPTIONS} ${JAVA_API_OPTIONS} + ${GO_API_OPTIONS} DEPENDS ${DOC_EXTRA_DEPENDS} COMMENT "Generating documentation" USES_TERMINAL ) +# Add separate target for Go documentation +if (Z3_BUILD_GO_BINDINGS) + set(MK_GO_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_go_doc.py") + add_custom_target(go_docs + COMMAND + "${Python3_EXECUTABLE}" "${MK_GO_DOC_SCRIPT}" + --output-dir "${DOC_DEST_DIR}/html/go" + --go-api-path "${PROJECT_SOURCE_DIR}/src/api/go" + COMMENT "Generating Go API documentation" + USES_TERMINAL + ) +endif() + # Remove generated documentation when running `clean` target. set_property(DIRECTORY APPEND PROPERTY ADDITIONAL_MAKE_CLEAN_FILES diff --git a/doc/README b/doc/README index e46554230..cfb34b4e5 100644 --- a/doc/README +++ b/doc/README @@ -1,7 +1,7 @@ API documentation ----------------- -To generate the API documentation for the C, C++, .NET, Java and Python APIs, we must execute +To generate the API documentation for the C, C++, .NET, Java, Python, and Go APIs, we must execute python mk_api_doc.py @@ -10,6 +10,12 @@ We must have doxygen installed in our system. The documentation will be stored in the subdirectory './api/html'. The main file is './api/html/index.html' +To include Go API documentation, use: + + python mk_api_doc.py --go + +Note: Go documentation requires Go to be installed (for godoc support). + Code documentation ------------------ diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index f5c4ff68c..ae3d6c931 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -15,24 +15,27 @@ import subprocess ML_ENABLED=False MLD_ENABLED=False JS_ENABLED=False +GO_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' +GO_API_PATH='../src/api/go' Z3PY_ENABLED=True DOTNET_ENABLED=True JAVA_ENABLED=True Z3OPTIONS_ENABLED=True DOTNET_API_SEARCH_PATHS=['../src/api/dotnet'] JAVA_API_SEARCH_PATHS=['../src/api/java'] +GO_API_SEARCH_PATHS=['../src/api/go'] 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, JS_ENABLED - global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS, JS_API_PATH + global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED, JS_ENABLED, GO_ENABLED + global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS, GO_API_SEARCH_PATHS, JS_API_PATH, GO_API_PATH parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -54,6 +57,11 @@ def parse_options(): default=False, help='Include JS/TS API documentation' ) + parser.add_argument('--go', + action='store_true', + default=False, + help='Include Go API documentation' + ) parser.add_argument('--doxygen-executable', dest='doxygen_executable', default=DOXYGEN_EXE, @@ -109,10 +117,17 @@ def parse_options(): default=JAVA_API_SEARCH_PATHS, help='Specify one or more paths to look for Java files (default: %(default)s).', ) + parser.add_argument('--go-search-paths', + dest='go_search_paths', + nargs='+', + default=GO_API_SEARCH_PATHS, + help='Specify one or more paths to look for Go files (default: %(default)s).', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml MLD_ENABLED = pargs.mld JS_ENABLED = pargs.js + GO_ENABLED = pargs.go BUILD_DIR = pargs.build DOXYGEN_EXE = pargs.doxygen_executable TEMP_DIR = pargs.temp_dir @@ -123,6 +138,7 @@ def parse_options(): JAVA_ENABLED = not pargs.no_java DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths JAVA_API_SEARCH_PATHS = pargs.java_search_paths + GO_API_SEARCH_PATHS = pargs.go_search_paths if Z3PY_ENABLED: if not os.path.exists(Z3PY_PACKAGE_PATH): @@ -288,6 +304,18 @@ try: print("Java documentation disabled") doxygen_config_substitutions['JAVA_API_FILES'] = '' doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '' + if GO_ENABLED: + print("Go documentation enabled") + doxygen_config_substitutions['GO_API_FILES'] = '*.go' + go_api_search_path_str = "" + for p in GO_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + go_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['GO_API_SEARCH_PATHS'] = go_api_search_path_str + else: + print("Go documentation disabled") + doxygen_config_substitutions['GO_API_FILES'] = '' + doxygen_config_substitutions['GO_API_SEARCH_PATHS'] = '' if JS_ENABLED: print('Javascript documentation enabled') else: @@ -350,6 +378,13 @@ try: prefix=bullet_point_prefix) else: website_dox_substitutions['JS_API'] = '' + if GO_ENABLED: + website_dox_substitutions['GO_API'] = ( + '{prefix}Go API' + ).format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['GO_API'] = '' configure_file( doc_path('website.dox.in'), temp_path('website.dox'), @@ -428,6 +463,97 @@ try: exit(1) print("Generated Javascript documentation.") + if GO_ENABLED: + go_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'go') + mk_dir(go_output_dir) + go_api_abs_path = os.path.abspath(GO_API_PATH) + + # Check if godoc is available + godoc_available = False + try: + subprocess.check_output(['go', 'version'], stderr=subprocess.STDOUT) + godoc_available = True + except (subprocess.CalledProcessError, FileNotFoundError): + print("WARNING: Go is not installed. Skipping godoc generation.") + godoc_available = False + + if godoc_available: + # Generate godoc HTML for each Go file + go_files = [ + 'z3.go', 'solver.go', 'tactic.go', 'bitvec.go', + 'fp.go', 'seq.go', 'datatype.go', 'optimize.go' + ] + + # Create a simple HTML index + index_html = os.path.join(go_output_dir, 'index.html') + with open(index_html, 'w') as f: + f.write('\n\n\n') + f.write('Z3 Go API Documentation\n') + f.write('\n') + f.write('\n\n') + f.write('

Z3 Go API Documentation

\n') + f.write('

Go bindings for the Z3 Theorem Prover.

\n') + f.write('

Package: github.com/Z3Prover/z3/src/api/go

\n') + f.write('\n') + + f.write('

Usage

\n') + f.write('
\n')
+                f.write('import "github.com/Z3Prover/z3/src/api/go"\n\n')
+                f.write('ctx := z3.NewContext()\n')
+                f.write('solver := ctx.NewSolver()\n')
+                f.write('x := ctx.MkIntConst("x")\n')
+                f.write('solver.Assert(ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort())))\n')
+                f.write('if solver.Check() == z3.Satisfiable {\n')
+                f.write('    fmt.Println("sat")\n')
+                f.write('}\n')
+                f.write('
\n') + + f.write('

Installation

\n') + f.write('

See README for build instructions.

\n') + f.write('

Go back to main API documentation.

\n') + f.write('\n\n') + + print("Generated Go documentation.") + print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY)) except Exception: exctype, value = sys.exc_info()[:2] diff --git a/doc/mk_go_doc.py b/doc/mk_go_doc.py new file mode 100644 index 000000000..5ba122979 --- /dev/null +++ b/doc/mk_go_doc.py @@ -0,0 +1,654 @@ +#!/usr/bin/env python +# Copyright (c) Microsoft Corporation 2025 +""" +Z3 Go API documentation generator script + +This script generates HTML documentation for the Z3 Go bindings. +It creates a browsable HTML interface for the Go API documentation. +""" + +import os +import sys +import subprocess +import argparse +import re + +SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__)) +GO_API_PATH = os.path.join(SCRIPT_DIR, '..', 'src', 'api', 'go') +OUTPUT_DIR = os.path.join(SCRIPT_DIR, 'api', 'html', 'go') + +def extract_types_and_functions(filepath): + """Extract type and function names from a Go source file.""" + types = [] + functions = [] + + try: + with open(filepath, 'r', encoding='utf-8') as f: + content = f.read() + + # Extract type declarations + type_pattern = r'type\s+(\w+)\s+(?:struct|interface)' + types = re.findall(type_pattern, content) + + # Extract function/method declarations + # Match both: func Name() and func (r *Type) Name() + func_pattern = r'func\s+(?:\([^)]+\)\s+)?(\w+)\s*\(' + functions = re.findall(func_pattern, content) + + except Exception as e: + print(f"Warning: Could not parse {filepath}: {e}") + + return types, functions + +def extract_detailed_api(filepath): + """Extract detailed type and function information with signatures and comments.""" + types_info = {} + functions_info = [] + context_methods = [] # Special handling for Context methods + + try: + with open(filepath, 'r', encoding='utf-8') as f: + lines = f.readlines() + i = 0 + + while i < len(lines): + line = lines[i].strip() + + # Extract type with comment + if line.startswith('type ') and ('struct' in line or 'interface' in line): + # Look back for comment + comment = "" + j = i - 1 + while j >= 0 and (lines[j].strip().startswith('//') or lines[j].strip() == ''): + if lines[j].strip().startswith('//'): + comment = lines[j].strip()[2:].strip() + " " + comment + j -= 1 + + match = re.match(r'type\s+(\w+)\s+', line) + if match: + type_name = match.group(1) + types_info[type_name] = { + 'comment': comment.strip(), + 'methods': [] + } + + # Extract function/method with signature and comment + if line.startswith('func '): + # Look back for comment + comment = "" + j = i - 1 + while j >= 0 and (lines[j].strip().startswith('//') or lines[j].strip() == ''): + if lines[j].strip().startswith('//'): + comment = lines[j].strip()[2:].strip() + " " + comment + j -= 1 + + # Extract full signature (may span multiple lines) + signature = line + k = i + 1 + while k < len(lines) and '{' not in signature: + signature += ' ' + lines[k].strip() + k += 1 + + # Remove body + if '{' in signature: + signature = signature[:signature.index('{')].strip() + + # Parse receiver if method + method_match = re.match(r'func\s+\(([^)]+)\)\s+(\w+)', signature) + func_match = re.match(r'func\s+(\w+)', signature) + + if method_match: + receiver = method_match.group(1).strip() + func_name = method_match.group(2) + # Extract receiver type + receiver_type = receiver.split()[-1].strip('*') + + # Only add if function name is public + if func_name[0].isupper(): + if receiver_type == 'Context': + # Special handling for Context methods - add to context_methods + context_methods.append({ + 'name': func_name, + 'signature': signature, + 'comment': comment.strip() + }) + elif receiver_type in types_info: + types_info[receiver_type]['methods'].append({ + 'name': func_name, + 'signature': signature, + 'comment': comment.strip() + }) + elif func_match: + func_name = func_match.group(1) + # Only add if it's public (starts with capital) + if func_name[0].isupper(): + functions_info.append({ + 'name': func_name, + 'signature': signature, + 'comment': comment.strip() + }) + + i += 1 + + # If we have Context methods but no other content, return them as functions + if context_methods and not types_info and not functions_info: + functions_info = context_methods + elif context_methods: + # Add Context pseudo-type + types_info['Context'] = { + 'comment': 'Context methods (receiver omitted for clarity)', + 'methods': context_methods + } + + except Exception as e: + print(f"Warning: Could not parse detailed API from {filepath}: {e}") + + return types_info, functions_info + +def extract_package_comment(filepath): + """Extract the package-level documentation comment from a Go file.""" + try: + with open(filepath, 'r', encoding='utf-8') as f: + lines = f.readlines() + comment_lines = [] + in_comment = False + + for line in lines: + stripped = line.strip() + if stripped.startswith('/*'): + in_comment = True + comment_lines.append(stripped[2:].strip()) + elif in_comment: + if '*/' in stripped: + comment_lines.append(stripped.replace('*/', '').strip()) + break + comment_lines.append(stripped.lstrip('*').strip()) + elif stripped.startswith('//'): + comment_lines.append(stripped[2:].strip()) + elif stripped.startswith('package'): + break + + return ' '.join(comment_lines).strip() if comment_lines else None + except Exception as e: + return None + +def parse_args(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('-o', '--output-dir', + dest='output_dir', + default=OUTPUT_DIR, + help='Output directory for documentation (default: %(default)s)', + ) + parser.add_argument('--go-api-path', + dest='go_api_path', + default=GO_API_PATH, + help='Path to Go API source files (default: %(default)s)', + ) + return parser.parse_args() + +def check_go_installed(): + """Check if Go is installed and available.""" + try: + # Try to find go in common locations + go_paths = [ + 'go', + 'C:\\Program Files\\Go\\bin\\go.exe', + 'C:\\Go\\bin\\go.exe', + ] + + for go_cmd in go_paths: + try: + result = subprocess.run([go_cmd, 'version'], + capture_output=True, + text=True, + check=True, + timeout=5) + print(f"Found Go: {result.stdout.strip()}") + return go_cmd + except (subprocess.CalledProcessError, FileNotFoundError, subprocess.TimeoutExpired): + continue + + print("WARNING: Go is not installed or not in PATH") + print("Install Go from https://golang.org/dl/ for enhanced documentation") + return None + except Exception as e: + print(f"WARNING: Could not check Go installation: {e}") + return None + +def extract_package_comment(go_file_path): + """Extract package-level documentation comment from a Go file.""" + try: + with open(go_file_path, 'r', encoding='utf-8') as f: + lines = f.readlines() + in_comment = False + comment_lines = [] + + for line in lines: + stripped = line.strip() + if stripped.startswith('/*'): + in_comment = True + comment_lines.append(stripped[2:].strip()) + elif in_comment: + if stripped.endswith('*/'): + comment_lines.append(stripped[:-2].strip()) + break + comment_lines.append(stripped.lstrip('*').strip()) + elif stripped.startswith('//'): + comment_lines.append(stripped[2:].strip()) + elif stripped.startswith('package '): + break + + return ' '.join(comment_lines).strip() + except Exception as e: + print(f"Warning: Could not extract comment from {go_file_path}: {e}") + return "" + +def generate_godoc_markdown(go_cmd, go_api_path, output_dir): + """Generate markdown documentation using godoc.""" + print("Generating documentation with godoc...") + + os.makedirs(output_dir, exist_ok=True) + + try: + # Change to the Go API directory + orig_dir = os.getcwd() + os.chdir(go_api_path) + + # Run go doc to get package documentation + result = subprocess.run( + [go_cmd, 'doc', '-all'], + capture_output=True, + text=True, + timeout=30 + ) + + if result.returncode == 0: + # Create markdown file + doc_text = result.stdout + godoc_md = os.path.join(output_dir, 'godoc.md') + + with open(godoc_md, 'w', encoding='utf-8') as f: + f.write('# Z3 Go API Documentation (godoc)\n\n') + f.write(doc_text) + + print(f"Generated godoc markdown at: {godoc_md}") + os.chdir(orig_dir) + return True + else: + print(f"godoc returned error: {result.stderr}") + os.chdir(orig_dir) + return False + + except Exception as e: + print(f"Error generating godoc markdown: {e}") + try: + os.chdir(orig_dir) + except: + pass + return False + +def generate_module_page(module_filename, description, go_api_path, output_dir): + """Generate a detailed HTML page for a single Go module.""" + file_path = os.path.join(go_api_path, module_filename) + if not os.path.exists(file_path): + return + + module_name = module_filename.replace('.go', '') + output_path = os.path.join(output_dir, f'{module_name}.html') + + # Extract detailed API information + types_info, functions_info = extract_detailed_api(file_path) + + with open(output_path, 'w', encoding='utf-8') as f: + f.write('\n\n\n') + f.write(' \n') + f.write(f' {module_filename} - Z3 Go API\n') + f.write(' \n') + f.write('\n\n') + + f.write('
\n') + f.write(f'

{module_filename}

\n') + f.write(f'

{description}

\n') + f.write('
\n') + + f.write('
\n') + f.write('
\n') + f.write(' ← Back to Index\n') + f.write(' Complete API Reference (markdown)\n') + f.write(' README\n') + f.write(' All Languages\n') + f.write('
\n') + + # Types section + if types_info: + f.write('

Types

\n') + for type_name in sorted(types_info.keys()): + type_data = types_info[type_name] + f.write('
\n') + f.write(f'

type {type_name}

\n') + if type_data['comment']: + f.write(f'

{type_data["comment"]}

\n') + + # Methods + if type_data['methods']: + f.write('
\n') + f.write('

Methods:

\n') + for method in sorted(type_data['methods'], key=lambda m: m['name']): + f.write('
\n') + f.write(f'

{method["name"]}

\n') + f.write(f'
{method["signature"]}
\n') + if method['comment']: + f.write(f'

{method["comment"]}

\n') + f.write('
\n') + f.write('
\n') + f.write('
\n') + + # Package functions section + if functions_info: + f.write('

Functions

\n') + f.write('
\n') + for func in sorted(functions_info, key=lambda f: f['name']): + f.write('
\n') + f.write(f'

{func["name"]}

\n') + f.write(f'
{func["signature"]}
\n') + if func['comment']: + f.write(f'

{func["comment"]}

\n') + f.write('
\n') + f.write('
\n') + + if not types_info and not functions_info: + f.write('

No public API documentation extracted. See godoc for complete reference.

\n') + + f.write('
\n') + f.write(' ← Back to Index\n') + f.write('
\n') + f.write('
\n') + f.write('\n\n') + + print(f"Generated module page: {output_path}") + +def generate_html_docs(go_api_path, output_dir): + """Generate HTML documentation for Go bindings.""" + + # Create output directory + os.makedirs(output_dir, exist_ok=True) + + # Go source files and their descriptions + go_files = { + 'z3.go': 'Core types (Context, Config, Symbol, Sort, Expr, FuncDecl, Quantifier, Lambda) and basic operations', + 'solver.go': 'Solver and Model API for SMT solving', + 'tactic.go': 'Tactics, Goals, Probes, and Parameters for goal-based solving', + 'arith.go': 'Arithmetic operations (integers, reals) and comparisons', + 'array.go': 'Array operations (select, store, constant arrays)', + 'bitvec.go': 'Bit-vector operations and constraints', + 'fp.go': 'IEEE 754 floating-point operations', + 'seq.go': 'Sequences, strings, and regular expressions', + 'datatype.go': 'Algebraic datatypes, tuples, and enumerations', + 'optimize.go': 'Optimization with maximize/minimize objectives', + 'fixedpoint.go': 'Fixedpoint solver for Datalog and constrained Horn clauses (CHC)', + 'log.go': 'Interaction logging for debugging and analysis', + } + + # Generate main index.html + index_path = os.path.join(output_dir, 'index.html') + with open(index_path, 'w', encoding='utf-8') as f: + f.write('\n') + f.write('\n') + f.write('\n') + f.write(' \n') + f.write(' \n') + f.write(' Z3 Go API Documentation\n') + f.write(' \n') + f.write('\n') + f.write('\n') + + f.write('
\n') + f.write('

Z3 Go API Documentation

\n') + f.write('

Go bindings for the Z3 Theorem Prover

\n') + f.write('
\n') + + f.write('
\n') + + # Overview section + f.write('
\n') + f.write('

Overview

\n') + f.write('

The Z3 Go bindings provide idiomatic Go access to the Z3 SMT solver. These bindings use CGO to wrap the Z3 C API and provide automatic memory management through Go finalizers.

\n') + f.write('

Package: github.com/Z3Prover/z3/src/api/go

\n') + f.write('
\n') + + # Quick start + f.write('
\n') + f.write('

Quick Start

\n') + f.write('
\n') + f.write(' 
package main\n\n')
+        f.write('import (\n')
+        f.write('    "fmt"\n')
+        f.write('    "github.com/Z3Prover/z3/src/api/go"\n')
+        f.write(')\n\n')
+        f.write('func main() {\n')
+        f.write('    // Create a context\n')
+        f.write('    ctx := z3.NewContext()\n\n')
+        f.write('    // Create integer variable\n')
+        f.write('    x := ctx.MkIntConst("x")\n\n')
+        f.write('    // Create solver\n')
+        f.write('    solver := ctx.NewSolver()\n\n')
+        f.write('    // Add constraint: x > 0\n')
+        f.write('    zero := ctx.MkInt(0, ctx.MkIntSort())\n')
+        f.write('    solver.Assert(ctx.MkGt(x, zero))\n\n')
+        f.write('    // Check satisfiability\n')
+        f.write('    if solver.Check() == z3.Satisfiable {\n')
+        f.write('        fmt.Println("sat")\n')
+        f.write('        model := solver.Model()\n')
+        f.write('        if val, ok := model.Eval(x, true); ok {\n')
+        f.write('            fmt.Println("x =", val.String())\n')
+        f.write('        }\n')
+        f.write('    }\n')
+        f.write('}
\n') + f.write('
\n') + f.write('
\n') + + # Installation + f.write('
\n') + f.write('

Installation

\n') + f.write('
\n') + f.write('

Prerequisites:

\n') + f.write('
    \n') + f.write('
  • Go 1.20 or later
    • \n') + f.write('
  • Z3 built as a shared library
    • \n') + f.write('
  • CGO enabled (default)
    • \n') + f.write('
\n') + f.write('

Build Z3 with Go bindings:

\n') + f.write('
\n') + f.write(' 
# Using CMake\n')
+        f.write('mkdir build && cd build\n')
+        f.write('cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ..\n')
+        f.write('make\n\n')
+        f.write('# Using Python build script\n')
+        f.write('python scripts/mk_make.py --go\n')
+        f.write('cd build && make
\n') + f.write('
\n') + f.write('

Set environment variables:

\n') + f.write('
\n') + f.write(' 
export CGO_CFLAGS="-I${Z3_ROOT}/src/api"\n')
+        f.write('export CGO_LDFLAGS="-L${Z3_ROOT}/build -lz3"\n')
+        f.write('export LD_LIBRARY_PATH="${Z3_ROOT}/build:$LD_LIBRARY_PATH"
\n') + f.write('
\n') + f.write('
\n') + f.write('
\n') + + # API modules with detailed documentation + f.write('
\n') + f.write('

API Modules

\n') + + for filename, description in go_files.items(): + file_path = os.path.join(go_api_path, filename) + if os.path.exists(file_path): + module_name = filename.replace('.go', '') + + # Generate individual module page + generate_module_page(filename, description, go_api_path, output_dir) + + # Extract types and functions from the file + types, functions = extract_types_and_functions(file_path) + + f.write(f'
\n') + f.write(f'

{filename}

\n') + f.write(f'

{description}

\n') + + if types: + f.write('

Types: ') + f.write(', '.join([f'{t}' for t in sorted(types)])) + f.write('

\n') + + if functions: + # Filter public functions + public_funcs = [f for f in functions if f and len(f) > 0 and f[0].isupper()] + if public_funcs: + f.write('

Key Functions: ') + # Show first 15 functions to keep it manageable + funcs_to_show = sorted(public_funcs)[:15] + f.write(', '.join([f'{func}()' for func in funcs_to_show])) + if len(public_funcs) > 15: + f.write(f' (+{len(public_funcs)-15} more)') + f.write('

\n') + + f.write(f'

→ View full API reference

\n') + f.write('
\n') + + f.write('
\n') + + # Features section + f.write('
\n') + f.write('

Features

\n') + f.write('
    \n') + f.write('
  • Core SMT: Boolean logic, arithmetic, arrays, quantifiers
    • \n') + f.write('
  • Bit-vectors: Fixed-size bit-vector arithmetic and operations
    • \n') + f.write('
  • Floating-point: IEEE 754 floating-point arithmetic
    • \n') + f.write('
  • Strings & Sequences: String constraints and sequence operations
    • \n') + f.write('
  • Regular Expressions: Pattern matching and regex constraints
    • \n') + f.write('
  • Datatypes: Algebraic datatypes, tuples, enumerations
    • \n') + f.write('
  • Tactics: Goal-based solving with tactic combinators
    • \n') + f.write('
  • Optimization: MaxSMT with maximize/minimize objectives
    • \n') + f.write('
  • Memory Management: Automatic via Go finalizers
    • \n') + f.write('
\n') + f.write('
\n') + + # Resources + f.write('
\n') + f.write('

Resources

\n') + f.write('
    \n') + f.write('
  • Z3 GitHub Repository
    • \n') + f.write('
  • All API Documentation
    • \n') + + # Check if README exists and copy it + readme_path = os.path.join(go_api_path, 'README.md') + if os.path.exists(readme_path): + # Copy README.md to output directory + readme_dest = os.path.join(output_dir, 'README.md') + try: + import shutil + shutil.copy2(readme_path, readme_dest) + f.write('
  • Go API README (markdown)
    • \n') + print(f"Copied README.md to: {readme_dest}") + except Exception as e: + print(f"Warning: Could not copy README.md: {e}") + + # Link to godoc.md if it will be generated + f.write('
  • Complete API Reference (godoc markdown)
    • \n') + + f.write('
\n') + f.write('
\n') + + f.write(' ← Back to main API documentation\n') + f.write('
\n') + f.write('\n') + f.write('\n') + + print(f"Generated Go documentation index at: {index_path}") + return True + +def main(): + args = parse_args() + + print("Z3 Go API Documentation Generator") + print("=" * 50) + + # Check if Go is installed + go_cmd = check_go_installed() + + # Verify Go API path exists + if not os.path.exists(args.go_api_path): + print(f"ERROR: Go API path does not exist: {args.go_api_path}") + return 1 + + # Generate documentation + print(f"\nGenerating documentation from: {args.go_api_path}") + print(f"Output directory: {args.output_dir}") + + # Try godoc first if Go is available + godoc_success = False + if go_cmd: + godoc_success = generate_godoc_markdown(go_cmd, args.go_api_path, args.output_dir) + + # Always generate our custom HTML documentation + if not generate_html_docs(args.go_api_path, args.output_dir): + print("ERROR: Failed to generate documentation") + return 1 + + if godoc_success: + print("\n✓ Generated both godoc markdown and custom HTML documentation") + + print("\n" + "=" * 50) + print("Documentation generated successfully!") + print(f"Open {os.path.join(args.output_dir, 'index.html')} in your browser.") + + return 0 + +if __name__ == '__main__': + try: + sys.exit(main()) + except KeyboardInterrupt: + print("\nInterrupted by user") + sys.exit(1) + except Exception as e: + print(f"ERROR: {e}") + import traceback + traceback.print_exc() + sys.exit(1) diff --git a/doc/test_go_doc/README.html b/doc/test_go_doc/README.html new file mode 100644 index 000000000..5faf285e6 --- /dev/null +++ b/doc/test_go_doc/README.html @@ -0,0 +1,303 @@ + + + + + Z3 Go API - README + + + +# Z3 Go Bindings + +This directory contains Go language bindings for the Z3 theorem prover. + +## Overview + +The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support: + +- **Core Z3 Types**: Context, Config, Symbol, AST, Sort, Expr, FuncDecl +- **Solver Operations**: Creating solvers, asserting constraints, checking satisfiability +- **Model Manipulation**: Extracting and evaluating models +- **Boolean Logic**: And, Or, Not, Implies, Iff, Xor +- **Arithmetic**: Add, Sub, Mul, Div, Mod, comparison operators +- **Bit-vectors**: Full bit-vector arithmetic, bitwise operations, shifts, comparisons +- **Floating Point**: IEEE 754 floating-point arithmetic with rounding modes +- **Arrays**: Select, Store, constant arrays +- **Sequences/Strings**: String operations, concatenation, contains, indexing +- **Regular Expressions**: Pattern matching, Kleene star/plus, regex operations +- **Quantifiers**: Forall, Exists +- **Functions**: Function declarations and applications +- **Tactics & Goals**: Goal-based solving and tactic combinators +- **Probes**: Goal property checking +- **Datatypes**: Algebraic datatypes, tuples, enumerations, lists +- **Parameters**: Solver and tactic configuration +- **Optimize**: Optimization problems with maximize/minimize objectives + +## Building + +### Prerequisites + +- Go 1.20 or later +- Z3 library built and installed +- CGO enabled + +### With CMake + +```bash +mkdir build && cd build +cmake -DBUILD_GO_BINDINGS=ON .. +make +``` + +### With Python Build System + +```bash +python scripts/mk_make.py --go +cd build +make +``` + +## Usage + +### Basic Example + +```go +package main + +import ( + "fmt" + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + // Create a context + ctx := z3.NewContext() + + // Create variables + x := ctx.MkIntConst("x") + y := ctx.MkIntConst("y") + + // Create constraints: x + y == 10 && x > y + ten := ctx.MkInt(10, ctx.MkIntSort()) + eq := ctx.MkEq(ctx.MkAdd(x, y), ten) + gt := ctx.MkGt(x, y) + + // Create solver and check + solver := ctx.NewSolver() + solver.Assert(eq) + solver.Assert(gt) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + if xVal, ok := model.Eval(x, true); ok { + fmt.Println("x =", xVal.String()) + } + if yVal, ok := model.Eval(y, true); ok { + fmt.Println("y =", yVal.String()) + } + } +} +``` + +### Running Examples + +```bash +cd examples/go + +# Set library path (Linux/Mac) +export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH +export CGO_CFLAGS="-I../../src/api" +export CGO_LDFLAGS="-L../../build -lz3" + +# Set library path (Windows) +set PATH=..\..\build;%PATH% +set CGO_CFLAGS=-I../../src/api +set CGO_LDFLAGS=-L../../build -lz3 + +# Run example +go run basic_example.go +``` + +## API Reference + +### Context + +- `NewContext()` - Create a new Z3 context +- `NewContextWithConfig(cfg *Config)` - Create context with configuration +- `SetParam(key, value string)` - Set context parameters + +### Creating Expressions + +- `MkBoolConst(name string)` - Create Boolean variable +- `MkIntConst(name string)` - Create integer variable +- `MkRealConst(name string)` - Create real variable +- `MkInt(value int, sort *Sort)` - Create integer constant +- `MkReal(num, den int)` - Create rational constant + +### Boolean Operations + +- `MkAnd(exprs ...*Expr)` - Conjunction +- `MkOr(exprs ...*Expr)` - Disjunction +- `MkNot(expr *Expr)` - Negation +- `MkImplies(lhs, rhs *Expr)` - Implication +- `MkIff(lhs, rhs *Expr)` - If-and-only-if +- `MkXor(lhs, rhs *Expr)` - Exclusive or + +### Arithmetic Operations + +- `MkAdd(exprs ...*Expr)` - Addition +- `MkSub(exprs ...*Expr)` - Subtraction +- `MkMul(exprs ...*Expr)` - Multiplication +- `MkDiv(lhs, rhs *Expr)` - Division +- `MkMod(lhs, rhs *Expr)` - Modulo +- `MkRem(lhs, rhs *Expr)` - Remainder + +### Comparison Operations + +- `MkEq(lhs, rhs *Expr)` - Equality +- `MkDistinct(exprs ...*Expr)` - Distinct +- `MkLt(lhs, rhs *Expr)` - Less than +- `MkLe(lhs, rhs *Expr)` - Less than or equal +- `MkGt(lhs, rhs *Expr)` - Greater than +- `MkGe(lhs, rhs *Expr)` - Greater than or equal + +### Solver Operations + +- `NewSolver()` - Create a new solver +- `Assert(constraint *Expr)` - Add constraint +- `Check()` - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown) +- `Model()` - Get model (if satisfiable) +- `Push()` - Create backtracking point +- `Pop(n uint)` - Remove backtracking points +- `Reset()` - Remove all assertions + +### Model Operations + +- `Eval(expr *Expr, modelCompletion bool)` - Evaluate expression in model +- `NumConsts()` - Number of constants in model +- `NumFuncs()` - Number of functions in model +- `String()` - Get string representation + +### Bit-vector Operations + +- `MkBvSort(sz uint)` - Create bit-vector sort +- `MkBVConst(name string, size uint)` - Create bit-vector variable +- `MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr)` - Arithmetic operations +- `MkBVAnd/Or/Xor/Not(...)` - Bitwise operations +- `MkBVShl/LShr/AShr(lhs, rhs *Expr)` - Shift operations +- `MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...)` - Comparisons +- `MkConcat(lhs, rhs *Expr)` - Bit-vector concatenation +- `MkExtract(high, low uint, expr *Expr)` - Extract bits +- `MkSignExt/ZeroExt(i uint, expr *Expr)` - Extend bit-vectors + +### Floating-Point Operations + +- `MkFPSort(ebits, sbits uint)` - Create floating-point sort +- `MkFPSort16/32/64/128()` - Standard IEEE 754 sorts +- `MkFPInf/NaN/Zero(sort *Sort, ...)` - Special values +- `MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr)` - Arithmetic with rounding +- `MkFPNeg/Abs/Sqrt(...)` - Unary operations +- `MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr)` - Comparisons +- `MkFPIsNaN/IsInf/IsZero(expr *Expr)` - Predicates + +### Sequence/String Operations + +- `MkStringSort()` - Create string sort +- `MkSeqSort(elemSort *Sort)` - Create sequence sort +- `MkString(value string)` - Create string constant +- `MkSeqConcat(exprs ...*Expr)` - Concatenation +- `MkSeqLength(seq *Expr)` - Length +- `MkSeqPrefix/Suffix/Contains(...)` - Predicates +- `MkSeqAt(seq, index *Expr)` - Element access +- `MkSeqExtract(seq, offset, length *Expr)` - Substring +- `MkStrToInt/IntToStr(...)` - Conversions + +### Regular Expression Operations + +- `MkReSort(seqSort *Sort)` - Create regex sort +- `MkToRe(seq *Expr)` - Convert string to regex +- `MkInRe(seq, re *Expr)` - String matches regex predicate +- `MkReStar(re *Expr)` - Kleene star (zero or more) +- `MkRePlus(re *Expr)` - Kleene plus (one or more) +- `MkReOption(re *Expr)` - Optional (zero or one) +- `MkRePower(re *Expr, n uint)` - Exactly n repetitions +- `MkReLoop(re *Expr, lo, hi uint)` - Bounded repetition +- `MkReConcat(regexes ...*Expr)` - Concatenation +- `MkReUnion(regexes ...*Expr)` - Alternation (OR) +- `MkReIntersect(regexes ...*Expr)` - Intersection +- `MkReComplement(re *Expr)` - Complement +- `MkReDiff(a, b *Expr)` - Difference +- `MkReEmpty/Full/Allchar(sort *Sort)` - Special regexes +- `MkReRange(lo, hi *Expr)` - Character range +- `MkSeqReplaceRe/ReAll(seq, re, replacement *Expr)` - Regex replace + +### Datatype Operations + +- `MkConstructor(name, recognizer string, ...)` - Create constructor +- `MkDatatypeSort(name string, constructors []*Constructor)` - Create datatype +- `MkDatatypeSorts(names []string, ...)` - Mutually recursive datatypes +- `MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)` - Tuples +- `MkEnumSort(name string, enumNames []string)` - Enumerations +- `MkListSort(name string, elemSort *Sort)` - Lists + +### Tactic Operations + +- `MkTactic(name string)` - Create tactic by name +- `MkGoal(models, unsatCores, proofs bool)` - Create goal +- `Apply(g *Goal)` - Apply tactic to goal +- `AndThen(t2 *Tactic)` - Sequential composition +- `OrElse(t2 *Tactic)` - Try first, fallback to second +- `Repeat(max uint)` - Repeat tactic +- `TacticWhen/Cond(...)` - Conditional tactics + +### Probe Operations + +- `MkProbe(name string)` - Create probe by name +- `Apply(g *Goal)` - Evaluate probe on goal +- `Lt/Gt/Le/Ge/Eq(p2 *Probe)` - Probe comparisons +- `And/Or/Not(...)` - Probe combinators + +### Parameter Operations + +- `MkParams()` - Create parameter set +- `SetBool/Uint/Double/Symbol(key string, value ...)` - Set parameters + +### Optimize Operations + +- `NewOptimize()` - Create optimization context +- `Assert(constraint *Expr)` - Add constraint +- `AssertSoft(constraint *Expr, weight, group string)` - Add soft constraint +- `Maximize(expr *Expr)` - Add maximization objective +- `Minimize(expr *Expr)` - Add minimization objective +- `Check(assumptions ...*Expr)` - Check and optimize +- `Model()` - Get optimal model +- `GetLower/Upper(index uint)` - Get objective bounds +- `Push/Pop()` - Backtracking +- `Assertions/Objectives()` - Get assertions and objectives +- `UnsatCore()` - Get unsat core + +## Memory Management + +The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. + +## Thread Safety + +Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context. + +## License + +Z3 is licensed under the MIT License. See LICENSE.txt in the repository root. + +## Contributing + +Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository. + +## References + +- [Z3 GitHub Repository](https://github.com/Z3Prover/z3) +- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html) +- [Z3 Guide](https://microsoft.github.io/z3guide/) + +
+

Back to Go API Documentation

+ + diff --git a/doc/test_go_doc/index.html b/doc/test_go_doc/index.html new file mode 100644 index 000000000..f9fb2a9f0 --- /dev/null +++ b/doc/test_go_doc/index.html @@ -0,0 +1,164 @@ + + + + + + Z3 Go API Documentation + + + +
+

Z3 Go API Documentation

+

Go bindings for the Z3 Theorem Prover

+
+
+
+

Overview

+

The Z3 Go bindings provide idiomatic Go access to the Z3 SMT solver. These bindings use CGO to wrap the Z3 C API and provide automatic memory management through Go finalizers.

+

Package: github.com/Z3Prover/z3/src/api/go

+
+
+

Quick Start

+
+ 
package main
+
+import (
+    "fmt"
+    "github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+    // Create a context
+    ctx := z3.NewContext()
+
+    // Create integer variable
+    x := ctx.MkIntConst("x")
+
+    // Create solver
+    solver := ctx.NewSolver()
+
+    // Add constraint: x > 0
+    zero := ctx.MkInt(0, ctx.MkIntSort())
+    solver.Assert(ctx.MkGt(x, zero))
+
+    // Check satisfiability
+    if solver.Check() == z3.Satisfiable {
+        fmt.Println("sat")
+        model := solver.Model()
+        if val, ok := model.Eval(x, true); ok {
+            fmt.Println("x =", val.String())
+        }
+    }
+}
+
+
+
+

Installation

+
+

Prerequisites:

+
    +
  • Go 1.20 or later
    • +
  • Z3 built as a shared library
    • +
  • CGO enabled (default)
    • +
+

Build Z3 with Go bindings:

+
+ 
# Using CMake
+mkdir build && cd build
+cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ..
+make
+
+# Using Python build script
+python scripts/mk_make.py --go
+cd build && make
+
+

Set environment variables:

+
+ 
export CGO_CFLAGS="-I${Z3_ROOT}/src/api"
+export CGO_LDFLAGS="-L${Z3_ROOT}/build -lz3"
+export LD_LIBRARY_PATH="${Z3_ROOT}/build:$LD_LIBRARY_PATH"
+
+
+
+
+

API Modules

+
    +
  • +

    z3.go

    +

    Package z3 provides Go bindings for the Z3 theorem prover. It wraps the Z3 C API using CGO.

    +
    • +
  • +

    solver.go

    +

    Solver and Model API for SMT solving

    +
    • +
  • +

    tactic.go

    +

    Tactics, Goals, Probes, and Parameters for goal-based solving

    +
    • +
  • +

    bitvec.go

    +

    Bit-vector operations and constraints

    +
    • +
  • +

    fp.go

    +

    IEEE 754 floating-point operations

    +
    • +
  • +

    seq.go

    +

    Sequences, strings, and regular expressions

    +
    • +
  • +

    datatype.go

    +

    Algebraic datatypes, tuples, and enumerations

    +
    • +
  • +

    optimize.go

    +

    Optimization with maximize/minimize objectives

    +
    • +
+
+
+

Features

+
    +
  • Core SMT: Boolean logic, arithmetic, arrays, quantifiers
    • +
  • Bit-vectors: Fixed-size bit-vector arithmetic and operations
    • +
  • Floating-point: IEEE 754 floating-point arithmetic
    • +
  • Strings & Sequences: String constraints and sequence operations
    • +
  • Regular Expressions: Pattern matching and regex constraints
    • +
  • Datatypes: Algebraic datatypes, tuples, enumerations
    • +
  • Tactics: Goal-based solving with tactic combinators
    • +
  • Optimization: MaxSMT with maximize/minimize objectives
    • +
  • Memory Management: Automatic via Go finalizers
    • +
+
+
+

Resources

+ +
+ ← Back to main API documentation +
+ + diff --git a/doc/website.dox.in b/doc/website.dox.in index 651652ce4..be9e1b093 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -8,5 +8,5 @@ This website hosts the automatically generated documentation for the Z3 APIs. - @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ + @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ @GO_API@ */ diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 1c367e141..cc238b01f 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -841,7 +841,8 @@ WARN_LOGFILE = INPUT = "@TEMP_DIR@" \ "@CXX_API_SEARCH_PATHS@" \ @DOTNET_API_SEARCH_PATHS@ \ - @JAVA_API_SEARCH_PATHS@ + @JAVA_API_SEARCH_PATHS@ \ + @GO_API_SEARCH_PATHS@ # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses @@ -879,7 +880,8 @@ FILE_PATTERNS = website.dox \ z3++.h \ @PYTHON_API_FILES@ \ @DOTNET_API_FILES@ \ - @JAVA_API_FILES@ + @JAVA_API_FILES@ \ + @GO_API_FILES@ # The RECURSIVE tag can be used to specify whether or not subdirectories should # be searched for input files as well. diff --git a/examples/go/README.md b/examples/go/README.md new file mode 100644 index 000000000..011f08579 --- /dev/null +++ b/examples/go/README.md @@ -0,0 +1,145 @@ +# Z3 Go Examples + +This directory contains examples demonstrating how to use the Z3 Go bindings. + +## Examples + +### basic_example.go + +Demonstrates fundamental Z3 operations: +- Creating contexts and solvers +- Defining integer and boolean variables +- Adding constraints +- Checking satisfiability +- Extracting models + +## Building and Running + +### Prerequisites + +1. Build Z3 with Go bindings enabled +2. Ensure Z3 library is in your library path +3. Go 1.20 or later + +### Linux/macOS + +```bash +# Build Z3 first +cd ../.. +mkdir build && cd build +cmake .. +make -j$(nproc) + +# Set up environment +cd ../examples/go +export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH +export CGO_CFLAGS="-I../../src/api" +export CGO_LDFLAGS="-L../../build -lz3" + +# Run examples +go run basic_example.go +``` + +### Windows + +```cmd +REM Build Z3 first +cd ..\.. +mkdir build +cd build +cmake .. +cmake --build . --config Release + +REM Set up environment +cd ..\examples\go +set PATH=..\..\build\Release;%PATH% +set CGO_CFLAGS=-I..\..\src\api +set CGO_LDFLAGS=-L..\..\build\Release -lz3 + +REM Run examples +go run basic_example.go +``` + +## Expected Output + +When you run `basic_example.go`, you should see output similar to: + +``` +Z3 Go Bindings - Basic Example +================================ + +Example 1: Solving x > 0 +Satisfiable! +Model: ... +x = 1 + +Example 2: Solving x + y = 10 ∧ x - y = 2 +Satisfiable! +x = 6 +y = 4 + +Example 3: Boolean satisfiability +Satisfiable! +p = false +q = true + +Example 4: Checking unsatisfiability +Status: unsat +The constraints are unsatisfiable (as expected) + +All examples completed successfully! +``` + +## Creating Your Own Examples + +1. Import the Z3 package: + ```go + import "github.com/Z3Prover/z3/src/api/go" + ``` + +2. Create a context: + ```go + ctx := z3.NewContext() + ``` + +3. Create variables and constraints: + ```go + x := ctx.MkIntConst("x") + constraint := ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort())) + ``` + +4. Solve: + ```go + solver := ctx.NewSolver() + solver.Assert(constraint) + if solver.Check() == z3.Satisfiable { + model := solver.Model() + // Use model... + } + ``` + +## Troubleshooting + +### "undefined reference to Z3_*" errors + +Make sure: +- Z3 is built and the library is in your library path +- CGO_LDFLAGS includes the correct library path +- On Windows, the DLL is in your PATH + +### "cannot find package" errors + +Make sure: +- CGO_CFLAGS includes the Z3 API header directory +- The go.mod file exists in src/api/go + +### CGO compilation errors + +Ensure: +- CGO is enabled (set CGO_ENABLED=1 if needed) +- You have a C compiler installed (gcc, clang, or MSVC) +- The Z3 headers are accessible + +## More Information + +See the README.md in src/api/go for complete API documentation. diff --git a/examples/go/advanced_example.go b/examples/go/advanced_example.go new file mode 100644 index 000000000..0db4b6daf --- /dev/null +++ b/examples/go/advanced_example.go @@ -0,0 +1,313 @@ +package main + +import ( + "fmt" + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + ctx := z3.NewContext() + fmt.Println("Z3 Go Bindings - Advanced Features Example") + fmt.Println("==========================================") + + // Example 1: Bit-vectors + fmt.Println("\nExample 1: Bit-vector operations") + x := ctx.MkBVConst("x", 8) + y := ctx.MkBVConst("y", 8) + + // x + y == 255 && x > y + sum := ctx.MkBVAdd(x, y) + ff := ctx.MkBV(255, 8) + + solver := ctx.NewSolver() + solver.Assert(ctx.MkEq(sum, ff)) + solver.Assert(ctx.MkBVUGT(x, y)) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if xVal, ok := model.Eval(x, true); ok { + fmt.Println("x =", xVal.String()) + } + if yVal, ok := model.Eval(y, true); ok { + fmt.Println("y =", yVal.String()) + } + } + + // Example 2: Floating-point arithmetic + fmt.Println("\nExample 2: Floating-point arithmetic") + solver.Reset() + + fpSort := ctx.MkFPSort32() + a := ctx.MkConst(ctx.MkStringSymbol("a"), fpSort) + b := ctx.MkConst(ctx.MkStringSymbol("b"), fpSort) + + // a + b > 0.0 (with rounding mode) + rm := ctx.MkConst(ctx.MkStringSymbol("rm"), ctx.MkFPRoundingModeSort()) + fpSum := ctx.MkFPAdd(rm, a, b) + zero := ctx.MkFPZero(fpSort, false) + + solver.Assert(ctx.MkFPGT(fpSum, zero)) + solver.Assert(ctx.MkFPGT(a, ctx.MkFPZero(fpSort, false))) + + if solver.Check() == z3.Satisfiable { + fmt.Println("Satisfiable! (Floating-point constraint satisfied)") + } + + // Example 3: Strings + fmt.Println("\nExample 3: String operations") + solver.Reset() + + s1 := ctx.MkConst(ctx.MkStringSymbol("s1"), ctx.MkStringSort()) + s2 := ctx.MkConst(ctx.MkStringSymbol("s2"), ctx.MkStringSort()) + + // s1 contains "hello" && length(s1) < 20 + hello := ctx.MkString("hello") + solver.Assert(ctx.MkSeqContains(s1, hello)) + + len1 := ctx.MkSeqLength(s1) + twenty := ctx.MkInt(20, ctx.MkIntSort()) + solver.Assert(ctx.MkLt(len1, twenty)) + + // s2 is s1 concatenated with "world" + world := ctx.MkString(" world") + solver.Assert(ctx.MkEq(s2, ctx.MkSeqConcat(s1, world))) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if s1Val, ok := model.Eval(s1, true); ok { + fmt.Println("s1 =", s1Val.String()) + } + if s2Val, ok := model.Eval(s2, true); ok { + fmt.Println("s2 =", s2Val.String()) + } + } + + // Example 4: Datatypes (List) + fmt.Println("\nExample 4: List datatype") + solver.Reset() + + intSort := ctx.MkIntSort() + listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl := + ctx.MkListSort("IntList", intSort) + + // Create list: cons(1, cons(2, nil)) + nilList := ctx.MkApp(nilDecl) + one := ctx.MkInt(1, intSort) + two := ctx.MkInt(2, intSort) + list2 := ctx.MkApp(consDecl, two, nilList) + list12 := ctx.MkApp(consDecl, one, list2) + + // Check that head(list12) == 1 + listVar := ctx.MkConst(ctx.MkStringSymbol("mylist"), listSort) + solver.Assert(ctx.MkEq(listVar, list12)) + + headOfList := ctx.MkApp(headDecl, listVar) + solver.Assert(ctx.MkEq(headOfList, one)) + + if solver.Check() == z3.Satisfiable { + fmt.Println("Satisfiable! List head is 1") + } + + // Example 5: Tactics and Goals + fmt.Println("\nExample 5: Using tactics") + + goal := ctx.MkGoal(true, false, false) + p := ctx.MkIntConst("p") + q := ctx.MkIntConst("q") + + // Add constraint: p > 0 && q > 0 && p + q == 10 + goal.Assert(ctx.MkGt(p, ctx.MkInt(0, ctx.MkIntSort()))) + goal.Assert(ctx.MkGt(q, ctx.MkInt(0, ctx.MkIntSort()))) + goal.Assert(ctx.MkEq(ctx.MkAdd(p, q), ctx.MkInt(10, ctx.MkIntSort()))) + + // Apply simplify tactic + tactic := ctx.MkTactic("simplify") + result := tactic.Apply(goal) + + fmt.Printf("Tactic produced %d subgoals\n", result.NumSubgoals()) + if result.NumSubgoals() > 0 { + subgoal := result.Subgoal(0) + fmt.Println("Simplified goal:", subgoal.String()) + } + + // Example 6: Enumerations + fmt.Println("\nExample 6: Enumeration types") + solver.Reset() + + colorSort, colorConsts, colorTesters := ctx.MkEnumSort( + "Color", + []string{"Red", "Green", "Blue"}, + ) + + red := ctx.MkApp(colorConsts[0]) + green := ctx.MkApp(colorConsts[1]) + blue := ctx.MkApp(colorConsts[2]) + + c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort) + c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort) + + // c1 != c2 && c1 != Red + solver.Assert(ctx.MkDistinct(c1, c2)) + solver.Assert(ctx.MkNot(ctx.MkEq(c1, red))) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if c1Val, ok := model.Eval(c1, true); ok { + fmt.Println("c1 =", c1Val.String()) + } + if c2Val, ok := model.Eval(c2, true); ok { + fmt.Println("c2 =", c2Val.String()) + } + } + + // Example 7: Tuples + fmt.Println("\nExample 7: Tuple types") + solver.Reset() + + tupleSort, mkTuple, projections := ctx.MkTupleSort( + "Point", + []string{"x", "y"}, + []*z3.Sort{ctx.MkIntSort(), ctx.MkIntSort()}, + ) + + // Create point (3, 4) + three := ctx.MkInt(3, ctx.MkIntSort()) + four := ctx.MkInt(4, ctx.MkIntSort()) + point := ctx.MkApp(mkTuple, three, four) + + p1 := ctx.MkConst(ctx.MkStringSymbol("p1"), tupleSort) + solver.Assert(ctx.MkEq(p1, point)) + + // Extract x coordinate + xCoord := ctx.MkApp(projections[0], p1) + solver.Assert(ctx.MkEq(xCoord, three)) + + if solver.Check() == z3.Satisfiable { + fmt.Println("Satisfiable! Tuple point created") + model := solver.Model() + if p1Val, ok := model.Eval(p1, true); ok { + fmt.Println("p1 =", p1Val.String()) + } + } + + // Example 8: Regular expressions + fmt.Println("\nExample 8: Regular expressions") + solver.Reset() + + // Create a string variable + str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort()) + + // Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c') + a := ctx.MkToRe(ctx.MkString("a")) + b := ctx.MkToRe(ctx.MkString("b")) + c := ctx.MkToRe(ctx.MkString("c")) + + // (a|b) + aOrB := ctx.MkReUnion(a, b) + + // (a|b)* + aOrBStar := ctx.MkReStar(aOrB) + + // c+ + cPlus := ctx.MkRePlus(c) + + // (a|b)*c+ + regex := ctx.MkReConcat(aOrBStar, cPlus) + + // Assert that string matches the regex + solver.Assert(ctx.MkInRe(str, regex)) + + // Also assert that length is less than 10 + strLen := ctx.MkSeqLength(str) + ten := ctx.MkInt(10, ctx.MkIntSort()) + solver.Assert(ctx.MkLt(strLen, ten)) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if strVal, ok := model.Eval(str, true); ok { + fmt.Println("String matching (a|b)*c+:", strVal.String()) + } + } + + // Example 8: Regular expressions + fmt.Println("\nExample 8: Regular expressions") + solver.Reset() + + // Create a string variable + str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort()) + + // Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c') + a := ctx.MkToRe(ctx.MkString("a")) + b := ctx.MkToRe(ctx.MkString("b")) + c := ctx.MkToRe(ctx.MkString("c")) + + // (a|b)* + aOrB := ctx.MkReUnion(a, b) + aOrBStar := ctx.MkReStar(aOrB) + + // c+ + cPlus := ctx.MkRePlus(c) + + // (a|b)*c+ + regex := ctx.MkReConcat(aOrBStar, cPlus) + + // Assert that string matches the regex + solver.Assert(ctx.MkInRe(str, regex)) + + // Also assert that length is less than 10 + strLen := ctx.MkSeqLength(str) + tenStr := ctx.MkInt(10, ctx.MkIntSort()) + solver.Assert(ctx.MkLt(strLen, tenStr)) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if strVal, ok := model.Eval(str, true); ok { + fmt.Println("String matching (a|b)*c+:", strVal.String()) + } + } + + // Example 9: Optimization + fmt.Println("\nExample 9: Optimization (maximize/minimize)") + + opt := ctx.NewOptimize() + + // Variables + xOpt := ctx.MkIntConst("x_opt") + yOpt := ctx.MkIntConst("y_opt") + + // Constraints: x + y <= 10, x >= 0, y >= 0 + tenOpt := ctx.MkInt(10, ctx.MkIntSort()) + zeroOpt := ctx.MkInt(0, ctx.MkIntSort()) + + opt.Assert(ctx.MkLe(ctx.MkAdd(xOpt, yOpt), tenOpt)) + opt.Assert(ctx.MkGe(xOpt, zeroOpt)) + opt.Assert(ctx.MkGe(yOpt, zeroOpt)) + + // Objective: maximize x + 2*y + twoOpt := ctx.MkInt(2, ctx.MkIntSort()) + objective := ctx.MkAdd(xOpt, ctx.MkMul(twoOpt, yOpt)) + objHandle := opt.Maximize(objective) + + if opt.Check() == z3.Satisfiable { + model := opt.Model() + fmt.Println("Optimal solution found!") + if xVal, ok := model.Eval(xOpt, true); ok { + fmt.Println("x =", xVal.String()) + } + if yVal, ok := model.Eval(yOpt, true); ok { + fmt.Println("y =", yVal.String()) + } + upper := opt.GetUpper(objHandle) + if upper != nil { + fmt.Println("Maximum value of x + 2*y =", upper.String()) + } + } + + fmt.Println("\nAll advanced examples completed successfully!") +} + diff --git a/examples/go/basic_example.go b/examples/go/basic_example.go new file mode 100644 index 000000000..73bcf84df --- /dev/null +++ b/examples/go/basic_example.go @@ -0,0 +1,98 @@ +package main + +import ( + "fmt" + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + // Create a new Z3 context + ctx := z3.NewContext() + fmt.Println("Z3 Go Bindings - Basic Example") + fmt.Println("================================") + + // Example 1: Simple integer constraint + fmt.Println("\nExample 1: Solving x > 0") + x := ctx.MkIntConst("x") + zero := ctx.MkInt(0, ctx.MkIntSort()) + constraint := ctx.MkGt(x, zero) + + solver := ctx.NewSolver() + solver.Assert(constraint) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + fmt.Println("Model:", model.String()) + if val, ok := model.Eval(x, true); ok { + fmt.Println("x =", val.String()) + } + } + + // Example 2: System of equations + fmt.Println("\nExample 2: Solving x + y = 10 ∧ x - y = 2") + solver.Reset() + y := ctx.MkIntConst("y") + ten := ctx.MkInt(10, ctx.MkIntSort()) + two := ctx.MkInt(2, ctx.MkIntSort()) + + eq1 := ctx.MkEq(ctx.MkAdd(x, y), ten) + eq2 := ctx.MkEq(ctx.MkSub(x, y), two) + + solver.Assert(eq1) + solver.Assert(eq2) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if xVal, ok := model.Eval(x, true); ok { + fmt.Println("x =", xVal.String()) + } + if yVal, ok := model.Eval(y, true); ok { + fmt.Println("y =", yVal.String()) + } + } + + // Example 3: Boolean logic + fmt.Println("\nExample 3: Boolean satisfiability") + solver.Reset() + p := ctx.MkBoolConst("p") + q := ctx.MkBoolConst("q") + + // (p ∨ q) ∧ (¬p ∨ ¬q) + formula := ctx.MkAnd( + ctx.MkOr(p, q), + ctx.MkOr(ctx.MkNot(p), ctx.MkNot(q)), + ) + + solver.Assert(formula) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + fmt.Println("Satisfiable!") + if pVal, ok := model.Eval(p, true); ok { + fmt.Println("p =", pVal.String()) + } + if qVal, ok := model.Eval(q, true); ok { + fmt.Println("q =", qVal.String()) + } + } + + // Example 4: Unsatisfiable constraint + fmt.Println("\nExample 4: Checking unsatisfiability") + solver.Reset() + a := ctx.MkIntConst("a") + one := ctx.MkInt(1, ctx.MkIntSort()) + + // a > 0 ∧ a < 0 (unsatisfiable) + solver.Assert(ctx.MkGt(a, zero)) + solver.Assert(ctx.MkLt(a, zero)) + + status := solver.Check() + fmt.Println("Status:", status.String()) + if status == z3.Unsatisfiable { + fmt.Println("The constraints are unsatisfiable (as expected)") + } + + fmt.Println("\nAll examples completed successfully!") +} diff --git a/examples/go/go.mod b/examples/go/go.mod new file mode 100644 index 000000000..7ee4bbce2 --- /dev/null +++ b/examples/go/go.mod @@ -0,0 +1,8 @@ +module z3-examples + +go 1.20 + +require github.com/Z3Prover/z3/src/api/go v0.0.0 + +replace github.com/Z3Prover/z3/src/api/go => ../../src/api/go + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 163056099..aa1069a5e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -93,6 +93,7 @@ DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) ASSEMBLY_VERSION=getenv("Z2_ASSEMBLY_VERSION", None) JAVA_ENABLED=False +GO_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False @@ -712,6 +713,7 @@ def display_help(exit_code): print(" --dotnet-key= sign the .NET assembly using the private key in .") print(" --assembly-version= provide version number for build") print(" --java generate Java bindings.") + print(" --go generate Go bindings.") print(" --ml generate OCaml bindings.") print(" --js generate JScript bindings.") print(" --python generate Python bindings.") @@ -745,7 +747,7 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED + global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, JAVA_ENABLED, GO_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64 try: @@ -809,6 +811,8 @@ def parse_options(): GMP = True elif opt in ('-j', '--java'): JAVA_ENABLED = True + elif opt in ('--go',): + GO_ENABLED = True elif opt == '--gprof': GPROF = True elif opt == '--githash': @@ -953,6 +957,9 @@ def is_verbose(): def is_java_enabled(): return JAVA_ENABLED +def is_go_enabled(): + return GO_ENABLED + def is_ml_enabled(): return ML_ENABLED diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65420484e..1a6608849 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -355,4 +355,16 @@ if (Z3_BUILD_JULIA_BINDINGS) add_subdirectory(api/julia) endif() +################################################################################ +# Go bindings +################################################################################ +option(Z3_BUILD_GO_BINDINGS "Build Go bindings for Z3" OFF) +if (Z3_BUILD_GO_BINDINGS) + if (NOT Z3_BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The Go bindings will not work with a static libz3. " + "You either need to disable Z3_BUILD_GO_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/go) +endif() + # TODO: Implement support for other bindigns diff --git a/src/api/go/CMakeLists.txt b/src/api/go/CMakeLists.txt new file mode 100644 index 000000000..f21bb4e37 --- /dev/null +++ b/src/api/go/CMakeLists.txt @@ -0,0 +1,54 @@ +# Z3 Go API + +# Note: This CMakeLists.txt is a placeholder for Go binding integration. +# Go bindings use CGO and are typically built using the Go toolchain directly. +# However, we can set up installation targets here. + +if(BUILD_GO_BINDINGS) + message(STATUS "Z3 Go bindings will be installed") + + # Install Go source files + install(FILES + ${CMAKE_CURRENT_SOURCE_DIR}/z3.go + ${CMAKE_CURRENT_SOURCE_DIR}/solver.go + ${CMAKE_CURRENT_SOURCE_DIR}/go.mod + ${CMAKE_CURRENT_SOURCE_DIR}/README.md + DESTINATION "${CMAKE_INSTALL_LIBDIR}/go/src/github.com/Z3Prover/z3/go" + ) + + # On Windows, we need to ensure the DLL is accessible + if(WIN32) + message(STATUS "Go bindings on Windows require libz3.dll in PATH") + endif() + + # Add a custom target to test Go bindings if Go is available + find_program(GO_EXECUTABLE go) + if(GO_EXECUTABLE) + message(STATUS "Found Go: ${GO_EXECUTABLE}") + + # Custom target to build Go bindings + add_custom_target(go-bindings + COMMAND ${CMAKE_COMMAND} -E env + CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api + CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3 + ${GO_EXECUTABLE} build -v + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + COMMENT "Building Go bindings" + DEPENDS libz3 + ) + + # Custom target to test Go examples + add_custom_target(test-go-examples + COMMAND ${CMAKE_COMMAND} -E env + CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api + CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3 + LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}:$ENV{LD_LIBRARY_PATH} + PATH=${CMAKE_BINARY_DIR}\;$ENV{PATH} + ${GO_EXECUTABLE} run ${CMAKE_SOURCE_DIR}/examples/go/basic_example.go + COMMENT "Running Go examples" + DEPENDS libz3 + ) + else() + message(STATUS "Go not found - Go bindings can be built manually") + endif() +endif() diff --git a/src/api/go/README.md b/src/api/go/README.md new file mode 100644 index 000000000..8814b72a1 --- /dev/null +++ b/src/api/go/README.md @@ -0,0 +1,331 @@ +# Z3 Go Bindings + +This directory contains Go language bindings for the Z3 theorem prover. + +## Overview + +The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support: + +- **Core Z3 Types**: Context, Config, Symbol, AST, Sort, Expr, FuncDecl +- **Solver Operations**: Creating solvers, asserting constraints, checking satisfiability +- **Model Manipulation**: Extracting and evaluating models +- **Boolean Logic**: And, Or, Not, Implies, Iff, Xor +- **Arithmetic**: Add, Sub, Mul, Div, Mod, comparison operators +- **Bit-vectors**: Full bit-vector arithmetic, bitwise operations, shifts, comparisons +- **Floating Point**: IEEE 754 floating-point arithmetic with rounding modes +- **Arrays**: Select, Store, constant arrays +- **Sequences/Strings**: String operations, concatenation, contains, indexing +- **Regular Expressions**: Pattern matching, Kleene star/plus, regex operations +- **Quantifiers**: Forall, Exists +- **Functions**: Function declarations and applications +- **Tactics & Goals**: Goal-based solving and tactic combinators +- **Probes**: Goal property checking +- **Datatypes**: Algebraic datatypes, tuples, enumerations, lists +- **Parameters**: Solver and tactic configuration +- **Optimize**: Optimization problems with maximize/minimize objectives + +## Building + +### Prerequisites + +- Go 1.20 or later +- Z3 library built and installed +- CGO enabled + +### With CMake + +```bash +mkdir build && cd build +cmake -DBUILD_GO_BINDINGS=ON .. +make +``` + +### With Python Build System + +```bash +python scripts/mk_make.py --go +cd build +make +``` + +## Usage + +### Basic Example + +```go +package main + +import ( + "fmt" + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + // Create a context + ctx := z3.NewContext() + + // Create variables + x := ctx.MkIntConst("x") + y := ctx.MkIntConst("y") + + // Create constraints: x + y == 10 && x > y + ten := ctx.MkInt(10, ctx.MkIntSort()) + eq := ctx.MkEq(ctx.MkAdd(x, y), ten) + gt := ctx.MkGt(x, y) + + // Create solver and check + solver := ctx.NewSolver() + solver.Assert(eq) + solver.Assert(gt) + + if solver.Check() == z3.Satisfiable { + model := solver.Model() + if xVal, ok := model.Eval(x, true); ok { + fmt.Println("x =", xVal.String()) + } + if yVal, ok := model.Eval(y, true); ok { + fmt.Println("y =", yVal.String()) + } + } +} +``` + +### Running Examples + +```bash +cd examples/go + +# Set library path (Linux/Mac) +export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH +export CGO_CFLAGS="-I../../src/api" +export CGO_LDFLAGS="-L../../build -lz3" + +# Set library path (Windows) +set PATH=..\..\build;%PATH% +set CGO_CFLAGS=-I../../src/api +set CGO_LDFLAGS=-L../../build -lz3 + +# Run example +go run basic_example.go +``` + +## API Reference + +### Context + +- `NewContext()` - Create a new Z3 context +- `NewContextWithConfig(cfg *Config)` - Create context with configuration +- `SetParam(key, value string)` - Set context parameters + +### Creating Expressions + +- `MkBoolConst(name string)` - Create Boolean variable +- `MkIntConst(name string)` - Create integer variable +- `MkRealConst(name string)` - Create real variable +- `MkInt(value int, sort *Sort)` - Create integer constant +- `MkReal(num, den int)` - Create rational constant + +### Boolean Operations + +- `MkAnd(exprs ...*Expr)` - Conjunction +- `MkOr(exprs ...*Expr)` - Disjunction +- `MkNot(expr *Expr)` - Negation +- `MkImplies(lhs, rhs *Expr)` - Implication +- `MkIff(lhs, rhs *Expr)` - If-and-only-if +- `MkXor(lhs, rhs *Expr)` - Exclusive or + +### Arithmetic Operations + +- `MkAdd(exprs ...*Expr)` - Addition +- `MkSub(exprs ...*Expr)` - Subtraction +- `MkMul(exprs ...*Expr)` - Multiplication +- `MkDiv(lhs, rhs *Expr)` - Division +- `MkMod(lhs, rhs *Expr)` - Modulo +- `MkRem(lhs, rhs *Expr)` - Remainder + +### Comparison Operations + +- `MkEq(lhs, rhs *Expr)` - Equality +- `MkDistinct(exprs ...*Expr)` - Distinct +- `MkLt(lhs, rhs *Expr)` - Less than +- `MkLe(lhs, rhs *Expr)` - Less than or equal +- `MkGt(lhs, rhs *Expr)` - Greater than +- `MkGe(lhs, rhs *Expr)` - Greater than or equal + +### Solver Operations + +- `NewSolver()` - Create a new solver +- `Assert(constraint *Expr)` - Add constraint +- `Check()` - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown) +- `Model()` - Get model (if satisfiable) +- `Push()` - Create backtracking point +- `Pop(n uint)` - Remove backtracking points +- `Reset()` - Remove all assertions + +### Model Operations + +- `Eval(expr *Expr, modelCompletion bool)` - Evaluate expression in model +- `NumConsts()` - Number of constants in model +- `NumFuncs()` - Number of functions in model +- `String()` - Get string representation + +### Bit-vector Operations + +- `MkBvSort(sz uint)` - Create bit-vector sort +- `MkBVConst(name string, size uint)` - Create bit-vector variable +- `MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr)` - Arithmetic operations +- `MkBVAnd/Or/Xor/Not(...)` - Bitwise operations +- `MkBVShl/LShr/AShr(lhs, rhs *Expr)` - Shift operations +- `MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...)` - Comparisons +- `MkConcat(lhs, rhs *Expr)` - Bit-vector concatenation +- `MkExtract(high, low uint, expr *Expr)` - Extract bits +- `MkSignExt/ZeroExt(i uint, expr *Expr)` - Extend bit-vectors + +### Floating-Point Operations + +- `MkFPSort(ebits, sbits uint)` - Create floating-point sort +- `MkFPSort16/32/64/128()` - Standard IEEE 754 sorts +- `MkFPInf/NaN/Zero(sort *Sort, ...)` - Special values +- `MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr)` - Arithmetic with rounding +- `MkFPNeg/Abs/Sqrt(...)` - Unary operations +- `MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr)` - Comparisons +- `MkFPIsNaN/IsInf/IsZero(expr *Expr)` - Predicates + +### Sequence/String Operations + +- `MkStringSort()` - Create string sort +- `MkSeqSort(elemSort *Sort)` - Create sequence sort +- `MkString(value string)` - Create string constant +- `MkSeqConcat(exprs ...*Expr)` - Concatenation +- `MkSeqLength(seq *Expr)` - Length +- `MkSeqPrefix/Suffix/Contains(...)` - Predicates +- `MkSeqAt(seq, index *Expr)` - Element access +- `MkSeqExtract(seq, offset, length *Expr)` - Substring +- `MkStrToInt/IntToStr(...)` - Conversions + +### Regular Expression Operations + +- `MkReSort(seqSort *Sort)` - Create regex sort +- `MkToRe(seq *Expr)` - Convert string to regex +- `MkInRe(seq, re *Expr)` - String matches regex predicate +- `MkReStar(re *Expr)` - Kleene star (zero or more) +- `MkRePlus(re *Expr)` - Kleene plus (one or more) +- `MkReOption(re *Expr)` - Optional (zero or one) +- `MkRePower(re *Expr, n uint)` - Exactly n repetitions +- `MkReLoop(re *Expr, lo, hi uint)` - Bounded repetition +- `MkReConcat(regexes ...*Expr)` - Concatenation +- `MkReUnion(regexes ...*Expr)` - Alternation (OR) +- `MkReIntersect(regexes ...*Expr)` - Intersection +- `MkReComplement(re *Expr)` - Complement +- `MkReDiff(a, b *Expr)` - Difference +- `MkReEmpty/Full/Allchar(sort *Sort)` - Special regexes +- `MkReRange(lo, hi *Expr)` - Character range +- `MkSeqReplaceRe/ReAll(seq, re, replacement *Expr)` - Regex replace + +### Datatype Operations + +- `MkConstructor(name, recognizer string, ...)` - Create constructor +- `MkDatatypeSort(name string, constructors []*Constructor)` - Create datatype +- `MkDatatypeSorts(names []string, ...)` - Mutually recursive datatypes +- `MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)` - Tuples +- `MkEnumSort(name string, enumNames []string)` - Enumerations +- `MkListSort(name string, elemSort *Sort)` - Lists + +### Tactic Operations + +- `MkTactic(name string)` - Create tactic by name +- `MkGoal(models, unsatCores, proofs bool)` - Create goal +- `Apply(g *Goal)` - Apply tactic to goal +- `AndThen(t2 *Tactic)` - Sequential composition +- `OrElse(t2 *Tactic)` - Try first, fallback to second +- `Repeat(max uint)` - Repeat tactic +- `TacticWhen/Cond(...)` - Conditional tactics + +### Probe Operations + +- `MkProbe(name string)` - Create probe by name +- `Apply(g *Goal)` - Evaluate probe on goal +- `Lt/Gt/Le/Ge/Eq(p2 *Probe)` - Probe comparisons +- `And/Or/Not(...)` - Probe combinators + +### Parameter Operations + +- `MkParams()` - Create parameter set +- `SetBool/Uint/Double/Symbol(key string, value ...)` - Set parameters + +### Optimize Operations + +- `NewOptimize()` - Create optimization context +- `Assert(constraint *Expr)` - Add constraint +- `AssertSoft(constraint *Expr, weight, group string)` - Add soft constraint +- `Maximize(expr *Expr)` - Add maximization objective +- `Minimize(expr *Expr)` - Add minimization objective +- `Check(assumptions ...*Expr)` - Check and optimize +- `Model()` - Get optimal model +- `GetLower/Upper(index uint)` - Get objective bounds +- `Push/Pop()` - Backtracking +- `Assertions/Objectives()` - Get assertions and objectives +- `UnsatCore()` - Get unsat core + +### Fixedpoint Operations (Datalog/CHC) + +- `NewFixedpoint()` - Create fixedpoint solver +- `RegisterRelation(funcDecl *FuncDecl)` - Register predicate +- `AddRule(rule *Expr, name *Symbol)` - Add Horn clause +- `AddFact(pred *FuncDecl, args []int)` - Add table fact +- `Query(query *Expr)` - Query constraints +- `QueryRelations(relations []*FuncDecl)` - Query relations +- `GetAnswer()` - Get satisfying instance or proof +- `Push/Pop()` - Backtracking + +### Quantifier Operations + +- `MkQuantifier(isForall bool, weight int, sorts, names, body, patterns)` - Create quantifier +- `MkQuantifierConst(isForall bool, weight int, bound, body, patterns)` - Create with bound vars +- `IsUniversal/IsExistential()` - Check quantifier type +- `GetNumBound()` - Number of bound variables +- `GetBoundName/Sort(idx int)` - Get bound variable info +- `GetBody()` - Get quantifier body +- `GetNumPatterns()` - Number of patterns +- `GetPattern(idx int)` - Get pattern + +### Lambda Operations + +- `MkLambda(sorts, names, body)` - Create lambda expression +- `MkLambdaConst(bound, body)` - Create lambda with bound variables +- `GetNumBound()` - Number of bound variables +- `GetBoundName/Sort(idx int)` - Get bound variable info +- `GetBody()` - Get lambda body + +### Type Variables + +- `MkTypeVariable(name *Symbol)` - Create polymorphic type variable sort + +### Logging + +- `OpenLog(filename string)` - Open interaction log +- `CloseLog()` - Close log +- `AppendLog(s string)` - Append to log +- `IsLogOpen()` - Check if log is open + +## Memory Management + +The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. + +## Thread Safety + +Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context. + +## License + +Z3 is licensed under the MIT License. See LICENSE.txt in the repository root. + +## Contributing + +Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository. + +## References + +- [Z3 GitHub Repository](https://github.com/Z3Prover/z3) +- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html) +- [Z3 Guide](https://microsoft.github.io/z3guide/) diff --git a/src/api/go/add_godoc.py b/src/api/go/add_godoc.py new file mode 100644 index 000000000..62bab03f1 --- /dev/null +++ b/src/api/go/add_godoc.py @@ -0,0 +1,89 @@ +#!/usr/bin/env python3 +""" +Add godoc comments to Z3 Go bindings systematically. +This script adds proper godoc documentation to all exported types and functions. +""" + +import os +import re + +# Godoc comment templates for common patterns +TYPE_COMMENTS = { + 'Config': '// Config represents a Z3 configuration object used to customize solver behavior.\n// Create with NewConfig and configure using SetParamValue before creating a Context.', + 'Context': '// Context represents a Z3 logical context.\n// All Z3 objects (sorts, expressions, solvers) are tied to the context that created them.\n// Contexts are not thread-safe - use separate contexts for concurrent operations.', + 'Symbol': '// Symbol represents a Z3 symbol, which can be either a string or integer identifier.\n// Symbols are used to name sorts, constants, and functions.', + 'AST': '// AST represents an Abstract Syntax Tree node in Z3.\n// This is the base type for all Z3 expressions, sorts, and function declarations.', + 'Sort': '// Sort represents a type in Z3\'s type system.\n// Common sorts include Bool, Int, Real, BitVec, Array, and user-defined datatypes.', + 'Expr': '// Expr represents a Z3 expression (term).\n// Expressions are typed AST nodes that can be evaluated, simplified, or used in constraints.', + 'FuncDecl': '// FuncDecl represents a function declaration in Z3.\n// Function declarations define the signature (domain and range sorts) of functions.', + 'Pattern': '// Pattern represents a pattern for quantifier instantiation.\n// Patterns guide Z3\'s E-matching algorithm for quantifier instantiation.', + 'Quantifier': '// Quantifier represents a quantified formula (forall or exists).\n// Quantifiers bind variables and include optional patterns for instantiation.', + 'Lambda': '// Lambda represents a lambda expression (anonymous function).\n// Lambda expressions can be used as array values or in higher-order reasoning.', + 'Statistics': '// Statistics holds performance and diagnostic information from Z3 solvers.\n// Use GetKey, GetUintValue, and GetDoubleValue to access individual statistics.', +} + +FUNCTION_COMMENTS = { + 'NewConfig': '// NewConfig creates a new Z3 configuration object.\n// Use SetParamValue to configure parameters before creating a context.', + 'NewContext': '// NewContext creates a new Z3 context with default configuration.\n// The context manages memory for all Z3 objects and must outlive any objects it creates.', + 'NewContextWithConfig': '// NewContextWithConfig creates a new Z3 context with the given configuration.\n// The configuration is consumed and should not be reused.', +} + +def add_godoc_comment(content, pattern, comment): + """Add godoc comment before a type or function declaration.""" + # Check if comment already exists + lines = content.split('\n') + result = [] + i = 0 + + while i < len(lines): + line = lines[i] + + # Check if this line matches our pattern + if re.match(pattern, line): + # Check if previous line is already a comment + if i > 0 and (result[-1].strip().startswith('//') or result[-1].strip().startswith('/*')): + # Comment exists, skip + result.append(line) + else: + # Add comment + result.append(comment) + result.append(line) + else: + result.append(line) + + i += 1 + + return '\n'.join(result) + +def process_file(filepath, type_comments, func_comments): + """Process a single Go file and add godoc comments.""" + print(f"Processing {filepath}...") + + with open(filepath, 'r', encoding='utf-8') as f: + content = f.read() + + # Add type comments + for type_name, comment in type_comments.items(): + pattern = f'^type {type_name} struct' + content = add_godoc_comment(content, pattern, comment) + + # Add function comments + for func_name, comment in func_comments.items(): + pattern = f'^func (\\([^)]+\\) )?{func_name}\\(' + content = add_godoc_comment(content, pattern, comment) + + with open(filepath, 'w', encoding='utf-8') as f: + f.write(content) + + print(f"Updated {filepath}") + +if __name__ == '__main__': + go_api_dir = os.path.dirname(os.path.abspath(__file__)) + + # Process z3.go with core types + z3_go = os.path.join(go_api_dir, 'z3.go') + if os.path.exists(z3_go): + process_file(z3_go, TYPE_COMMENTS, FUNCTION_COMMENTS) + + print("\nGodoc comments added successfully!") + print("Run 'go doc' to verify documentation.") diff --git a/src/api/go/arith.go b/src/api/go/arith.go new file mode 100644 index 000000000..12c01e195 --- /dev/null +++ b/src/api/go/arith.go @@ -0,0 +1,126 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" + +// Arithmetic operations and sorts + +// MkIntSort creates the integer sort. +func (c *Context) MkIntSort() *Sort { + return newSort(c, C.Z3_mk_int_sort(c.ptr)) +} + +// MkRealSort creates the real number sort. +func (c *Context) MkRealSort() *Sort { + return newSort(c, C.Z3_mk_real_sort(c.ptr)) +} + +// MkInt creates an integer constant from an int. +func (c *Context) MkInt(value int, sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_int(c.ptr, C.int(value), sort.ptr)) +} + +// MkInt64 creates an integer constant from an int64. +func (c *Context) MkInt64(value int64, sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_int64(c.ptr, C.int64_t(value), sort.ptr)) +} + +// MkReal creates a real constant from numerator and denominator. +func (c *Context) MkReal(num, den int) *Expr { + return newExpr(c, C.Z3_mk_real(c.ptr, C.int(num), C.int(den))) +} + +// MkIntConst creates an integer constant (variable) with the given name. +func (c *Context) MkIntConst(name string) *Expr { + sym := c.MkStringSymbol(name) + return c.MkConst(sym, c.MkIntSort()) +} + +// MkRealConst creates a real constant (variable) with the given name. +func (c *Context) MkRealConst(name string) *Expr { + sym := c.MkStringSymbol(name) + return c.MkConst(sym, c.MkRealSort()) +} + +// MkAdd creates an addition. +func (c *Context) MkAdd(exprs ...*Expr) *Expr { + if len(exprs) == 0 { + return c.MkInt(0, c.MkIntSort()) + } + if len(exprs) == 1 { + return exprs[0] + } + cExprs := make([]C.Z3_ast, len(exprs)) + for i, e := range exprs { + cExprs[i] = e.ptr + } + return newExpr(c, C.Z3_mk_add(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkSub creates a subtraction. +func (c *Context) MkSub(exprs ...*Expr) *Expr { + if len(exprs) == 0 { + return c.MkInt(0, c.MkIntSort()) + } + if len(exprs) == 1 { + return newExpr(c, C.Z3_mk_unary_minus(c.ptr, exprs[0].ptr)) + } + cExprs := make([]C.Z3_ast, len(exprs)) + for i, e := range exprs { + cExprs[i] = e.ptr + } + return newExpr(c, C.Z3_mk_sub(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkMul creates a multiplication. +func (c *Context) MkMul(exprs ...*Expr) *Expr { + if len(exprs) == 0 { + return c.MkInt(1, c.MkIntSort()) + } + if len(exprs) == 1 { + return exprs[0] + } + cExprs := make([]C.Z3_ast, len(exprs)) + for i, e := range exprs { + cExprs[i] = e.ptr + } + return newExpr(c, C.Z3_mk_mul(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkDiv creates a division. +func (c *Context) MkDiv(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_div(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkMod creates a modulo operation. +func (c *Context) MkMod(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_mod(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkRem creates a remainder operation. +func (c *Context) MkRem(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_rem(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkLt creates a less-than constraint. +func (c *Context) MkLt(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_lt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkLe creates a less-than-or-equal constraint. +func (c *Context) MkLe(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_le(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkGt creates a greater-than constraint. +func (c *Context) MkGt(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_gt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkGe creates a greater-than-or-equal constraint. +func (c *Context) MkGe(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_ge(c.ptr, lhs.ptr, rhs.ptr)) +} diff --git a/src/api/go/array.go b/src/api/go/array.go new file mode 100644 index 000000000..98e947301 --- /dev/null +++ b/src/api/go/array.go @@ -0,0 +1,29 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" + +// Array operations and sorts + +// MkArraySort creates an array sort. +func (c *Context) MkArraySort(domain, range_ *Sort) *Sort { + return newSort(c, C.Z3_mk_array_sort(c.ptr, domain.ptr, range_.ptr)) +} + +// MkSelect creates an array read (select) operation. +func (c *Context) MkSelect(array, index *Expr) *Expr { + return newExpr(c, C.Z3_mk_select(c.ptr, array.ptr, index.ptr)) +} + +// MkStore creates an array write (store) operation. +func (c *Context) MkStore(array, index, value *Expr) *Expr { + return newExpr(c, C.Z3_mk_store(c.ptr, array.ptr, index.ptr, value.ptr)) +} + +// MkConstArray creates a constant array. +func (c *Context) MkConstArray(sort *Sort, value *Expr) *Expr { + return newExpr(c, C.Z3_mk_const_array(c.ptr, sort.ptr, value.ptr)) +} diff --git a/src/api/go/bitvec.go b/src/api/go/bitvec.go new file mode 100644 index 000000000..9ffd220ac --- /dev/null +++ b/src/api/go/bitvec.go @@ -0,0 +1,160 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" + +// Bit-vector operations + +// MkBVConst creates a bit-vector constant with the given name and size. +func (c *Context) MkBVConst(name string, size uint) *Expr { + sym := c.MkStringSymbol(name) + return c.MkConst(sym, c.MkBvSort(size)) +} + +// MkBV creates a bit-vector numeral from an integer. +func (c *Context) MkBV(value int, size uint) *Expr { + return newExpr(c, C.Z3_mk_int(c.ptr, C.int(value), c.MkBvSort(size).ptr)) +} + +// MkBVFromInt64 creates a bit-vector from an int64. +func (c *Context) MkBVFromInt64(value int64, size uint) *Expr { + return newExpr(c, C.Z3_mk_int64(c.ptr, C.int64_t(value), c.MkBvSort(size).ptr)) +} + +// MkBVAdd creates a bit-vector addition. +func (c *Context) MkBVAdd(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvadd(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSub creates a bit-vector subtraction. +func (c *Context) MkBVSub(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsub(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVMul creates a bit-vector multiplication. +func (c *Context) MkBVMul(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvmul(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVUDiv creates an unsigned bit-vector division. +func (c *Context) MkBVUDiv(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvudiv(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSDiv creates a signed bit-vector division. +func (c *Context) MkBVSDiv(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsdiv(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVURem creates an unsigned bit-vector remainder. +func (c *Context) MkBVURem(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvurem(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSRem creates a signed bit-vector remainder. +func (c *Context) MkBVSRem(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsrem(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVNeg creates a bit-vector negation. +func (c *Context) MkBVNeg(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvneg(c.ptr, expr.ptr)) +} + +// MkBVAnd creates a bit-vector bitwise AND. +func (c *Context) MkBVAnd(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvand(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVOr creates a bit-vector bitwise OR. +func (c *Context) MkBVOr(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvor(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVXor creates a bit-vector bitwise XOR. +func (c *Context) MkBVXor(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvxor(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVNot creates a bit-vector bitwise NOT. +func (c *Context) MkBVNot(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvnot(c.ptr, expr.ptr)) +} + +// MkBVShl creates a bit-vector shift left. +func (c *Context) MkBVShl(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvshl(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVLShr creates a bit-vector logical shift right. +func (c *Context) MkBVLShr(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvlshr(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVAShr creates a bit-vector arithmetic shift right. +func (c *Context) MkBVAShr(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvashr(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVULT creates an unsigned bit-vector less-than. +func (c *Context) MkBVULT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvult(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSLT creates a signed bit-vector less-than. +func (c *Context) MkBVSLT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvslt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVULE creates an unsigned bit-vector less-than-or-equal. +func (c *Context) MkBVULE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvule(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSLE creates a signed bit-vector less-than-or-equal. +func (c *Context) MkBVSLE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsle(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVUGE creates an unsigned bit-vector greater-than-or-equal. +func (c *Context) MkBVUGE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvuge(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSGE creates a signed bit-vector greater-than-or-equal. +func (c *Context) MkBVSGE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsge(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVUGT creates an unsigned bit-vector greater-than. +func (c *Context) MkBVUGT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvugt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkBVSGT creates a signed bit-vector greater-than. +func (c *Context) MkBVSGT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_bvsgt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkConcat creates a bit-vector concatenation. +func (c *Context) MkConcat(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_concat(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkExtract creates a bit-vector extraction. +func (c *Context) MkExtract(high, low uint, expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_extract(c.ptr, C.uint(high), C.uint(low), expr.ptr)) +} + +// MkSignExt creates a bit-vector sign extension. +func (c *Context) MkSignExt(i uint, expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_sign_ext(c.ptr, C.uint(i), expr.ptr)) +} + +// MkZeroExt creates a bit-vector zero extension. +func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr)) +} diff --git a/src/api/go/datatype.go b/src/api/go/datatype.go new file mode 100644 index 000000000..2dd9d8555 --- /dev/null +++ b/src/api/go/datatype.go @@ -0,0 +1,293 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "runtime" + "unsafe" +) + +// Constructor represents a datatype constructor. +type Constructor struct { + ctx *Context + ptr C.Z3_constructor +} + +// newConstructor creates a new Constructor and manages its reference count. +func newConstructor(ctx *Context, ptr C.Z3_constructor) *Constructor { + c := &Constructor{ctx: ctx, ptr: ptr} + C.Z3_constructor_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(c, func(cons *Constructor) { + C.Z3_constructor_dec_ref(cons.ctx.ptr, cons.ptr) + }) + return c +} + +// MkConstructor creates a constructor for a datatype. +// name is the constructor name, recognizer is the recognizer name, +// fieldNames are the names of the fields, and fieldSorts are the sorts of the fields. +// fieldSortRefs can be 0 for non-recursive fields or the datatype index for recursive fields. +func (c *Context) MkConstructor(name, recognizer string, fieldNames []string, fieldSorts []*Sort, fieldSortRefs []uint) *Constructor { + cName := C.CString(name) + cRecognizer := C.CString(recognizer) + defer C.free(unsafe.Pointer(cName)) + defer C.free(unsafe.Pointer(cRecognizer)) + + numFields := uint(len(fieldNames)) + if numFields != uint(len(fieldSorts)) || numFields != uint(len(fieldSortRefs)) { + panic("fieldNames, fieldSorts, and fieldSortRefs must have the same length") + } + + var cFieldNames *C.Z3_symbol + var cSorts *C.Z3_sort + var cSortRefs *C.uint + + if numFields > 0 { + fieldSyms := make([]C.Z3_symbol, numFields) + for i, fname := range fieldNames { + fieldSyms[i] = c.MkStringSymbol(fname).ptr + } + cFieldNames = &fieldSyms[0] + + sorts := make([]C.Z3_sort, numFields) + for i, s := range fieldSorts { + if s != nil { + sorts[i] = s.ptr + } + } + cSorts = &sorts[0] + + refs := make([]C.uint, numFields) + for i, r := range fieldSortRefs { + refs[i] = C.uint(r) + } + cSortRefs = &refs[0] + } + + sym := c.MkStringSymbol(name) + recSym := c.MkStringSymbol(recognizer) + + return newConstructor(c, C.Z3_mk_constructor( + c.ptr, + sym.ptr, + recSym.ptr, + C.uint(numFields), + cFieldNames, + cSorts, + cSortRefs, + )) +} + +// ConstructorList represents a list of datatype constructors. +type ConstructorList struct { + ctx *Context + ptr C.Z3_constructor_list +} + +// newConstructorList creates a new ConstructorList and manages its reference count. +func newConstructorList(ctx *Context, ptr C.Z3_constructor_list) *ConstructorList { + cl := &ConstructorList{ctx: ctx, ptr: ptr} + C.Z3_constructor_list_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(cl, func(list *ConstructorList) { + C.Z3_constructor_list_dec_ref(list.ctx.ptr, list.ptr) + }) + return cl +} + +// MkConstructorList creates a list of constructors for a datatype. +func (c *Context) MkConstructorList(constructors []*Constructor) *ConstructorList { + numCons := uint(len(constructors)) + if numCons == 0 { + return nil + } + + cons := make([]C.Z3_constructor, numCons) + for i, constr := range constructors { + cons[i] = constr.ptr + } + + return newConstructorList(c, C.Z3_mk_constructor_list(c.ptr, C.uint(numCons), &cons[0])) +} + +// MkDatatypeSort creates a datatype sort from a constructor list. +func (c *Context) MkDatatypeSort(name string, constructors []*Constructor) *Sort { + sym := c.MkStringSymbol(name) + + numCons := uint(len(constructors)) + cons := make([]C.Z3_constructor, numCons) + for i, constr := range constructors { + cons[i] = constr.ptr + } + + return newSort(c, C.Z3_mk_datatype(c.ptr, sym.ptr, C.uint(numCons), &cons[0])) +} + +// MkDatatypeSorts creates multiple mutually recursive datatype sorts. +func (c *Context) MkDatatypeSorts(names []string, constructorLists [][]*Constructor) []*Sort { + numTypes := uint(len(names)) + if numTypes != uint(len(constructorLists)) { + panic("names and constructorLists must have the same length") + } + + syms := make([]C.Z3_symbol, numTypes) + for i, name := range names { + syms[i] = c.MkStringSymbol(name).ptr + } + + cLists := make([]C.Z3_constructor_list, numTypes) + for i, constrs := range constructorLists { + cons := make([]C.Z3_constructor, len(constrs)) + for j, constr := range constrs { + cons[j] = constr.ptr + } + cLists[i] = C.Z3_mk_constructor_list(c.ptr, C.uint(len(constrs)), &cons[0]) + } + + resultSorts := make([]C.Z3_sort, numTypes) + + C.Z3_mk_datatypes(c.ptr, C.uint(numTypes), &syms[0], &resultSorts[0], &cLists[0]) + + // Clean up constructor lists + for i := range cLists { + C.Z3_constructor_list_dec_ref(c.ptr, cLists[i]) + } + + sorts := make([]*Sort, numTypes) + for i := range resultSorts { + sorts[i] = newSort(c, resultSorts[i]) + } + + return sorts +} + +// GetDatatypeSortConstructor returns the i-th constructor of a datatype sort. +func (c *Context) GetDatatypeSortConstructor(sort *Sort, i uint) *FuncDecl { + return newFuncDecl(c, C.Z3_get_datatype_sort_constructor(c.ptr, sort.ptr, C.uint(i))) +} + +// GetDatatypeSortRecognizer returns the i-th recognizer of a datatype sort. +func (c *Context) GetDatatypeSortRecognizer(sort *Sort, i uint) *FuncDecl { + return newFuncDecl(c, C.Z3_get_datatype_sort_recognizer(c.ptr, sort.ptr, C.uint(i))) +} + +// GetDatatypeSortConstructorAccessor returns the accessor for the i-th field of the j-th constructor. +func (c *Context) GetDatatypeSortConstructorAccessor(sort *Sort, constructorIdx, accessorIdx uint) *FuncDecl { + return newFuncDecl(c, C.Z3_get_datatype_sort_constructor_accessor( + c.ptr, sort.ptr, C.uint(constructorIdx), C.uint(accessorIdx))) +} + +// GetDatatypeSortNumConstructors returns the number of constructors in a datatype sort. +func (c *Context) GetDatatypeSortNumConstructors(sort *Sort) uint { + return uint(C.Z3_get_datatype_sort_num_constructors(c.ptr, sort.ptr)) +} + +// Tuple sorts (special case of datatypes) + +// MkTupleSort creates a tuple sort with the given field sorts. +func (c *Context) MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort) (*Sort, *FuncDecl, []*FuncDecl) { + sym := c.MkStringSymbol(name) + + numFields := uint(len(fieldNames)) + if numFields != uint(len(fieldSorts)) { + panic("fieldNames and fieldSorts must have the same length") + } + + fieldSyms := make([]C.Z3_symbol, numFields) + for i, fname := range fieldNames { + fieldSyms[i] = c.MkStringSymbol(fname).ptr + } + + sorts := make([]C.Z3_sort, numFields) + for i, s := range fieldSorts { + sorts[i] = s.ptr + } + + var mkTupleDecl C.Z3_func_decl + projDecls := make([]C.Z3_func_decl, numFields) + + tupleSort := C.Z3_mk_tuple_sort( + c.ptr, + sym.ptr, + C.uint(numFields), + &fieldSyms[0], + &sorts[0], + &mkTupleDecl, + &projDecls[0], + ) + + projections := make([]*FuncDecl, numFields) + for i := range projDecls { + projections[i] = newFuncDecl(c, projDecls[i]) + } + + return newSort(c, tupleSort), newFuncDecl(c, mkTupleDecl), projections +} + +// Enumeration sorts (special case of datatypes) + +// MkEnumSort creates an enumeration sort with the given constants. +func (c *Context) MkEnumSort(name string, enumNames []string) (*Sort, []*FuncDecl, []*FuncDecl) { + sym := c.MkStringSymbol(name) + + numEnums := uint(len(enumNames)) + enumSyms := make([]C.Z3_symbol, numEnums) + for i, ename := range enumNames { + enumSyms[i] = c.MkStringSymbol(ename).ptr + } + + enumConsts := make([]C.Z3_func_decl, numEnums) + enumTesters := make([]C.Z3_func_decl, numEnums) + + enumSort := C.Z3_mk_enumeration_sort( + c.ptr, + sym.ptr, + C.uint(numEnums), + &enumSyms[0], + &enumConsts[0], + &enumTesters[0], + ) + + consts := make([]*FuncDecl, numEnums) + for i := range enumConsts { + consts[i] = newFuncDecl(c, enumConsts[i]) + } + + testers := make([]*FuncDecl, numEnums) + for i := range enumTesters { + testers[i] = newFuncDecl(c, enumTesters[i]) + } + + return newSort(c, enumSort), consts, testers +} + +// List sorts (special case of datatypes) + +// MkListSort creates a list sort with the given element sort. +func (c *Context) MkListSort(name string, elemSort *Sort) (*Sort, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl) { + sym := c.MkStringSymbol(name) + + var nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl C.Z3_func_decl + + listSort := C.Z3_mk_list_sort( + c.ptr, + sym.ptr, + elemSort.ptr, + &nilDecl, + &isNilDecl, + &consDecl, + &isConsDecl, + &headDecl, + &tailDecl, + ) + + return newSort(c, listSort), + newFuncDecl(c, nilDecl), + newFuncDecl(c, consDecl), + newFuncDecl(c, isNilDecl), + newFuncDecl(c, isConsDecl), + newFuncDecl(c, headDecl), + newFuncDecl(c, tailDecl) +} diff --git a/src/api/go/fixedpoint.go b/src/api/go/fixedpoint.go new file mode 100644 index 000000000..c22926467 --- /dev/null +++ b/src/api/go/fixedpoint.go @@ -0,0 +1,282 @@ +// Copyright (c) Microsoft Corporation 2025 +// Z3 Go API: Fixedpoint solver for Datalog and CHC (Constrained Horn Clauses) + +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "runtime" + "unsafe" +) + +// Fixedpoint represents a fixedpoint solver for Datalog/CHC queries +type Fixedpoint struct { + ctx *Context + ptr C.Z3_fixedpoint +} + +// newFixedpoint creates a new Fixedpoint solver with proper memory management +func newFixedpoint(ctx *Context, ptr C.Z3_fixedpoint) *Fixedpoint { + fp := &Fixedpoint{ctx: ctx, ptr: ptr} + C.Z3_fixedpoint_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(fp, func(f *Fixedpoint) { + C.Z3_fixedpoint_dec_ref(f.ctx.ptr, f.ptr) + }) + return fp +} + +// NewFixedpoint creates a new fixedpoint solver +func (ctx *Context) NewFixedpoint() *Fixedpoint { + ptr := C.Z3_mk_fixedpoint(ctx.ptr) + return newFixedpoint(ctx, ptr) +} + +// GetHelp returns a string describing all available fixedpoint solver parameters +func (f *Fixedpoint) GetHelp() string { + cstr := C.Z3_fixedpoint_get_help(f.ctx.ptr, f.ptr) + return C.GoString(cstr) +} + +// SetParams sets the fixedpoint solver parameters +func (f *Fixedpoint) SetParams(params *Params) { + C.Z3_fixedpoint_set_params(f.ctx.ptr, f.ptr, params.ptr) +} + +// GetParamDescrs retrieves parameter descriptions for the fixedpoint solver +func (f *Fixedpoint) GetParamDescrs() *ParamDescrs { + ptr := C.Z3_fixedpoint_get_param_descrs(f.ctx.ptr, f.ptr) + return newParamDescrs(f.ctx, ptr) +} + +// Assert adds a constraint into the fixedpoint solver +func (f *Fixedpoint) Assert(constraint *Expr) { + C.Z3_fixedpoint_assert(f.ctx.ptr, f.ptr, constraint.ptr) +} + +// RegisterRelation registers a predicate as a recursive relation +func (f *Fixedpoint) RegisterRelation(funcDecl *FuncDecl) { + C.Z3_fixedpoint_register_relation(f.ctx.ptr, f.ptr, funcDecl.ptr) +} + +// AddRule adds a rule (Horn clause) to the fixedpoint solver +// The rule should be an implication of the form body => head +// where head is a relation and body is a conjunction of relations +func (f *Fixedpoint) AddRule(rule *Expr, name *Symbol) { + var namePtr C.Z3_symbol + if name != nil { + namePtr = name.ptr + } else { + namePtr = 0 + } + C.Z3_fixedpoint_add_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr) +} + +// AddFact adds a table fact to the fixedpoint solver +func (f *Fixedpoint) AddFact(pred *FuncDecl, args []int) { + if len(args) == 0 { + C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, 0, nil) + return + } + + cArgs := make([]C.uint, len(args)) + for i, arg := range args { + cArgs[i] = C.uint(arg) + } + C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, C.uint(len(args)), &cArgs[0]) +} + +// Query queries the fixedpoint solver with a constraint +// Returns Satisfiable if there is a derivation, Unsatisfiable if not +func (f *Fixedpoint) Query(query *Expr) Status { + result := C.Z3_fixedpoint_query(f.ctx.ptr, f.ptr, query.ptr) + switch result { + case C.Z3_L_TRUE: + return Satisfiable + case C.Z3_L_FALSE: + return Unsatisfiable + default: + return Unknown + } +} + +// QueryRelations queries the fixedpoint solver with an array of relations +// Returns Satisfiable if any relation is non-empty, Unsatisfiable otherwise +func (f *Fixedpoint) QueryRelations(relations []*FuncDecl) Status { + if len(relations) == 0 { + return Unknown + } + + cRelations := make([]C.Z3_func_decl, len(relations)) + for i, rel := range relations { + cRelations[i] = rel.ptr + } + + result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0]) + switch result { + case C.Z3_L_TRUE: + return Satisfiable + case C.Z3_L_FALSE: + return Unsatisfiable + default: + return Unknown + } +} + +// UpdateRule updates a named rule in the fixedpoint solver +func (f *Fixedpoint) UpdateRule(rule *Expr, name *Symbol) { + var namePtr C.Z3_symbol + if name != nil { + namePtr = name.ptr + } else { + namePtr = 0 + } + C.Z3_fixedpoint_update_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr) +} + +// GetAnswer retrieves the satisfying instance or instances of solver, +// or definitions for the recursive predicates that show unsatisfiability +func (f *Fixedpoint) GetAnswer() *Expr { + ptr := C.Z3_fixedpoint_get_answer(f.ctx.ptr, f.ptr) + if ptr == nil { + return nil + } + return newExpr(f.ctx, ptr) +} + +// GetReasonUnknown retrieves explanation why fixedpoint engine returned status Unknown +func (f *Fixedpoint) GetReasonUnknown() string { + cstr := C.Z3_fixedpoint_get_reason_unknown(f.ctx.ptr, f.ptr) + return C.GoString(cstr) +} + +// GetNumLevels retrieves the number of levels explored for a given predicate +func (f *Fixedpoint) GetNumLevels(predicate *FuncDecl) int { + return int(C.Z3_fixedpoint_get_num_levels(f.ctx.ptr, f.ptr, predicate.ptr)) +} + +// GetCoverDelta retrieves the cover delta for a given predicate and level +func (f *Fixedpoint) GetCoverDelta(level int, predicate *FuncDecl) *Expr { + ptr := C.Z3_fixedpoint_get_cover_delta(f.ctx.ptr, f.ptr, C.int(level), predicate.ptr) + if ptr == nil { + return nil + } + return newExpr(f.ctx, ptr) +} + +// AddCover adds a cover constraint to a predicate at a given level +func (f *Fixedpoint) AddCover(level int, predicate *FuncDecl, property *Expr) { + C.Z3_fixedpoint_add_cover(f.ctx.ptr, f.ptr, C.int(level), predicate.ptr, property.ptr) +} + +// String returns the string representation of the fixedpoint solver +func (f *Fixedpoint) String() string { + cstr := C.Z3_fixedpoint_to_string(f.ctx.ptr, f.ptr, 0, nil) + return C.GoString(cstr) +} + +// GetStatistics retrieves statistics for the fixedpoint solver +func (f *Fixedpoint) GetStatistics() *Statistics { + ptr := C.Z3_fixedpoint_get_statistics(f.ctx.ptr, f.ptr) + return newStatistics(f.ctx, ptr) +} + +// GetRules retrieves the current rules as a string +func (f *Fixedpoint) GetRules() string { + return f.String() +} + +// GetAssertions retrieves the fixedpoint assertions as an AST vector +func (f *Fixedpoint) GetAssertions() *ASTVector { + ptr := C.Z3_fixedpoint_get_assertions(f.ctx.ptr, f.ptr) + return newASTVector(f.ctx, ptr) +} + +// Push creates a backtracking point +func (f *Fixedpoint) Push() { + C.Z3_fixedpoint_push(f.ctx.ptr, f.ptr) +} + +// Pop backtracks one backtracking point +func (f *Fixedpoint) Pop() { + C.Z3_fixedpoint_pop(f.ctx.ptr, f.ptr) +} + +// SetPredicateRepresentation sets the predicate representation for a given relation +func (f *Fixedpoint) SetPredicateRepresentation(funcDecl *FuncDecl, kinds []C.Z3_symbol) { + if len(kinds) == 0 { + C.Z3_fixedpoint_set_predicate_representation(f.ctx.ptr, f.ptr, funcDecl.ptr, 0, nil) + return + } + C.Z3_fixedpoint_set_predicate_representation(f.ctx.ptr, f.ptr, funcDecl.ptr, C.uint(len(kinds)), &kinds[0]) +} + +// FromString parses a Datalog program from a string +func (f *Fixedpoint) FromString(s string) { + cstr := C.CString(s) + defer C.free(unsafe.Pointer(cstr)) + C.Z3_fixedpoint_from_string(f.ctx.ptr, f.ptr, cstr) +} + +// FromFile parses a Datalog program from a file +func (f *Fixedpoint) FromFile(filename string) { + cstr := C.CString(filename) + defer C.free(unsafe.Pointer(cstr)) + C.Z3_fixedpoint_from_file(f.ctx.ptr, f.ptr, cstr) +} + +// Statistics represents statistics for Z3 solvers +type Statistics struct { + ctx *Context + ptr C.Z3_stats +} + +// newStatistics creates a new Statistics object with proper memory management +func newStatistics(ctx *Context, ptr C.Z3_stats) *Statistics { + stats := &Statistics{ctx: ctx, ptr: ptr} + C.Z3_stats_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(stats, func(s *Statistics) { + C.Z3_stats_dec_ref(s.ctx.ptr, s.ptr) + }) + return stats +} + +// String returns the string representation of statistics +func (s *Statistics) String() string { + cstr := C.Z3_stats_to_string(s.ctx.ptr, s.ptr) + return C.GoString(cstr) +} + +// Size returns the number of statistical data entries +func (s *Statistics) Size() int { + return int(C.Z3_stats_size(s.ctx.ptr, s.ptr)) +} + +// GetKey returns the key (name) of a statistical data entry at the given index +func (s *Statistics) GetKey(idx int) string { + cstr := C.Z3_stats_get_key(s.ctx.ptr, s.ptr, C.uint(idx)) + return C.GoString(cstr) +} + +// IsUint returns true if the statistical data at the given index is unsigned integer +func (s *Statistics) IsUint(idx int) bool { + return C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx)) != 0 +} + +// IsDouble returns true if the statistical data at the given index is double +func (s *Statistics) IsDouble(idx int) bool { + return C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx)) != 0 +} + +// GetUintValue returns the unsigned integer value at the given index +func (s *Statistics) GetUintValue(idx int) uint64 { + return uint64(C.Z3_stats_get_uint_value(s.ctx.ptr, s.ptr, C.uint(idx))) +} + +// GetDoubleValue returns the double value at the given index +func (s *Statistics) GetDoubleValue(idx int) float64 { + return float64(C.Z3_stats_get_double_value(s.ctx.ptr, s.ptr, C.uint(idx))) +} diff --git a/src/api/go/fp.go b/src/api/go/fp.go new file mode 100644 index 000000000..116d681aa --- /dev/null +++ b/src/api/go/fp.go @@ -0,0 +1,139 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "unsafe" +) + +// Floating-point operations + +// MkFPSort creates a floating-point sort. +func (c *Context) MkFPSort(ebits, sbits uint) *Sort { + return newSort(c, C.Z3_mk_fpa_sort(c.ptr, C.uint(ebits), C.uint(sbits))) +} + +// MkFPSort16 creates a 16-bit floating-point sort. +func (c *Context) MkFPSort16() *Sort { + return newSort(c, C.Z3_mk_fpa_sort_16(c.ptr)) +} + +// MkFPSort32 creates a 32-bit floating-point sort (single precision). +func (c *Context) MkFPSort32() *Sort { + return newSort(c, C.Z3_mk_fpa_sort_32(c.ptr)) +} + +// MkFPSort64 creates a 64-bit floating-point sort (double precision). +func (c *Context) MkFPSort64() *Sort { + return newSort(c, C.Z3_mk_fpa_sort_64(c.ptr)) +} + +// MkFPSort128 creates a 128-bit floating-point sort (quadruple precision). +func (c *Context) MkFPSort128() *Sort { + return newSort(c, C.Z3_mk_fpa_sort_128(c.ptr)) +} + +// MkFPRoundingModeSort creates the rounding mode sort. +func (c *Context) MkFPRoundingModeSort() *Sort { + return newSort(c, C.Z3_mk_fpa_rounding_mode_sort(c.ptr)) +} + +// MkFPNumeral creates a floating-point numeral from a string. +func (c *Context) MkFPNumeral(value string, sort *Sort) *Expr { + cStr := C.CString(value) + defer C.free(unsafe.Pointer(cStr)) + return newExpr(c, C.Z3_mk_numeral(c.ptr, cStr, sort.ptr)) +} + +// MkFPInf creates a floating-point infinity. +func (c *Context) MkFPInf(sort *Sort, negative bool) *Expr { + return newExpr(c, C.Z3_mk_fpa_inf(c.ptr, sort.ptr, C.bool(negative))) +} + +// MkFPNaN creates a floating-point NaN. +func (c *Context) MkFPNaN(sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_fpa_nan(c.ptr, sort.ptr)) +} + +// MkFPZero creates a floating-point zero. +func (c *Context) MkFPZero(sort *Sort, negative bool) *Expr { + return newExpr(c, C.Z3_mk_fpa_zero(c.ptr, sort.ptr, C.bool(negative))) +} + +// MkFPAdd creates a floating-point addition. +func (c *Context) MkFPAdd(rm, lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_add(c.ptr, rm.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPSub creates a floating-point subtraction. +func (c *Context) MkFPSub(rm, lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_sub(c.ptr, rm.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPMul creates a floating-point multiplication. +func (c *Context) MkFPMul(rm, lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_mul(c.ptr, rm.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPDiv creates a floating-point division. +func (c *Context) MkFPDiv(rm, lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_div(c.ptr, rm.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPNeg creates a floating-point negation. +func (c *Context) MkFPNeg(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_neg(c.ptr, expr.ptr)) +} + +// MkFPAbs creates a floating-point absolute value. +func (c *Context) MkFPAbs(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_abs(c.ptr, expr.ptr)) +} + +// MkFPSqrt creates a floating-point square root. +func (c *Context) MkFPSqrt(rm, expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_sqrt(c.ptr, rm.ptr, expr.ptr)) +} + +// MkFPLT creates a floating-point less-than. +func (c *Context) MkFPLT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_lt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPGT creates a floating-point greater-than. +func (c *Context) MkFPGT(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_gt(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPLE creates a floating-point less-than-or-equal. +func (c *Context) MkFPLE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_leq(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPGE creates a floating-point greater-than-or-equal. +func (c *Context) MkFPGE(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_geq(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPEq creates a floating-point equality. +func (c *Context) MkFPEq(lhs, rhs *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_eq(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkFPIsNaN creates a predicate checking if a floating-point number is NaN. +func (c *Context) MkFPIsNaN(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_is_nan(c.ptr, expr.ptr)) +} + +// MkFPIsInf creates a predicate checking if a floating-point number is infinite. +func (c *Context) MkFPIsInf(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_is_infinite(c.ptr, expr.ptr)) +} + +// MkFPIsZero creates a predicate checking if a floating-point number is zero. +func (c *Context) MkFPIsZero(expr *Expr) *Expr { + return newExpr(c, C.Z3_mk_fpa_is_zero(c.ptr, expr.ptr)) +} diff --git a/src/api/go/go.mod b/src/api/go/go.mod new file mode 100644 index 000000000..f3372382b --- /dev/null +++ b/src/api/go/go.mod @@ -0,0 +1,6 @@ +module github.com/Z3Prover/z3/src/api/go + +go 1.20 + +// This package provides Go bindings for the Z3 theorem prover. +// It uses CGO to wrap the Z3 C API. diff --git a/src/api/go/log.go b/src/api/go/log.go new file mode 100644 index 000000000..dc43419ae --- /dev/null +++ b/src/api/go/log.go @@ -0,0 +1,67 @@ +// Copyright (c) Microsoft Corporation 2025 +// Z3 Go API: Logging functionality + +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "sync" + "unsafe" +) + +var ( + logMutex sync.Mutex + isLogOpen bool +) + +// OpenLog opens an interaction log file +// Returns true if successful, false otherwise +func OpenLog(filename string) bool { + logMutex.Lock() + defer logMutex.Unlock() + + cFilename := C.CString(filename) + defer C.free(unsafe.Pointer(cFilename)) + + result := C.Z3_open_log(cFilename) + if result != 0 { + isLogOpen = true + return true + } + return false +} + +// CloseLog closes the interaction log +func CloseLog() { + logMutex.Lock() + defer logMutex.Unlock() + + C.Z3_close_log() + isLogOpen = false +} + +// AppendLog appends a user-provided string to the interaction log +// Panics if the log is not open +func AppendLog(s string) { + logMutex.Lock() + defer logMutex.Unlock() + + if !isLogOpen { + panic("Log is not open") + } + + cStr := C.CString(s) + defer C.free(unsafe.Pointer(cStr)) + C.Z3_append_log(cStr) +} + +// IsLogOpen returns true if the interaction log is open +func IsLogOpen() bool { + logMutex.Lock() + defer logMutex.Unlock() + return isLogOpen +} diff --git a/src/api/go/optimize.go b/src/api/go/optimize.go new file mode 100644 index 000000000..bc6940a22 --- /dev/null +++ b/src/api/go/optimize.go @@ -0,0 +1,218 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "runtime" + "unsafe" +) + +// Optimize represents a Z3 optimization context for solving optimization problems. +// Unlike Solver which only checks satisfiability, Optimize can find optimal solutions +// with respect to objective functions. +type Optimize struct { + ctx *Context + ptr C.Z3_optimize +} + +// NewOptimize creates a new optimization context. +func (c *Context) NewOptimize() *Optimize { + opt := &Optimize{ + ctx: c, + ptr: C.Z3_mk_optimize(c.ptr), + } + C.Z3_optimize_inc_ref(c.ptr, opt.ptr) + runtime.SetFinalizer(opt, func(o *Optimize) { + C.Z3_optimize_dec_ref(o.ctx.ptr, o.ptr) + }) + return opt +} + +// String returns the string representation of the optimize context. +func (o *Optimize) String() string { + return C.GoString(C.Z3_optimize_to_string(o.ctx.ptr, o.ptr)) +} + +// Assert adds a constraint to the optimizer. +func (o *Optimize) Assert(constraint *Expr) { + C.Z3_optimize_assert(o.ctx.ptr, o.ptr, constraint.ptr) +} + +// AssertAndTrack adds a constraint with a tracking literal for unsat core extraction. +func (o *Optimize) AssertAndTrack(constraint, track *Expr) { + C.Z3_optimize_assert_and_track(o.ctx.ptr, o.ptr, constraint.ptr, track.ptr) +} + +// AssertSoft adds a soft constraint with a weight. +// Soft constraints are used for MaxSMT problems. +// Returns a handle to the objective. +func (o *Optimize) AssertSoft(constraint *Expr, weight string, group string) uint { + cWeight := C.CString(weight) + cGroup := C.CString(group) + defer C.free(unsafe.Pointer(cWeight)) + defer C.free(unsafe.Pointer(cGroup)) + + sym := o.ctx.MkStringSymbol(group) + return uint(C.Z3_optimize_assert_soft(o.ctx.ptr, o.ptr, constraint.ptr, cWeight, sym.ptr)) +} + +// Maximize adds a maximization objective. +// Returns a handle to the objective that can be used to retrieve bounds. +func (o *Optimize) Maximize(expr *Expr) uint { + return uint(C.Z3_optimize_maximize(o.ctx.ptr, o.ptr, expr.ptr)) +} + +// Minimize adds a minimization objective. +// Returns a handle to the objective that can be used to retrieve bounds. +func (o *Optimize) Minimize(expr *Expr) uint { + return uint(C.Z3_optimize_minimize(o.ctx.ptr, o.ptr, expr.ptr)) +} + +// Check checks the satisfiability of the constraints and optimizes objectives. +func (o *Optimize) Check(assumptions ...*Expr) Status { + var result C.Z3_lbool + if len(assumptions) == 0 { + result = C.Z3_optimize_check(o.ctx.ptr, o.ptr, 0, nil) + } else { + cAssumptions := make([]C.Z3_ast, len(assumptions)) + for i, a := range assumptions { + cAssumptions[i] = a.ptr + } + result = C.Z3_optimize_check(o.ctx.ptr, o.ptr, C.uint(len(assumptions)), &cAssumptions[0]) + } + return Status(result) +} + +// Model returns the model if the constraints are satisfiable. +func (o *Optimize) Model() *Model { + modelPtr := C.Z3_optimize_get_model(o.ctx.ptr, o.ptr) + if modelPtr == nil { + return nil + } + return newModel(o.ctx, modelPtr) +} + +// Push creates a backtracking point. +func (o *Optimize) Push() { + C.Z3_optimize_push(o.ctx.ptr, o.ptr) +} + +// Pop removes a backtracking point. +func (o *Optimize) Pop() { + C.Z3_optimize_pop(o.ctx.ptr, o.ptr) +} + +// GetLower retrieves a lower bound for the objective at the given index. +func (o *Optimize) GetLower(index uint) *Expr { + result := C.Z3_optimize_get_lower(o.ctx.ptr, o.ptr, C.uint(index)) + if result == nil { + return nil + } + return newExpr(o.ctx, result) +} + +// GetUpper retrieves an upper bound for the objective at the given index. +func (o *Optimize) GetUpper(index uint) *Expr { + result := C.Z3_optimize_get_upper(o.ctx.ptr, o.ptr, C.uint(index)) + if result == nil { + return nil + } + return newExpr(o.ctx, result) +} + +// GetLowerAsVector retrieves a lower bound as a vector (inf, value, eps). +// The objective value is unbounded if inf is non-zero, +// otherwise it's represented as value + eps * EPSILON. +func (o *Optimize) GetLowerAsVector(index uint) []*Expr { + vec := C.Z3_optimize_get_lower_as_vector(o.ctx.ptr, o.ptr, C.uint(index)) + size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec)) + if size != 3 { + return nil + } + return []*Expr{ + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)), + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)), + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)), + } +} + +// GetUpperAsVector retrieves an upper bound as a vector (inf, value, eps). +// The objective value is unbounded if inf is non-zero, +// otherwise it's represented as value + eps * EPSILON. +func (o *Optimize) GetUpperAsVector(index uint) []*Expr { + vec := C.Z3_optimize_get_upper_as_vector(o.ctx.ptr, o.ptr, C.uint(index)) + size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec)) + if size != 3 { + return nil + } + return []*Expr{ + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)), + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)), + newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)), + } +} + +// ReasonUnknown returns the reason why the result is unknown. +func (o *Optimize) ReasonUnknown() string { + return C.GoString(C.Z3_optimize_get_reason_unknown(o.ctx.ptr, o.ptr)) +} + +// GetHelp returns help information for the optimizer. +func (o *Optimize) GetHelp() string { + return C.GoString(C.Z3_optimize_get_help(o.ctx.ptr, o.ptr)) +} + +// SetParams sets parameters for the optimizer. +func (o *Optimize) SetParams(params *Params) { + C.Z3_optimize_set_params(o.ctx.ptr, o.ptr, params.ptr) +} + +// Assertions returns the assertions in the optimizer. +func (o *Optimize) Assertions() []*Expr { + vec := C.Z3_optimize_get_assertions(o.ctx.ptr, o.ptr) + size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec)) + result := make([]*Expr, size) + for i := uint(0); i < size; i++ { + result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i))) + } + return result +} + +// Objectives returns the objectives in the optimizer. +func (o *Optimize) Objectives() []*Expr { + vec := C.Z3_optimize_get_objectives(o.ctx.ptr, o.ptr) + size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec)) + result := make([]*Expr, size) + for i := uint(0); i < size; i++ { + result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i))) + } + return result +} + +// UnsatCore returns the unsat core if the constraints are unsatisfiable. +func (o *Optimize) UnsatCore() []*Expr { + vec := C.Z3_optimize_get_unsat_core(o.ctx.ptr, o.ptr) + size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec)) + result := make([]*Expr, size) + for i := uint(0); i < size; i++ { + result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i))) + } + return result +} + +// FromFile parses an SMT-LIB2 file with optimization objectives and constraints. +func (o *Optimize) FromFile(filename string) { + cFilename := C.CString(filename) + defer C.free(unsafe.Pointer(cFilename)) + C.Z3_optimize_from_file(o.ctx.ptr, o.ptr, cFilename) +} + +// FromString parses an SMT-LIB2 string with optimization objectives and constraints. +func (o *Optimize) FromString(s string) { + cStr := C.CString(s) + defer C.free(unsafe.Pointer(cStr)) + C.Z3_optimize_from_string(o.ctx.ptr, o.ptr, cStr) +} diff --git a/src/api/go/seq.go b/src/api/go/seq.go new file mode 100644 index 000000000..3da8a716a --- /dev/null +++ b/src/api/go/seq.go @@ -0,0 +1,232 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "unsafe" +) + +// Sequence and string operations + +// MkSeqSort creates a sequence sort. +func (c *Context) MkSeqSort(elemSort *Sort) *Sort { + return newSort(c, C.Z3_mk_seq_sort(c.ptr, elemSort.ptr)) +} + +// MkStringSort creates a string sort (sequence of characters). +func (c *Context) MkStringSort() *Sort { + return newSort(c, C.Z3_mk_string_sort(c.ptr)) +} + +// MkString creates a string constant. +func (c *Context) MkString(value string) *Expr { + cStr := C.CString(value) + defer C.free(unsafe.Pointer(cStr)) + return newExpr(c, C.Z3_mk_string(c.ptr, cStr)) +} + +// MkEmptySeq creates an empty sequence. +func (c *Context) MkEmptySeq(sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_seq_empty(c.ptr, sort.ptr)) +} + +// MkSeqUnit creates a unit sequence containing a single element. +func (c *Context) MkSeqUnit(elem *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_unit(c.ptr, elem.ptr)) +} + +// MkSeqConcat creates a sequence concatenation. +func (c *Context) MkSeqConcat(exprs ...*Expr) *Expr { + if len(exprs) == 0 { + return nil + } + if len(exprs) == 1 { + return exprs[0] + } + cExprs := make([]C.Z3_ast, len(exprs)) + for i, e := range exprs { + cExprs[i] = e.ptr + } + return newExpr(c, C.Z3_mk_seq_concat(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkSeqLength creates a sequence length operation. +func (c *Context) MkSeqLength(seq *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_length(c.ptr, seq.ptr)) +} + +// MkSeqPrefix creates a sequence prefix predicate. +func (c *Context) MkSeqPrefix(prefix, seq *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_prefix(c.ptr, prefix.ptr, seq.ptr)) +} + +// MkSeqSuffix creates a sequence suffix predicate. +func (c *Context) MkSeqSuffix(suffix, seq *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_suffix(c.ptr, suffix.ptr, seq.ptr)) +} + +// MkSeqContains creates a sequence contains predicate. +func (c *Context) MkSeqContains(seq, substr *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_contains(c.ptr, seq.ptr, substr.ptr)) +} + +// MkSeqAt creates a sequence element access operation. +func (c *Context) MkSeqAt(seq, index *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_at(c.ptr, seq.ptr, index.ptr)) +} + +// MkSeqExtract creates a sequence extract (substring) operation. +func (c *Context) MkSeqExtract(seq, offset, length *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_extract(c.ptr, seq.ptr, offset.ptr, length.ptr)) +} + +// MkSeqReplace creates a sequence replace operation. +func (c *Context) MkSeqReplace(seq, src, dst *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_replace(c.ptr, seq.ptr, src.ptr, dst.ptr)) +} + +// MkSeqIndexOf creates a sequence index-of operation. +func (c *Context) MkSeqIndexOf(seq, substr, offset *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_index(c.ptr, seq.ptr, substr.ptr, offset.ptr)) +} + +// MkStrToInt creates a string-to-integer conversion. +func (c *Context) MkStrToInt(str *Expr) *Expr { + return newExpr(c, C.Z3_mk_str_to_int(c.ptr, str.ptr)) +} + +// MkIntToStr creates an integer-to-string conversion. +func (c *Context) MkIntToStr(num *Expr) *Expr { + return newExpr(c, C.Z3_mk_int_to_str(c.ptr, num.ptr)) +} + +// Regular expression operations + +// MkReSort creates a regular expression sort. +func (c *Context) MkReSort(seqSort *Sort) *Sort { + return newSort(c, C.Z3_mk_re_sort(c.ptr, seqSort.ptr)) +} + +// MkToRe converts a sequence to a regular expression that accepts exactly that sequence. +func (c *Context) MkToRe(seq *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_to_re(c.ptr, seq.ptr)) +} + +// MkInRe creates a membership predicate for a sequence in a regular expression. +func (c *Context) MkInRe(seq, re *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_in_re(c.ptr, seq.ptr, re.ptr)) +} + +// MkReStar creates a Kleene star (zero or more repetitions) of a regular expression. +func (c *Context) MkReStar(re *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_star(c.ptr, re.ptr)) +} + +// MkRePlus creates a Kleene plus (one or more repetitions) of a regular expression. +func (c *Context) MkRePlus(re *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_plus(c.ptr, re.ptr)) +} + +// MkReOption creates an optional regular expression (zero or one repetition). +func (c *Context) MkReOption(re *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_option(c.ptr, re.ptr)) +} + +// MkRePower creates a regular expression that matches exactly n repetitions. +func (c *Context) MkRePower(re *Expr, n uint) *Expr { + return newExpr(c, C.Z3_mk_re_power(c.ptr, re.ptr, C.uint(n))) +} + +// MkReLoop creates a regular expression with bounded repetition (between lo and hi times). +// If hi is 0, it means unbounded (at least lo times). +func (c *Context) MkReLoop(re *Expr, lo, hi uint) *Expr { + return newExpr(c, C.Z3_mk_re_loop(c.ptr, re.ptr, C.uint(lo), C.uint(hi))) +} + +// MkReConcat creates a concatenation of regular expressions. +func (c *Context) MkReConcat(regexes ...*Expr) *Expr { + if len(regexes) == 0 { + return nil + } + if len(regexes) == 1 { + return regexes[0] + } + cRegexes := make([]C.Z3_ast, len(regexes)) + for i, re := range regexes { + cRegexes[i] = re.ptr + } + return newExpr(c, C.Z3_mk_re_concat(c.ptr, C.uint(len(regexes)), &cRegexes[0])) +} + +// MkReUnion creates a union (alternation) of regular expressions. +func (c *Context) MkReUnion(regexes ...*Expr) *Expr { + if len(regexes) == 0 { + return nil + } + if len(regexes) == 1 { + return regexes[0] + } + cRegexes := make([]C.Z3_ast, len(regexes)) + for i, re := range regexes { + cRegexes[i] = re.ptr + } + return newExpr(c, C.Z3_mk_re_union(c.ptr, C.uint(len(regexes)), &cRegexes[0])) +} + +// MkReIntersect creates an intersection of regular expressions. +func (c *Context) MkReIntersect(regexes ...*Expr) *Expr { + if len(regexes) == 0 { + return nil + } + if len(regexes) == 1 { + return regexes[0] + } + cRegexes := make([]C.Z3_ast, len(regexes)) + for i, re := range regexes { + cRegexes[i] = re.ptr + } + return newExpr(c, C.Z3_mk_re_intersect(c.ptr, C.uint(len(regexes)), &cRegexes[0])) +} + +// MkReComplement creates the complement of a regular expression. +func (c *Context) MkReComplement(re *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_complement(c.ptr, re.ptr)) +} + +// MkReDiff creates the difference of two regular expressions (a - b). +func (c *Context) MkReDiff(a, b *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_diff(c.ptr, a.ptr, b.ptr)) +} + +// MkReEmpty creates an empty regular expression (accepts no strings). +func (c *Context) MkReEmpty(sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_re_empty(c.ptr, sort.ptr)) +} + +// MkReFull creates a full regular expression (accepts all strings). +func (c *Context) MkReFull(sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_re_full(c.ptr, sort.ptr)) +} + +// MkReAllchar creates a regular expression that accepts all single characters. +func (c *Context) MkReAllchar(sort *Sort) *Expr { + return newExpr(c, C.Z3_mk_re_allchar(c.ptr, sort.ptr)) +} + +// MkReRange creates a regular expression for a character range [lo, hi]. +func (c *Context) MkReRange(lo, hi *Expr) *Expr { + return newExpr(c, C.Z3_mk_re_range(c.ptr, lo.ptr, hi.ptr)) +} + +// MkSeqReplaceRe replaces the first occurrence matching a regular expression. +func (c *Context) MkSeqReplaceRe(seq, re, replacement *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_replace_re(c.ptr, seq.ptr, re.ptr, replacement.ptr)) +} + +// MkSeqReplaceReAll replaces all occurrences matching a regular expression. +func (c *Context) MkSeqReplaceReAll(seq, re, replacement *Expr) *Expr { + return newExpr(c, C.Z3_mk_seq_replace_re_all(c.ptr, seq.ptr, re.ptr, replacement.ptr)) +} diff --git a/src/api/go/solver.go b/src/api/go/solver.go new file mode 100644 index 000000000..3dec5cc70 --- /dev/null +++ b/src/api/go/solver.go @@ -0,0 +1,263 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "runtime" + "unsafe" +) + +// Status represents the result of a satisfiability check. +type Status int + +const ( + // Unsatisfiable means the constraints are unsatisfiable. + Unsatisfiable Status = -1 + // Unknown means Z3 could not determine satisfiability. + Unknown Status = 0 + // Satisfiable means the constraints are satisfiable. + Satisfiable Status = 1 +) + +// String returns the string representation of the status. +func (s Status) String() string { + switch s { + case Unsatisfiable: + return "unsat" + case Unknown: + return "unknown" + case Satisfiable: + return "sat" + default: + return "unknown" + } +} + +// Solver represents a Z3 solver. +type Solver struct { + ctx *Context + ptr C.Z3_solver +} + +// NewSolver creates a new solver for the given context. +func (c *Context) NewSolver() *Solver { + s := &Solver{ + ctx: c, + ptr: C.Z3_mk_solver(c.ptr), + } + C.Z3_solver_inc_ref(c.ptr, s.ptr) + runtime.SetFinalizer(s, func(solver *Solver) { + C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr) + }) + return s +} + +// NewSolverForLogic creates a solver for a specific logic. +func (c *Context) NewSolverForLogic(logic string) *Solver { + sym := c.MkStringSymbol(logic) + s := &Solver{ + ctx: c, + ptr: C.Z3_mk_solver_for_logic(c.ptr, sym.ptr), + } + C.Z3_solver_inc_ref(c.ptr, s.ptr) + runtime.SetFinalizer(s, func(solver *Solver) { + C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr) + }) + return s +} + +// String returns the string representation of the solver. +func (s *Solver) String() string { + return C.GoString(C.Z3_solver_to_string(s.ctx.ptr, s.ptr)) +} + +// Assert adds a constraint to the solver. +func (s *Solver) Assert(constraint *Expr) { + C.Z3_solver_assert(s.ctx.ptr, s.ptr, constraint.ptr) +} + +// AssertAndTrack adds a constraint with a tracking literal. +func (s *Solver) AssertAndTrack(constraint, track *Expr) { + C.Z3_solver_assert_and_track(s.ctx.ptr, s.ptr, constraint.ptr, track.ptr) +} + +// Check checks the satisfiability of the constraints. +func (s *Solver) Check() Status { + result := C.Z3_solver_check(s.ctx.ptr, s.ptr) + return Status(result) +} + +// CheckAssumptions checks satisfiability under assumptions. +func (s *Solver) CheckAssumptions(assumptions ...*Expr) Status { + if len(assumptions) == 0 { + return s.Check() + } + cAssumptions := make([]C.Z3_ast, len(assumptions)) + for i, a := range assumptions { + cAssumptions[i] = a.ptr + } + result := C.Z3_solver_check_assumptions(s.ctx.ptr, s.ptr, C.uint(len(assumptions)), &cAssumptions[0]) + return Status(result) +} + +// Model returns the model if the constraints are satisfiable. +func (s *Solver) Model() *Model { + modelPtr := C.Z3_solver_get_model(s.ctx.ptr, s.ptr) + if modelPtr == nil { + return nil + } + return newModel(s.ctx, modelPtr) +} + +// Push creates a backtracking point. +func (s *Solver) Push() { + C.Z3_solver_push(s.ctx.ptr, s.ptr) +} + +// Pop removes backtracking points. +func (s *Solver) Pop(n uint) { + C.Z3_solver_pop(s.ctx.ptr, s.ptr, C.uint(n)) +} + +// Reset removes all assertions from the solver. +func (s *Solver) Reset() { + C.Z3_solver_reset(s.ctx.ptr, s.ptr) +} + +// NumScopes returns the number of backtracking points. +func (s *Solver) NumScopes() uint { + return uint(C.Z3_solver_get_num_scopes(s.ctx.ptr, s.ptr)) +} + +// Assertions returns the assertions in the solver. +func (s *Solver) Assertions() []*Expr { + vec := C.Z3_solver_get_assertions(s.ctx.ptr, s.ptr) + size := uint(C.Z3_ast_vector_size(s.ctx.ptr, vec)) + result := make([]*Expr, size) + for i := uint(0); i < size; i++ { + result[i] = newExpr(s.ctx, C.Z3_ast_vector_get(s.ctx.ptr, vec, C.uint(i))) + } + return result +} + +// UnsatCore returns the unsat core if the constraints are unsatisfiable. +func (s *Solver) UnsatCore() []*Expr { + vec := C.Z3_solver_get_unsat_core(s.ctx.ptr, s.ptr) + size := uint(C.Z3_ast_vector_size(s.ctx.ptr, vec)) + result := make([]*Expr, size) + for i := uint(0); i < size; i++ { + result[i] = newExpr(s.ctx, C.Z3_ast_vector_get(s.ctx.ptr, vec, C.uint(i))) + } + return result +} + +// ReasonUnknown returns the reason why the result is unknown. +func (s *Solver) ReasonUnknown() string { + return C.GoString(C.Z3_solver_get_reason_unknown(s.ctx.ptr, s.ptr)) +} + +// Model represents a Z3 model (satisfying assignment). +type Model struct { + ctx *Context + ptr C.Z3_model +} + +// newModel creates a new Model and manages its reference count. +func newModel(ctx *Context, ptr C.Z3_model) *Model { + m := &Model{ctx: ctx, ptr: ptr} + C.Z3_model_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(m, func(model *Model) { + C.Z3_model_dec_ref(model.ctx.ptr, model.ptr) + }) + return m +} + +// String returns the string representation of the model. +func (m *Model) String() string { + return C.GoString(C.Z3_model_to_string(m.ctx.ptr, m.ptr)) +} + +// NumConsts returns the number of constants in the model. +func (m *Model) NumConsts() uint { + return uint(C.Z3_model_get_num_consts(m.ctx.ptr, m.ptr)) +} + +// NumFuncs returns the number of function interpretations in the model. +func (m *Model) NumFuncs() uint { + return uint(C.Z3_model_get_num_funcs(m.ctx.ptr, m.ptr)) +} + +// GetConstDecl returns the i-th constant declaration in the model. +func (m *Model) GetConstDecl(i uint) *FuncDecl { + return newFuncDecl(m.ctx, C.Z3_model_get_const_decl(m.ctx.ptr, m.ptr, C.uint(i))) +} + +// GetFuncDecl returns the i-th function declaration in the model. +func (m *Model) GetFuncDecl(i uint) *FuncDecl { + return newFuncDecl(m.ctx, C.Z3_model_get_func_decl(m.ctx.ptr, m.ptr, C.uint(i))) +} + +// Eval evaluates an expression in the model. +// If modelCompletion is true, Z3 will assign an interpretation for uninterpreted constants. +func (m *Model) Eval(expr *Expr, modelCompletion bool) (*Expr, bool) { + var result C.Z3_ast + var completion C.bool + if modelCompletion { + completion = C.bool(true) + } else { + completion = C.bool(false) + } + success := C.Z3_model_eval(m.ctx.ptr, m.ptr, expr.ptr, completion, &result) + if success == C.bool(false) { + return nil, false + } + return newExpr(m.ctx, result), true +} + +// GetConstInterp returns the interpretation of a constant. +func (m *Model) GetConstInterp(decl *FuncDecl) *Expr { + result := C.Z3_model_get_const_interp(m.ctx.ptr, m.ptr, decl.ptr) + if result == nil { + return nil + } + return newExpr(m.ctx, result) +} + +// FuncInterp represents a function interpretation in a model. +type FuncInterp struct { + ctx *Context + ptr C.Z3_func_interp +} + +// GetFuncInterp returns the interpretation of a function. +func (m *Model) GetFuncInterp(decl *FuncDecl) *FuncInterp { + result := C.Z3_model_get_func_interp(m.ctx.ptr, m.ptr, decl.ptr) + if result == nil { + return nil + } + fi := &FuncInterp{ctx: m.ctx, ptr: result} + C.Z3_func_interp_inc_ref(m.ctx.ptr, result) + runtime.SetFinalizer(fi, func(f *FuncInterp) { + C.Z3_func_interp_dec_ref(f.ctx.ptr, f.ptr) + }) + return fi +} + +// NumEntries returns the number of entries in the function interpretation. +func (fi *FuncInterp) NumEntries() uint { + return uint(C.Z3_func_interp_get_num_entries(fi.ctx.ptr, fi.ptr)) +} + +// GetElse returns the else value of the function interpretation. +func (fi *FuncInterp) GetElse() *Expr { + result := C.Z3_func_interp_get_else(fi.ctx.ptr, fi.ptr) + return newExpr(fi.ctx, result) +} + +// GetArity returns the arity of the function interpretation. +func (fi *FuncInterp) GetArity() uint { + return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr)) +} diff --git a/src/api/go/tactic.go b/src/api/go/tactic.go new file mode 100644 index 000000000..167850146 --- /dev/null +++ b/src/api/go/tactic.go @@ -0,0 +1,294 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +import "C" +import ( + "runtime" + "unsafe" +) + +// Tactic represents a Z3 tactic for transforming goals. +type Tactic struct { + ctx *Context + ptr C.Z3_tactic +} + +// newTactic creates a new Tactic and manages its reference count. +func newTactic(ctx *Context, ptr C.Z3_tactic) *Tactic { + t := &Tactic{ctx: ctx, ptr: ptr} + C.Z3_tactic_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(t, func(tactic *Tactic) { + C.Z3_tactic_dec_ref(tactic.ctx.ptr, tactic.ptr) + }) + return t +} + +// MkTactic creates a tactic with the given name. +func (c *Context) MkTactic(name string) *Tactic { + cName := C.CString(name) + defer C.free(unsafe.Pointer(cName)) + return newTactic(c, C.Z3_mk_tactic(c.ptr, cName)) +} + +// Apply applies the tactic to a goal. +func (t *Tactic) Apply(g *Goal) *ApplyResult { + return newApplyResult(t.ctx, C.Z3_tactic_apply(t.ctx.ptr, t.ptr, g.ptr)) +} + +// GetHelp returns help information for the tactic. +func (t *Tactic) GetHelp() string { + return C.GoString(C.Z3_tactic_get_help(t.ctx.ptr, t.ptr)) +} + +// AndThen creates a tactic that applies t1 and then t2. +func (t *Tactic) AndThen(t2 *Tactic) *Tactic { + return newTactic(t.ctx, C.Z3_tactic_and_then(t.ctx.ptr, t.ptr, t2.ptr)) +} + +// OrElse creates a tactic that applies t1, and if it fails, applies t2. +func (t *Tactic) OrElse(t2 *Tactic) *Tactic { + return newTactic(t.ctx, C.Z3_tactic_or_else(t.ctx.ptr, t.ptr, t2.ptr)) +} + +// Repeat creates a tactic that applies t repeatedly (at most max times). +func (t *Tactic) Repeat(max uint) *Tactic { + return newTactic(t.ctx, C.Z3_tactic_repeat(t.ctx.ptr, t.ptr, C.uint(max))) +} + +// When creates a conditional tactic that applies t only if probe p evaluates to true. +func (c *Context) TacticWhen(p *Probe, t *Tactic) *Tactic { + return newTactic(c, C.Z3_tactic_when(c.ptr, p.ptr, t.ptr)) +} + +// TacticCond creates a conditional tactic: if p then t1 else t2. +func (c *Context) TacticCond(p *Probe, t1, t2 *Tactic) *Tactic { + return newTactic(c, C.Z3_tactic_cond(c.ptr, p.ptr, t1.ptr, t2.ptr)) +} + +// TacticFail creates a tactic that always fails. +func (c *Context) TacticFail() *Tactic { + return newTactic(c, C.Z3_tactic_fail(c.ptr)) +} + +// TacticSkip creates a tactic that always succeeds. +func (c *Context) TacticSkip() *Tactic { + return newTactic(c, C.Z3_tactic_skip(c.ptr)) +} + +// Goal represents a set of formulas that can be solved or transformed. +type Goal struct { + ctx *Context + ptr C.Z3_goal +} + +// newGoal creates a new Goal and manages its reference count. +func newGoal(ctx *Context, ptr C.Z3_goal) *Goal { + g := &Goal{ctx: ctx, ptr: ptr} + C.Z3_goal_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(g, func(goal *Goal) { + C.Z3_goal_dec_ref(goal.ctx.ptr, goal.ptr) + }) + return g +} + +// MkGoal creates a new goal. +func (c *Context) MkGoal(models, unsatCores, proofs bool) *Goal { + return newGoal(c, C.Z3_mk_goal(c.ptr, C.bool(models), C.bool(unsatCores), C.bool(proofs))) +} + +// Assert adds a constraint to the goal. +func (g *Goal) Assert(constraint *Expr) { + C.Z3_goal_assert(g.ctx.ptr, g.ptr, constraint.ptr) +} + +// Size returns the number of formulas in the goal. +func (g *Goal) Size() uint { + return uint(C.Z3_goal_size(g.ctx.ptr, g.ptr)) +} + +// Formula returns the i-th formula in the goal. +func (g *Goal) Formula(i uint) *Expr { + return newExpr(g.ctx, C.Z3_goal_formula(g.ctx.ptr, g.ptr, C.uint(i))) +} + +// NumExprs returns the number of expressions in the goal. +func (g *Goal) NumExprs() uint { + return uint(C.Z3_goal_num_exprs(g.ctx.ptr, g.ptr)) +} + +// IsDecidedSat returns true if the goal is decided to be satisfiable. +func (g *Goal) IsDecidedSat() bool { + return bool(C.Z3_goal_is_decided_sat(g.ctx.ptr, g.ptr)) +} + +// IsDecidedUnsat returns true if the goal is decided to be unsatisfiable. +func (g *Goal) IsDecidedUnsat() bool { + return bool(C.Z3_goal_is_decided_unsat(g.ctx.ptr, g.ptr)) +} + +// Reset removes all formulas from the goal. +func (g *Goal) Reset() { + C.Z3_goal_reset(g.ctx.ptr, g.ptr) +} + +// String returns the string representation of the goal. +func (g *Goal) String() string { + return C.GoString(C.Z3_goal_to_string(g.ctx.ptr, g.ptr)) +} + +// ApplyResult represents the result of applying a tactic to a goal. +type ApplyResult struct { + ctx *Context + ptr C.Z3_apply_result +} + +// newApplyResult creates a new ApplyResult and manages its reference count. +func newApplyResult(ctx *Context, ptr C.Z3_apply_result) *ApplyResult { + ar := &ApplyResult{ctx: ctx, ptr: ptr} + C.Z3_apply_result_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(ar, func(result *ApplyResult) { + C.Z3_apply_result_dec_ref(result.ctx.ptr, result.ptr) + }) + return ar +} + +// NumSubgoals returns the number of subgoals in the result. +func (ar *ApplyResult) NumSubgoals() uint { + return uint(C.Z3_apply_result_get_num_subgoals(ar.ctx.ptr, ar.ptr)) +} + +// Subgoal returns the i-th subgoal. +func (ar *ApplyResult) Subgoal(i uint) *Goal { + return newGoal(ar.ctx, C.Z3_apply_result_get_subgoal(ar.ctx.ptr, ar.ptr, C.uint(i))) +} + +// String returns the string representation of the apply result. +func (ar *ApplyResult) String() string { + return C.GoString(C.Z3_apply_result_to_string(ar.ctx.ptr, ar.ptr)) +} + +// Probe represents a probe for checking properties of goals. +type Probe struct { + ctx *Context + ptr C.Z3_probe +} + +// newProbe creates a new Probe and manages its reference count. +func newProbe(ctx *Context, ptr C.Z3_probe) *Probe { + p := &Probe{ctx: ctx, ptr: ptr} + C.Z3_probe_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(p, func(probe *Probe) { + C.Z3_probe_dec_ref(probe.ctx.ptr, probe.ptr) + }) + return p +} + +// MkProbe creates a probe with the given name. +func (c *Context) MkProbe(name string) *Probe { + cName := C.CString(name) + defer C.free(unsafe.Pointer(cName)) + return newProbe(c, C.Z3_mk_probe(c.ptr, cName)) +} + +// Apply evaluates the probe on a goal. +func (p *Probe) Apply(g *Goal) float64 { + return float64(C.Z3_probe_apply(p.ctx.ptr, p.ptr, g.ptr)) +} + +// ProbeConst creates a probe that always evaluates to the given value. +func (c *Context) ProbeConst(val float64) *Probe { + return newProbe(c, C.Z3_probe_const(c.ptr, C.double(val))) +} + +// ProbeLt creates a probe that evaluates to true if p1 < p2. +func (p *Probe) Lt(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_lt(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeGt creates a probe that evaluates to true if p1 > p2. +func (p *Probe) Gt(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_gt(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeLe creates a probe that evaluates to true if p1 <= p2. +func (p *Probe) Le(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_le(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeGe creates a probe that evaluates to true if p1 >= p2. +func (p *Probe) Ge(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_ge(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeEq creates a probe that evaluates to true if p1 == p2. +func (p *Probe) Eq(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_eq(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeAnd creates a probe that is the conjunction of p1 and p2. +func (p *Probe) And(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_and(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeOr creates a probe that is the disjunction of p1 and p2. +func (p *Probe) Or(p2 *Probe) *Probe { + return newProbe(p.ctx, C.Z3_probe_or(p.ctx.ptr, p.ptr, p2.ptr)) +} + +// ProbeNot creates a probe that is the negation of p. +func (p *Probe) Not() *Probe { + return newProbe(p.ctx, C.Z3_probe_not(p.ctx.ptr, p.ptr)) +} + +// Params represents a parameter set. +type Params struct { + ctx *Context + ptr C.Z3_params +} + +// newParams creates a new Params and manages its reference count. +func newParams(ctx *Context, ptr C.Z3_params) *Params { + params := &Params{ctx: ctx, ptr: ptr} + C.Z3_params_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(params, func(p *Params) { + C.Z3_params_dec_ref(p.ctx.ptr, p.ptr) + }) + return params +} + +// MkParams creates a new parameter set. +func (c *Context) MkParams() *Params { + return newParams(c, C.Z3_mk_params(c.ptr)) +} + +// SetBool sets a Boolean parameter. +func (p *Params) SetBool(key string, value bool) { + sym := p.ctx.MkStringSymbol(key) + C.Z3_params_set_bool(p.ctx.ptr, p.ptr, sym.ptr, C.bool(value)) +} + +// SetUint sets an unsigned integer parameter. +func (p *Params) SetUint(key string, value uint) { + sym := p.ctx.MkStringSymbol(key) + C.Z3_params_set_uint(p.ctx.ptr, p.ptr, sym.ptr, C.uint(value)) +} + +// SetDouble sets a double parameter. +func (p *Params) SetDouble(key string, value float64) { + sym := p.ctx.MkStringSymbol(key) + C.Z3_params_set_double(p.ctx.ptr, p.ptr, sym.ptr, C.double(value)) +} + +// SetSymbol sets a symbol parameter. +func (p *Params) SetSymbol(key string, value *Symbol) { + sym := p.ctx.MkStringSymbol(key) + C.Z3_params_set_symbol(p.ctx.ptr, p.ptr, sym.ptr, value.ptr) +} + +// String returns the string representation of the parameters. +func (p *Params) String() string { + return C.GoString(C.Z3_params_to_string(p.ctx.ptr, p.ptr)) +} diff --git a/src/api/go/z3.go b/src/api/go/z3.go new file mode 100644 index 000000000..810308047 --- /dev/null +++ b/src/api/go/z3.go @@ -0,0 +1,763 @@ +// Package z3 provides Go bindings for the Z3 theorem prover. +// +// Z3 is a high-performance SMT (Satisfiability Modulo Theories) solver +// developed at Microsoft Research. These bindings wrap the Z3 C API using +// CGO and provide idiomatic Go interfaces with automatic memory management. +// +// # Basic Usage +// +// Create a context and solver: +// +// ctx := z3.NewContext() +// solver := ctx.NewSolver() +// +// Create variables and constraints: +// +// x := ctx.MkIntConst("x") +// y := ctx.MkIntConst("y") +// solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ctx.MkInt(10, ctx.MkIntSort()))) +// solver.Assert(ctx.MkGt(x, y)) +// +// Check satisfiability and get model: +// +// if solver.Check() == z3.Satisfiable { +// model := solver.Model() +// xVal, _ := model.Eval(x, true) +// fmt.Println("x =", xVal.String()) +// } +// +// # Memory Management +// +// All Z3 objects are automatically managed using Go finalizers. Reference +// counting is handled transparently - you don't need to manually free objects. +// +// # Supported Features +// +// - Boolean logic, integer and real arithmetic +// - Bit-vectors and floating-point arithmetic +// - Arrays, sequences, and strings +// - Regular expressions +// - Algebraic datatypes +// - Quantifiers and lambda expressions +// - Tactics and goal-based solving +// - Optimization (MaxSMT) +// - Fixedpoint solver (Datalog/CHC) +// +// For more examples, see the examples/go directory in the Z3 repository. +package z3 + +/* +#cgo CFLAGS: -I${SRCDIR}/.. +#cgo LDFLAGS: -lz3 +#include "z3.h" +#include +*/ +import "C" +import ( +"runtime" +"unsafe" +) + +// Config represents a Z3 configuration object. +type Config struct { +ptr C.Z3_config +} + +// NewConfig creates a new Z3 configuration. +func NewConfig() *Config { +cfg := &Config{ptr: C.Z3_mk_config()} +runtime.SetFinalizer(cfg, func(c *Config) { +C.Z3_del_config(c.ptr) +}) +return cfg +} + +// SetParamValue sets a configuration parameter. +func (c *Config) SetParamValue(paramID, paramValue string) { +cParamID := C.CString(paramID) +cParamValue := C.CString(paramValue) +defer C.free(unsafe.Pointer(cParamID)) +defer C.free(unsafe.Pointer(cParamValue)) +C.Z3_set_param_value(c.ptr, cParamID, cParamValue) +} + +// Context represents a Z3 logical context. +type Context struct { +ptr C.Z3_context +} + +// NewContext creates a new Z3 context with default configuration. +func NewContext() *Context { +ctx := &Context{ptr: C.Z3_mk_context_rc(C.Z3_mk_config())} +runtime.SetFinalizer(ctx, func(c *Context) { +C.Z3_del_context(c.ptr) +}) +return ctx +} + +// NewContextWithConfig creates a new Z3 context with the given configuration. +func NewContextWithConfig(cfg *Config) *Context { +ctx := &Context{ptr: C.Z3_mk_context_rc(cfg.ptr)} +runtime.SetFinalizer(ctx, func(c *Context) { +C.Z3_del_context(c.ptr) +}) +return ctx +} + +// SetParam sets a global or context parameter. +func (c *Context) SetParam(key, value string) { +cKey := C.CString(key) +cValue := C.CString(value) +defer C.free(unsafe.Pointer(cKey)) +defer C.free(unsafe.Pointer(cValue)) +C.Z3_update_param_value(c.ptr, cKey, cValue) +} + +// Symbol represents a Z3 symbol. +type Symbol struct { +ctx *Context +ptr C.Z3_symbol +} + +// MkIntSymbol creates an integer symbol. +func (c *Context) MkIntSymbol(i int) *Symbol { +return &Symbol{ +ctx: c, +ptr: C.Z3_mk_int_symbol(c.ptr, C.int(i)), +} +} + +// MkStringSymbol creates a string symbol. +func (c *Context) MkStringSymbol(s string) *Symbol { +cStr := C.CString(s) +defer C.free(unsafe.Pointer(cStr)) +return &Symbol{ +ctx: c, +ptr: C.Z3_mk_string_symbol(c.ptr, cStr), +} +} + +// String returns the string representation of the symbol. +func (s *Symbol) String() string { +kind := C.Z3_get_symbol_kind(s.ctx.ptr, s.ptr) +if kind == C.Z3_INT_SYMBOL { +return string(rune(C.Z3_get_symbol_int(s.ctx.ptr, s.ptr))) +} +return C.GoString(C.Z3_get_symbol_string(s.ctx.ptr, s.ptr)) +} + +// AST represents a Z3 abstract syntax tree node. +type AST struct { +ctx *Context +ptr C.Z3_ast +} + +// incRef increments the reference count of the AST. +func (a *AST) incRef() { +C.Z3_inc_ref(a.ctx.ptr, a.ptr) +} + +// decRef decrements the reference count of the AST. +func (a *AST) decRef() { +C.Z3_dec_ref(a.ctx.ptr, a.ptr) +} + +// String returns the string representation of the AST. +func (a *AST) String() string { +return C.GoString(C.Z3_ast_to_string(a.ctx.ptr, a.ptr)) +} + +// Hash returns the hash code of the AST. +func (a *AST) Hash() uint32 { +return uint32(C.Z3_get_ast_hash(a.ctx.ptr, a.ptr)) +} + +// Equal checks if two ASTs are equal. +func (a *AST) Equal(other *AST) bool { +if a.ctx != other.ctx { +return false +} +return bool(C.Z3_is_eq_ast(a.ctx.ptr, a.ptr, other.ptr)) +} + +// Sort represents a Z3 sort (type). +type Sort struct { +ctx *Context +ptr C.Z3_sort +} + +// newSort creates a new Sort and manages its reference count. +func newSort(ctx *Context, ptr C.Z3_sort) *Sort { +sort := &Sort{ctx: ctx, ptr: ptr} +C.Z3_inc_ref(ctx.ptr, C.Z3_sort_to_ast(ctx.ptr, ptr)) +runtime.SetFinalizer(sort, func(s *Sort) { +C.Z3_dec_ref(s.ctx.ptr, C.Z3_sort_to_ast(s.ctx.ptr, s.ptr)) +}) +return sort +} + +// String returns the string representation of the sort. +func (s *Sort) String() string { +return C.GoString(C.Z3_sort_to_string(s.ctx.ptr, s.ptr)) +} + +// Equal checks if two sorts are equal. +func (s *Sort) Equal(other *Sort) bool { +if s.ctx != other.ctx { +return false +} +return bool(C.Z3_is_eq_sort(s.ctx.ptr, s.ptr, other.ptr)) +} + +// MkBoolSort creates the Boolean sort. +func (c *Context) MkBoolSort() *Sort { +return newSort(c, C.Z3_mk_bool_sort(c.ptr)) +} + +// MkBvSort creates a bit-vector sort of the given size. +func (c *Context) MkBvSort(sz uint) *Sort { +return newSort(c, C.Z3_mk_bv_sort(c.ptr, C.uint(sz))) +} + +// Expr represents a Z3 expression. +type Expr struct { +ctx *Context +ptr C.Z3_ast +} + +// newExpr creates a new Expr and manages its reference count. +func newExpr(ctx *Context, ptr C.Z3_ast) *Expr { +expr := &Expr{ctx: ctx, ptr: ptr} +C.Z3_inc_ref(ctx.ptr, ptr) +runtime.SetFinalizer(expr, func(e *Expr) { +C.Z3_dec_ref(e.ctx.ptr, e.ptr) +}) +return expr +} + +// String returns the string representation of the expression. +func (e *Expr) String() string { +return C.GoString(C.Z3_ast_to_string(e.ctx.ptr, e.ptr)) +} + +// Equal checks if two expressions are equal. +func (e *Expr) Equal(other *Expr) bool { +if e.ctx != other.ctx { +return false +} +return bool(C.Z3_is_eq_ast(e.ctx.ptr, e.ptr, other.ptr)) +} + +// GetSort returns the sort of the expression. +func (e *Expr) GetSort() *Sort { +return newSort(e.ctx, C.Z3_get_sort(e.ctx.ptr, e.ptr)) +} + +// MkTrue creates the Boolean constant true. +func (c *Context) MkTrue() *Expr { +return newExpr(c, C.Z3_mk_true(c.ptr)) +} + +// MkFalse creates the Boolean constant false. +func (c *Context) MkFalse() *Expr { +return newExpr(c, C.Z3_mk_false(c.ptr)) +} + +// MkBool creates a Boolean constant. +func (c *Context) MkBool(value bool) *Expr { +if value { +return c.MkTrue() +} +return c.MkFalse() +} + +// MkNumeral creates a numeral from a string. +func (c *Context) MkNumeral(numeral string, sort *Sort) *Expr { +cStr := C.CString(numeral) +defer C.free(unsafe.Pointer(cStr)) +return newExpr(c, C.Z3_mk_numeral(c.ptr, cStr, sort.ptr)) +} + +// MkConst creates a constant (variable) with the given name and sort. +func (c *Context) MkConst(name *Symbol, sort *Sort) *Expr { +return newExpr(c, C.Z3_mk_const(c.ptr, name.ptr, sort.ptr)) +} + +// MkBoolConst creates a Boolean constant (variable) with the given name. +func (c *Context) MkBoolConst(name string) *Expr { +sym := c.MkStringSymbol(name) +return c.MkConst(sym, c.MkBoolSort()) +} + +// Boolean operations + +// MkAnd creates a conjunction. +func (c *Context) MkAnd(exprs ...*Expr) *Expr { +if len(exprs) == 0 { +return c.MkTrue() +} +if len(exprs) == 1 { +return exprs[0] +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_and(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkOr creates a disjunction. +func (c *Context) MkOr(exprs ...*Expr) *Expr { +if len(exprs) == 0 { +return c.MkFalse() +} +if len(exprs) == 1 { +return exprs[0] +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_or(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// MkNot creates a negation. +func (c *Context) MkNot(expr *Expr) *Expr { +return newExpr(c, C.Z3_mk_not(c.ptr, expr.ptr)) +} + +// MkImplies creates an implication. +func (c *Context) MkImplies(lhs, rhs *Expr) *Expr { +return newExpr(c, C.Z3_mk_implies(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkIff creates a bi-implication (if and only if). +func (c *Context) MkIff(lhs, rhs *Expr) *Expr { +return newExpr(c, C.Z3_mk_iff(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkXor creates exclusive or. +func (c *Context) MkXor(lhs, rhs *Expr) *Expr { +return newExpr(c, C.Z3_mk_xor(c.ptr, lhs.ptr, rhs.ptr)) +} + +if len(exprs) == 1 { +return exprs[0] +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_add(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +if len(exprs) == 1 { +return newExpr(c, C.Z3_mk_unary_minus(c.ptr, exprs[0].ptr)) +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_sub(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +if len(exprs) == 1 { +return exprs[0] +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_mul(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// Comparison operations + +// MkEq creates an equality. +func (c *Context) MkEq(lhs, rhs *Expr) *Expr { +return newExpr(c, C.Z3_mk_eq(c.ptr, lhs.ptr, rhs.ptr)) +} + +// MkDistinct creates a distinct constraint. +func (c *Context) MkDistinct(exprs ...*Expr) *Expr { +if len(exprs) <= 1 { +return c.MkTrue() +} +cExprs := make([]C.Z3_ast, len(exprs)) +for i, e := range exprs { +cExprs[i] = e.ptr +} +return newExpr(c, C.Z3_mk_distinct(c.ptr, C.uint(len(exprs)), &cExprs[0])) +} + +// FuncDecl represents a function declaration. +type FuncDecl struct { +ctx *Context +ptr C.Z3_func_decl +} + +// newFuncDecl creates a new FuncDecl and manages its reference count. +func newFuncDecl(ctx *Context, ptr C.Z3_func_decl) *FuncDecl { +fd := &FuncDecl{ctx: ctx, ptr: ptr} +C.Z3_inc_ref(ctx.ptr, C.Z3_func_decl_to_ast(ctx.ptr, ptr)) +runtime.SetFinalizer(fd, func(f *FuncDecl) { +C.Z3_dec_ref(f.ctx.ptr, C.Z3_func_decl_to_ast(f.ctx.ptr, f.ptr)) +}) +return fd +} + +// String returns the string representation of the function declaration. +func (f *FuncDecl) String() string { +return C.GoString(C.Z3_func_decl_to_string(f.ctx.ptr, f.ptr)) +} + +// GetName returns the name of the function declaration. +func (f *FuncDecl) GetName() *Symbol { +return &Symbol{ +ctx: f.ctx, +ptr: C.Z3_get_decl_name(f.ctx.ptr, f.ptr), +} +} + +// GetArity returns the arity (number of parameters) of the function. +func (f *FuncDecl) GetArity() int { +return int(C.Z3_get_arity(f.ctx.ptr, f.ptr)) +} + +// GetDomain returns the sort of the i-th parameter. +func (f *FuncDecl) GetDomain(i int) *Sort { +return newSort(f.ctx, C.Z3_get_domain(f.ctx.ptr, f.ptr, C.uint(i))) +} + +// GetRange returns the sort of the return value. +func (f *FuncDecl) GetRange() *Sort { +return newSort(f.ctx, C.Z3_get_range(f.ctx.ptr, f.ptr)) +} + +// MkFuncDecl creates a function declaration. +func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl { +cDomain := make([]C.Z3_sort, len(domain)) +for i, s := range domain { +cDomain[i] = s.ptr +} +var domainPtr *C.Z3_sort +if len(domain) > 0 { +domainPtr = &cDomain[0] +} +return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr)) +} + +// MkApp creates a function application. +func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr { +cArgs := make([]C.Z3_ast, len(args)) +for i, a := range args { +cArgs[i] = a.ptr +} +var argsPtr *C.Z3_ast +if len(args) > 0 { +argsPtr = &cArgs[0] +} +return newExpr(c, C.Z3_mk_app(c.ptr, decl.ptr, C.uint(len(args)), argsPtr)) +} + +// Quantifier operations + +// MkForall creates a universal quantifier. +func (c *Context) MkForall(bound []*Expr, body *Expr) *Expr { +cBound := make([]C.Z3_ast, len(bound)) +for i, b := range bound { +cBound[i] = b.ptr +} +var boundPtr *C.Z3_ast +if len(bound) > 0 { +boundPtr = &cBound[0] +} +return newExpr(c, C.Z3_mk_forall_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) +} + +// MkExists creates an existential quantifier. +func (c *Context) MkExists(bound []*Expr, body *Expr) *Expr { +cBound := make([]C.Z3_ast, len(bound)) +for i, b := range bound { +cBound[i] = b.ptr +} +var boundPtr *C.Z3_ast +if len(bound) > 0 { +boundPtr = &cBound[0] +} +return newExpr(c, C.Z3_mk_exists_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) +} + +// Simplify simplifies an expression. +func (e *Expr) Simplify() *Expr { +return newExpr(e.ctx, C.Z3_simplify(e.ctx.ptr, e.ptr)) +} + +// MkTypeVariable creates a type variable sort for use in polymorphic functions and datatypes +func (c *Context) MkTypeVariable(name *Symbol) *Sort { +return newSort(c, C.Z3_mk_type_variable(c.ptr, name.ptr)) +} + +// Quantifier represents a quantified formula (forall or exists) +type Quantifier struct { +ctx *Context +ptr C.Z3_ast +} + +// newQuantifier creates a new Quantifier with proper memory management +func newQuantifier(ctx *Context, ptr C.Z3_ast) *Quantifier { +q := &Quantifier{ctx: ctx, ptr: ptr} +C.Z3_inc_ref(ctx.ptr, ptr) +runtime.SetFinalizer(q, func(qf *Quantifier) { +C.Z3_dec_ref(qf.ctx.ptr, qf.ptr) +}) +return q +} + +// AsExpr converts a Quantifier to an Expr +func (q *Quantifier) AsExpr() *Expr { +return newExpr(q.ctx, q.ptr) +} + +// IsUniversal returns true if this is a universal quantifier (forall) +func (q *Quantifier) IsUniversal() bool { +return C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr) != 0 +} + +// IsExistential returns true if this is an existential quantifier (exists) +func (q *Quantifier) IsExistential() bool { +return C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr) != 0 +} + +// GetWeight returns the weight of the quantifier +func (q *Quantifier) GetWeight() int { +return int(C.Z3_get_quantifier_weight(q.ctx.ptr, q.ptr)) +} + +// GetNumPatterns returns the number of patterns +func (q *Quantifier) GetNumPatterns() int { +return int(C.Z3_get_quantifier_num_patterns(q.ctx.ptr, q.ptr)) +} + +// GetPattern returns the pattern at the given index +func (q *Quantifier) GetPattern(idx int) *Pattern { +ptr := C.Z3_get_quantifier_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx)) +return newPattern(q.ctx, ptr) +} + +// GetNumNoPatterns returns the number of no-patterns +func (q *Quantifier) GetNumNoPatterns() int { +return int(C.Z3_get_quantifier_num_no_patterns(q.ctx.ptr, q.ptr)) +} + +// GetNoPattern returns the no-pattern at the given index +func (q *Quantifier) GetNoPattern(idx int) *Pattern { +ptr := C.Z3_get_quantifier_no_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx)) +return newPattern(q.ctx, ptr) +} + +// GetNumBound returns the number of bound variables +func (q *Quantifier) GetNumBound() int { +return int(C.Z3_get_quantifier_num_bound(q.ctx.ptr, q.ptr)) +} + +// GetBoundName returns the name of the bound variable at the given index +func (q *Quantifier) GetBoundName(idx int) *Symbol { +ptr := C.Z3_get_quantifier_bound_name(q.ctx.ptr, q.ptr, C.uint(idx)) +return newSymbol(q.ctx, ptr) +} + +// GetBoundSort returns the sort of the bound variable at the given index +func (q *Quantifier) GetBoundSort(idx int) *Sort { +ptr := C.Z3_get_quantifier_bound_sort(q.ctx.ptr, q.ptr, C.uint(idx)) +return newSort(q.ctx, ptr) +} + +// GetBody returns the body of the quantifier +func (q *Quantifier) GetBody() *Expr { +ptr := C.Z3_get_quantifier_body(q.ctx.ptr, q.ptr) +return newExpr(q.ctx, ptr) +} + +// String returns the string representation of the quantifier +func (q *Quantifier) String() string { +return q.AsExpr().String() +} + +// MkQuantifier creates a quantifier with patterns +func (c *Context) MkQuantifier(isForall bool, weight int, sorts []*Sort, names []*Symbol, body *Expr, patterns []*Pattern) *Quantifier { +var forallInt C.int +if isForall { +forallInt = 1 +} else { +forallInt = 0 +} + +numBound := len(sorts) +if numBound != len(names) { +panic("Number of sorts must match number of names") +} + +var cSorts []C.Z3_sort +var cNames []C.Z3_symbol +if numBound > 0 { +cSorts = make([]C.Z3_sort, numBound) +cNames = make([]C.Z3_symbol, numBound) +for i := 0; i < numBound; i++ { +cSorts[i] = sorts[i].ptr +cNames[i] = names[i].ptr +} +} + +var cPatterns []C.Z3_pattern +var patternsPtr *C.Z3_pattern +numPatterns := len(patterns) +if numPatterns > 0 { +cPatterns = make([]C.Z3_pattern, numPatterns) +for i := 0; i < numPatterns; i++ { +cPatterns[i] = patterns[i].ptr +} +patternsPtr = &cPatterns[0] +} + +var sortsPtr *C.Z3_sort +var namesPtr *C.Z3_symbol +if numBound > 0 { +sortsPtr = &cSorts[0] +namesPtr = &cNames[0] +} + +ptr := C.Z3_mk_quantifier(c.ptr, forallInt, C.uint(weight), C.uint(numPatterns), patternsPtr, +C.uint(numBound), sortsPtr, namesPtr, body.ptr) +return newQuantifier(c, ptr) +} + +// MkQuantifierConst creates a quantifier using constant bound variables +func (c *Context) MkQuantifierConst(isForall bool, weight int, bound []*Expr, body *Expr, patterns []*Pattern) *Quantifier { +var forallInt C.int +if isForall { +forallInt = 1 +} else { +forallInt = 0 +} + +numBound := len(bound) +var cBound []C.Z3_app +var boundPtr *C.Z3_app +if numBound > 0 { +cBound = make([]C.Z3_app, numBound) +for i := 0; i < numBound; i++ { +cBound[i] = C.Z3_app(bound[i].ptr) +} +boundPtr = &cBound[0] +} + +var cPatterns []C.Z3_pattern +var patternsPtr *C.Z3_pattern +numPatterns := len(patterns) +if numPatterns > 0 { +cPatterns = make([]C.Z3_pattern, numPatterns) +for i := 0; i < numPatterns; i++ { +cPatterns[i] = patterns[i].ptr +} +patternsPtr = &cPatterns[0] +} + +ptr := C.Z3_mk_quantifier_const(c.ptr, forallInt, C.uint(weight), C.uint(numBound), boundPtr, +C.uint(numPatterns), patternsPtr, body.ptr) +return newQuantifier(c, ptr) +} + +// Lambda represents a lambda expression +type Lambda struct { +ctx *Context +ptr C.Z3_ast +} + +// newLambda creates a new Lambda with proper memory management +func newLambda(ctx *Context, ptr C.Z3_ast) *Lambda { +l := &Lambda{ctx: ctx, ptr: ptr} +C.Z3_inc_ref(ctx.ptr, ptr) +runtime.SetFinalizer(l, func(lam *Lambda) { +C.Z3_dec_ref(lam.ctx.ptr, lam.ptr) +}) +return l +} + +// AsExpr converts a Lambda to an Expr +func (l *Lambda) AsExpr() *Expr { +return newExpr(l.ctx, l.ptr) +} + +// GetNumBound returns the number of bound variables +func (l *Lambda) GetNumBound() int { +return int(C.Z3_get_quantifier_num_bound(l.ctx.ptr, l.ptr)) +} + +// GetBoundName returns the name of the bound variable at the given index +func (l *Lambda) GetBoundName(idx int) *Symbol { +ptr := C.Z3_get_quantifier_bound_name(l.ctx.ptr, l.ptr, C.uint(idx)) +return newSymbol(l.ctx, ptr) +} + +// GetBoundSort returns the sort of the bound variable at the given index +func (l *Lambda) GetBoundSort(idx int) *Sort { +ptr := C.Z3_get_quantifier_bound_sort(l.ctx.ptr, l.ptr, C.uint(idx)) +return newSort(l.ctx, ptr) +} + +// GetBody returns the body of the lambda expression +func (l *Lambda) GetBody() *Expr { +ptr := C.Z3_get_quantifier_body(l.ctx.ptr, l.ptr) +return newExpr(l.ctx, ptr) +} + +// String returns the string representation of the lambda +func (l *Lambda) String() string { +return l.AsExpr().String() +} + +// MkLambda creates a lambda expression with sorts and names +func (c *Context) MkLambda(sorts []*Sort, names []*Symbol, body *Expr) *Lambda { +numBound := len(sorts) +if numBound != len(names) { +panic("Number of sorts must match number of names") +} + +var cSorts []C.Z3_sort +var cNames []C.Z3_symbol +var sortsPtr *C.Z3_sort +var namesPtr *C.Z3_symbol + +if numBound > 0 { +cSorts = make([]C.Z3_sort, numBound) +cNames = make([]C.Z3_symbol, numBound) +for i := 0; i < numBound; i++ { +cSorts[i] = sorts[i].ptr +cNames[i] = names[i].ptr +} +sortsPtr = &cSorts[0] +namesPtr = &cNames[0] +} + +ptr := C.Z3_mk_lambda(c.ptr, C.uint(numBound), sortsPtr, namesPtr, body.ptr) +return newLambda(c, ptr) +} + +// MkLambdaConst creates a lambda expression using constant bound variables +func (c *Context) MkLambdaConst(bound []*Expr, body *Expr) *Lambda { +numBound := len(bound) +var cBound []C.Z3_app +var boundPtr *C.Z3_app + +if numBound > 0 { +cBound = make([]C.Z3_app, numBound) +for i := 0; i < numBound; i++ { +cBound[i] = C.Z3_app(bound[i].ptr) +} +boundPtr = &cBound[0] +} + +ptr := C.Z3_mk_lambda_const(c.ptr, C.uint(numBound), boundPtr, body.ptr) +return newLambda(c, ptr) +}