Write x + y == 10 instead of verbose Z3 API calls. Natural C# syntax for Microsoft's Z3 theorem prover with unlimited precision arithmetic.
using var context = new Z3Context();
using var scope = context.SetUp();
var x = context.IntConst("x");
var y = context.IntConst("y");
using var solver = context.CreateSolver();
solver.Assert(x + y == 10); // Natural syntax
solver.Assert(x * 2 == y - 1); // Mathematical operators
if (solver.Check() == Z3Status.Satisfiable)
{
var model = solver.GetModel();
Console.WriteLine($"x = {model.GetIntValue(x)}"); // BigInteger
Console.WriteLine($"y = {model.GetIntValue(y)}");
}
using System.Numerics;
// BigInteger - no integer overflow
var huge = BigInteger.Parse("999999999999999999999999999999");
solver.Assert(x == huge);
// Exact rationals - no floating point errors
var r = context.RealConst("r");
solver.Assert(r == new Real(1, 3)); // Exactly 1/3
solver.Assert(r * 3 == 1); // Perfect arithmetic
Type Safety
// Compile-time type checking
var prices = context.ArrayConst<IntExpr, RealExpr>("prices");
solver.Assert(prices[0] == 10.5m); // Index: Int, Value: Real
solver.Assert(prices[1] > prices[0]); // Type-safe comparisons
// Seamless conversions
solver.Assert(x.ToReal() + r == 5.5m); // Int → Real
Custom .NET Data Types
// Real class - exact rational arithmetic (not decimal/double)
var oneThird = new Real(1, 3);
var twoThirds = new Real(2, 3);
Console.WriteLine(oneThird + twoThirds); // "1" (exact)
// Bv class - compile-time sized bitvectors with type safety
var bv8 = new Bv<Size8>(0b10101010);
var bv16 = bv8.Resize<Size16>(signed: false); // Resize to 16 bits
Console.WriteLine(bv8.ToULong()); // 170
Console.WriteLine(bv8.ToBinaryString()); // "10101010"
// Direct arithmetic and bitwise operations
var result = bv8 + new Bv<Size8>(5); // Type-safe arithmetic
var masked = bv8 & new Bv<Size8>(0xFF); // Bitwise operations
var x = context.IntConst("x");
var y = context.IntConst("y");
// Universal quantification: ∀x. x + 0 = x
var identity = context.ForAll(x, x + 0 == x);
solver.Assert(identity);
// Existential quantification: ∃y. x + y = 10
var existsSolution = context.Exists(y, x + y == 10);
solver.Assert(existsSolution);
// Multiple variables: ∀x,y. x * y = y * x
var commutativity = context.ForAll(x, y, x * y == y * x);
solver.Assert(commutativity);
Uninterpreted Functions
// Define function signature: Int → Int
var func = context.Func<IntExpr, IntExpr>("f");
// Apply function to arguments
solver.Assert(func.Apply(5) == 10);
solver.Assert(func.Apply(x) > 0);
// Consistency: same inputs produce same outputs
solver.Assert(func.Apply(5) == func.Apply(5));
Optimization
using var optimizer = context.CreateOptimizer();
// Integer optimization - returns IntObjective
var x = context.IntConst("x");
var y = context.IntConst("y");
optimizer.Assert(x + y <= 100);
optimizer.Assert(x >= 0);
optimizer.Assert(y >= 0);
var intObjective = optimizer.Maximize(3 * x + 2 * y);
if (optimizer.Check() == Z3Status.Satisfiable) {
var model = optimizer.GetModel();
var optimalValue = optimizer.GetUpper(intObjective); // Returns IntExpr
Console.WriteLine($"Max: {model.GetIntValue(optimalValue)}");
}
// Real optimization - returns RealObjective
var r = context.RealConst("r");
optimizer.Assert(r >= 0);
optimizer.Assert(r <= 10.5m);
var realObjective = optimizer.Maximize(r);
if (optimizer.Check() == Z3Status.Satisfiable) {
var model2 = optimizer.GetModel();
var optimalValue = optimizer.GetUpper(realObjective); // Returns ArithmeticExpr
// Check if result is integer or real
if (optimalValue.IsIntExpr()) {
Console.WriteLine($"Integer result: {model2.GetIntValue(optimalValue.AsIntExpr())}");
} else {
Console.WriteLine($"Real result: {model2.GetRealValue(optimalValue.AsRealExpr())}");
}
}
var x = context.IntConst("x");
// Create boolean trackers for each constraint
var t1 = context.BoolConst("t1");
var t2 = context.BoolConst("t2");
var t3 = context.BoolConst("t3");
// Link trackers to constraints
solver.Assert(t1.Implies(x > 100));
solver.Assert(t2.Implies(x < 50));
solver.Assert(t3.Implies(x > 0));
// Check with tracked assumptions
if (solver.CheckAssumptions(t1, t2, t3) == Z3Status.Unsatisfiable) {
// Get minimal conflicting subset
var core = solver.GetUnsatCore();
Console.WriteLine("Conflicting constraints:");
foreach (var tracker in core) {
Console.WriteLine($" {tracker}");
}
// Output: t1, t2 (the actual conflict)
}
Requirements
.NET 9.0+
Z3 library (auto-discovered on Windows/macOS/Linux)
