Documentation

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

This module contains the implementation of a bitblaster for BitVec expressions (BVExpr). That is, expressions that evaluate to BitVec again. Its used as a building block in bitblasting general BitVec problems with boolean substructure.

Instances For
    Instances For
      @[inline]
      Equations
        Instances For
          @[inline]
          def Std.Tactic.BVDecide.BVExpr.Cache.insert {aig : Sat.AIG BVBit} {w : Nat} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) :
          Cache aig
          Equations
            Instances For
              @[inline]
              def Std.Tactic.BVDecide.BVExpr.Cache.get? {aig : Sat.AIG BVBit} {w : Nat} (cache : Cache aig) (expr : BVExpr w) :
              Option (aig.RefVec w)
              Equations
                Instances For
                  @[inline]
                  def Std.Tactic.BVDecide.BVExpr.Cache.cast {aig1 aig2 : Sat.AIG BVBit} (cache : Cache aig1) (h : aig1.decls.size aig2.decls.size) :
                  Cache aig2
                  Equations
                    Instances For
                      • val : α
                      • cache : Cache aig
                      Instances For
                        Instances For
                          def Std.Tactic.BVDecide.BVExpr.bitblast {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) :
                          Return aig w
                          Equations
                            Instances For
                              @[irreducible]
                              def Std.Tactic.BVDecide.BVExpr.bitblast.goCache {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
                              Return aig w
                              Equations
                                Instances For
                                  @[irreducible]
                                  def Std.Tactic.BVDecide.BVExpr.bitblast.go {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
                                  Return aig w
                                  Equations
                                    Instances For
                                      @[irreducible]
                                      theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (goCache aig expr cache).result.val.aig.decls.size) :
                                      (goCache aig expr cache).result.val.aig.decls[idx] = aig.decls[idx]
                                      @[irreducible]
                                      theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr cache).result.val.aig.decls.size) :
                                      (go aig expr cache).result.val.aig.decls[idx] = aig.decls[idx]
                                      theorem Std.Tactic.BVDecide.BVExpr.bitblast_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) 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]