∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (n : α) (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false),
  { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.mkAtomCached n =
    match cache.get? (Std.Sat.AIG.Decl.atom n) with
    | some hit =>
      { aig := { decls := decls, cache := cache, hdag := ⋯, hzero := hzero, hconst := hconst },
        ref := { gate := hit.idx, invert := false, hgate := ⋯ } }
    | none =>
      let g := decls.size;
      have cache_1 := Std.Sat.AIG.Cache.insert decls cache (Std.Sat.AIG.Decl.atom n);
      let decls_1 := decls.push (Std.Sat.AIG.Decl.atom n);
      have hdag := ⋯;
      have hzero' := ⋯;
      have hconst := ⋯;
      { aig := { decls := decls_1, cache := cache_1, hdag := hdag, hzero := hzero', hconst := hconst },
        ref := { gate := g, invert := false, hgate := ⋯ } }