Z3 Theorem Prover

https://github.com/z3prover/z3
Admin
The Z3 Theorem Prover
Tokens:90,360
Snippets:962
Trust Score:6.9
License:MIT
Update:1 month ago
Show doc for...
Tokens:
Raw
### Run Z3 Go Examples

Source: https://github.com/z3prover/z3/blob/master/doc/test_go_doc/README.html

Environment setup and execution commands for running Go examples on Linux/Mac and Windows.

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

--------------------------------

### Install Z3 OCaml Bindings

Source: https://github.com/z3prover/z3/blob/master/src/api/ml/README.md

Commands to build and install the Z3 OCaml artifacts.

```bash
ocamlfind install z3 build/api/ml/* build/libz3-static.a
```

```bash
python2.7 scripts/mk_make.py --ml --staticlib
make -C build
```

--------------------------------

### Install and Verify a3-python

Source: https://github.com/z3prover/z3/blob/master/a3/a3-python.md

Install the tool via pip and verify the installation using the command line.

```bash
pip install a3-python
```

```bash
a3 --version || python -m a3 --version || echo "a3 command not found in PATH"
```

--------------------------------

### Configure Z3 build with custom Python path

Source: https://github.com/z3prover/z3/blob/master/README.md

Example of using mk_make.py to specify a custom installation prefix and Python package directory.

```bash
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages
```

--------------------------------

### Install Go source files

Source: https://github.com/z3prover/z3/blob/master/src/api/go/CMakeLists.txt

Installs the necessary Go source files and configuration to the specified library directory.

```cmake
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"
    )
```

--------------------------------

### Configuring Environment for Z3 Go Examples

Source: https://github.com/z3prover/z3/blob/master/src/api/go/README.md

Sets the necessary library paths and CGO flags for Linux, macOS, and Windows before running Go 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
```

--------------------------------

### Install Z3 using vcpkg

Source: https://github.com/z3prover/z3/blob/master/README.md

Commands to clone the vcpkg repository, bootstrap the tool, and install the Z3 package.

```bash
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3
```

--------------------------------

### Basic Z3 Go Usage Example

Source: https://github.com/z3prover/z3/blob/master/doc/test_go_doc/README.html

A simple example demonstrating how to create a context, define variables, assert constraints, and solve for a model.

```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())
		}
	}
}
```

--------------------------------

### Install pkg-config file

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Installs the generated z3.pc file to the designated package configuration directory.

```cmake
install(
  FILES "${PROJECT_BINARY_DIR}/z3.pc"
  DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}"
)
```

--------------------------------

### Configure Z3 Installation Paths

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Sets up installation directories for pkgconfig and CMake package files using GNUInstallDirs.

```cmake
include(GNUInstallDirs)
set(CMAKE_INSTALL_PKGCONFIGDIR
  "${CMAKE_INSTALL_LIBDIR}/pkgconfig"
  CACHE
  PATH
  "Directory to install pkgconfig files"
)

set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR
  "${CMAKE_INSTALL_LIBDIR}/cmake/z3"
  CACHE
  PATH
  "Directory to install Z3 CMake package files"
)
message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"")
message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"")
message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"")
```

--------------------------------

### Install Z3 to a custom prefix

Source: https://github.com/z3prover/z3/blob/master/README.md

Configures the installation path for Z3 binaries and libraries.

```bash
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install
```

--------------------------------

### Configure OCaml Bindings Installation

Source: https://github.com/z3prover/z3/blob/master/src/api/ml/CMakeLists.txt

Sets installation directories for OCaml packages and stubs, and defines the list of files to be installed.

```cmake
option(Z3_INSTALL_OCAML_BINDINGS "Install OCaml bindings when invoking install target" ON)
if (Z3_INSTALL_OCAML_BINDINGS)
  if (NOT Z3_OCAML_PACKAGE_INSTALLDIR)
    set(Z3_OCAML_PACKAGE_INSTALLDIR
      "${CMAKE_INSTALL_LIBDIR}/ocaml/z3"
      CACHE
      PATH
      "Directory to install Z3 OCaml package files relative to install prefix"
    )
  endif()

  if (NOT Z3_OCAML_STUB_INSTALLDIR)
    set(Z3_OCAML_STUB_INSTALLDIR
      "${CMAKE_INSTALL_LIBDIR}/ocaml/stublibs"
      CACHE
      PATH
      "Directory to install Z3 OCaml stub libraries relative to install prefix"
    )
  endif()

  set(z3_ocaml_package_install_files
    "${META_OUTPUT_FILE}"
    "${z3ml_bin}/z3.cmi"
    "${z3ml_src}/z3.mli"
    "${z3ml_bin}/z3.cmx"
    "${z3ml_bin}/z3enums.cmi"
    "${z3ml_bin}/z3enums.cmx"
    "${z3ml_bin}/z3enums.mli"
    "${z3ml_bin}/z3native.cmi"
    "${z3ml_bin}/z3native.cmx"
    "${z3ml_bin}/z3native.mli"
    "${z3ml_bin}/libz3ml.a"
    "${z3ml_bin}/z3ml.a"
    "${z3ml_bin}/z3ml.cma"
    "${z3ml_bin}/z3ml.cmxa"
    "${z3ml_bin}/z3ml.cmxs"
  )

  install(
    FILES ${z3_ocaml_package_install_files}
    DESTINATION "${Z3_OCAML_PACKAGE_INSTALLDIR}"
  )

  install(
    FILES "${z3ml_bin}/dllz3ml.so"
    DESTINATION "${Z3_OCAML_STUB_INSTALLDIR}"
  )
```

--------------------------------

### Build and Run Z3 Go Examples on Windows

Source: https://github.com/z3prover/z3/blob/master/examples/go/README.md

Commands to build the Z3 library and configure environment variables for running Go examples on 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
```

--------------------------------

### Configure Installation of Julia Bindings

Source: https://github.com/z3prover/z3/blob/master/src/api/julia/CMakeLists.txt

Sets up the installation rules for the z3jl library if enabled.

```cmake
option(Z3_INSTALL_JULIA_BINDINGS "Install Julia bindings when invoking install target" ON)
if(Z3_INSTALL_JULIA_BINDINGS)
    install(TARGETS z3jl
        LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
        ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}"
        RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}"
    )
endif()
```

--------------------------------

### Build and Run Z3 Go Examples on Linux/macOS

Source: https://github.com/z3prover/z3/blob/master/examples/go/README.md

Commands to build the Z3 library and configure environment variables for running Go examples on Unix-like systems.

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

--------------------------------

### Install Z3 Python wrapper

Source: https://github.com/z3prover/z3/blob/master/README.md

Command to install the Z3 Python solver package from PyPI.

```bash
pip install z3-solver
```

--------------------------------

### Configure example targets

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Conditionally enables the build of Z3 API examples if the project is being built as a top-level project.

```cmake
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
    "Build Z3 api examples" ON
    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
if (Z3_ENABLE_EXAMPLE_TARGETS)
  add_subdirectory(examples)
endif()
```

--------------------------------

### Install and Uninstall Z3

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Standard commands for installing or removing the Z3 build using Make.

```bash
make install
```

```bash
make uninstall
```

--------------------------------

### Install CMake Configuration Files

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Installs the generated Z3Config.cmake and Z3ConfigVersion.cmake files to the package directory.

```cmake
install(
  FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)

install(
  FILES "${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)
```

--------------------------------

### Build Z3 in a Python virtual environment

Source: https://github.com/z3prover/z3/blob/master/README.md

Steps to set up a virtual environment, configure the build, compile, and verify the installation.

```bash
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...
```

--------------------------------

### Build Z3 with make on Linux/macOS

Source: https://github.com/z3prover/z3/blob/master/README.md

Standard sequence to configure, build, and install Z3 using make.

```bash
python scripts/mk_make.py
cd build
make
sudo make install
```

--------------------------------

### Copy Python Examples to Build Directory

Source: https://github.com/z3prover/z3/blob/master/examples/python/CMakeLists.txt

Iterates through the example files and creates custom commands to copy them to the build destination, flattening the directory structure.

```cmake
set(build_z3_python_examples_target_depends "")
foreach (example_file ${python_example_files})
  get_filename_component(example_file_name "${example_file}" NAME)
  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${example_file_name}"
    COMMAND "${CMAKE_COMMAND}" "-E" "copy"
      "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
      # We flatten the hierarchy so that all python files have
      # the `z3` directory in their directory so that their import
      # statements "just work".
      "${z3py_bindings_build_dest}/${example_file_name}"
    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
    COMMENT "Copying \"${example_file}\" to ${z3py_bindings_build_dest}/${example_file_name}"
  )
  list(APPEND build_z3_python_examples_target_depends "${z3py_bindings_build_dest}/${example_file_name}")
endforeach()
```

--------------------------------

### Initialize Z3 with Custom File Location

Source: https://github.com/z3prover/z3/blob/master/src/api/js/PUBLISHED_README.md

Initialization example for Deno using locateFile to resolve the WASM path.

```typescript
import { init } from 'npm:z3-solver';

const api = await init({
  locateFile: (file, _prefix): string =>
    import.meta.resolve(`npm:z3-solver/build/${file}`), // _prefix is unused here
});
```

--------------------------------

### New Match Log Example

Source: https://github.com/z3prover/z3/wiki/Equality-Explanation-Logging

Example of a log entry generated when a quantifier trigger is matched.

```text
[new-match] 0x7f9eb587d440 #166 #165 #476 ; #419 (#418 #477)
```

--------------------------------

### Verify Z3 installation with a test program

Source: https://github.com/z3prover/z3/blob/master/doc/JAVA_IDE_SETUP.md

A simple Java program to initialize a Z3 context, check a basic constraint, and print the version.

```java
import com.microsoft.z3.*;

public class Z3Test {
    public static void main(String[] args) {
        System.out.println("Creating Z3 context...");
        Context ctx = new Context();
        System.out.println("Z3 version: " + Version.getFullVersion());
        
        // Simple example: x > 0
        IntExpr x = ctx.mkIntConst("x");
        Solver solver = ctx.mkSolver();
        solver.add(ctx.mkGt(x, ctx.mkInt(0)));
        
        if (solver.check() == Status.SATISFIABLE) {
            System.out.println("SAT");
            System.out.println("Model: " + solver.getModel());
        }
        
        ctx.close();
        System.out.println("Success!");
    }
}
```

--------------------------------

### Theory Solver Equality Log Example

Source: https://github.com/z3prover/z3/wiki/Equality-Explanation-Logging

Example of an equality added by a theory solver.

```text
[eq-expl] #1 th arith ; #2
```

--------------------------------

### Broken archive creation example

Source: https://github.com/z3prover/z3/blob/master/src/api/ml/README.md

An example of an unsupported archive creation command that includes a static library within another archive.

```bash
ar rcs api/ml/libz3ml.a libz3-static.a api/ml/z3native_stubs.o
```

--------------------------------

### Conditionally Add Binding Examples

Source: https://github.com/z3prover/z3/blob/master/examples/CMakeLists.txt

Adds subdirectories for Python and .NET examples if the respective bindings are enabled.

```cmake
if (Z3_BUILD_PYTHON_BINDINGS)
  add_subdirectory(python)
endif()

if (Z3_BUILD_DOTNET_BINDINGS)
    add_subdirectory(dotnet)
endif()
```

--------------------------------

### Refined Installation Checker

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

An advanced implementation supporting single dependencies and multi-argument conflicts, with a solver function to extract the installation model.

```python
def DependsOn(pack, deps):
    if is_expr(deps):
        return Implies(pack, deps)
    else:
        return And([ Implies(pack, dep) for dep in deps ])

def Conflict(*packs):
    return Or([ Not(pack) for pack in packs ])

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

def install_check(*problem):
    s = Solver()
    s.add(*problem)
    if s.check() == sat:
        m = s.model()
        r = []
        for x in m:
            if is_true(m[x]):
                # x is a Z3 declaration
                # x() returns the Z3 expression
                # x.name() returns a string
                r.append(x())
        print r
    else:
        print "invalid installation profile"

print "Check 1"
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z)

print "Check 2"
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z, g)
```

--------------------------------

### Set Initial Values in SMTLIB2

Source: https://github.com/z3prover/z3/blob/master/RELEASE_NOTES.md

Demonstrates how to provide initial values for variables in the solver context to guide the search process.

```smtlib2
(declare-const x Int)
(set-initial-value x 10)
(push)
(assert (> x 0))
(check-sat)
(get-model)
```

--------------------------------

### Configure C and C++ External Projects

Source: https://github.com/z3prover/z3/blob/master/examples/CMakeLists.txt

Sets up build arguments for C and C++ example projects, including handling for linker workarounds and build types.

```cmake
include(ExternalProject)

option(Z3_C_EXAMPLES_FORCE_CXX_LINKER
  "Force C++ linker when building C example projects" OFF)

if (Z3_C_EXAMPLES_FORCE_CXX_LINKER)
  # HACK: This is a workaround for UBSan.
  message(STATUS "Forcing C++ linker to be used when building example C projects")
  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG
    "-DFORCE_CXX_LINKER=ON"
  )
else()
  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "")
endif()

if (DEFINED CMAKE_CONFIGURATION_TYPES)
  message(WARNING
    "Cannot set built type of external project when building with a "
    "multi-configuration generator")
  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG "")
else()
  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG
    "-DCMAKE_BUILD_TYPE:STRING=${CMAKE_BUILD_TYPE}"
  )
endif()
```

--------------------------------

### Configure OCaml example execution

Source: https://github.com/z3prover/z3/blob/master/src/api/ml/CMakeLists.txt

Defines custom commands to compile and run OCaml bytecode and native examples after the bindings are built.

```cmake
add_custom_command(
  TARGET build_z3_ocaml_bindings POST_BUILD
  COMMAND "${OCAMLFIND}" ocamlc
    -cclib "${libz3_path}/libz3${so_ext}"
    -o "${z3ml_bin}/ml_example.byte"
    -package zarith
    -linkpkg
    -I "${z3ml_bin}"
    -dllpath "${z3ml_bin}"
    "${z3ml_bin}/z3ml.cma"
    "${z3ml_example_src}"
  COMMAND env DYLD_LIBRARY_PATH=${PROJECT_BINARY_DIR} ocamlrun ${z3ml_bin}/ml_example.byte > ${z3ml_bin}/ml_example.bc.log
  COMMENT "Run OCaml bytecode example"
  VERBATIM
)
```

```cmake
add_custom_command(
  TARGET build_z3_ocaml_bindings POST_BUILD
  COMMAND "${OCAMLFIND}" ocamlopt
    -cclib "${libz3_path}/libz3${so_ext}"
    -o "${z3ml_bin}/ml_example"
    -package zarith
    -linkpkg
    -I "${z3ml_bin}"
    "${z3ml_bin}/z3ml.cmxa"
    "${z3ml_example_src}"
  COMMAND env DYLD_LIBRARY_PATH=${PROJECT_BINARY_DIR} ${z3ml_bin}/ml_example > ${z3ml_bin}/ml_example.log
  COMMENT "Run OCaml native example"
  VERBATIM
)
```

--------------------------------

### Define and install public headers

Source: https://github.com/z3prover/z3/blob/master/src/CMakeLists.txt

Sets the public header properties for libz3 and defines installation paths for the library and its headers.

```cmake
set (libz3_public_headers
  z3_algebraic.h
  z3_api.h
  z3_ast_containers.h
  z3_fixedpoint.h
  z3_fpa.h
  z3.h
  c++/z3++.h
  z3_macros.h
  z3_optimization.h
  z3_polynomial.h
  z3_rcf.h
  z3_v1.h
  z3_spacer.h
)
foreach (header ${libz3_public_headers})
  set_property(TARGET libz3 APPEND PROPERTY
    PUBLIC_HEADER "${PROJECT_SOURCE_DIR}/src/api/${header}")
endforeach()
set_property(TARGET libz3 APPEND PROPERTY
    PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/z3_version.h")

install(TARGETS libz3
  EXPORT Z3_EXPORTED_TARGETS
  LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
  ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
  RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}" # For Windows. DLLs are runtime targets for CMake
  PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
)
```

--------------------------------

### Define Python Example Files and Build Destination

Source: https://github.com/z3prover/z3/blob/master/examples/python/CMakeLists.txt

Sets the list of Python source files and the target directory for the build process.

```cmake
set(python_example_files
  all_interval_series.py
  complex/complex.py
  example.py
  hamiltonian/hamiltonian.py
  mus/marco.py
  mus/mss.py
  socrates.py
  visitor.py
)

set(z3py_bindings_build_dest "${PROJECT_BINARY_DIR}/python")
```

--------------------------------

### Solve Basic Installation Problem

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

Uses Z3Py to solve a set of dependency and conflict constraints for a group of packages.

```python
def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

solve(DependsOn(a, [b, c, z]),
      DependsOn(b, [d]),
      DependsOn(c, [Or(d, e), Or(f, g)]),
      Conflict(d, e),
      a, z)
```

--------------------------------

### Implement Z3 FetchContent fallback

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Attempt to find a system Z3 installation, falling back to FetchContent if not found or if the version is insufficient.

```cmake
set(Z3_MIN_VERSION "4.15.3")

# First, try to find Z3 on the system
find_package(Z3 ${Z3_MIN_VERSION} CONFIG QUIET)

if(Z3_FOUND)
    message(STATUS "Found system Z3 version ${Z3_VERSION_STRING}")
    # Z3_LIBRARIES will contain z3::libz3
else()
    message(STATUS "System Z3 not found or version too old, fetching Z3 ${Z3_MIN_VERSION}")
    
    # Fallback to FetchContent
    include(FetchContent)
    FetchContent_Declare(Z3
        GIT_REPOSITORY https://github.com/Z3Prover/z3
        GIT_TAG        z3-${Z3_MIN_VERSION}
    )
    FetchContent_MakeAvailable(Z3)
    
    # Add the C++ API include directory for z3++.h
    if(TARGET libz3)
        target_include_directories(libz3 INTERFACE
            $<BUILD_INTERFACE:${z3_SOURCE_DIR}/src/api/c++>
        )
    endif()
    
    # Create an alias to match the system install target name
    if(NOT TARGET z3::libz3)
        add_library(z3::libz3 ALIAS libz3)
    endif()
endif()

# Now use Z3 consistently regardless of how it was found
target_link_libraries(yourTarget PRIVATE z3::libz3)
```

--------------------------------

### View Debug Trace Output

Source: https://github.com/z3prover/z3/blob/master/Z3-AGENT.md

Example output showing the internal execution flow and Z3 solver results.

```text
[DEBUG] started run 31 (skill=solve, hash=d64beb5a61842362)
[DEBUG] found z3: build/release/z3
[DEBUG] cmd: build/release/z3 -in
[DEBUG] stdin:
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)
[DEBUG] exit_code=0 duration=28ms
[DEBUG] stdout:
sat
(
  (define-fun x () Int
    1)
  (define-fun y () Int
    1)
)
[DEBUG] finished run 31: sat (28ms)
sat
  x = 1
  y = 1
```

--------------------------------

### Matching Loop Example

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/advanced-examples.htm

Shows a pattern that can lead to infinite instantiation chains, known as a matching loop.

```python
ForAll([x, y], Implies(subtype(x, y),
                       subtype(array_of(x), array_of(y))),
       patterns=[subtype(x, y)])
```

--------------------------------

### Validate and Install Python Bindings

Source: https://github.com/z3prover/z3/blob/master/src/api/python/CMakeLists.txt

Checks if the Python package directory is within the install prefix and defines the installation destination for Z3 bindings.

```cmake
if (IS_ABSOLUTE "${CMAKE_INSTALL_PYTHON_PKG_DIR}")
    string(FIND "${CMAKE_INSTALL_PYTHON_PKG_DIR}" "${CMAKE_INSTALL_PREFIX}" position)
    if (NOT ("${position}" EQUAL 0))
      message(WARNING "The directory to install the python bindings \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\" "
              "is not under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
              " Running the install target may lead to a broken installation. "
              "To change the install directory modify the CMAKE_INSTALL_PYTHON_PKG_DIR cache variable."
              )
    endif()
  endif()
  # Using DESTDIR still seems to work even if we use an absolute path
  message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
  install(FILES ${build_z3_python_bindings_target_depends}
    DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
  )
else()
  message(STATUS "Not emitting rules to install Z3 python bindings")
endif()
```

--------------------------------

### Configure Z3 with CMake options

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Example command to configure a Z3 build with specific CMake flags using the -D option.

```bash
cmake -DCMAKE_BUILD_TYPE=Release -DZ3_ENABLE_TRACING_FOR_NON_DEBUG=FALSE ../
```

--------------------------------

### Basic Z3 Constraint Solving in Go

Source: https://github.com/z3prover/z3/blob/master/src/api/go/README.md

Demonstrates creating a context, defining integer variables, asserting constraints, and checking for satisfiability.

```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())
        }
    }
}
```

--------------------------------

### Literal Equality Log Example

Source: https://github.com/z3prover/z3/wiki/Equality-Explanation-Logging

Example of an equality provided directly to Z3.

```text
[mk-app] #3 = #1 #2
[eq-expl] #1 lit #3 ; #2
```

--------------------------------

### Build Python bindings with pre-installed libz3

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Builds only the Python bindings against an existing libz3 installation to save time when targeting multiple Python versions.

```bash
# First, build and install libz3 (once)
mkdir build-libz3
cd build-libz3
cmake -DZ3_BUILD_LIBZ3_SHARED=ON -DCMAKE_INSTALL_PREFIX=/path/to/prefix ../
make
make install

# Then, build Python bindings for each Python version (quickly, without rebuilding libz3)
cd ..
mkdir build-py310
cd build-py310
cmake -DZ3_BUILD_LIBZ3_CORE=OFF \
      -DZ3_BUILD_PYTHON_BINDINGS=ON \
      -DCMAKE_INSTALL_PREFIX=/path/to/prefix \
      -DPython3_EXECUTABLE=/path/to/python3.10 ../
make
make install
```

--------------------------------

### Configure Z3 Project and Executable

Source: https://github.com/z3prover/z3/blob/master/examples/userPropagator/CMakeLists.txt

Initializes the project, finds the Z3 package, and sets up the executable with necessary source files and include directories.

```cmake
project(Z3_USER_PROPAGATOR_EXAMPLE CXX)
cmake_minimum_required(VERSION 3.4)
find_package(Z3
  REQUIRED
  CONFIG
  # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
  # This should prevent us from accidentally picking up an installed
  # copy of Z3. This is here to benefit Z3's build system when building
  # this project. When making your own project you probably shouldn't
  # use this option.
  NO_DEFAULT_PATH
)

################################################################################
# Z3 C++ API bindings require C++11, but this code needs later.
################################################################################
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_STANDARD_REQUIRED ON)

message(STATUS "Z3_FOUND: ${Z3_FOUND}")
message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
message(STATUS "Z3_DIR: ${Z3_DIR}")

add_executable(user_propagator_example
        example.cpp
        common.h
        user_propagator.h
        user_propagator_with_theory.h
        user_propagator_subquery_maximisation.h
        user_propagator_internal_maximisation.h
        user_propagator_created_maximisation.h)

target_include_directories(user_propagator_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
target_link_libraries(user_propagator_example PRIVATE ${Z3_LIBRARIES})
```

--------------------------------

### Root Equality Log Example

Source: https://github.com/z3prover/z3/wiki/Equality-Explanation-Logging

Example of a term identified as the root of its equivalence class.

```text
[eq-expl] #1 root
```

--------------------------------

### Configure 64-bit Z3 build on Windows

Source: https://github.com/z3prover/z3/blob/master/README.md

Initializes the build environment for a 64-bit configuration on Windows using the -x flag.

```bash
python scripts/mk_make.py -x
```

--------------------------------

### Perform Staged Installs

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Commands for installing or uninstalling Z3 into a specific directory using DESTDIR.

```bash
mkdir staged
make install DESTDIR=/full/path/to/staged/
```

```bash
make uninstall DESTDIR=/full/path/to/staged
```

--------------------------------

### Configure 32-bit Z3 build on Windows

Source: https://github.com/z3prover/z3/blob/master/README.md

Initializes the build environment for a 32-bit configuration on Windows.

```bash
python scripts/mk_make.py
```

--------------------------------

### Initialize Z3 Context and Solve Constraints

Source: https://github.com/z3prover/z3/blob/master/src/api/js/PUBLISHED_README.md

Demonstrates initializing the Z3 context and using a solver to check a simple integer constraint.

```javascript
const { init } = require('z3-solver');
const { Context } = await init();
const { Solver, Int, And } = new Context('main');

const x = Int.const('x');

const solver = new Solver();
solver.add(And(x.ge(0), x.le(9)));
console.log(await solver.check());
// sat
```

--------------------------------

### Congruence Closure Equality Log Example

Source: https://github.com/z3prover/z3/wiki/Equality-Explanation-Logging

Example of an equality derived from the congruence closure of other equalities.

```text
[mk-app] #5 f #1 #2
[mk-app] #6 f #3 #4
[eq-expl] #5 cg (#1 #3) (#2 #4) ; #6
```

--------------------------------

### Bug Report Examples

Source: https://github.com/z3prover/z3/blob/master/a3/a3-rust.md

Concrete examples of bug reports identifying integer overflows in specific functions.

```text
✗ BUG FOUND in function: elf
Bug type: Integer overflow in add operation: _2 add _20 (type: u64, bounds: u64 [0, 9223372036854775807])

✗ BUG FOUND in function: stack
Bug type: Integer overflow in add operation: _2 add _4 (type: u64, bounds: u64 [0, 9223372036854775807])
```

--------------------------------

### Define ExternalProject for C++ Examples

Source: https://github.com/z3prover/z3/blob/master/examples/CMakeLists.txt

Registers C++-based example projects as external builds dependent on libz3.

```cmake
ExternalProject_Add(cpp_example
  DEPENDS libz3
  # Configure step
  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++"
  CMAKE_ARGS
    "-DZ3_DIR=${PROJECT_BINARY_DIR}"
    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
  # Build step
  BUILD_ALWAYS ON
  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
  # Install Step
  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
)
set_target_properties(cpp_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
```

```cmake
ExternalProject_Add(userPropagator
        DEPENDS libz3
        # Configure step
        SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/userPropagator"
        CMAKE_ARGS
        "-DZ3_DIR=${PROJECT_BINARY_DIR}"
        "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
        # Build step
        BUILD_ALWAYS ON
        BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/userPropagator_build_dir"
        # Install Step
        INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
        )
set_target_properties(userPropagator PROPERTIES EXCLUDE_FROM_ALL TRUE)
```

--------------------------------

### Define ExternalProject for C Examples

Source: https://github.com/z3prover/z3/blob/master/examples/CMakeLists.txt

Registers C-based example projects as external builds dependent on libz3.

```cmake
ExternalProject_Add(c_example
  DEPENDS libz3
  # Configure step
  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c"
  CMAKE_ARGS
    "-DZ3_DIR=${PROJECT_BINARY_DIR}"
    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
  # Build step
  BUILD_ALWAYS ON
  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
  # Install Step
  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
)
set_target_properties(c_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
```

```cmake
ExternalProject_Add(c_maxsat_example
  DEPENDS libz3
  # Configure step
  SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat"
  CMAKE_ARGS
    "-DZ3_DIR=${PROJECT_BINARY_DIR}"
    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
  # Build step
  BUILD_ALWAYS ON
  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
  # Install Step
  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
)
set_target_properties(c_maxsat_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
```

--------------------------------

### Build TPTP with CMake

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Step-by-step instructions for configuring and building the TPTP target.

```bash
cd z3
mkdir release
cd release
cmake3 -DZ3_BUILD_LIBZ3_SHARED=FALSE -DCMAKE_BUILD_TYPE=RelWithDebInfo -G "Unix Makefiles" ../
make
make z3_tptp5
cp examples/tptp_build_dir/z3_tptp5 ../../bin/z3_tptp
```

--------------------------------

### Recursive function compilation example

Source: https://github.com/z3prover/z3/blob/master/doc/design_recfuns.md

Example showing how a factorial function definition is decomposed into auxiliary predicates and constraints.

```text
A_fact_0[n] => fact(n) = 1
A_fact_1[n] => fact(n) = n * fact(n-1)
A_fact_0[n] <=> n < 2
A_fact_1[n] <=> ¬(n < 2)
```

--------------------------------

### Solve a simple integer constraint in Go

Source: https://github.com/z3prover/z3/blob/master/doc/test_go_doc/index.html

Demonstrates creating a context, defining an integer variable, asserting a constraint, and checking satisfiability.

```go
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())
        }
    }
}
```

--------------------------------

### Detect Python Installation Directory

Source: https://github.com/z3prover/z3/blob/master/src/api/python/CMakeLists.txt

Uses the Python interpreter to determine the appropriate site-packages directory for installation if not explicitly provided.

```cmake
option(Z3_INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
if (Z3_INSTALL_PYTHON_BINDINGS)
  message(STATUS "Emitting rules to install Z3 python bindings")
  # Try to guess the installation path for the bindings
  if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
    message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
    execute_process(
      COMMAND "${Python3_EXECUTABLE}" "-c"
        "import sysconfig; print(sysconfig.get_path('purelib'))"
      RESULT_VARIABLE exit_code
      OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR
      OUTPUT_STRIP_TRAILING_WHITESPACE
    )

    if (NOT ("${exit_code}" EQUAL 0))
      message(FATAL_ERROR "Failed to determine your Python package directory")
    endif()
    message(STATUS "Detected Python package directory: \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
    # Set a cache variable that the user can modify if needed
    set(CMAKE_INSTALL_PYTHON_PKG_DIR
      "${CMAKE_INSTALL_PYTHON_PKG_DIR}"
      CACHE PATH
      "Path to install python bindings. This can be relative or absolute.")
    mark_as_advanced(CMAKE_INSTALL_PYTHON_PKG_DIR)
  else()
    message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR already set (\"${CMAKE_INSTALL_PYTHON_PKG_DIR}\")"
                   ". Not trying to guess.")
  endif()
```

--------------------------------

### Compose and Apply Tactics

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/jupyter/strategies.ipynb

Demonstrates creating a goal, composing built-in tactics with 'Then', and applying them to the goal.

```python
!pip install "z3-solver"

from z3 import *

x, y = Reals('x y')
g  = Goal()
g.add(x > 0, y > 0, x == y + 2)
print(g)

t1 = Tactic('simplify')
t2 = Tactic('solve-eqs')
t  = Then(t1, t2)
print(t(g))
```

--------------------------------

### Create Build Target for Python Examples

Source: https://github.com/z3prover/z3/blob/master/examples/python/CMakeLists.txt

Defines a custom target that triggers the copy commands for all Python example files.

```cmake
add_custom_target(build_z3_python_examples
  ALL
  DEPENDS
    ${build_z3_python_examples_target_depends}
)
```

--------------------------------

### Build Z3 with Java Bindings

Source: https://github.com/z3prover/z3/blob/master/doc/JAVA_IDE_SETUP.md

Commands to clone, configure, and build Z3 from source to generate Java bindings.

```bash
# Clone the repository
git clone https://github.com/Z3Prover/z3.git
cd z3

# Configure with Java support
python scripts/mk_make.py --java

# Build
cd build
make

# The Java bindings will be in the build directory
# - com.microsoft.z3.jar
# - libz3java.so / libz3java.dll / libz3java.dylib
# - libz3.so / libz3.dll / libz3.dylib
```

--------------------------------

### Install Z3 CMake Targets

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Exports the Z3 targets to a CMake file within the installation directory if the core library is built.

```cmake
if (Z3_BUILD_LIBZ3_CORE)
  install(EXPORT
    Z3_EXPORTED_TARGETS
    FILE "Z3Targets.cmake"
    NAMESPACE z3::
    DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
  )
endif()
```

--------------------------------

### Build Z3 using Bazel

Source: https://github.com/z3prover/z3/blob/master/README.md

Command to initiate the build process for Z3 using the Bazel build system.

```bash
bazel build //...
```

--------------------------------

### Build Z3 with nmake on Windows

Source: https://github.com/z3prover/z3/blob/master/README.md

Compiles the project using nmake after configuration.

```bash
cd build
nmake
```

--------------------------------

### Install Z3 Java Bindings

Source: https://github.com/z3prover/z3/blob/master/src/api/java/CMakeLists.txt

Defines installation paths and rules for the Z3 Java JAR and JNI bridge library, configurable via CMake options.

```cmake
option(Z3_INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
if (Z3_INSTALL_JAVA_BINDINGS)
  # Provide cache variables for the install locations that the user can change.
  # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
  # files on Linux distributions
  if (NOT Z3_JAVA_JAR_INSTALLDIR)
     set(Z3_JAVA_JAR_INSTALLDIR
       "${CMAKE_INSTALL_DATAROOTDIR}/java"
       CACHE
       PATH
       "Directory to install Z3 Java jar file relative to install prefix"
     )
  endif()
  if (NOT Z3_JAVA_JNI_LIB_INSTALLDIR)
    set(Z3_JAVA_JNI_LIB_INSTALLDIR
       "${CMAKE_INSTALL_LIBDIR}"
       CACHE
       PATH
       "Directory to install Z3 Java JNI bridge library relative to install prefix"
     )
  endif()
  install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
  install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
endif()
```

--------------------------------

### Build with Ninja

Source: https://github.com/z3prover/z3/blob/master/README-CMake.md

Configure and build a project using the Ninja generator.

```bash
mkdir build
cd build
cmake -G "Ninja" ../
ninja
```

--------------------------------

### Configure and Build .NET Project

Source: https://github.com/z3prover/z3/blob/master/src/api/dotnet/CMakeLists.txt

Configures the project file from a template and registers the .NET build target.

```cmake
configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj)
ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj
    VERSION ${Z3_DOTNET_NUPKG_VERSION}
    PLATFORM ${Z3_DOTNET_PLATFORM}
    SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in 
            ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props
            ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets
            ${Z3_DOTNET_ASSEMBLY_SOURCES}
    PACKAGE Microsoft.Z3
    PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$<CONFIG>"
    )
add_dependencies(BUILD_Microsoft.Z3 libz3)
```

--------------------------------

### Uninstall Z3

Source: https://github.com/z3prover/z3/blob/master/README.md

Removes the installed Z3 files using make.

```bash
sudo make uninstall
```

--------------------------------

### Managing Multiple Solvers

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/advanced-examples.htm

Demonstrates creating multiple solver instances and copying assertions between them.

```python
x, y = Ints('x y')
s1 = Solver()
s1.add(x > 10, y > 10)
s2 = Solver()
# solver s2 is empty
print s2
# copy assertions from s1 to s2
s2.add(s1.assertions())
print s2
```

--------------------------------

### Define Conflict Constraint

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

Creates a Z3 constraint ensuring that two packages cannot both be installed.

```python
def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))
```

--------------------------------

### Use comments in Z3Py

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

Shows the use of single-line comments starting with the hash character.

```python
# This is a comment
x = Real('x') # comment: creating x
print x**2 + 2*x + 2  # comment: printing polynomial
```

--------------------------------

### Compile Z3Py with Visual Studio (64-bit)

Source: https://github.com/z3prover/z3/wiki/Using-Z3Py-on-Windows

Execute build commands in a Visual Studio x64 Command Prompt using the -x flag.

```bash
python scripts/mk_make.py -x
cd build
nmake
```

--------------------------------

### Check Installation Validity

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/jupyter/guide.ipynb

A function to check if a set of constraints is satisfiable and print the resulting model.

```python
def install_check(*problem):
    s = Solver()
    s.add(*problem)
    if s.check() == sat:
        m = s.model()
        r = []
        for x in m:
            if is_true(m[x]):
                # x is a Z3 declaration
                # x() returns the Z3 expression
                # x.name() returns a string
                r.append(x())
        print(r)
    else:
        print("invalid installation profile")

print("Check 1")
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, [d]),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z)

print("Check 2")
install_check(DependsOn(a, [b, c, z]),
              #DependsOn(b, d),
              DependsOn(b, [d]),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z, g)
```

--------------------------------

### Configure Relocatable Z3Config.cmake

Source: https://github.com/z3prover/z3/blob/master/CMakeLists.txt

Uses configure_package_config_file to generate a relocatable configuration file for the install tree.

```cmake
configure_package_config_file("${PROJECT_SOURCE_DIR}/cmake/Z3Config.cmake.in"
  "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
  INSTALL_DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
  PATH_VARS Z3_FIRST_PACKAGE_INCLUDE_DIR
)
```

--------------------------------

### Configure .NET Build Environment

Source: https://github.com/z3prover/z3/blob/master/examples/dotnet/CMakeLists.txt

Sets up the .NET platform architecture and configures project files for the build process.

```cmake
find_package(Dotnet REQUIRED)

if(TARGET_ARCHITECTURE STREQUAL "i686")
    set(Z3_DOTNET_PLATFORM "x86")
else()
    set(Z3_DOTNET_PLATFORM "AnyCPU")
endif()

configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY)
configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Program.cs Program.cs       COPYONLY)
```

--------------------------------

### Build Z3 Go Bindings with Python

Source: https://github.com/z3prover/z3/blob/master/doc/test_go_doc/README.html

Commands to build the Go bindings using the Python-based build script.

```bash
python scripts/mk_make.py --go
cd build
make
```

--------------------------------

### Combine polynomial and Boolean constraints

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

Example of mixing real number arithmetic and Boolean logic.

```python
p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
```

--------------------------------

### Handle unknown solver results

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/html/guide-examples.htm

Example of a system of constraints that Z3 cannot solve, resulting in an unknown status.

```python
x = Real('x')
s = Solver()
s.add(2**x == 3)
print s.check()
```

--------------------------------

### Import Z3

Source: https://github.com/z3prover/z3/blob/master/examples/python/tutorial/jupyter/guide.ipynb

Initializes the Z3 library for use in Python.

```python
from z3 import *
```
Tokens:
Raw