HepLean Documentation

Std.Tactic.BVDecide.Bitblast

This directory contains the implementation of the bitblaster itself. It is split up into two parts:

  1. Bitblasting of generic boolean substructures for SMT-like problems in BoolExpr.
  2. The specific bitblaster for BitVec problems with boolean substructure in BVExpr.