logicaffeine_verify/
lib.rs

1#![cfg_attr(docsrs, feature(doc_cfg))]
2#![doc = include_str!("../README.md")]
3
4pub mod equivalence;
5pub mod consistency;
6pub mod error;
7pub mod ir;
8pub mod license;
9pub mod solver;
10pub mod type_infer;
11pub mod kinduction;
12pub mod interpolation;
13pub mod liveness;
14pub mod ic3;
15pub mod compositional;
16pub mod strategy;
17pub mod security;
18pub mod multiclock;
19pub mod parameterized;
20pub mod smtlib;
21pub mod certificate;
22pub mod incremental;
23pub mod abstraction;
24pub mod automata;
25pub mod synthesis;
26
27pub use equivalence::{check_equivalence, EquivalenceResult, Trace, CycleState, SignalValue};
28pub use consistency::{
29    check_consistency, check_spec_consistency,
30    ConsistencyResult, ConsistencyReport, ConsistencyConfig,
31    LabeledFormula, SatisfiabilityResult,
32    VacuityFinding, RedundancyFinding, PairwiseConflict,
33};
34pub use error::{VerificationError, VerificationErrorKind, VerificationResult};
35pub use ir::{BitVecOp, VerifyExpr, VerifyOp, VerifyType};
36pub use license::{LicensePlan, LicenseValidator};
37pub use solver::{rename_var_in_expr, Verifier, VerificationSession};
logicaffeine_verify/lib.rs

logicaffeine_verify/
lib.rs
