Struct Verifier 

pub struct Verifier { /* private fields */ }

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

The verifier uses a 10-second timeout by default. For more complex proofs with multiple constraints, use VerificationSession instead.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();

// Boolean validity
assert!(verifier.check_bool(true).is_ok());
assert!(verifier.check_bool(false).is_err());

// Integer bounds
assert!(verifier.check_int_greater_than(10, 5).is_ok());

Implementations

impl Verifier

pub fn new() -> Self

Create a new verifier with a 10-second timeout.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();

pub fn check_bool(&self, value: bool) -> VerificationResult

Check if a boolean value is valid (always true).

Returns Ok(()) if the value is true, an error otherwise.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();
assert!(verifier.check_bool(true).is_ok());
assert!(verifier.check_bool(false).is_err());

pub fn check_int_greater_than( &self, value: i64, bound: i64, ) -> VerificationResult

Verify that value > bound.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();
assert!(verifier.check_int_greater_than(10, 5).is_ok());  // 10 > 5
assert!(verifier.check_int_greater_than(3, 5).is_err());  // 3 > 5 is false

pub fn check_int_less_than(&self, value: i64, bound: i64) -> VerificationResult

Verify that value < bound.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();
assert!(verifier.check_int_less_than(3, 5).is_ok());   // 3 < 5
assert!(verifier.check_int_less_than(10, 5).is_err()); // 10 < 5 is false

pub fn check_int_equals(&self, left: i64, right: i64) -> VerificationResult

Verify that left == right.

Examples

use logicaffeine_verify::Verifier;

let verifier = Verifier::new();
assert!(verifier.check_int_equals(42, 42).is_ok());
assert!(verifier.check_int_equals(1, 2).is_err());

pub fn context(&self) -> VerificationContext

Create a verification context for more complex proofs.

Use this when you need to build custom verification logic with multiple variables and constraints.

Examples

use logicaffeine_verify::Verifier;
use z3::ast::Bool;

let verifier = Verifier::new();
let ctx = verifier.context();
let solver = ctx.solver();

// P ∨ ¬P is a tautology
let p = ctx.bool_var("p");
let tautology = Bool::or(&[&p, &p.not()]);
assert!(ctx.check_valid(&solver, &tautology).is_ok());

Trait Implementations

impl Default for Verifier

fn default() -> Self

Returns the “default value” for a type.