Documentation Index
Fetch the complete documentation index at: https://mintlify.com/Z3Prover/z3/llms.txt
Use this file to discover all available pages before exploring further.
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 configurationz3::solver - The satisfiability solverz3::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;
}
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 satisfiablez3::unsat - The constraints are unsatisfiablez3::unknown - Z3 could not determine satisfiability
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
