This module contains the implementation of a bitblaster for BitVec equality.
def
Std.Tactic.BVDecide.BVPred.mkEq
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(pair : aig.BinaryRefVec w)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkEq
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
:
Std.Sat.AIG.LawfulOperator α (fun (x : Std.Sat.AIG α) => x.BinaryRefVec w) Std.Tactic.BVDecide.BVPred.mkEq
Equations
- Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkEq = { le_size := ⋯, decl_eq := ⋯ }