Module ir 

Verification IR (Intermediate Representation)

A lightweight AST for Z3 verification that decouples from the main Logicaffeine AST. This avoids circular dependencies: logicaffeine depends on logicaffeine_verify, so logicaffeine_verify cannot depend on logicaffeine.

Usage

Build expressions using the VerifyExpr constructors:

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

// Build: x > 5 && y < 10
let expr = VerifyExpr::and(
    VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5)),
    VerifyExpr::lt(VerifyExpr::var("y"), VerifyExpr::int(10)),
);

Encoding Strategy

Complex types (modals, temporals, predicates) become uninterpreted functions. Z3 reasons about their structure without semantic understanding.

For example, given Possible(A) -> Possible(B) and Possible(A), Z3 deduces Possible(B).

Enums

BitVecOp

Bitvector operations for hardware verification.

VerifyExpr

Expression AST for verification.

VerifyOp

Binary operations in the verification IR.

VerifyType

Type declarations for verification variables.