Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred

This module contains the implementation of a bitblaster for predicates over BitVec expressions (BVPred).

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Std.Tactic.BVDecide.BVPred.bitblast_decl_eq (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (bitblast aig input).result.val.aig.decls.size) :
      (bitblast aig input).result.val.aig.decls[idx] = aig.decls[idx]