Function check_equivalence 

pub fn check_equivalence(
    fol_expr: &VerifyExpr,
    sva_expr: &VerifyExpr,
    signals: &[String],
    bound: usize,
) -> EquivalenceResult

Check whether two VerifyExpr formulas are semantically equivalent.

Both formulas should be bounded (timestep-unrolled) — i.e., all temporal operators have been expanded to conjunctions/disjunctions over timesteps, and signal references use the “name@timestep” naming convention.

The signals parameter lists signal names (without @timestep) to declare as boolean variables at each timestep.

Example

use logicaffeine_verify::ir::{VerifyExpr, VerifyOp};
use logicaffeine_verify::equivalence::{check_equivalence, EquivalenceResult};

let fol = VerifyExpr::binary(VerifyOp::Implies,
    VerifyExpr::Var("req@0".into()),
    VerifyExpr::Var("ack@0".into()),
);
let sva = VerifyExpr::binary(VerifyOp::Implies,
    VerifyExpr::Var("req@0".into()),
    VerifyExpr::Var("ack@0".into()),
);
let result = check_equivalence(&fol, &sva, &["req".into(), "ack".into()], 1);
assert!(matches!(result, EquivalenceResult::Equivalent));