### Configure Z3 CMake Project Setup

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

Initializes a CMake project for Z3 user propagator examples with C++ language support. Uses find_package() to locate Z3 with NO_DEFAULT_PATH to ensure explicit Z3_DIR specification, preventing accidental use of system-installed Z3 copies.

```cmake
project(Z3_USER_PROPAGATOR_EXAMPLE CXX)
cmake_minimum_required(VERSION 3.4)
find_package(Z3
  REQUIRED
  CONFIG
  NO_DEFAULT_PATH
)
```

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

### Install Problem Solver using Z3Py

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

Determines if a set of packages can be installed based on their dependencies and conflicts. It defines Boolean variables for each package and uses Z3Py functions like `And`, `Implies`, `Or`, `Not`, and `Bools` to model the installation logic. The `install_check` function verifies the consistency of the package requirements.

```python
from Z3 import *

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

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

### Build and install Z3 in Python virtual environment

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

Set up Python virtual environment, build Z3 with Python bindings, and verify installation. This approach isolates Z3 installation and ensures proper Python package management without requiring non-standard prefix handling.

```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 C Example Project with libz3 (CMake)

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

Configures and builds a C example project that depends on the libz3 library. It utilizes CMake's ExternalProject module to fetch and build the example as a separate target. The configuration includes setting Z3_DIR and optionally forcing a C++ linker.

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

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

### Install Z3 NuGet Package and Documentation Files

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

Installs the Z3 .NET NuGet package (.nupkg file) and its associated XML documentation to the CMake installation directory. Uses PROJECT_BINARY_DIR to locate built artifacts and CMAKE_INSTALL_LIBDIR to determine the destination path within the installation prefix.

```cmake
install(FILES "${PROJECT_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
install(FILES "${PROJECT_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
```

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

### CMake Configuration for Z3 C Example

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

This CMakeLists.txt file sets up a C/C++ project that uses the Z3 library. It specifies C standards, finds the Z3 package, configures include paths and libraries, and adds platform-specific commands for Windows.

```cmake
# Example C project
################################################################################
# NOTE: Even though this is a C project, libz3 uses C++. When using libz3
# as a static library if we don't configure this project to also support
# C++ we will use the C linker rather than the C++ linker and will not link
# the C++ standard library in resulting in a link failure.
project(Z3_C_EXAMPLE C CXX)
cmake_minimum_required(VERSION 3.4)
set(CMAKE_C_STANDARD_REQUIRED ON)
set(CMAKE_C_STANDARD 99)
set(CMAKE_C_EXTENSIONS OFF)

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
)
message(STATUS "Z3_FOUND: ${Z3_FOUND}")
message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
message(STATUS "Z3_DIR: ${Z3_DIR}")

add_executable(c_example test_capi.c)

option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
if (FORCE_CXX_LINKER)
  # This is a hack for avoiding UBSan linking errors
  message(STATUS "Forcing use of C++ linker")
  set_target_properties(c_example
    PROPERTIES
    LINKER_LANGUAGE CXX
  )
endif()

target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})

if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
  # On Windows we need to copy the Z3 libraries
  # into the same directory as the executable
  # so that they can be found.
  foreach (z3_lib ${Z3_LIBRARIES})
    message(STATUS "Adding copy rule for ${z3_lib}")
    add_custom_command(TARGET c_example
      POST_BUILD
      COMMAND
        ${CMAKE_COMMAND} -E copy_if_different
        $<TARGET_FILE:${z3_lib}>
        $<TARGET_FILE_DIR:c_example>
    )
  endforeach()
endif()

```

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

### Clone and bootstrap vcpkg for Z3 installation

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

Bootstrap vcpkg package manager and install Z3 using bash or PowerShell scripts. Vcpkg provides a full platform package manager for Z3 installation across different operating systems.

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

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

### Z3Py: Install Check with Solver Model

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

Implements an `install_check` function using Z3Py's solver. It adds problem constraints, checks for satisfiability, and if satisfiable, extracts and prints the true propositions from the model. If not satisfiable, it indicates an invalid installation profile.

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

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

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

### Build Dotnet Examples (CMake)

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

Conditionally includes the Dotnet examples subdirectory for building if the Z3_BUILD_DOTNET_BINDINGS option is enabled. This facilitates the inclusion of .NET-related examples within the main Z3 build process.

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

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

### Configure Z3 C++ Example Project with CMake

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

This snippet shows the main CMake configuration for a C++ project using Z3. It finds the Z3 package, sets C++11 standards, and configures the build target 'cpp_example'. Dependencies include Z3 and standard CMake modules. It outputs compiler flags and library paths.

```cmake
project(Z3_C_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
)

set(CMAKE_CXX_STANDARD 11)
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(cpp_example example.cpp)
target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})

target_compile_options(cpp_example PRIVATE ${Z3_COMPONENT_CXX_FLAGS})

if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
  # On Windows we need to copy the Z3 libraries
  # into the same directory as the executable
  # so that they can be found.
  foreach (z3_lib ${Z3_LIBRARIES})
    message(STATUS "Adding copy rule for ${z3_lib}")
    add_custom_command(TARGET cpp_example
      POST_BUILD
      COMMAND
        ${CMAKE_COMMAND} -E copy_if_different
        $<TARGET_FILE:${z3_lib}>
        $<TARGET_FILE_DIR:cpp_example>
    )
  endforeach()
endif()
```

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

### Build TPTP5 C++ Example Project with libz3 (CMake)

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

Builds a C++ example project for TPTP5 (Thousands of Problems for Theorem Provers) using libz3. This CMake configuration uses ExternalProject to manage the build process, setting the source directory and necessary build arguments.

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

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

### Build C++ Example Project with libz3 (CMake)

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

Configures and builds a C++ example project that links against the libz3 library. This CMake script employs the ExternalProject module, specifying the source directory and passing build-related arguments like Z3_DIR and the build type.

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

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

### Install Z3 Python wrapper from PyPI

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

Install Z3 Python bindings using pip package manager from PyPI. This provides the latest release of Z3 with Python language support.

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

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

### Build MaxSAT C Example Project with libz3 (CMake)

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

Configures and builds a C example project specifically for MaxSAT problems, depending on the libz3 library. It uses CMake's ExternalProject module, setting the source directory to 'maxsat' and passing necessary configuration arguments.

```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 Z3 Python bindings with custom prefix and package directory

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

Build Z3 Python bindings with non-standard installation prefix and custom Python package directory. This approach allows specifying custom paths for both the installation prefix and Python site-packages location.

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

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

### Build Python Examples (CMake)

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

Conditionally includes the Python examples subdirectory for building if the Z3_BUILD_PYTHON_BINDINGS option is enabled in the CMake configuration. This allows for modular building of language-specific bindings.

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

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

### Package Installation Constraint Encoding with Z3

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

This Python code demonstrates how to model package dependencies and conflicts using Z3. It defines boolean variables for packages and provides helper functions `DependsOn` and `Conflict` to generate Z3 constraints representing these relationships. This allows for checking the feasibility of installing a set of packages.

```python
from z3 import *

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

#DependsOn(a, [b, c, z])
#DependsOn is a simple Python function that creates Z3 constraints that capture the depends clause semantics.

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

#Thus, DependsOn(a, [b, c, z]) generates the constraint
# And(Implies(a, b), Implies(a, c), Implies(a, z))

print(DependsOn(a, [b, c, z]))

#That is, if users install package a, they must also install packages b, c and z.

#If package d conflicts with package e, we write Conflict(d, e). Conflict is also a simple Python function.

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

# Conflict(d, e) generates the constraint Or(Not(d), Not(e)). 
# With these two functions, we can easily encode the example 

```

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

### Build User Propagator C++ Example Project with libz3 (CMake)

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

Configures and builds a C++ example project demonstrating user-defined propagators with libz3. The CMake script employs ExternalProject, specifying the source directory and passing build configuration arguments.

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

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

### Handling Unsatisfiable Systems in Python Z3Py

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

Demonstrates a scenario where a system of constraints has no solution, resulting in an unsatisfiable outcome when using the solve function in Z3Py.

```python
from z3 import *
x = Real('x')
solve(x > 4, x < 0)
```

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

### Basic Datalog: Declare Relations, Rules, and Query

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

Illustrates basic Datalog constructs in Z3Py for fixed-point computations. It shows how to register relations, define rules, set the engine to 'datalog', and pose queries. This example demonstrates adding facts and querying again to see the effect of new facts.

```python
fp = Fixedpoint()
a, b, c = Bools('a b c')
p.register_relation(a.decl(), b.decl(), c.decl())
fp.rule(a,b)
fp.rule(b,c)
fp.set(engine='datalog')

print "current set of rules\n", fp
print fp.query(a)

fp.fact(c)
print "updated set of rules\n", fp
print fp.query(a)
print fp.get_answer()
```

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

### Z3 Unsolvable Constraint Example

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

Demonstrates a scenario where Z3 returns 'unknown' as the result of `check()`. This occurs when Z3 cannot determine satisfiability, such as with non-polynomial constraints like 2**x.

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

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

### Z3 Model Inspection

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

Demonstrates how to obtain and inspect a model for a set of satisfiable constraints. It shows how to get the model using `s.model()`, access variable interpretations using `m[variable]`, and iterate through model declarations.

```python
x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print s.check()

m = s.model()
print "x = %s" % m[x]

print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])
```

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

### Basic Z3 Solver API Usage

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

Introduces the fundamental Z3 Solver API. It demonstrates creating a solver instance, adding constraints using `add`, checking satisfiability with `check`, and managing assertion scopes using `push` and `pop`.

```python
x = Int('x')
y = Int('y')

s = Solver()
print(s)

s.add(x > 10, y == x + 2)
print(s)
print("Solving constraints in the solver s ...")
print(s.check())

print("Create a new scope...")
s.push()
s.add(y < 11)
print(s)
print("Solving updated set of constraints...")
print(s.check())

print("Restoring state...")
s.pop()
print(s)
print("Solving restored set of constraints...")
print(s.check())
```

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

### Configure Z3 Package Finding in CMake

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

This snippet demonstrates how to find the Z3 package using CMake. It requires the Z3 package to be installed and specifies 'NO_DEFAULT_PATH' to ensure that only Z3 found via '-DZ3_DIR' is used, preventing accidental linking with system-installed Z3 copies. This is crucial for Z3's own build system.

```cmake
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 Basic Solver API

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

Introduces the fundamental Z3 Solver API. It shows how to create a solver instance, add constraints using `add()`, check for satisfiability with `check()`, and manage assertion scopes using `push()` and `pop()`.

```python
x = Int('x')
y = Int('y')

s = Solver()
print s

s.add(x > 10, y == x + 2)
print s
print "Solving constraints in the solver s ..."
print s.check()

print "Create a new scope..."
s.push()
s.add(y < 11)
print s
print "Solving updated set of constraints..."
print s.check()

print "Restoring state..."
s.pop()
print s
print "Solving restored set of constraints..."
print s.check()
```

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

### CMake: Install Z3 Package Configuration

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

Installs Z3's CMake package configuration files (`Z3Targets.cmake`, `Z3Config.cmake`, `Z3ConfigVersion.cmake`, `z3.pc`) to the installation directory. It configures `Z3Config.cmake` to be re-locatable, ensuring clients can use Z3 even if installed in a non-standard prefix.

```cmake
install(EXPORT
  Z3_EXPORTED_TARGETS
  FILE "Z3Targets.cmake"
  NAMESPACE z3::
  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)
set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${PROJECT_BINARY_DIR}/cmake/Z3Config.cmake")
set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}")
set(Z3_SECOND_INCLUDE_DIR "")
set(Z3_CXX_PACKAGE_INCLUDE_DIR "")
set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
set(CONFIG_FILE_TYPE "install tree")
# We use `configure_package_config_file()` to try and create CMake files
# that are re-locatable so that it doesn't matter if the files aren't placed
# in the original install prefix.
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
)
unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)
unset(Z3_CXX_PACKAGE_INCLUDE_DIR)
unset(AUTO_GEN_MSG)
unset(CONFIG_FILE_TYPE)

# Add install rule to install ${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}
install(
  FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)

# Add install rule to install ${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake
install(
  FILES "${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)

# Add install rule to install ${PROJECT_BINARY_DIR}/z3.pc
install(
  FILES "${PROJECT_BINARY_DIR}/z3.pc"
  DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}"
)

```

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

### Configure .NET Bindings Installation Option in CMake

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

Sets a CMake option to control whether Z3 .NET bindings should be installed during the build process. This boolean option defaults to ON, allowing users to enable or disable .NET bindings installation at configuration time.

```cmake
option(Z3_INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
```

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

### Create Solver using SMT Tactic

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

Demonstrates creating a solver that wraps the main Z3 solver using the 'smt' tactic. It adds an integer constraint and checks for satisfiability, then prints the model.

```python
x, y = Ints('x y')
s = Tactic('smt').solver()
s.add(x > y + 1)
print(s.check())
print(s.model())
```

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

### Wrapping Main Solver with `smt` Tactic

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

Shows how the `smt` tactic can be used to wrap the main solver in Z3. It demonstrates creating an integer arithmetic solver, adding a constraint, checking satisfiability, and retrieving the model.

```python
x, y = Ints('x y')
s = Tactic('smt').solver()
s.add(x > y + 1)
print s.check()
print s.model()
```

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

### Configuring Z3 Installation Directories in CMake

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

Sets and configures installation directories for Z3-related files, including pkgconfig files and CMake package files. It also reports the final installation paths for libraries, binaries, and include directories.

```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}\" ")
```

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

### Configure Z3 Project with CMake Command Line

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

This example shows the general command-line workflow for configuring a project with CMake. It covers creating a build directory, navigating into it, and running CMake to configure the project, specifying the build type for single-configuration generators.

```bash
# 1. Create a new build directory
mkdir build
cd build

# 2. Configure the project (replace ../ with the path to your source directory)
# For single-configuration generators (e.g., NMake, Ninja), specify the build type:
cmake -G "NMake Makefiles" -DCMAKE_BUILD_TYPE=Release ../

# For multi-configuration generators (e.g., Visual Studio), do not set CMAKE_BUILD_TYPE here.
# cmake -G "Visual Studio 16 2019" ../

# 3. Generate the build system (often done by the 'cmake' command itself)

# 4. Invoke the build system to build the project
nmake
# or
# msbuild Z3.sln /p:Configuration=Release
```

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

### Install Z3 Java JAR and JNI Library with CMake

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

Deploys Z3 Java JAR file and JNI bridge library to specified installation directories using CMake install commands. Requires Z3_INSTALL_JAVA_BINDINGS option to be enabled.

```cmake
install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
```

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

### Configure Python Bindings Installation Path

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

This configure script option allows users to specify a custom installation path for Z3Py (Python bindings). The --with-python parameter accepts a directory path where the Python bindings will be installed during the make install-z3py step.

```bash
./configure --with-python=<path>
```

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

### CMake: Conditional Z3 Example Targets Build

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

Conditionally enables the building of Z3 API examples based on the `Z3_ENABLE_EXAMPLE_TARGETS` CMake option. This option is set to ON by default only when the source directory is the project's main source directory, ensuring examples are built during standard development but not necessarily in other configurations.

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

```

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

### Create and Print Z3 Rational and Real Numbers

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

Illustrates the creation of Z3 rational and real numbers, and how they are handled in arithmetic operations. It contrasts Python's integer division with Z3's rational division and shows different methods for constructing Z3 rational and real values, including using `RealVal` and string representations.

```python
print(1/3)
print(RealVal(1)/3)

x = Real('x')
print(x + 1/3)
print(x + "1/3")
print(x + 0.25)
```

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

### Configure Public Headers and Install libz3 Target in CMake

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

Sets up public header files for the libz3 target and configures installation destinations across multiple platforms. Handles library installation to platform-specific directories including Windows DLL runtime and import library locations.

```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}"
  RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}"
  PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
)
```

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

### Configure Z3 Environment with set_option

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

Demonstrates how to configure Z3's global settings using the `set_option` function. This includes setting precision for decimal output and controlling the conversion of rational numbers to decimal notation. It also shows how to reset these options.

```python
set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=20)
solve(3*x == 1)
set_option(rational_to_decimal=False)
solve(6*x == 37)
```

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

### Bakery Algorithm Transitions and Query in Python

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

Implements Lamport's two-process Bakery algorithm using the `TransitionSystem` class. Defines distinct states and transitions for two processes, then queries for a specific system state. Dependencies include Z3 and the `TransitionSystem` class.

```python
set_option(relevancy=0, verbose=1)

L = Datatype('L')
L.declare('L0')
L.declare('L1')
L.declare('L2')
L = L.create()
L0 = L.L0
L1 = L.L1
L2 = L.L2

y0 = Int('y0')
y1 = Int('y1')
l = Const('l', L)
m = Const('m', L)

t1 = { "guard" : l == L0,
       "effect" : [ L1, y1 + 1, m, y1 ] }
t2 = { "guard" : And(l == L1, Or([y0 <= y1, y1 == 0])),
       "effect" : [ L2, y0, m, y1 ] }
t3 = { "guard" : l == L2,
       "effect" : [ L0, IntVal(0), m, y1 ]}

s1 = { "guard" : m == L0,
       "effect" : [ l, y0, L1, y0 + 1 ] }
s2 = { "guard" : And(m == L1, Or([y1 <= y0, y0 == 0])),
       "effect" : [ l, y0, L2, y1 ] }
s3 = { "guard" : m == L2,
       "effect" : [ l, y0, L0, IntVal(0) ]}

ptr = TransitionSystem( And(l == L0, y0 == 0, m == L0, y1 == 0),
			[t1, t2, t3, s1, s2, s3],
			[l, y0, m, y1])

ptr.query(And([l == L2, m == L2]))

```

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

### Use System Z3 or Fetch with CMake

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

This approach uses `find_package` to detect a system-installed Z3 that meets the minimum version. If not found, it falls back to fetching Z3 from its GitHub repository using `FetchContent`. This ensures a consistent `z3::libz3` target regardless of the Z3 source.

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

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

### Configure Z3 Python Bindings Installation (CMake)

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

This CMake code snippet configures the installation of Z3's Python bindings. It checks if the `Z3_INSTALL_PYTHON_BINDINGS` option is enabled. If so, it attempts to automatically detect the Python package directory using `sysconfig` and the `Python3_EXECUTABLE`. If the directory is not found or the user has not explicitly set `CMAKE_INSTALL_PYTHON_PKG_DIR`, it provides a default and marks it as advanced. Finally, it installs the bindings to the determined destination, issuing a warning if the destination is not within the CMAKE_INSTALL_PREFIX.

```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}\" " ) # noqa
    # 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()

  # Check if path exists under the install prefix if it is absolute. If the
  # path is relative it will be installed under the install prefix so there
  # if nothing to check
  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()
```

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

### Direct Solver API Usage with `With` and `aig` Tactic

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

Illustrates direct usage of the solver API, configuring the solver with `With` and incorporating the `aig` tactic for compressing Boolean formulas. It shows adding constraints, checking satisfiability, and evaluating expressions using the model.

```python
bv_solver = Then(With('simplify', mul2concat=True),
                 'solve-eqs',
                 'bit-blast',
                 'aig',
                 'sat').solver()
x, y = BitVecs('x y', 16)
bv_solver.add(x*32 + y == 13, x & y < 10, y > -100)
print bv_solver.check()
m = bv_solver.model()
print m
print x*32 + y, "==", m.evaluate(x*32 + y)
print x & y, "==", m.evaluate(x & y)
```

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

### Set C++ Standard to C++20 for Z3 API

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

Configures CMake to use C++20 standard as required by the Z3 user propagator example code. Sets CMAKE_CXX_STANDARD_REQUIRED to enforce strict compliance with the specified standard version.

```cmake
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
```

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

### Compile and Run OCaml Native Example

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

Compiles an OCaml native executable from ml_example.ml using ocamlopt for optimized performance, linking against Z3 library and zarith package, then executes it with DYLD_LIBRARY_PATH environment variable to resolve runtime library dependencies, redirecting output to log file.

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

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

### Combine Tactic with Solver and Goal Conversion

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

Shows how to apply a tactic to a goal, obtain subgoals, select one, and solve it using a separate solver. It also demonstrates using model converters to translate a subgoal model back to the original goal's context.

```python
t = Then('simplify', 
         'normalize-bounds', 
         'solve-eqs')

x, y, z = Ints('x y z')
g = Goal()
g.add(x > 10, y == x + 3, z > y)

r = t(g)
# r contains only one subgoal
print(r)

s = Solver()
s.add(r[0])
print(s.check())
# Model for the subgoal
print(s.model())
# Model for the original goal
print(r[0].convert_model(s.model()))
```

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

### Install Z3 Julia Bindings Library in CMake

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

Conditionally installs the z3jl shared library to system library and binary directories based on the Z3_INSTALL_JULIA_BINDINGS option (enabled by default). Supports library, archive, and runtime destinations for cross-platform compatibility.

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

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

### Compile and Run OCaml Bytecode Example

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

Builds an OCaml bytecode executable from ml_example.ml source using ocamlc, linking against Z3 library and zarith package, then executes it with DYLD_LIBRARY_PATH environment variable set to locate runtime dependencies, capturing output to a log file.

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

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

### Solve Unsatisfiable Constraints in Z3

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

Shows how to identify and handle unsatisfiable systems of constraints within Z3. The example demonstrates adding constraints that inherently contradict each other, leading to an unsatisfiable result when `solve` is called.

```python
x = Real('x')
solve(x > 4, x < 0)
```

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

### Combining Tactics and Solvers with Model Conversion

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

Demonstrates combining tactics with solvers. It shows applying a tactic to a goal, creating subgoals, selecting a subgoal, and solving it. It also illustrates using model converters to transform a subgoal's model into a model for the original goal.

```python
t = Then('simplify', 
         'normalize-bounds', 
         'solve-eqs')
x, y, z = Ints('x y z')
g = Goal()
g.add(x > 10, y == x + 3, z > y)
r = t(g)
# r contains only one subgoal
print r
s = Solver()
s.add(r[0])
print s.check()
# Model for the subgoal
print s.model()
# Model for the original goal
print r.convert_model(s.model())
```

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

### Register Local .NET NuGet Repository

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

Executes CMake code during installation to register a local NuGet repository, replacing the build-time repository with the installation-time repository. Includes the FindDotnet CMake module and calls DOTNET_REGISTER_LOCAL_REPOSITORY to configure package source discovery.

```cmake
install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" \"${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget\")")
```

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

### E-Matching Example (Z3)

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

Provides an example of E-matching in Z3, where terms are considered equal modulo congruence and pattern matching occurs modulo ground equalities. This demonstrates how Z3 deduces equalities based on asserted facts and patterns.

```python
f = Function('f', IntSort(), IntSort())
g = Function('g', IntSort(), IntSort())
a, b, c = Ints('a b c')
x = Int('x')

s = Solver()
s.set(auto_config=False, mbqi=False)

s.add( ForAll(x, f(g(x)) == x, patterns = [f(g(x))]),
       a == g(b),
       b == c,
       f(a) != c )

print (s.check())
```