Module solver 

Z3 solver wrapper for Logicaffeine verification.

This module provides two APIs for Z3-based verification:

Low-Level API: Verifier and VerificationContext

Direct Z3 access for single-shot checks and custom verification logic. Use when you need fine-grained control over the solver.

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();
assert!(verifier.check_bool(true).is_ok());
assert!(verifier.check_int_greater_than(10, 5).is_ok());

High-Level API: VerificationSession

Works with the VerifyExpr IR for accumulating declarations and assumptions before verification. Recommended for most use cases.

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let mut session = VerificationSession::new();
session.declare("x", VerifyType::Int);
session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));
assert!(session.verify(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_ok());

Structs

VerificationContext

A verification context for building constraints incrementally.

VerificationSession

A verification session for working with the Verification IR.

Verifier

Low-level Z3-based verifier for single-shot validity checks.

Functions

rename_var_in_expr

Rename a variable in a VerifyExpr (simple textual substitution). Recursively traverses ALL variants — no silent drops.