Documentation

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

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

source
structure Std.Tactic.BVDecide.Return (aig : Sat.AIG BVBit) :
Type
Instances For
    source
    def Std.Tactic.BVDecide.BVPred.bitblast (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
    Return aig
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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]
      source
      theorem Std.Tactic.BVDecide.BVPred.bitblast_le_size (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
      aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size