Getting Started with Z3 C++ API

This guide introduces the core concepts and classes of the Z3 C++ API with practical examples.

Basic Concepts

The Z3 C++ API is built around a few key classes:

z3::context - Manages all Z3 objects and configuration
z3::solver - The satisfiability solver
z3::expr - Represents expressions (formulas and terms)
z3::sort - Represents types (Bool, Int, Real, etc.)

Your First Z3 Program

Let’s start with a simple satisfiability problem:

#include <iostream>
#include <z3++.h>

int main() {
    z3::context c;
    
    // Create Boolean variables
    z3::expr x = c.bool_const("x");
    z3::expr y = c.bool_const("y");
    
    // Create a solver
    z3::solver s(c);
    
    // Add constraints
    s.add(x || y);      // x OR y
    s.add(!x || !y);    // NOT x OR NOT y
    
    // Check satisfiability
    if (s.check() == z3::sat) {
        std::cout << "sat\n";
        std::cout << s.get_model() << "\n";
    } else {
        std::cout << "unsat\n";
    }
    
    return 0;
}

Output:

sat
x -> false
y -> true

Working with the Context

The z3::context is the foundation of all Z3 operations. Every Z3 object is associated with a context.

z3::context c;

// Create different sorts
z3::sort bool_sort = c.bool_sort();
z3::sort int_sort = c.int_sort();
z3::sort real_sort = c.real_sort();
z3::sort bv_sort = c.bv_sort(32);  // 32-bit bitvector

Creating Constants

z3::context c;

// Boolean constant
z3::expr b = c.bool_const("b");

// Integer constant
z3::expr x = c.int_const("x");

// Real constant
z3::expr r = c.real_const("r");

// Bitvector constant (32-bit)
z3::expr bv = c.bv_const("bv", 32);

Creating Values

z3::context c;

// Boolean values
z3::expr t = c.bool_val(true);
z3::expr f = c.bool_val(false);

// Integer values
z3::expr zero = c.int_val(0);
z3::expr forty_two = c.int_val(42);

// Real values
z3::expr pi = c.real_val("3.14159");
z3::expr half = c.real_val(1, 2);  // 1/2 as a fraction

Using the Solver

The z3::solver is used to check satisfiability of formulas.

Basic Solver Operations

z3::context c;
z3::solver s(c);

z3::expr x = c.int_const("x");
z3::expr y = c.int_const("y");

// Add constraints
s.add(x > 0);
s.add(x < 10);
s.add(y == x + 3);

// Check satisfiability
z3::check_result result = s.check();

if (result == z3::sat) {
    z3::model m = s.get_model();
    std::cout << "x = " << m.eval(x) << "\n";
    std::cout << "y = " << m.eval(y) << "\n";
}

Possible Results

The check() method returns one of three values:

z3::sat - The constraints are satisfiable
z3::unsat - The constraints are unsatisfiable
z3::unknown - Z3 could not determine satisfiability

Extracting Models

When a formula is satisfiable, you can extract a model:

z3::context c;
z3::solver s(c);

z3::expr x = c.int_const("x");
z3::expr y = c.int_const("y");

s.add(x >= 1);
s.add(y < x + 3);

if (s.check() == z3::sat) {
    z3::model m = s.get_model();
    
    // Evaluate expressions in the model
    std::cout << "x = " << m.eval(x) << "\n";
    std::cout << "y = " << m.eval(y) << "\n";
    std::cout << "x + y = " << m.eval(x + y) << "\n";
}

Building Expressions

The C++ API provides operator overloading for building expressions naturally.

Boolean Operations

z3::context c;
z3::expr p = c.bool_const("p");
z3::expr q = c.bool_const("q");

z3::expr not_p = !p;
z3::expr p_and_q = p && q;
z3::expr p_or_q = p || q;
z3::expr p_implies_q = implies(p, q);
z3::expr p_iff_q = p == q;

Arithmetic Operations

z3::context c;
z3::expr x = c.int_const("x");
z3::expr y = c.int_const("y");

z3::expr sum = x + y;
z3::expr diff = x - y;
z3::expr prod = x * y;
z3::expr quot = x / y;
z3::expr negation = -x;

Comparison Operations

z3::context c;
z3::expr x = c.int_const("x");
z3::expr y = c.int_const("y");

z3::expr eq = (x == y);
z3::expr neq = (x != y);
z3::expr lt = (x < y);
z3::expr le = (x <= y);
z3::expr gt = (x > y);
z3::expr ge = (x >= y);

Common Examples

Solving Linear Constraints

#include <iostream>
#include <z3++.h>

int main() {
    z3::context c;
    z3::solver s(c);
    
    z3::expr x = c.int_const("x");
    z3::expr y = c.int_const("y");
    
    // Find values satisfying: 2x + 3y = 10 and x >= 0
    s.add(2 * x + 3 * y == 10);
    s.add(x >= 0);
    s.add(y >= 0);
    
    if (s.check() == z3::sat) {
        z3::model m = s.get_model();
        std::cout << "x = " << m.eval(x) << "\n";
        std::cout << "y = " << m.eval(y) << "\n";
    }
    
    return 0;
}

Proving a Theorem

To prove a theorem, we check if its negation is unsatisfiable:

#include <iostream>
#include <z3++.h>

int main() {
    z3::context c;
    z3::solver s(c);
    
    z3::expr x = c.bool_const("x");
    z3::expr y = c.bool_const("y");
    
    // Prove De Morgan's law: not(x and y) == (not x) or (not y)
    z3::expr conjecture = (!(x && y)) == (!x || !y);
    
    // Add the negation
    s.add(!conjecture);
    
    if (s.check() == z3::unsat) {
        std::cout << "Theorem proved!\n";
    } else {
        std::cout << "Counterexample found\n";
    }
    
    return 0;
}

Using Push/Pop for Incremental Solving

The solver maintains a stack of assertions:

z3::context c;
z3::solver s(c);

z3::expr x = c.int_const("x");

s.add(x > 0);
std::cout << s.check() << "\n";  // sat

// Create backtracking point
s.push();

s.add(x < 0);
std::cout << s.check() << "\n";  // unsat

// Restore to backtracking point
s.pop();

std::cout << s.check() << "\n";  // sat again

Working with Bitvectors

z3::context c;
z3::solver s(c);

z3::expr x = c.bv_const("x", 32);  // 32-bit bitvector
z3::expr y = c.bv_const("y", 32);

// Bitwise operations
s.add((x ^ y) - 103 == x * y);

if (s.check() == z3::sat) {
    z3::model m = s.get_model();
    std::cout << "x = " << m.eval(x) << "\n";
    std::cout << "y = " << m.eval(y) << "\n";
}

Error Handling

The C++ API throws exceptions on errors:

try {
    z3::context c;
    z3::expr x = c.bool_const("x");
    
    // This will throw - can't add boolean and integer
    z3::expr bad = x + 1;
} catch (z3::exception& e) {
    std::cout << "Error: " << e << "\n";
}

Configuration

You can configure Z3 through the context:

z3::config cfg;
cfg.set("auto_config", true);
cfg.set("timeout", 30000);  // 30 seconds

z3::context c(cfg);

Next Steps

API Reference - Detailed documentation of all classes
Examples - More complex examples

Python

C++

C

Java

.NET

JavaScript/TypeScript

Go

OCaml

C++ API Getting Started

Getting Started with Z3 C++ API

Basic Concepts

Your First Z3 Program

Working with the Context

Creating Constants

Creating Values

Using the Solver

Basic Solver Operations

Possible Results

Extracting Models

Building Expressions

Boolean Operations

Arithmetic Operations

Comparison Operations

Common Examples

Solving Linear Constraints

Proving a Theorem

Using Push/Pop for Incremental Solving

Working with Bitvectors

Error Handling

Configuration

Next Steps

​Getting Started with Z3 C++ API

​Basic Concepts

​Your First Z3 Program

​Working with the Context

​Creating Constants

​Creating Values

​Using the Solver

​Basic Solver Operations

​Possible Results

​Extracting Models

​Building Expressions

​Boolean Operations

​Arithmetic Operations

​Comparison Operations

​Common Examples

​Solving Linear Constraints

​Proving a Theorem

​Using Push/Pop for Incremental Solving

​Working with Bitvectors

​Error Handling

​Configuration

​Next Steps

Getting Started with Z3 C++ API

Basic Concepts

Your First Z3 Program

Working with the Context

Creating Constants

Creating Values

Using the Solver

Basic Solver Operations

Possible Results

Extracting Models

Building Expressions

Boolean Operations

Arithmetic Operations

Comparison Operations

Common Examples

Solving Linear Constraints

Proving a Theorem

Using Push/Pop for Incremental Solving

Working with Bitvectors

Error Handling

Configuration

Next Steps