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
    Equations
    • One or more equations did not get rendered due to their size.
    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]