Documentation

Std.Tactic.BVDecide.Bitblast.EfficientEval

This module contains efficient evaluation for the reification data types of bv_decide, used for evaluating counterexamples during CEGAR.

source
def Std.Tactic.BVDecide.EfficientEval.BVExpr.evalEfficient {w : Nat} (assign : Nat → BVExpr.PackedBitVec) (expr : BVExpr w) :
BitVec w
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Std.Tactic.BVDecide.EfficientEval.BVPred.evalEfficient (assign : Nat → BVExpr.PackedBitVec) (expr : BVPred) :
    Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Std.Tactic.BVDecide.EfficientEval.BVLogicalExpr.evalEfficient (assign : Nat → BVExpr.PackedBitVec) (expr : BVLogicalExpr) :
      Bool
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For