List of all items

Structs

• ArenaCounters
• Assumptions
• BitVec
• ConstraintId
• Context
• ContextConfig
• Expr
• ExprMap
• ExprSet
• Facts
• FnEnv
• KnownBits
• Mark
• Proof
• Reliance
• SRange
• Substitution
• SymbolId
• URange
• Width
• check::CheckConfig
• check::Counterexample
• check::Evidence
• check::Preemption
• check::RewriteCheckConfig
• check::RewriteReport
• check::RuleCheck
• engine::Admission
• engine::Allowance
• engine::Budget
• engine::CertStats
• engine::Deadline
• engine::Each
• engine::Engine
• engine::EngineBuilder
• engine::MbaStats
• engine::Outcome
• engine::PassCounts
• engine::RootOutcome
• engine::RuleCensus
• engine::RuleCounts
• engine::Run
• engine::Site
• engine::Stats
• engine::Strategy
• engine::Verify
• eqsat::AdmissionReport
• eqsat::EqsatStats
• eqsat::Fragment
• eqsat::SaturateConfig
• eqsat::Saturator
• eqsat::SearchReport
• eqsat::SearchRoot
• eqsat::SearchRun
• ext::ExtArgs
• ext::ExtId
• ext::ExtInverse
• ext::ExtSig
• ext::ExtTraits
• ext::Registry
• ext::RegistryBuilder
• fp::FpArgs
• fp::FpFormat
• lift::Block
• mba::Bindings
• mba::CacheKey
• mba::MNode
• mba::MbaBudget
• mba::MbaConfig
• mba::MbaExpr
• mba::MbaLimits
• mba::MbaTrust
• mba::MemoryCache
• mba::NativeProver
• mba::NfOptions
• mba::NfStats
• mba::NoCache
• mba::NormalFormSolver
• mba::Shape
• mba::SignatureSolver
• mba::ThreadedSolver
• memory::Memory
• memory::Version
• prove::Certificate
• prove::Config
• prove::Exhaustion
• prove::Question
• prove::Stats
• prove::WidthReport
• prove::aig::Aig
• prove::aig::Cnf
• prove::domain::Limits
• prove::domain::Stats
• prove::domain::TupleDomain
• prove::finite::CheckedPair
• prove::finite::VerifyLimits
• prove::sat::Limits
• prove::sat::Lit
• prove::sat::Solver
• rules::CompileError
• rules::CompileLimits
• rules::CompileOptions
• rules::Diagnostic
• rules::Ledger
• rules::RuleProgram
• rules::ir::FpNode
• rules::ir::Group
• rules::ir::LetDef
• rules::ir::Param
• rules::ir::Rule
• rules::ir::RuleId
• rules::ir::WExpr
• smtlib::Import
• synth::Config
• text::Display
• text::ParseOptions
• text::PrintOptions
• text::SyntaxError
• transform::Assignment
• transform::Config
• transform::Counterexample
• transform::FnText
• transform::Inference
• transform::Report
• transform::SyntaxError
• transform::ir::Block
• transform::ir::Body
• transform::ir::Inst
• transform::ir::InstAttrs
• transform::ir::ParamAttrs
• transform::ir::Transform
• translate::Lowered
• translate::Lowering
• translate::Template

Enums

• BinOp
• Bounded
• CmpOp
• CmpOpExt
• Error
• ParseError
• Query
• SymbolKey
• Truth
• UnOp
• ValueError
• View
• WidthError
• check::ExampleFailure
• check::PreemptionKind
• check::RewriteFailure
• check::Verdict
• engine::BuildError
• engine::By
• engine::Cap
• engine::Decline
• engine::End
• engine::Event
• engine::Exhausted
• engine::Phase
• engine::Reject
• engine::Sharing
• eqsat::Publication
• eqsat::RootEnd
• eqsat::UnsupportedPolicy
• ext::ExtError
• ext::InverseArg
• ext::Invertible
• fp::FpCmpOp
• fp::FpKind
• fp::FpOp
• fp::FpTest
• fp::RoundingMode
• mba::CacheEntry
• mba::Claim
• mba::MOp
• mba::MbaAnswer
• mba::MbaError
• mba::Refusal
• mba::Verdict
• memory::Endian
• prove::Outcome
• prove::RuleOutcome
• prove::SampleMode
• prove::Unknown
• prove::domain::Analysis
• prove::domain::Stop
• prove::finite::VerifyError
• prove::sat::Answer
• prove::sat::Step
• rules::Level
• rules::ir::ConstPred
• rules::ir::FactPred
• rules::ir::FloatLit
• rules::ir::Literal
• rules::ir::ParamKind
• rules::ir::RNode
• rules::ir::Rounding
• rules::ir::RuleKind
• rules::ir::Sort
• rules::ir::WCmp
• rules::ir::WCons
• transform::Mismatch
• transform::Shown
• transform::Verdict
• transform::ir::CFun
• transform::ir::FPred
• transform::ir::IPred
• transform::ir::Intrinsic
• transform::ir::Lit
• transform::ir::Node
• transform::ir::Op
• transform::ir::PFun
• transform::ir::Term
• transform::ir::Ty

Traits

• Env
• engine::Clock
• engine::Hooks
• engine::Observer
• engine::Rewrite
• ext::ExtOp
• mba::EquivalenceProver
• mba::MbaCacheStore
• mba::MbaSolver
• translate::Raise
• translate::Semantics

Functions

• check::check_examples
• check::check_program
• check::check_rule
• check::preempted
• check::preempted_rule
• check::rewrite
• ext::check
• fp::x87_load
• fp::x87_store
• lift::llvm
• lift::pcode
• lift::vex
• mba::lift
• mba::lower
• prove::blast::add
• prove::blast::add_carry
• prove::blast::and
• prove::blast::bitrev
• prove::blast::bswap
• prove::blast::clz
• prove::blast::count
• prove::blast::ctz
• prove::blast::eq
• prove::blast::konst
• prove::blast::mul
• prove::blast::mul_carry_save
• prove::blast::mulhi
• prove::blast::mux
• prove::blast::neg
• prove::blast::not
• prove::blast::or
• prove::blast::pdep
• prove::blast::pext
• prove::blast::popcnt
• prove::blast::rotate
• prove::blast::sdiv
• prove::blast::shift
• prove::blast::sle
• prove::blast::slt
• prove::blast::small
• prove::blast::srem
• prove::blast::sub
• prove::blast::udivrem
• prove::blast::ule
• prove::blast::ult
• prove::blast::xor
• prove::domain::analyze
• prove::drup::check
• prove::equal
• prove::rule
• prove::rule_all_widths
• prove::satisfy
• prove::valid
• prove::valid_under
• rules::builtin_sources
• rules::explain
• rules::lean::lean
• rules::lean::rule_instance
• rules::lean::rule_theorem
• smtlib::equivalence_query
• smtlib::equivalence_query_under
• smtlib::export
• smtlib::import
• smtlib::rule_obligation
• smtlib::satisfiability_query
• synth::synthesize
• transform::function_pair
• transform::functions
• transform::infer
• transform::ir::flags::parse
• transform::pairs
• transform::pairs_each
• transform::parse_transforms
• transform::smt
• transform::validate
• transform::verify
• traps::rotate
• traps::sdiv
• traps::shift
• traps::srem
• traps::udiv
• traps::urem

Type Aliases

• prove::Model
• prove::aig::L
• prove::blast::Bits
• prove::sat::Var
• rules::ir::NodeId
• transform::Pair
• transform::Question
• transform::ir::NodeId

Constants

• ext::MAX_ARGS
• ext::MAX_OPS
• ext::MAX_OUTPUTS
• prove::aig::FALSE
• prove::aig::TRUE
• transform::ir::flags::AFN
• transform::ir::flags::ARCP
• transform::ir::flags::CONTRACT
• transform::ir::flags::DISJOINT
• transform::ir::flags::EXACT
• transform::ir::flags::FAST_MATH
• transform::ir::flags::NINF
• transform::ir::flags::NNAN
• transform::ir::flags::NNEG
• transform::ir::flags::NSW
• transform::ir::flags::NSZ
• transform::ir::flags::NUW
• transform::ir::flags::REASSOC
• transform::ir::flags::REWRITE
• transform::ir::flags::SAMESIGN