Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append

This module contains the implementation of a bitblaster for BitVec.append.

  • lw : Nat
  • rw : Nat
  • lhs : aig.RefVec self.lw
  • rhs : aig.RefVec self.rw
  • h : combined = self.rw + self.lw
Instances For
    theorem Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.h {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {combined : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined) :
    combined = self.rw + self.lw
    Equations
    Instances For
      instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend {α : Type} [Hashable α] [DecidableEq α] :
      Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend
      Equations
      • =