From f241cc832b3750c464cac60a762463d88e25777a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 23 Mar 2025 14:05:01 +0100 Subject: [PATCH] perf: bv_decide don't drop the expression level cache (#7636) This PR makes sure that the expression level cache in bv_decide is maintained across the entire bitblaster instead of just locally per BitVec expression. The PR was split off from the first one (#7606) as this mostly entails pulling the invariant through and is thus much more mechanical. --- .../Bitblast/BVExpr/Circuit/Impl.lean | 16 +- .../Bitblast/BVExpr/Circuit/Impl/Expr.lean | 34 ++- .../Bitblast/BVExpr/Circuit/Impl/Pred.lean | 132 ++++++------ .../BVExpr/Circuit/Impl/Substructure.lean | 203 ++++++++++++++++++ .../Bitblast/BVExpr/Circuit/Lemmas.lean | 98 +++++++-- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 42 +++- .../Circuit/Lemmas/Operations/GetLsbD.lean | 3 +- .../Bitblast/BVExpr/Circuit/Lemmas/Pred.lean | 83 +++++-- .../Tactic/BVDecide/Bitblast/BoolExpr.lean | 4 +- .../BVDecide/Bitblast/BoolExpr/Circuit.lean | 162 -------------- tests/lean/run/aig_optimizations.lean | 20 +- tests/lean/run/aig_shared.lean | 48 ----- 12 files changed, 500 insertions(+), 345 deletions(-) create mode 100644 src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean delete mode 100644 src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean delete mode 100644 tests/lean/run/aig_shared.lean diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean index a7962f571a..90d10e263f 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean @@ -4,23 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude -import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred -import Std.Tactic.BVDecide.Bitblast.BoolExpr.Circuit +import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure /-! This module contains the implementation of a bitblaster for general `BitVec` problems with boolean substructure (`BVLogicalExpr`). It is the main entrypoint into the bitblasting framework. -/ - -namespace Std.Tactic.BVDecide - -open Std.Sat - -namespace BVLogicalExpr - -def bitblast (expr : BVLogicalExpr) : AIG.Entrypoint BVBit := - ofBoolExprCached expr BVPred.bitblast - -end BVLogicalExpr - -end Std.Tactic.BVDecide diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 62da1f0857..00433b2fbd 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -93,13 +93,18 @@ def Cache.cast (cache : Cache aig1) (h : aig1.decls.size ≤ aig2.decls.size) : · exact h ⟨map, this⟩ +structure WithCache (α : Type u) (aig : AIG BVBit) where + val : α + cache : Cache aig + structure Return (aig : AIG BVBit) (w : Nat) where result : AIG.ExtendingRefVecEntry aig w cache : Cache result.val.aig set_option maxHeartbeats 400000 in -def bitblast (aig : AIG BVBit) (expr : BVExpr w) : AIG.RefVecEntry BVBit w := - goCache aig expr .empty |>.result.val +def bitblast (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : Return aig w := + let ⟨expr, cache⟩ := input + goCache aig expr cache where goCache {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w := match cache.get? expr with @@ -370,15 +375,22 @@ end end bitblast -instance : AIG.LawfulVecOperator BVBit (fun _ w => BVExpr w) bitblast where - le_size := by - intro _ aig expr - unfold bitblast - exact (bitblast.goCache aig expr _).result.property - decl_eq := by - intros - unfold bitblast - apply bitblast.goCache_decl_eq +theorem bitblast_decl_eq (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : + ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + intros + unfold bitblast + apply bitblast.goCache_decl_eq + +theorem bitblast_le_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : + aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by + exact (bitblast aig input).result.property + +theorem bitblast_lt_size_of_lt_aig_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) + (h : x < aig.decls.size) : + x < (bitblast aig input).result.val.aig.decls.size := by + apply Nat.lt_of_lt_of_le + · exact h + · exact bitblast_le_size aig input end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean index d3e2728f76..1647738281 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean @@ -18,81 +18,89 @@ namespace Std.Tactic.BVDecide open Std.Sat +structure Return (aig : AIG BVBit) where + result : AIG.ExtendingEntrypoint aig + cache : BVExpr.Cache result.val.aig + namespace BVPred -def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit := +def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return aig := + let ⟨pred, cache⟩ := input match pred with | .bin lhs op rhs => - let res := lhs.bitblast aig - let aig := res.aig - let lhsRefs := res.vec - let res := rhs.bitblast aig - let aig := res.aig - let rhsRefs := res.vec - let lhsRefs := lhsRefs.cast <| AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast) .. + let ⟨⟨⟨aig, lhsRefs⟩, hlhs⟩, cache⟩ := BVExpr.bitblast aig ⟨lhs, cache⟩ + let ⟨⟨⟨aig, rhsRefs⟩, hrhs⟩, cache⟩ := BVExpr.bitblast aig ⟨rhs, cache⟩ + let lhsRefs := lhsRefs.cast hrhs match op with - | .eq => mkEq aig ⟨lhsRefs, rhsRefs⟩ - | .ult => mkUlt aig ⟨lhsRefs, rhsRefs⟩ + | .eq => + let res := mkEq aig ⟨lhsRefs, rhsRefs⟩ + let cache := cache.cast (AIG.LawfulOperator.le_size (f := mkEq) ..) + have := by + apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq) + dsimp only at hlhs hrhs + omega + ⟨⟨res, this⟩, cache⟩ + | .ult => + let res := mkUlt aig ⟨lhsRefs, rhsRefs⟩ + have := AIG.LawfulOperator.le_size (f := mkUlt) .. + let cache := cache.cast this + have := by + apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt) + dsimp only at hlhs hrhs + omega + ⟨⟨res, this⟩, cache⟩ | .getLsbD expr idx => /- Note: This blasts the entire expression up to `w` despite only needing it up to `idx`. However the vast majority of operations are interested in all bits so the API is currently not designed to support this use case. -/ - let res := expr.bitblast aig - let aig := res.aig - let refs := res.vec - blastGetLsbD aig ⟨refs, idx⟩ - -instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where - le_size := by - intro aig pred - unfold bitblast - cases pred with - | bin lhs op rhs => - cases op with - | eq => - apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq) - apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast) - apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast) - | ult => - apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt) - apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast) - apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast) - | getLsbD expr idx => + let ⟨⟨⟨aig, refs⟩, hrefs⟩, cache⟩ := BVExpr.bitblast aig ⟨expr, cache⟩ + let res := blastGetLsbD aig ⟨refs, idx⟩ + let cache := cache.cast (AIG.LawfulOperator.le_size (f := blastGetLsbD) ..) + have := by apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD) - apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast) - decl_eq := by - intro aig pred idx h1 h2 - cases pred with - | bin lhs op rhs => - cases op with - | eq => - simp only [bitblast] - rw [AIG.LawfulOperator.decl_eq (f := mkEq)] - rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)] - rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)] - · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast) - assumption - · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast) - apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast) - assumption - | ult => - simp only [bitblast] - rw [AIG.LawfulOperator.decl_eq (f := mkUlt)] - rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)] - rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)] - · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast) - assumption - · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast) - apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast) - assumption - | getLsbD expr idx => + exact hrefs + ⟨⟨res, this⟩, cache⟩ + +theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : + ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + intro idx h1 h2 + rcases input with ⟨pred, cache⟩ + unfold BVPred.bitblast + cases pred with + | bin lhs op rhs => + cases op with + | eq => + dsimp only + rw [AIG.LawfulOperator.decl_eq (f := mkEq)] + rw [BVExpr.bitblast_decl_eq] + rw [BVExpr.bitblast_decl_eq] + · apply BVExpr.bitblast_lt_size_of_lt_aig_size + assumption + · apply BVExpr.bitblast_lt_size_of_lt_aig_size + apply BVExpr.bitblast_lt_size_of_lt_aig_size + assumption + | ult => simp only [bitblast] - rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)] - rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)] - apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast) - assumption + rw [AIG.LawfulOperator.decl_eq (f := mkUlt)] + rw [BVExpr.bitblast_decl_eq] + rw [BVExpr.bitblast_decl_eq] + · apply BVExpr.bitblast_lt_size_of_lt_aig_size + assumption + · apply BVExpr.bitblast_lt_size_of_lt_aig_size + apply BVExpr.bitblast_lt_size_of_lt_aig_size + assumption + | getLsbD expr idx => + simp only [bitblast] + rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)] + rw [BVExpr.bitblast_decl_eq] + apply BVExpr.bitblast_lt_size_of_lt_aig_size + assumption + +theorem bitblast_le_size (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : + aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by + exact (bitblast aig input).result.property end BVPred diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean new file mode 100644 index 0000000000..42c071d0d1 --- /dev/null +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean @@ -0,0 +1,203 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred + +/-! +This module contains the logic to turn a `BVLogicalExpr` into an `AIG` with maximum subterm sharing, +through the use of a cache that re-uses sub-circuits if possible. Additionally a term level cache +is used to prevent rerunning bitblasting on commong bitvector subexpressions. +-/ + +namespace Std.Tactic.BVDecide + +open Std.Sat Std.Sat.AIG + +namespace BVLogicalExpr + +/-- +Turn a `BoolExpr` into an `Entrypoint`. +-/ +def bitblast (expr : BVLogicalExpr) : Entrypoint BVBit := + go AIG.empty expr .empty |>.result.val +where + go (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) : Return aig := + match expr with + | .literal var => BVPred.bitblast aig ⟨var, cache⟩ + | .const val => + have := LawfulOperator.le_size (f := mkConstCached) .. + ⟨⟨aig.mkConstCached val, this⟩, cache.cast this⟩ + | .not expr => + let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, cache⟩ := go aig expr cache + let ret := aig.mkNotCached exprRef + have := LawfulOperator.le_size (f := mkNotCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached) + exact hexpr + ⟨⟨ret, this⟩, cache⟩ + | .ite discr lhs rhs => + let ⟨⟨⟨aig, discrRef⟩, dextend⟩, cache⟩ := go aig discr cache + let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache + let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache + let discrRef := discrRef.cast <| by + dsimp only at lextend rextend ⊢ + omega + let lhsRef := lhsRef.cast <| by + dsimp only at rextend ⊢ + omega + + let input := ⟨discrRef, lhsRef, rhsRef⟩ + let ret := aig.mkIfCached input + have := LawfulOperator.le_size (f := mkIfCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkIfCached) + dsimp only at dextend lextend rextend + omega + ⟨⟨ret, this⟩, cache⟩ + | .gate g lhs rhs => + let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache + let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache + let lhsRef := lhsRef.cast <| by + dsimp only at rextend ⊢ + omega + let input := ⟨lhsRef, rhsRef⟩ + match g with + | .and => + let ret := aig.mkAndCached input + have := LawfulOperator.le_size (f := mkAndCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached) + dsimp only at lextend rextend + omega + ⟨⟨ret, this⟩, cache⟩ + | .xor => + let ret := aig.mkXorCached input + have := LawfulOperator.le_size (f := mkXorCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkXorCached) + dsimp only at lextend rextend + omega + ⟨⟨ret, this⟩, cache⟩ + | .beq => + let ret := aig.mkBEqCached input + have := LawfulOperator.le_size (f := mkBEqCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkBEqCached) + dsimp only at lextend rextend + omega + ⟨⟨ret, this⟩, cache⟩ + | .or => + let ret := aig.mkOrCached input + have := LawfulOperator.le_size (f := mkOrCached) .. + let cache := cache.cast this + have := by + apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached) + dsimp only at lextend rextend + omega + ⟨⟨ret, this⟩, cache⟩ + +namespace bitblast + +theorem go_le_size (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) : + aig.decls.size ≤ (go aig expr cache).result.val.aig.decls.size := + (go aig expr cache).result.property + +theorem go_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr) + (cache : BVExpr.Cache aig) (h : x < aig.decls.size) : + x < (go aig expr cache).result.val.aig.decls.size := by + apply Nat.lt_of_lt_of_le + · exact h + · apply go_le_size + +theorem go_decl_eq (idx) (aig : AIG BVBit) (cache : BVExpr.Cache aig) (h : idx < aig.decls.size) (hbounds) : + (go aig expr cache).result.val.aig.decls[idx]'hbounds = aig.decls[idx] := by + induction expr generalizing aig with + | const => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)] + | literal => + simp only [go] + rw [BVPred.bitblast_decl_eq] + | not expr ih => + simp only [go] + have := go_le_size aig expr cache + specialize ih aig cache (by omega) (by omega) + rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)] + assumption + | ite discr lhs rhs dih lih rih => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih] + · apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + | gate g lhs rhs lih rih => + cases g with + | and => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih] + · apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + | xor => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih] + · apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + | beq => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih] + · apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + | or => + simp only [go] + rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih] + · apply go_lt_size_of_lt_aig_size + assumption + · apply go_lt_size_of_lt_aig_size + apply go_lt_size_of_lt_aig_size + assumption + +theorem go_isPrefix_aig {aig : AIG BVBit} (cache : BVExpr.Cache aig) : + IsPrefix aig.decls (go aig expr cache).result.val.aig.decls := by + apply IsPrefix.of + · intro idx h + apply go_decl_eq + · apply go_le_size + +theorem go_denote_mem_prefix (aig : AIG BVBit) (cache : BVExpr.Cache aig) (hstart) : + ⟦ + (go aig expr cache).result.val.aig, + ⟨start, inv, go_lt_size_of_lt_aig_size (h := hstart) ..⟩, + assign + ⟧ + = + ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) + apply go_isPrefix_aig + +end bitblast +end BVLogicalExpr + +end Std.Tactic.BVDecide diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean index 81804adfa9..7e3491b8cb 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean @@ -20,25 +20,99 @@ open Std.Sat.AIG namespace BVLogicalExpr -theorem bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) : - ⟦ofBoolExprCached.go aig expr BVPred.bitblast, assign.toAIGAssignment⟧ = expr.eval assign := by +namespace bitblast + +mutual + +theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) + (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) : + BVExpr.Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache := by induction expr generalizing aig with - | const => simp [ofBoolExprCached.go] - | literal => simp [ofBoolExprCached.go] - | not expr ih => simp [ofBoolExprCached.go, ih] - | gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih] + | const => + simp only [go] + apply BVExpr.Cache.Inv_cast + apply LawfulOperator.isPrefix_aig (f := mkConstCached) + exact hinv + | literal => + simp only [go] + apply BVPred.bitblast_Inv_of_Inv + exact hinv + | not expr ih => + simp only [go] + apply BVExpr.Cache.Inv_cast + · apply LawfulOperator.isPrefix_aig (f := mkNotCached) + · apply ih + exact hinv + | gate g lhs rhs lih rih => + cases g + all_goals + simp [go, Gate.eval] + apply BVExpr.Cache.Inv_cast + · apply LawfulOperator.isPrefix_aig + · apply rih + apply lih + exact hinv | ite discr lhs rhs dih lih rih => - simp only [ofBoolExprCached.go, Ref.cast_eq, denote_mkIfCached, - ofBoolExprCached.go_denote_entry, eval_ite] - rw [ofBoolExprCached.go_denote_mem_prefix, ofBoolExprCached.go_denote_mem_prefix] - · simp [dih, lih, rih] - · simp [Ref.hgate] + simp only [go] + apply BVExpr.Cache.Inv_cast + · apply LawfulOperator.isPrefix_aig (f := mkIfCached) + · apply rih + apply lih + apply dih + exact hinv + +theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) + (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) : + ⟦(go aig expr cache).result, assign.toAIGAssignment⟧ = expr.eval assign := by + induction expr generalizing aig with + | const => simp [go] + | literal => + simp only [go, eval_literal] + rw [BVPred.denote_bitblast] + exact hinv + | not expr ih => + specialize ih _ _ hinv + simp [go, ih] + | gate g lhs rhs lih rih => + cases g + all_goals + simp [go, Gate.eval] + congr 1 + · rw [go_denote_mem_prefix] + apply lih + exact hinv + · apply rih + apply go_Inv_of_Inv + exact hinv + | ite discr lhs rhs dih lih rih => + simp only [go, Ref.cast_eq, denote_mkIfCached, denote_projected_entry, + eval_ite, Bool.ite_eq_cond_iff] + apply ite_congr + · rw [go_denote_mem_prefix] + rw [go_denote_mem_prefix] + · specialize dih _ _ hinv + simp [dih] + · simp [Ref.hgate] + · intro h + rw [go_denote_mem_prefix] + apply lih + apply go_Inv_of_Inv + exact hinv + · intro h + apply rih + apply go_Inv_of_Inv + apply go_Inv_of_Inv + exact hinv + +end + +end bitblast theorem denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) : ⟦bitblast expr, assign.toAIGAssignment⟧ = expr.eval assign := by unfold bitblast - unfold ofBoolExprCached rw [bitblast.go_eval_eq_eval] + apply BVExpr.Cache.Inv_empty theorem unsat_of_bitblast (expr : BVLogicalExpr) : expr.bitblast.Unsat → expr.Unsat := by intro h assign diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index ac5d0a7422..67f916f362 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -121,8 +121,8 @@ end Cache namespace bitblast -theorem goCache_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) : - (goCache aig expr .empty).result.val = bitblast aig expr := by +theorem goCache_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : + goCache aig expr cache = bitblast aig ⟨expr, cache⟩ := by rfl theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) @@ -478,20 +478,46 @@ termination_by idx => (sizeOf expr, 0, idx) end - end bitblast -@[simp] -theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : +theorem bitblast_aig_IsPrefix (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : + IsPrefix aig.decls (bitblast aig input).result.val.aig.decls := by + apply IsPrefix.of + · intros + apply bitblast_decl_eq + · intros + apply (bitblast aig input).result.property + +theorem bitblast_denote_mem_prefix (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) + (assign : Assignment) (start : Nat) (hstart) : + ⟦ + (bitblast aig input).result.val.aig, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (bitblast aig input).result.property⟩, + assign.toAIGAssignment + ⟧ + = + ⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) + apply bitblast_aig_IsPrefix + +theorem bitblast_Inv_of_Inv (input : WithCache (BVExpr w) aig) + (hinv : Cache.Inv assign aig input.cache) : + Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache := by + unfold bitblast + apply bitblast.goCache_Inv_of_Inv + exact hinv + +theorem denote_bitblast (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : Assignment) + (hinv : Cache.Inv assign aig input.cache) : ∀ (idx : Nat) (hidx : idx < w), - ⟦(bitblast aig expr).aig, (bitblast aig expr).vec.get idx hidx, assign.toAIGAssignment⟧ + ⟦(bitblast aig input).result.val.aig, (bitblast aig input).result.val.vec.get idx hidx, assign.toAIGAssignment⟧ = - (expr.eval assign).getLsbD idx + (input.val.eval assign).getLsbD idx := by intros rw [← bitblast.goCache_val_eq_bitblast] rw [bitblast.goCache_denote_eq] - apply Cache.Inv_empty + exact hinv end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean index c3ba9d088f..e456f1d347 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean @@ -35,8 +35,7 @@ theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec omega @[simp] -theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) - (assign : α → Bool) : +theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) (assign : α → Bool) : ⟦blastGetLsbD aig target, assign⟧ = if h : target.idx < target.w then diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean index ddd3f678f2..0e0117a07d 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean @@ -22,9 +22,58 @@ open Std.Sat.AIG namespace BVPred -@[simp] -theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assignment) : - ⟦bitblast aig pred, assign.toAIGAssignment⟧ = pred.eval assign := by +theorem bitblast_aig_IsPrefix (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : + IsPrefix aig.decls (bitblast aig input).result.val.aig.decls := by + apply IsPrefix.of + · intros + apply bitblast_decl_eq + · intros + apply (bitblast aig input).result.property + +theorem bitblast_denote_mem_prefix (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) + (assign : BVExpr.Assignment) (start : Nat) (hstart) : + ⟦ + (bitblast aig input).result.val.aig, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (bitblast aig input).result.property⟩, + assign.toAIGAssignment + ⟧ + = + ⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) + apply bitblast_aig_IsPrefix + +theorem bitblast_Inv_of_Inv (input : BVExpr.WithCache BVPred aig) + (hinv : BVExpr.Cache.Inv assign aig input.cache) : + BVExpr.Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache := by + unfold bitblast + dsimp only + split + · next op _ _ => + cases op + · dsimp only + apply BVExpr.Cache.Inv_cast + · apply AIG.LawfulOperator.isPrefix_aig (f := mkEq) + · apply BVExpr.bitblast_Inv_of_Inv + apply BVExpr.bitblast_Inv_of_Inv + exact hinv + · dsimp only + apply BVExpr.Cache.Inv_cast + · apply AIG.LawfulOperator.isPrefix_aig (f := mkUlt) + · apply BVExpr.bitblast_Inv_of_Inv + apply BVExpr.bitblast_Inv_of_Inv + exact hinv + · dsimp only + apply BVExpr.Cache.Inv_cast + · apply AIG.LawfulOperator.isPrefix_aig (f := blastGetLsbD) + · apply BVExpr.bitblast_Inv_of_Inv + exact hinv + +theorem denote_bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) + (assign : BVExpr.Assignment) (hinv : BVExpr.Cache.Inv assign aig input.cache ) : + ⟦(bitblast aig input).result.val.aig, (bitblast aig input).result.val.ref, assign.toAIGAssignment⟧ + = + input.val.eval assign := by + rcases input with ⟨pred, cache⟩ cases pred with | bin lhs op rhs => cases op with @@ -32,26 +81,36 @@ theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assig simp only [bitblast, eval_bin, BVBinPred.eval_eq] rw [mkEq_denote_eq] · intros - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)] - · simp + rw [BVExpr.bitblast_denote_mem_prefix] + · simp only [RefVec.get_cast, Ref.cast_eq] rw [BVExpr.denote_bitblast] + exact hinv · simp [Ref.hgate] · intros - simp + rw [BVExpr.denote_bitblast] + apply BVExpr.bitblast_Inv_of_Inv + exact hinv | ult => simp only [bitblast, eval_bin, BVBinPred.eval_ult] rw [mkUlt_denote_eq] · intros - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)] - · simp + rw [BVExpr.bitblast_denote_mem_prefix] + · simp only [RefVec.get_cast, Ref.cast_eq] rw [BVExpr.denote_bitblast] + exact hinv · simp [Ref.hgate] · intros - simp + rw [BVExpr.denote_bitblast] + apply BVExpr.bitblast_Inv_of_Inv + exact hinv | getLsbD expr idx => - simp only [bitblast, denote_blastGetLsbD, BVExpr.denote_bitblast, dite_eq_ite, - Bool.if_false_right, eval_getLsbD, Bool.and_iff_right_iff_imp, decide_eq_true_eq] - apply BitVec.lt_of_getLsbD + simp only [bitblast, denote_projected_entry, denote_blastGetLsbD, eval_getLsbD] + split + · rw [BVExpr.denote_bitblast] + exact hinv + · symm + apply BitVec.getLsbD_ge + omega end BVPred diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean index 1f408d11b0..78140d46fb 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean @@ -5,9 +5,7 @@ Authors: Henrik Böving -/ prelude import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic -import Std.Tactic.BVDecide.Bitblast.BoolExpr.Circuit /-! -This directory contains the definition and bitblaster of generic boolean substructures for -SMT-like problems. +This directory contains the definition of generic boolean substructures for SMT-like problems. -/ diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean deleted file mode 100644 index 6dce59215f..0000000000 --- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean +++ /dev/null @@ -1,162 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Henrik Böving --/ -prelude -import Std.Sat.AIG.CachedGates -import Std.Sat.AIG.CachedGatesLemmas -import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic -import Std.Sat.AIG.If - -/-! -This module contains the logic to turn a `BoolExpr Nat` into an `AIG` with maximum subterm sharing, -through the use of a cache that re-uses sub-circuits if possible. --/ - -namespace Std.Tactic.BVDecide - -open Std.Sat Std.Sat.AIG - -variable {β : Type} [Hashable β] [DecidableEq β] - -/-- -Turn a `BoolExpr` into an `Entrypoint`. --/ -@[specialize] -def ofBoolExprCached (expr : BoolExpr α) (atomHandler : AIG β → α → Entrypoint β) - [LawfulOperator β (fun _ => α) atomHandler] : Entrypoint β := - go AIG.empty expr atomHandler |>.val -where - @[specialize] - go (aig : AIG β) (expr : BoolExpr α) (atomHandler : AIG β → α → Entrypoint β) - [LawfulOperator β (fun _ => α) atomHandler] : - ExtendingEntrypoint aig := - match expr with - | .literal var => ⟨atomHandler aig var, by apply LawfulOperator.le_size⟩ - | .const val => ⟨aig.mkConstCached val, (by apply LawfulOperator.le_size)⟩ - | .not expr => - let ⟨⟨aig, exprRef⟩, _⟩ := go aig expr atomHandler - let ret := aig.mkNotCached exprRef - have := LawfulOperator.le_size (f := mkNotCached) aig exprRef - ⟨ret, by dsimp only [ret] at *; omega⟩ - | .ite discr lhs rhs => - let ⟨⟨aig, discrRef⟩, dextend⟩ := go aig discr atomHandler - let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler - let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler - let discrRef := discrRef.cast <| by - dsimp only at lextend rextend ⊢ - omega - let lhsRef := lhsRef.cast <| by - dsimp only at rextend ⊢ - omega - - let input := ⟨discrRef, lhsRef, rhsRef⟩ - let ret := aig.mkIfCached input - have := LawfulOperator.le_size (f := mkIfCached) aig input - ⟨ret, by dsimp only [ret] at lextend rextend dextend ⊢; omega⟩ - | .gate g lhs rhs => - let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler - let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler - let lhsRef := lhsRef.cast <| by - dsimp only at rextend ⊢ - omega - let input := ⟨lhsRef, rhsRef⟩ - match g with - | .and => - let ret := aig.mkAndCached input - have := LawfulOperator.le_size (f := mkAndCached) aig input - ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩ - | .xor => - let ret := aig.mkXorCached input - have := LawfulOperator.le_size (f := mkXorCached) aig input - ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩ - | .beq => - let ret := aig.mkBEqCached input - have := LawfulOperator.le_size (f := mkBEqCached) aig input - ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩ - | .or => - let ret := aig.mkOrCached input - have := LawfulOperator.le_size (f := mkOrCached) aig input - ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩ - -namespace ofBoolExprCached - -variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler] - -theorem go_le_size (expr : BoolExpr α) (aig : AIG β) : - aig.decls.size ≤ (ofBoolExprCached.go aig expr atomHandler).val.aig.decls.size := - (ofBoolExprCached.go aig expr atomHandler).property - -theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) : - (ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx]'hbounds = aig.decls[idx] := by - induction expr generalizing aig with - | const => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)] - | literal => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := atomHandler)] - | not expr ih => - simp only [go] - have := go_le_size atomHandler expr aig - specialize ih aig (by omega) (by omega) - rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)] - assumption - | ite discr lhs rhs dih lih rih => - have := go_le_size atomHandler discr aig - have := go_le_size atomHandler lhs (go aig discr atomHandler).val.aig - have := go_le_size atomHandler rhs (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig - specialize dih aig (by omega) (by omega) - specialize lih (go aig discr atomHandler).val.aig (by omega) (by omega) - specialize rih (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig (by omega) (by omega) - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih] - | gate g lhs rhs lih rih => - have := go_le_size atomHandler lhs aig - have := go_le_size atomHandler rhs (go aig lhs atomHandler).val.aig - specialize lih aig (by omega) (by omega) - specialize rih (go aig lhs atomHandler).val.aig (by omega) (by omega) - cases g with - | and => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih] - | xor => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih] - | beq => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih] - | or => - simp only [go] - rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih] - -theorem go_isPrefix_aig {aig : AIG β} : - IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by - apply IsPrefix.of - · intro idx h - apply ofBoolExprCached.go_decl_eq - · apply go_le_size - -theorem go_denote_mem_prefix : - ⟦ - (go aig expr atomHandler).val.aig, - ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩, - assign - ⟧ - = - ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by - apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) - apply go_isPrefix_aig - -@[simp] -theorem go_denote_entry (entry : Entrypoint β) {h} : - ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧ - = - ⟦entry, assign⟧ := by - apply denote.eq_of_isPrefix - apply ofBoolExprCached.go_isPrefix_aig - -end ofBoolExprCached - -end Std.Tactic.BVDecide diff --git a/tests/lean/run/aig_optimizations.lean b/tests/lean/run/aig_optimizations.lean index 13e8394125..1929e16141 100644 --- a/tests/lean/run/aig_optimizations.lean +++ b/tests/lean/run/aig_optimizations.lean @@ -1,9 +1,9 @@ -import Std.Tactic.BVDecide.Bitblast.BoolExpr +import Std.Tactic.BVDecide.Bitblast open Std.Sat open Std.Tactic.BVDecide -def mkFalseCollapsible (n : Nat) : BoolExpr Nat := +def mkFalseCollapsible (n : Nat) : BVLogicalExpr := match n with | 0 => .const false | n + 1 => @@ -12,13 +12,13 @@ def mkFalseCollapsible (n : Nat) : BoolExpr Nat := /-- info: #[Std.Sat.AIG.Decl.const false] -/ #guard_msgs in -#eval ofBoolExprCached (mkFalseCollapsible 1) AIG.mkAtomCached |>.aig.decls +#eval BVLogicalExpr.bitblast (mkFalseCollapsible 1) |>.aig.decls /-- info: #[Std.Sat.AIG.Decl.const false] -/ #guard_msgs in -#eval ofBoolExprCached (mkFalseCollapsible 16) AIG.mkAtomCached |>.aig.decls +#eval BVLogicalExpr.bitblast (mkFalseCollapsible 16) |>.aig.decls -def mkTrueCollapsible (n : Nat) : BoolExpr Nat := +def mkTrueCollapsible (n : Nat) : BVLogicalExpr := match n with | 0 => .const true | n + 1 => @@ -27,13 +27,13 @@ def mkTrueCollapsible (n : Nat) : BoolExpr Nat := /-- info: #[Std.Sat.AIG.Decl.const true] -/ #guard_msgs in -#eval ofBoolExprCached (mkTrueCollapsible 1) AIG.mkAtomCached |>.aig.decls +#eval BVLogicalExpr.bitblast (mkTrueCollapsible 1) |>.aig.decls /-- info: #[Std.Sat.AIG.Decl.const true] -/ #guard_msgs in -#eval ofBoolExprCached (mkTrueCollapsible 16) AIG.mkAtomCached |>.aig.decls +#eval BVLogicalExpr.bitblast (mkTrueCollapsible 16) |>.aig.decls -def mkConstantCollapsible (n : Nat) : BoolExpr Nat := +def mkConstantCollapsible (n : Nat) : BVLogicalExpr := match n with | 0 => .const false | n + 1 => @@ -43,11 +43,11 @@ def mkConstantCollapsible (n : Nat) : BoolExpr Nat := /-- info: (2, Std.Sat.AIG.Decl.const false) -/ #guard_msgs in #eval - let entry := ofBoolExprCached (mkConstantCollapsible 1) AIG.mkAtomCached + let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 1) (entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!) /-- info: (2, Std.Sat.AIG.Decl.const false) -/ #guard_msgs in #eval - let entry := ofBoolExprCached (mkConstantCollapsible 16) AIG.mkAtomCached + let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 16) (entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!) diff --git a/tests/lean/run/aig_shared.lean b/tests/lean/run/aig_shared.lean deleted file mode 100644 index 0aa1b129b2..0000000000 --- a/tests/lean/run/aig_shared.lean +++ /dev/null @@ -1,48 +0,0 @@ -import Std.Tactic.BVDecide.Bitblast.BoolExpr - -open Std.Sat -open Std.Tactic.BVDecide - -def mkSharedTree (n : Nat) : BoolExpr Nat := - match n with - | 0 => .literal 0 - | n + 1 => - let tree := mkSharedTree n - .gate .xor tree tree - -/-- -info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true] --/ -#guard_msgs in -#eval ofBoolExprCached (mkSharedTree 1) AIG.mkAtomCached |>.aig.decls - -/-- -info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true, - Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true] --/ -#guard_msgs in -#eval ofBoolExprCached (mkSharedTree 2) AIG.mkAtomCached |>.aig.decls - -/-- -info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true, - Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true, - Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true] --/ -#guard_msgs in -#eval ofBoolExprCached (mkSharedTree 4) AIG.mkAtomCached |>.aig.decls - -/-- -info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true, - Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true, - Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true, - Std.Sat.AIG.Decl.gate 8 8 true true, Std.Sat.AIG.Decl.gate 8 9 true true, Std.Sat.AIG.Decl.gate 10 10 true true, - Std.Sat.AIG.Decl.gate 10 11 true true, Std.Sat.AIG.Decl.gate 12 12 true true, Std.Sat.AIG.Decl.gate 12 13 true true, - Std.Sat.AIG.Decl.gate 14 14 true true, Std.Sat.AIG.Decl.gate 14 15 true true, Std.Sat.AIG.Decl.gate 16 16 true true, - Std.Sat.AIG.Decl.gate 16 17 true true, Std.Sat.AIG.Decl.gate 18 18 true true, Std.Sat.AIG.Decl.gate 18 19 true true, - Std.Sat.AIG.Decl.gate 20 20 true true, Std.Sat.AIG.Decl.gate 20 21 true true, Std.Sat.AIG.Decl.gate 22 22 true true, - Std.Sat.AIG.Decl.gate 22 23 true true, Std.Sat.AIG.Decl.gate 24 24 true true, Std.Sat.AIG.Decl.gate 24 25 true true, - Std.Sat.AIG.Decl.gate 26 26 true true, Std.Sat.AIG.Decl.gate 26 27 true true, Std.Sat.AIG.Decl.gate 28 28 true true, - Std.Sat.AIG.Decl.gate 28 29 true true, Std.Sat.AIG.Decl.gate 30 30 true true, Std.Sat.AIG.Decl.gate 30 31 true true] --/ -#guard_msgs in -#eval ofBoolExprCached (mkSharedTree 16) AIG.mkAtomCached |>.aig.decls