Enum VerifyExpr 

pub enum VerifyExpr {
    Int(i64),
    Bool(bool),
    Var(String),
    Binary {
        op: VerifyOp,
        left: Box<VerifyExpr>,
        right: Box<VerifyExpr>,
    },
    Not(Box<VerifyExpr>),
    ForAll {
        vars: Vec<(String, VerifyType)>,
        body: Box<VerifyExpr>,
    },
    Exists {
        vars: Vec<(String, VerifyType)>,
        body: Box<VerifyExpr>,
    },
    Apply {
        name: String,
        args: Vec<VerifyExpr>,
    },
    ApplyInt {
        name: String,
        args: Vec<VerifyExpr>,
    },
    BitVecConst {
        width: u32,
        value: u64,
    },
    BitVecBinary {
        op: BitVecOp,
        left: Box<VerifyExpr>,
        right: Box<VerifyExpr>,
    },
    BitVecExtract {
        high: u32,
        low: u32,
        operand: Box<VerifyExpr>,
    },
    BitVecConcat(Box<VerifyExpr>, Box<VerifyExpr>),
    AtState {
        state: Box<VerifyExpr>,
        expr: Box<VerifyExpr>,
    },
    Transition {
        from: Box<VerifyExpr>,
        to: Box<VerifyExpr>,
    },
    Select {
        array: Box<VerifyExpr>,
        index: Box<VerifyExpr>,
    },
    Store {
        array: Box<VerifyExpr>,
        index: Box<VerifyExpr>,
        value: Box<VerifyExpr>,
    },
    Iff(Box<VerifyExpr>, Box<VerifyExpr>),
}

Expression AST for verification.

This IR is designed to be easily encodable into Z3 ASTs.

Variants

Int(i64)

Integer literal

Bool(bool)

Boolean literal

Var(String)

Variable reference

Binary

Binary operation

Fields

op: VerifyOp

left: Box<VerifyExpr>

right: Box<VerifyExpr>

Not(Box<VerifyExpr>)

Logical negation

ForAll

Universal quantifier: forall x: T. P(x)

Fields

vars: Vec<(String, VerifyType)>

body: Box<VerifyExpr>

Exists

Existential quantifier: exists x: T. P(x)

Fields

vars: Vec<(String, VerifyType)>

body: Box<VerifyExpr>

Apply

Uninterpreted function application (the “catch-all”)

Used for predicates, modals, temporals, etc. that we can’t directly encode semantically. Z3 treats these as opaque functions and reasons about them structurally.

Examples:

• Mortal(socrates) -> Apply { name: "Mortal", args: [Var("socrates")] }
• Possible(P) -> Apply { name: "Possible", args: [P] }

Fields

name: String

args: Vec<VerifyExpr>

ApplyInt

Uninterpreted INT-valued function application: Int^n → Int.

For function symbols in TERM position — sum(a, b) (the Link-lattice join ⊕), GovernmentOf(x), has(x, y) — where VerifyExpr::Apply (which encodes as Int^n → Bool) would be ill-sorted.

Fields

name: String

args: Vec<VerifyExpr>

BitVecConst

Bitvector constant with explicit width.

Fields

width: u32

value: u64

BitVecBinary

Bitvector binary operation.

Fields

op: BitVecOp

left: Box<VerifyExpr>

right: Box<VerifyExpr>

BitVecExtract

Bitvector bit extraction: operand[high:low].

Fields

high: u32

low: u32

operand: Box<VerifyExpr>

BitVecConcat(Box<VerifyExpr>, Box<VerifyExpr>)

Bitvector concatenation.

AtState

Expression evaluated at a specific state (for BMC unrolling).

Fields

state: Box<VerifyExpr>

expr: Box<VerifyExpr>

Transition

State transition relation: from → to.

Fields

from: Box<VerifyExpr>

to: Box<VerifyExpr>

Select

Array select: array[index].

Fields

array: Box<VerifyExpr>

index: Box<VerifyExpr>

Store

Array store: array[index] := value.

Fields

array: Box<VerifyExpr>

index: Box<VerifyExpr>

value: Box<VerifyExpr>

Iff(Box<VerifyExpr>, Box<VerifyExpr>)

Biconditional: left ↔ right. Used for Z3 equivalence queries.

Implementations

impl VerifyExpr

pub fn var(name: impl Into<String>) -> Self

Create a variable reference.

Examples

use logicaffeine_verify::VerifyExpr;

let x = VerifyExpr::var("x");
let counter = VerifyExpr::var("counter");

pub fn int(n: i64) -> Self

Create an integer literal.

Examples

use logicaffeine_verify::VerifyExpr;

let five = VerifyExpr::int(5);
let negative = VerifyExpr::int(-42);

pub fn bool(b: bool) -> Self

Create a boolean literal.

Examples

use logicaffeine_verify::VerifyExpr;

let truth = VerifyExpr::bool(true);
let falsity = VerifyExpr::bool(false);

pub fn binary(op: VerifyOp, left: VerifyExpr, right: VerifyExpr) -> Self

Create a binary operation.

For common operations, prefer the convenience methods like eq, gt, and, etc.

Examples

use logicaffeine_verify::{VerifyExpr, VerifyOp};

// x + y
let sum = VerifyExpr::binary(
    VerifyOp::Add,
    VerifyExpr::var("x"),
    VerifyExpr::var("y"),
);

pub fn not(expr: VerifyExpr) -> Self

Create a negation.

Examples

use logicaffeine_verify::VerifyExpr;

// ¬p
let not_p = VerifyExpr::not(VerifyExpr::var("p"));

// ¬(x > 5)
let not_gt = VerifyExpr::not(
    VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))
);

pub fn apply(name: impl Into<String>, args: Vec<VerifyExpr>) -> Self

Create an uninterpreted function application.

Use this for predicates, modals, temporals, and other constructs that cannot be directly encoded semantically. Z3 treats these as opaque functions and reasons about them structurally.

Examples

use logicaffeine_verify::VerifyExpr;

// Mortal(socrates)
let mortal = VerifyExpr::apply("Mortal", vec![VerifyExpr::var("socrates")]);

// Possible(P) for modal logic
let possible_p = VerifyExpr::apply("Possible", vec![VerifyExpr::var("P")]);

// Before(e1, e2) for temporal relations
let before = VerifyExpr::apply("Before", vec![
    VerifyExpr::var("e1"),
    VerifyExpr::var("e2"),
]);

pub fn apply_int(name: impl Into<String>, args: Vec<VerifyExpr>) -> Self

Create an uninterpreted INT-valued function application (Int^n → Int) for function symbols in term position, e.g. the lattice join sum(a, b).

pub fn forall(vars: Vec<(String, VerifyType)>, body: VerifyExpr) -> Self

Create a universal quantifier.

Examples

use logicaffeine_verify::{VerifyExpr, VerifyType};

// ∀x: Object. Mortal(x) → Human(x)
let all_mortals_are_human = VerifyExpr::forall(
    vec![("x".to_string(), VerifyType::Object)],
    VerifyExpr::implies(
        VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
        VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
    ),
);

pub fn exists(vars: Vec<(String, VerifyType)>, body: VerifyExpr) -> Self

Create an existential quantifier.

Examples

use logicaffeine_verify::{VerifyExpr, VerifyType};

// ∃x: Object. Mortal(x)
let something_is_mortal = VerifyExpr::exists(
    vec![("x".to_string(), VerifyType::Object)],
    VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
);

pub fn eq(left: VerifyExpr, right: VerifyExpr) -> Self

Equality: left == right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_equals_10 = VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10));

pub fn gt(left: VerifyExpr, right: VerifyExpr) -> Self

Greater than: left > right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_gt_5 = VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5));

pub fn lt(left: VerifyExpr, right: VerifyExpr) -> Self

Less than: left < right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_lt_100 = VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(100));

pub fn gte(left: VerifyExpr, right: VerifyExpr) -> Self

Greater than or equal: left >= right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_gte_0 = VerifyExpr::gte(VerifyExpr::var("x"), VerifyExpr::int(0));

pub fn lte(left: VerifyExpr, right: VerifyExpr) -> Self

Less than or equal: left <= right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_lte_max = VerifyExpr::lte(VerifyExpr::var("x"), VerifyExpr::var("max"));

pub fn neq(left: VerifyExpr, right: VerifyExpr) -> Self

Inequality: left != right.

Examples

use logicaffeine_verify::VerifyExpr;

let x_neq_0 = VerifyExpr::neq(VerifyExpr::var("x"), VerifyExpr::int(0));

pub fn and(left: VerifyExpr, right: VerifyExpr) -> Self

Conjunction: left && right.

Examples

use logicaffeine_verify::VerifyExpr;

// x > 0 && x < 100
let in_range = VerifyExpr::and(
    VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)),
    VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(100)),
);

pub fn or(left: VerifyExpr, right: VerifyExpr) -> Self

Disjunction: left || right.

Examples

use logicaffeine_verify::VerifyExpr;

// x < 0 || x > 100
let out_of_range = VerifyExpr::or(
    VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(0)),
    VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(100)),
);

pub fn implies(left: VerifyExpr, right: VerifyExpr) -> Self

Material implication: left → right.

Examples

use logicaffeine_verify::VerifyExpr;

// Mortal(x) → Human(x)
let mortals_are_human = VerifyExpr::implies(
    VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
    VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
);

pub fn bv_const(width: u32, value: u64) -> Self

Create a bitvector constant.

pub fn bv_binary(op: BitVecOp, left: VerifyExpr, right: VerifyExpr) -> Self

Create a bitvector binary operation.

pub fn iff(left: VerifyExpr, right: VerifyExpr) -> Self

Biconditional: left ↔ right.

Trait Implementations

impl Clone for VerifyExpr

fn clone(&self) -> VerifyExpr

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for VerifyExpr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for VerifyExpr

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for VerifyExpr

fn eq(&self, other: &VerifyExpr) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for VerifyExpr

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for VerifyExpr