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
        • { map := map, hbound := hbound }.insert expr refs = { map := map.insert { w := w, expr := expr } refs.refs, hbound := }
        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
          • One or more equations did not get rendered due to their size.
          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
            • { map := map, hbound := hbound }.cast h = { map := map, hbound := }
            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
                    • One or more equations did not get rendered due to their size.
                    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]