Spaceorc.Z3Wrap 0.0.8

Z3Wrap

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)}");
}

Why Z3Wrap?

Natural Syntax vs Z3 API

// Z3Wrap - readable
solver.Assert(x + y == 10);
solver.Assert(p.Implies(q & r));

// Raw Z3 - verbose
solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ctx.MkInt(10)));
solver.Assert(ctx.MkImplies(p, ctx.MkAnd(q, r)));

Unlimited Precision

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

Installation

dotnet add package Spaceorc.Z3Wrap
brew install z3  # macOS (or apt-get install libz3-4 on Linux)

Z3 library is auto-discovered on Windows/macOS/Linux.

Complete Feature Set

• Booleans: p & q, p | q, !p, p.Implies(q)
• Integers: BigInteger arithmetic with +, -, *, /, %
• Reals: Exact rational arithmetic with Real(1,3) fractions
• BitVectors: Type-safe compile-time sizes with Bv<Size32>, overflow detection
• Arrays: Generic ArrayExpr<TIndex, TValue> with natural indexing
• Quantifiers: First-order logic with ForAll and Exists
• Functions: Uninterpreted functions with type-safe signatures
• Optimization: Maximize/minimize objectives with soft constraints
• Solver: Push/pop scopes for constraint backtracking
• Debugging: Unsatisfiable cores for conflict identification

Advanced Examples

BitVector Operations

var bv = context.BvConst<Size32>("bv");

solver.Assert((bv & 0xFF) == 0x42);      // Bitwise operations
solver.Assert(bv << 2 == bv * 4);        // Shift equivalence
solver.Assert((bv ^ 0xFFFFFFFF) == ~bv); // XOR/NOT relationship

// Overflow detection
solver.Assert(context.AddNoOverflow(bv, 100U));

Quantifiers (First-Order Logic)

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())}");
    }
}

Solver Backtracking

solver.Push();
solver.Assert(x < 10);
if (solver.Check() == Z3Status.Unsatisfiable) {
    solver.Pop();  // Backtrack
    solver.Assert(x >= 10);
}

Unsatisfiable Cores (Debugging Conflicts)

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)

License: MIT