Skip to content
This repository was archived by the owner on Aug 29, 2024. It is now read-only.

Commit

Permalink
fix: tests that got trivialized by new AIG rules
Browse files Browse the repository at this point in the history
  • Loading branch information
@hargoniX
hargoniX committed Jun 25, 2024
1 parent 0eedbf0 commit 55dcf0e
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 76 deletions.
28 changes: 18 additions & 10 deletions Test/AIG/Shared.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,29 +5,37 @@ def mkSharedTree (n : Nat) : BoolExpr Nat :=
| 0 => .literal 0
| n + 1 =>
let tree := mkSharedTree n
.gate .and tree tree
.gate .or tree tree

/-- info: #[Decl.atom 0, Decl.gate 0 0 false false] -/
/-- info: #[Decl.atom 0, Decl.gate 0 0 true true, Decl.const true, Decl.gate 1 2 true false] -/
#guard_msgs in
#eval AIG.ofBoolExprCachedDirect (mkSharedTree 1) |>.aig.decls

/-- info: #[Decl.atom 0, Decl.gate 0 0 false false, Decl.gate 1 1 false false] -/
/--
info: #[Decl.atom 0, Decl.gate 0 0 true true, Decl.const true, Decl.gate 1 2 true false, Decl.gate 3 3 true true,
Decl.gate 2 4 false true]
-/
#guard_msgs in
#eval AIG.ofBoolExprCachedDirect (mkSharedTree 2) |>.aig.decls

/--
info: #[Decl.atom 0, Decl.gate 0 0 false false, Decl.gate 1 1 false false, Decl.gate 2 2 false false,
Decl.gate 3 3 false false]
info: #[Decl.atom 0, Decl.gate 0 0 true true, Decl.const true, Decl.gate 1 2 true false, Decl.gate 3 3 true true,
Decl.gate 2 4 false true, Decl.gate 5 5 true true, Decl.gate 2 6 false true, Decl.gate 7 7 true true,
Decl.gate 2 8 false true]
-/
#guard_msgs in
#eval AIG.ofBoolExprCachedDirect (mkSharedTree 4) |>.aig.decls

/--
info: #[Decl.atom 0, Decl.gate 0 0 false false, Decl.gate 1 1 false false, Decl.gate 2 2 false false,
Decl.gate 3 3 false false, Decl.gate 4 4 false false, Decl.gate 5 5 false false, Decl.gate 6 6 false false,
Decl.gate 7 7 false false, Decl.gate 8 8 false false, Decl.gate 9 9 false false, Decl.gate 10 10 false false,
Decl.gate 11 11 false false, Decl.gate 12 12 false false, Decl.gate 13 13 false false, Decl.gate 14 14 false false,
Decl.gate 15 15 false false]
info: #[Decl.atom 0, Decl.gate 0 0 true true, Decl.const true, Decl.gate 1 2 true false, Decl.gate 3 3 true true,
Decl.gate 2 4 false true, Decl.gate 5 5 true true, Decl.gate 2 6 false true, Decl.gate 7 7 true true,
Decl.gate 2 8 false true, Decl.gate 9 9 true true, Decl.gate 2 10 false true, Decl.gate 11 11 true true,
Decl.gate 2 12 false true, Decl.gate 13 13 true true, Decl.gate 2 14 false true, Decl.gate 15 15 true true,
Decl.gate 2 16 false true, Decl.gate 17 17 true true, Decl.gate 2 18 false true, Decl.gate 19 19 true true,
Decl.gate 2 20 false true, Decl.gate 21 21 true true, Decl.gate 2 22 false true, Decl.gate 23 23 true true,
Decl.gate 2 24 false true, Decl.gate 25 25 true true, Decl.gate 2 26 false true, Decl.gate 27 27 true true,
Decl.gate 2 28 false true, Decl.gate 29 29 true true, Decl.gate 2 30 false true, Decl.gate 31 31 true true,
Decl.gate 2 32 false true]
-/
#guard_msgs in
#eval AIG.ofBoolExprCachedDirect (mkSharedTree 16) |>.aig.decls
69 changes: 3 additions & 66 deletions Test/Bv/Trace.lean-trace_unit_1-8-2.lrat
View file
Original file line number Diff line number Diff line change
@@ -1,66 +1,3 @@
199 -705 0 1 3 0
200 -642 -704 0 199 7 0
201 642 0 197 196 0
202 -704 0 201 200 0
203 643 0 201 193 0
204 -703 0 202 201 10 0
205 644 0 203 201 190 0
206 -702 0 204 201 13 0
207 645 0 205 201 187 0
208 -701 0 206 201 16 0
209 646 0 207 201 184 0
210 -700 0 208 201 19 0
211 647 0 209 201 181 0
212 -699 0 210 201 22 0
213 648 0 211 201 178 0
214 -698 0 212 201 25 0
215 649 0 213 201 175 0
216 -697 0 214 201 28 0
217 650 0 215 201 172 0
218 -696 0 216 201 31 0
219 651 0 217 201 169 0
220 -695 0 218 201 34 0
221 652 0 219 201 166 0
222 -694 0 220 201 37 0
223 653 0 221 201 163 0
224 -693 0 222 201 40 0
225 654 0 223 201 160 0
226 -692 0 224 201 43 0
227 655 0 225 201 157 0
228 -691 0 226 201 46 0
229 656 0 227 201 154 0
230 -690 0 228 201 49 0
231 657 0 229 201 151 0
232 -689 0 230 201 52 0
233 658 0 231 201 148 0
234 -688 0 232 201 55 0
235 659 0 233 201 145 0
236 -687 0 234 201 58 0
237 660 0 235 201 142 0
238 -686 0 236 201 61 0
239 661 0 237 201 139 0
240 -685 0 238 201 64 0
241 662 0 239 201 136 0
242 -684 0 240 201 67 0
243 663 0 241 201 133 0
244 -683 0 242 201 70 0
245 664 0 243 201 130 0
246 -682 0 244 201 73 0
247 665 0 245 201 127 0
248 -681 0 246 201 76 0
249 666 0 247 201 124 0
250 -680 0 248 201 79 0
251 667 0 249 201 121 0
252 -679 0 250 201 82 0
253 668 0 251 201 118 0
254 -678 0 252 201 85 0
255 669 0 253 201 115 0
256 -677 0 254 201 88 0
257 670 0 255 201 112 0
258 -676 0 256 201 91 0
259 671 0 257 201 109 0
260 -675 0 258 201 94 0
261 672 0 259 201 106 0
262 -674 0 260 201 97 0
263 673 0 261 201 103 0
264 0 262 263 201 100 0
10 -642 0 1 3 0
11 130 0 10 7 0
12 0 11 8 0

0 comments on commit 55dcf0e

Please sign in to comment.