-
Notifications
You must be signed in to change notification settings - Fork 2
/
bex.leo
970 lines (815 loc) · 41.9 KB
/
bex.leo
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
<?xml version="1.0" encoding="utf-8"?>
<!-- Created by Leo: http://leoeditor.com/leo_toc.html -->
<leo_file xmlns:leo="http://leoeditor.com/namespaces/leo-python-editor/1.1" >
<leo_header file_format="2"/>
<globals/>
<preferences/>
<find_panel_settings/>
<vnodes>
<v t="tangentstorm.20220203082928.1"><vh>bex concepts</vh>
<v t="tangentstorm.20220203082928.2"><vh>nids and vids</vh>
<v t="tangentstorm.20220203082928.3"><vh>O and I</vh>
<v t="tangentstorm.20220203082928.4"><vh>boolean constants (nid.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082928.5"><vh>virs and vars</vh></v>
<v t="tangentstorm.20220203082928.6"><vh>funs</vh></v>
</v>
<v t="tangentstorm.20220203082928.7"><vh>ops</vh></v>
<v t="tangentstorm.20220203082928.8"><vh>ast</vh></v>
</v>
<v t="tangentstorm.20220203082937.1"><vh>upcoming features</vh>
<v t="tangentstorm.20220203082937.2"><vh>bex world solver</vh></v>
</v>
<v t="tangentstorm.20220203082953.1"><vh>@path d:/ver/bex/src</vh>
<v t="tangentstorm.20220203082953.2"><vh>@clean vid.rs</vh>
<v t="tangentstorm.20220203082953.3"><vh>enum VidEnum (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.4"><vh>pub enum VidOrdering (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.5"><vh>pub struct VID (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.6"><vh>fn cmp_depth_idx (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.7"><vh>pub fn cmp_depth (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.8"><vh>pub fn topmost (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.9"><vh>pub fn botmost (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.10"><vh>pub fn topmost_of3 (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.11"><vh>impl VID (vid.rs)</vh>
<v t="tangentstorm.20220203082953.12"><vh>predicates</vh></v>
<v t="tangentstorm.20220203082953.13"><vh>comparisons (is_above/is_below)</vh></v>
<v t="tangentstorm.20220203082953.14"><vh>pub fn shift_up (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.15"><vh>pub fn var_ix (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.16"><vh>pub fn vir_ix (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.17"><vh>pub fn vid_ix (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.18"><vh>pub fn bitmask (vid.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082953.19"><vh>impl fmt::Display for VID (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.20"><vh>impl fmt::Debug for VID { // for test suite output (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.21"><vh>impl VID (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.22"><vh>impl Ord for VID (vid.rs)</vh></v>
<v t="tangentstorm.20220203082953.23"><vh>impl PartialOrd for VID (vid.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082953.24"><vh>@clean nid.rs</vh>
<v t="tangentstorm.20220203082953.25"><vh>pub struct NID (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.26"><vh>boolean constants (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.27"><vh>support routines</vh></v>
<v t="tangentstorm.20220203082953.28"><vh>impl std::ops::Not for NID (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.29"><vh>impl fmt::Display for NID (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.30"><vh>impl fmt::Debug for NID { // for test suite output (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.31"><vh>tests</vh></v>
<v t="tangentstorm.20220203082953.32"><vh>scaffolding</vh></v>
<v t="tangentstorm.20220203082953.33"><vh>pub fn no_var (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.34"><vh>pub fn ixn (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.35"><vh>fn vid_to_old (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.36"><vh>fn old_to_vid (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.37"><vh>impl NID (nid.rs)</vh>
<v t="tangentstorm.20220203082953.38"><vh>constructors</vh></v>
<v t="tangentstorm.20220203082953.39"><vh>pub fn vid (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.40"><vh>predicates</vh></v>
<v t="tangentstorm.20220203082953.41"><vh>pub fn idx (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.42"><vh>pub fn tbl (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.43"><vh>pub fn arity (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.44"><vh>pub fn fun_flip_inputs (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.45"><vh>fn permute_bits (nid.rs)</vh></v>
<v t="tangentstorm.20220203082953.46"><vh>pub fn fun_lift_input (nid.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082953.47"><vh>more tests</vh></v>
</v>
<v t="tangentstorm.20220203082953.48"><vh>@clean ast.rs</vh>
<v t="tangentstorm.20220203082953.49"><vh>pub struct RawASTBase (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.50"><vh>impl RawASTBase (ast.rs)</vh>
<v t="tangentstorm.20220203082953.51"><vh>pub fn empty (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.52"><vh>pub fn len (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.53"><vh>pub fn is_empty (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.54"><vh>fn nid (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.55"><vh>pub fn load (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.56"><vh>fn when (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.57"><vh>fn walk where F: FnMut(NID (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.58"><vh>fn step where F:FnMut(NID (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.59"><vh>pub fn show (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.60"><vh>pub fn masks_and_costs (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.61"><vh>pub fn reftable (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.62"><vh>fn markdeps (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.63"><vh>pub fn permute (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.64"><vh>pub fn repack (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.65"><vh>pub fn get_ops (ast.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082953.66"><vh>impl Base for RawASTBase (ast.rs)</vh>
<v t="tangentstorm.20220203082953.67"><vh>fn new (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.68"><vh>fn when_hi (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.69"><vh>fn when_lo (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.70"><vh>fn def (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.71"><vh>fn tag (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.72"><vh>fn and (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.73"><vh>fn xor (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.74"><vh>fn or (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.75"><vh>fn sub (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.76"><vh>fn get (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.77"><vh>fn save (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.78"><vh>fn dot (ast.rs)</vh></v>
</v>
<v t="tangentstorm.20220203082953.79"><vh>pub struct ASTBase (ast.rs)</vh>
<v t="tangentstorm.20220203082953.80"><vh>impl Base for ASTBase (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.81"><vh>impl ASTBase (ast.rs)</vh></v>
<v t="tangentstorm.20220203082953.82"><vh>test suite</vh></v>
</v>
</v>
</v>
</vnodes>
<tnodes>
<t tx="tangentstorm.20220203082928.1">@language rust
</t>
<t tx="tangentstorm.20220203082928.2">@
Bex uses graphs to represent boolean expressions.
Graphs consist of nodes (or "vertices" in some circles) and edges.
In bex, every node has an identifier, called a NID (for "node ID").
The word "NID" rhymes with "lid".
Except for parethesis, pretty much every token in the language of propositional logic can be represented by a NID.
</t>
<t tx="tangentstorm.20220203082928.3">@
For example, the constant NIDs `O` and `I` represent the values false (or 0,off,etc.) and true (or 1, "on", etc.), respectively.
-
</t>
<t tx="tangentstorm.20220203082928.4">/// NID of the virtual node represeting the constant function 0, or "always false."
pub const O:NID = new(T);
/// NID of the virtual node represeting the constant function 1, or "always true."
pub const I:NID = new(T|INV);
</t>
<t tx="tangentstorm.20220203082928.5"></t>
<t tx="tangentstorm.20220203082928.6">@
The 'fun' bit indicates that the nid represents a boolean function of up to 5 inputs.
For each arity (number of inputs) n, there are 2^2^n possible truth tables:
i.6x NB. http://jsoftware.com
0 1 2 3 4 5
2^2^i.6x
2 4 16 256 65536 4294967296
For example, the two zero-input functions are O and I.
The four one-input functions are:
x -> O
x -> I
x -> x
x -> ~x
(The first three of these are redundant, and the last one is the "not" operator.)
The sixteen two-input functions include logical connectives like AND, OR, XOR, and
so on, as well as "not x", "not y", and of course the degenerate functions
"(x,y)->O" and "(x,y)->I".
The 256 three-input functions include such useful as "majority" and "if z then x else y".
There aren't standard names for the boolean functions with extra inputs,
but any boolean expression of five or fewer inputs can be represented by a single nid
in this way.</t>
<t tx="tangentstorm.20220203082928.7"></t>
<t tx="tangentstorm.20220203082928.8"></t>
<t tx="tangentstorm.20220203082937.1"></t>
<t tx="tangentstorm.20220203082937.2">@
The world solver is an approach to solving boolean expressions by decomposition.
The general approach works *as if* we chose an input variable to remove from the expression, and made two copies of the expression, with the chosen variable replaced by each of the constants "0" and "1". We then simplify the expressions as much as possible, and then perform the same type of substitution for the next variable, but on each of the new copies.
The trick is to minimize wasted memory and time spent re-calculating things.
Rather than making complete copies of the AST at each point, we imagine something like a tree of "alternate worlds". The root of the tree is not the AST itself, but rather a mapping of the input variables to the "twigs" of the AST that take those variables, and an "overlay" that maps node identifiers to transformed twigs.
The solver does a breadth-first, bottom-up transformation of the graph.
Leaves are always literals (either constants or input variables).
Constants can always be eliminated by replacing the function in the downstream nodes (unless of course the entire expresion simplifies to a constant).
</t>
<t tx="tangentstorm.20220203082953.1">@language rust
@tabwidth -4
</t>
<t tx="tangentstorm.20220203082953.10">pub fn topmost_of3(x:VID, y:VID, z:VID)->VID { topmost(x, topmost(y, z)) }
</t>
<t tx="tangentstorm.20220203082953.11">impl VID {
pub const fn top()->VID { VID { v:T }}
pub const fn nov()->VID { VID { v:NoV }}
pub const fn var(i:u32)->VID { VID { v: Var(i) }}
pub const fn vir(i:u32)->VID { VID { v: Vir(i) }}
@others
</t>
<t tx="tangentstorm.20220203082953.12">pub fn is_top(&self)->bool { VID{ v:T } == *self }
pub fn is_nov(&self)->bool { if let VID{ v:NoV } = self { true } else { false } }
pub fn is_var(&self)->bool { if let VID{ v:Var(_) } = self { true } else { false } }
pub fn is_vir(&self)->bool { if let VID{ v:Vir(_) } = self { true } else { false } }
</t>
<t tx="tangentstorm.20220203082953.13">pub fn is_above(&self, other:&VID)->bool { self.cmp_depth(&other) == VidOrdering::Above }
pub fn is_below(&self, other:&VID)->bool { self.cmp_depth(&other) == VidOrdering::Below }
</t>
<t tx="tangentstorm.20220203082953.14">pub fn shift_up(&self)->VID {
match self.v {
NoV => panic!("VID::nov().shift_up() is undefined"),
T => panic!("VID::top().shift_up() is undefined"), //VID::var(0),
// these two might panic on over/underflow:
Var(x) => VID::var(x+1),
Vir(x) => VID::vir(x+1)}}
</t>
<t tx="tangentstorm.20220203082953.15">pub fn var_ix(&self)->usize {
if let Var(x) = self.v { x as usize } else { panic!("var_ix({:?})", self) }}
</t>
<t tx="tangentstorm.20220203082953.16">pub fn vir_ix(&self)->usize {
if let Vir(x) = self.v { x as usize } else { panic!("vir_ix({:?})", self) }}
</t>
<t tx="tangentstorm.20220203082953.17">pub fn vid_ix(&self)->usize { match self.v {
T => panic!("x.vid_ix() makes no sense when x==T. Test with nid::is_const first."),
NoV => panic!("x.vid_ix() makes no sense when x==VID::NoV. Test with x.is_nov first."),
Var(x) | Vir(x) => x as usize }}
</t>
<t tx="tangentstorm.20220203082953.18">pub fn bitmask(&self)->u64 { match self.v {
NoV|T => 0,
Var(x) | Vir(x) => if x < 64 { 1 << x as u64 } else { 0 }}}}
</t>
<t tx="tangentstorm.20220203082953.19">/// Pretty-printer for NIDS that reveal some of their internal data.
impl fmt::Display for VID {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self.v {
T => write!(f, "T"),
NoV => write!(f, "NoV"),
Var(x) => write!(f, "x{}", x),
Vir(x) => write!(f, "v{}", x) }}}
</t>
<t tx="tangentstorm.20220203082953.2">/// Variable Identifiers
use std::cmp::Ordering;
use std::fmt;
@others
</t>
<t tx="tangentstorm.20220203082953.20">/// Same as fmt::Display. Mostly so it's easier to see the problem when an assertion fails.
impl fmt::Debug for VID { // for test suite output
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { write!(f, "{}", self) }}
</t>
<t tx="tangentstorm.20220203082953.21">
</t>
<t tx="tangentstorm.20220203082953.22">impl VID {
#[deprecated(note="VID scaffolding")]
pub fn u(&self)->usize { match self.v {
T => 536870912, // 1<<29, same as nid::T,
NoV => panic!("can't turn NoV into a number"),
Var(x) => x as usize,
Vir(x) => x as usize }}}
/// this is only so I can order ops. VID should otherwise always be
/// compared with is_above / iS_below or cmp_depth, for clarity.
impl Ord for VID {
fn cmp(&self, other: &Self)-> Ordering {
match self.cmp_depth(other) {
VidOrdering::Above => Ordering::Less,
VidOrdering::Level => Ordering::Equal,
VidOrdering::Below => Ordering::Greater}}}
</t>
<t tx="tangentstorm.20220203082953.23">impl PartialOrd for VID {
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
Some(self.cmp(other))}}
</t>
<t tx="tangentstorm.20220203082953.24">/* Bitmask diagram:
NID | VAR
----+----------------------
63 | 31 : INV
62 | 30 : VAR
61 | 29 : T (const / max vid)
60 | 28 : RVAR
*/
use std::fmt;
// -- core data types ---
/// (OLD) Variable ID: uniquely identifies an input variable in the BDD.
/// This name is private to the nid module since vid::VID supercedes it.
type VID = usize;
/// Index into a (usually VID-specific) vector.
pub type IDX = u32;
@others
</t>
<t tx="tangentstorm.20220203082953.25">/// A NID represents a node in a Base. Essentially, this acts like a tuple
/// containing a VID and IDX, but for performance reasons, it is packed into a u64.
/// See below for helper functions that manipulate and analyze the packed bits.
#[derive(PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy, Serialize, Deserialize)]
pub struct NID { n: u64 }
/// Just a constructor so I can add extra temp fields in development without breaking code.
const fn new (n:u64)->NID { NID{n} }
// -- bits in the nid ---
/// Single-bit mask representing that a NID is inverted.
const INV:u64 = 1<<63; // is inverted?
/// Single-bit mask indicating that a NID represents a variable. (The corresponding
/// "virtual" nodes have I as their hi branch and O as their lo branch. They're simple
/// and numerous enough that we don't bother actually storing them.)
const VAR:u64 = 1<<62; // is variable?
/// Single-bit mask indicating that the NID represents a constant. The corresponding
/// virtual node branches on constant "true" value, hence the letter T. There is only
/// one such node -- O (I is its inverse) but having this bit in the NID lets us
/// easily detect and optimize the cases.
const T:u64 = 1<<61; // T: max VID (hack so O/I nodes show up at bottom)
/// In addition, for solving, we want to distinguish between "virtual" variables which
/// represent some intermediate, unsimplified calculation, and "real" variables, which
/// represent actual input variables. That's what this bit does.
const RVAR:u64 = 1<<60; // is *real* variable?
/// This bit indicates that the NID is meant to be used as a function.
/// (All nids represent functions, but this bit indicates that rather
/// than referring to an existing node, it is a function of <=5 inputs
/// and the entire truth table is stored in the index field.
// !TODO: Decide whether or not to merge F(unction) with T(able). If separate,
// then F+T might mean treat this as a function with a table, and F+!T would
// tell the interpreter to apply some previously defined expression as a function.
const F:u64 = 1<<59;
/// Constant used to extract the index part of a NID.
const IDX_MASK:u64 = (1<<32)-1;
</t>
<t tx="tangentstorm.20220203082953.26">/// NID of the virtual node represeting the constant function 0, or "always false."
pub const O:NID = new(T);
/// NID of the virtual node represeting the constant function 1, or "always true."
pub const I:NID = new(T|INV);
</t>
<t tx="tangentstorm.20220203082953.27">// NID support routines
/// Does the NID represent a variable?
#[inline(always)] pub fn is_var(x:NID)->bool { (x.n & VAR) != 0 }
/// Does the NID represent a *real* variable?
#[inline(always)] pub fn is_rvar(x:NID)->bool { (x.n & RVAR) != 0 }
/// Does the NID represent a VID?
#[inline(always)] pub fn is_vid(x:NID)->bool { (x.n & VAR) != 0 }
/// Is n a literal (variable or constant)?
#[inline] pub fn is_lit(x:NID)->bool { is_vid(x) | is_const(x) }
/// Is the NID inverted? That is, does it represent `not(some other nid)`?
#[inline(always)] pub fn is_inv(x:NID)->bool { (x.n & INV) != 0 }
/// Return the NID with the 'INV' flag removed.
// !! pos()? abs()? I don't love any of these names.
#[inline(always)] pub fn raw(x:NID)->NID { new(x.n & !INV) }
/// Does the NID refer to one of the two constant nodes (O or I)?
#[inline(always)] pub fn is_const(x:NID)->bool { (x.n & T) != 0 }
/// Map the NID to an index. (I,e, if n=idx(x), then x is the nth node branching on var(x))
#[inline(always)] pub fn idx(x:NID)->usize { (x.n & IDX_MASK) as usize }
/// On which variable does this node branch? (I and O branch on TV)
#[inline(always)] pub fn vid(x:NID)->VID { ((x.n & !(INV|VAR)) >> 32) as VID}
/// Toggle the INV bit, applying a logical "NOT" operation to the corressponding node.
#[deprecated(note="use !nid instead")]
#[inline(always)] pub fn not(x:NID)->NID { NID { n:x.n^INV } }
/// Construct the NID for the (virtual) node corresponding to an input variable.
/// Private since moving to vid::VID, because this didn't set the "real" bit, and
/// I want the real bit to eventually go away in favor of an unset "virtual" bit.
#[inline(always)] fn nv(v:VID)->NID { NID { n:((v as u64) << 32)|VAR }}
/// Construct a NID with the given variable and index.
#[inline(always)] pub fn nvi(v:VID,i:IDX)->NID { new(((v as u64) << 32) + i as u64) }
/// construct an F node
#[inline(always)] pub const fn fun(arity:u8,tbl:u32)->NID { NID { n:F+(tbl as u64)+((arity as u64)<< 32)}}
#[inline(always)] pub fn is_fun(x:&NID)->bool { x.n & F == F }
#[inline(always)] pub fn tbl(x:&NID)->Option<u32> { if is_fun(x){ Some(idx(*x) as u32)} else {None}}
#[inline(always)] pub fn arity(x:&NID)->u8 {
if is_fun(x){ (x.n >> 32 & 0xff) as u8 }
else if is_lit(*x) { 0 }
// !! TODO: decide what arity means for general nids.
// !! if the node is already bound to variables. We could think of this as the number
// !! of distinct variables it contains, *or* we could think of it as an expression that
// !! takes no parameters. (Maybe the F bit, combined with the "T=Table" bit toggles this?)
// !! Also, it's not obvious how to track the number of variables when combining two nodes
// !! without a lot of external storage. The best we can do is look at the top var and
// !! get an upper bound. With virs, we can't even do that. In any case, I don't actually
// !! need this at the moment, so I will just leave it unimplemented.
else { todo!("arity is only implemented for fun and lit nids at the moment") }}
</t>
<t tx="tangentstorm.20220203082953.28">impl std::ops::Not for NID {
type Output = NID;
fn not(self)-> NID {NID { n: self.n^INV }}}
</t>
<t tx="tangentstorm.20220203082953.29">
/// Pretty-printer for NIDS that reveal some of their internal data.
impl fmt::Display for NID {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
if is_const(*self) { if is_inv(*self) { write!(f, "I") } else { write!(f, "O") } }
else if self.is_fun() {
let ar:u8 = self.arity().unwrap();
let ft:u32 = self.tbl().unwrap() & ((2<<ar as u32)-1);
if ar == 2 { write!(f, "<{:04b}>", ft)} // TODO: dynamically format to a length
else { write!(f, "<{:b}>", ft) }}
else { if is_inv(*self) { write!(f, "¬")?; }
if is_var(*self) { write!(f, "{}", self.vid()) }
else if is_rvar(*self) { write!(f, "@[{}:{}]", self.vid(), idx(*self)) }
else if vid(*self) == NOVAR { write!(f, "#{}", idx(*self)) }
else { write!(f, "@[v{}:{}]", vid(*self), idx(*self)) }}}}
</t>
<t tx="tangentstorm.20220203082953.3">/// this will probably go away in favor of a bitmask at some point
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Debug, Hash, Serialize, Deserialize)]
enum VidEnum {
// How I (eventually) want the ordering, to be (once biggest vars go on top:)
T, // Special meta-constant on which I and O branch.
NoV, // Special case for AST nodes not tied to a variable
Var(u32), // Real Vars go in the middle, with biggest u32 on top.
Vir(u32), // Virtual are "biggest", so go to the top.
}
</t>
<t tx="tangentstorm.20220203082953.30">/// Same as fmt::Display. Mostly so it's easier to see the problem when an assertion fails.
impl fmt::Debug for NID { // for test suite output
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { write!(f, "{}", self) }}
</t>
<t tx="tangentstorm.20220203082953.31">
#[test] fn test_nids() {
assert_eq!(O.n, 2305843009213693952); assert_eq!(O, new(0x2000000000000000));
assert_eq!(I.n, 11529215046068469760); assert_eq!(I, new(0xa000000000000000));
assert_eq!(NID::vir(0), new(0x4000000000000000u64));
assert_eq!(NID::var(0), new(0x5000000000000000u64));
assert_eq!(NID::vir(1), new(0x4000000100000000u64));
assert!(vid(NID::vir(0)) < vid(NID::var(0)));
assert_eq!(nvi(0,0), new(0x0000000000000000u64));
assert_eq!(nvi(1,0), new(0x0000000100000000u64)); }
#[test] fn test_var() {
assert_eq!(vid(O), 536_870_912, "var(O)");
assert_eq!(vid(I), vid(O), "INV bit shouldn't be part of variable");
assert_eq!(vid(NID::vir(0)), 0);
assert_eq!(vid(NID::var(0)), 268_435_456);}
#[test] fn test_cmp() {
let v = |x:usize|->NID { nv(x) }; let x=|x:u32|->NID { NID::var(x) };
let o=|x:NID|vid(x); let n=|x:NID|x.vid();
assert!(o(O) == o(I), "old:no=no"); assert!(n(O) == n(I), "new:no=no");
assert!(o(O) > o(v(0)), "old:no>v0"); assert!(n(O).is_below(&n(v(0))), "new:no bel v0");
assert!(o(O) > o(x(0)), "old:no>x0"); assert!(n(O).is_below(&n(x(0))), "new:no bel x0");
assert!(o(v(0)) < o(x(0)), "old:v0>x0"); assert!(n(v(0)).is_above(&n(x(0))), "new:v0 abv x0");
assert!(o(v(1)) < o(x(0)), "old:v1<x0"); assert!(n(v(1)).is_above(&n(x(0))), "new:v1 abv x0");}
</t>
<t tx="tangentstorm.20220203082953.32">// scaffolding for moving ASTBase over to use NIDS
const NOVAR:VID = (1<<26) as VID; // 134_217_728
const TOP:VID = (T>>32) as VID; // 536_870_912, // 1<<29, same as nid::T
</t>
<t tx="tangentstorm.20220203082953.33">pub fn no_var(x:NID)->bool { vid(x)==NOVAR }
/// return a nid that is not tied to a variable
pub fn ixn(ix:IDX)->NID { nvi(NOVAR, ix) }
</t>
<t tx="tangentstorm.20220203082953.34">
use vid;
</t>
<t tx="tangentstorm.20220203082953.35">fn vid_to_old(v:vid::VID)->VID {
if v.is_nov() { NOVAR }
else if v.is_top() { TOP }
else if v.is_var() { v.var_ix() | (RVAR>>32) as VID }
else if v.is_vir() { v.vir_ix() as VID }
else { panic!("unknown vid::VID {:?}?", v) }}
</t>
<t tx="tangentstorm.20220203082953.36">fn old_to_vid(o:VID)->vid::VID {
if o == TOP { vid::VID::top() }
else if o == NOVAR { vid::VID::nov() }
else if o & (RVAR>>32) as VID > 0 { vid::VID::var((o & !(RVAR>>32) as VID) as u32) }
else { vid::VID::vir(o as u32) }}
/// helper for 'fun' (function table) nids
/// u32 x contains the bits to permute.
/// pv is a permutation vector (the bytes 0..=31 in some order)
// b=pv[i] means to grab bit b from x and move to position i in the result.
fn permute_bits(x:u32, pv:&[u8])->u32 {
let mut r:u32 = 0;
for (i,b) in pv.iter().enumerate() { r |= ((x & (1<<b)) >> b) << i; }
r }
</t>
<t tx="tangentstorm.20220203082953.37">// TODO: add n.is_vid() to replace current is_var()
// TODO: is_var() should only be true for vars, not both virs and vars.
// TODO: probably also need is_nov() for consistency.
impl NID {
@others
</t>
<t tx="tangentstorm.20220203082953.38">pub fn var(v:u32)->Self { Self::from_vid(vid::VID::var(v)) }
pub fn vir(v:u32)->Self { Self::from_vid(vid::VID::vir(v)) }
pub fn from_var(v:vid::VID)->Self { NID::var(v.var_ix() as u32)}
pub fn from_vir(v:vid::VID)->Self { NID::vir(v.vir_ix() as u32)}
pub fn from_vid(v:vid::VID)->Self { nv(vid_to_old(v)) }
pub fn from_vid_idx(v:vid::VID, i:IDX)->Self { nvi(vid_to_old(v), i) }
</t>
<t tx="tangentstorm.20220203082953.39">pub fn vid(&self)->vid::VID { old_to_vid(vid(*self)) }
</t>
<t tx="tangentstorm.20220203082953.4">#[derive(Eq, PartialEq)]
pub enum VidOrdering {
Above,
Level,
Below }
</t>
<t tx="tangentstorm.20220203082953.40">pub fn is_const(&self)->bool { is_const(*self) }
pub fn is_vid(&self)->bool { is_vid(*self)}
pub fn is_var(&self)->bool { self.is_vid() && self.vid().is_var() }
pub fn is_vir(&self)->bool { self.is_vid() && self.vid().is_vir() }
pub fn is_lit(&self)->bool { is_lit(*self) }
pub fn is_inv(&self)->bool { is_inv(*self) }
</t>
<t tx="tangentstorm.20220203082953.41">pub fn idx(&self)->usize { idx(*self) }
pub const fn fun(arity:u8, tbl:u32)->Self { fun(arity,tbl) }
pub fn is_fun(&self)->bool { is_fun(self) }
</t>
<t tx="tangentstorm.20220203082953.42">pub fn tbl(&self)->Option<u32> { tbl(self) }
</t>
<t tx="tangentstorm.20220203082953.43">pub fn arity(&self)->Option<u8> { Some(arity(self)) }
/// is it possible nid depends on var v?
/// the goal here is to avoid exploring a subgraph if we don't have to.
#[inline] pub fn might_depend_on(&self, v:vid::VID)->bool {
if is_const(*self) { false }
else if is_var(*self) { self.vid() == v }
else { let sv = self.vid(); sv == v || sv.is_above(&v) }}
</t>
<t tx="tangentstorm.20220203082953.44">/// given a function, return the function you'd get if you inverted one or more of the input bits.
/// bits is a bitmap where setting the (2^i)'s-place bit means to invert the `i`th input.
/// For example: if `bits=0b00101` maps inputs `x0, x1, x2, x3, x4` to `!x0, x1, !x2, x3, x4`
pub fn fun_flip_inputs(&self, bits:u8)->NID {
let mut res:u32 = self.tbl().unwrap();
let flip = |i:u8| (bits & (1<<i)) != 0;
macro_rules! p { ($x:expr) => { res = permute_bits(res, $x); }}
if flip(4) { p!(&[16,17,18,19,20,21,22,23,16,17,18,19,20,21,22,23,8 ,9 ,10,11,12,13,14,15,8 ,9 ,10,11,12,13,14,15]) }
if flip(3) { p!(&[8 ,9 ,10,11,12,13,14,15,0 ,1 ,2 ,3 ,4 ,5 ,6 ,7 ,24,25,26,27,28,29,30,31,16,17,18,19,20,21,22,23]) }
if flip(2) { p!(&[4 ,5 ,6 ,7 ,0 ,1 ,2 ,3 ,12,13,14,15,8 ,9 ,10,11,20,21,22,23,16,17,18,19,28,29,30,31,24,25,26,27]) }
if flip(1) { p!(&[2 ,3 ,0 ,1 ,6 ,7 ,4 ,5 ,10,11,8 ,9 ,14,15,12,13,18,19,16,17,22,23,20,21,26,27,24,25,30,31,28,29]) }
if flip(0) { p!(&[1 ,0 ,3 ,2 ,5 ,4 ,7 ,6 ,9 ,8 ,11,10,13,12,15,14,17,16,19,18,21,20,23,22,25,24,27,26,29,28,31,30]) }
NID::fun(self.arity().unwrap(), res)}
</t>
<t tx="tangentstorm.20220203082953.45"></t>
<t tx="tangentstorm.20220203082953.46">/// given a function, return the function you'd get if you "lift" one of the inputs
/// by swapping it with its neighbors. (so bit=0 permutes inputs x0,x1,x2,x3,x4 to x1,x0,x2,x3,x4)
pub fn fun_lift_input(&self, bit:u8)->NID {
macro_rules! p { ($x:expr) => { NID::fun(self.arity().unwrap(), permute_bits(self.tbl().unwrap(), $x)) }}
match bit {
3 => p!(&[0 ,1 ,2 ,3 ,4 ,5 ,6 ,7 ,16,17,18,19,20,21,22,23,8 ,9 ,10,11,12,13,14,15,24,25,26,27,28,29,30,31]),
2 => p!(&[0 ,1 ,2 ,3 ,8 ,9 ,10,11,4 ,5 ,6 ,7 ,12,13,14,15,16,17,18,19,24,25,26,27,20,21,22,23,28,29,30,31]),
1 => p!(&[0 ,1 ,4 ,5 ,2 ,3 ,6 ,7 ,8 ,9 ,12,13,10,11,14,15,16,17,20,21,18,19,22,23,24,25,28,29,26,27,30,31]),
0 => p!(&[0 ,2 ,1 ,3 ,4 ,6 ,5 ,7 ,8 ,10,9 ,11,12,14,13,15,16,18,17,19,20,22,21,23,24,26,25,27,28,30,29,31]),
_ => panic!("{}", "lifted input bit must be in {0,1,2,3}")}}}
</t>
<t tx="tangentstorm.20220203082953.47">
#[test] fn test_fun() {
assert!(!NID::var(1).is_fun(), "var(1) should not be fun.");
assert!(!NID::vir(1).is_fun(), "vir(1) should not be fun.");
assert!(!NID::from_vid_idx(vid::NOV, 0).is_fun(), "idx var should not be fun");}
</t>
<t tx="tangentstorm.20220203082953.48">// a concrete implemetation:
use std::collections::{HashMap,HashSet};
use io;
use base::*;
use {nid, nid::NID};
use {vid, vid::VID};
use {ops, ops::Ops};
use simp;
#[derive(Serialize, Deserialize, Debug)]
@others
</t>
<t tx="tangentstorm.20220203082953.49">pub struct RawASTBase {
bits: Vec<Ops>, // all known bits (simplified)
tags: HashMap<String, NID>, // support for naming/tagging bits.
hash: HashMap<Ops, NID>, // expression cache (simple+complex)
}
type VarMaskFn = fn(&RawASTBase,vid::VID)->u64;
</t>
<t tx="tangentstorm.20220203082953.5">use self::VidEnum::*;
#[derive(Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub struct VID { v:VidEnum }
pub const NOV:VID = VID::nov();
pub const TOP:VID = VID::top();
</t>
<t tx="tangentstorm.20220203082953.50">/// An ASTBase that does not use extra simplification rules.
impl RawASTBase {
@others
} // impl RawASTBase
</t>
<t tx="tangentstorm.20220203082953.51">pub fn empty()->RawASTBase { RawASTBase{ bits:vec![], tags:HashMap::new(), hash:HashMap::new() }}
</t>
<t tx="tangentstorm.20220203082953.52">pub fn len(&self)->usize { self.bits.len() }
</t>
<t tx="tangentstorm.20220203082953.53">pub fn is_empty(&self)->bool { self.bits.is_empty() }
</t>
<t tx="tangentstorm.20220203082953.54">fn nid(&mut self, ops:Ops)->NID {
match self.hash.get(&ops) {
Some(&n) => n,
None => {
let nid = nid::ixn(self.bits.len() as u32);
self.bits.push(ops.clone());
self.hash.insert(ops, nid);
nid }}}
</t>
<t tx="tangentstorm.20220203082953.55">pub fn load(path:&str)->::std::io::Result<RawASTBase> {
let s = io::get(path)?;
Ok(bincode::deserialize(&s).unwrap()) }
</t>
<t tx="tangentstorm.20220203082953.56">fn when(&mut self, v:vid::VID, val:NID, nid:NID)->NID {
if nid.is_vid() && nid.vid() == v { val }
else if nid.is_lit() { nid }
else {
let ops = self.get_ops(nid).clone();
let rpn:Vec<NID> = ops.to_rpn().map(|&nid|{
if nid.is_fun() { nid }
else { self.when(v, val, nid) }}).collect();
self.nid(ops::rpn(&rpn)) }}
</t>
<t tx="tangentstorm.20220203082953.57">fn walk<F>(&self, n:NID, f:&mut F) where F: FnMut(NID) {
let mut seen = HashSet::new();
self.step(n,f,&mut seen)}
</t>
<t tx="tangentstorm.20220203082953.58">fn step<F>(&self, n:NID, f:&mut F, seen:&mut HashSet<NID>) where F:FnMut(NID) {
if !seen.contains(&nid::raw(n)) {
seen.insert(nid::raw(n));
f(n);
for op in self.get_ops(n).to_rpn() {
if !op.is_fun() {
self.step(*op, f, seen) }}}}
</t>
<t tx="tangentstorm.20220203082953.59">pub fn show(&self, n:NID) { self.show_named(n, "+ast+") }
/// given a function that maps input bits to 64-bit masks, color each node
/// in the base according to its inputs (thus tracking the spread of influence
/// of up to 64 bits (or groups of bits).
///
/// while we're at it, calculate the cost of each bit, where constants have cost 0,
/// inputs have a cost of 1, and everything else is 1 + max(cost of input bits)
/// (TOOD: break masks_and_costs into two functions)
</t>
<t tx="tangentstorm.20220203082953.6">fn cmp_depth_idx(x:u32, y:&u32)->VidOrdering {
match x.cmp(y) {
Ordering::Less => VidOrdering::Below,
Ordering::Equal => VidOrdering::Level,
Ordering::Greater => VidOrdering::Above }}
</t>
<t tx="tangentstorm.20220203082953.60">pub fn masks_and_costs(&self, vm:VarMaskFn)->(Vec<u64>, Vec<u32>) {
use std::cmp::max;
let mut masks = vec![];
let mut costs = vec![];
for bit in self.bits.iter() {
let (mask, cost) = {
let cost = |x:NID| {
if x.is_const() { 0 }
else if x.is_vid() { 1 }
else if nid::no_var(x) { costs[nid::idx(x)] }
else { todo!("cost({:?})", x) }};
let mask = |x:NID| {
if nid::is_const(x) { 0 }
else if x.is_vid() { vm(self, x.vid()) }
else if nid::no_var(x) { masks[nid::idx(x)] }
else { todo!("mask({:?})", x) }};
let mut m = 0u64;
let mut c = 0u32;
for &op in bit.to_rpn() {
if ! op.is_fun() {
m |= mask(op);
c = max(c, cost(op)); }}
(m, c+1) };
masks.push(mask);
costs.push(cost)}
(masks, costs)}
</t>
<t tx="tangentstorm.20220203082953.61">/// this returns a ragged 2d vector of direct references for each bit in the base
pub fn reftable(&self) -> Vec<Vec<NID>> {
todo!("test case for reftable!"); /*
let bits = &self.bits;
let mut res:Vec<Vec<NID>> = vec![vec![]; bits.len()];
for (n, &bit) in bits.iter().enumerate() {
let mut f = |x:NID| res[nid::idx(x)].push(n);
match bit {
Op::And(x,y) => { f(x); f(y); }
Op::Xor(x,y) => { f(x); f(y); }
Op::Or(x,y) => { f(x); f(y); }
Op::Ch(x,y,z) => { f(x); f(y); f(z); }
Op::Mj(x,y,z) => { f(x); f(y); f(z); } } }
res*/ }
</t>
<t tx="tangentstorm.20220203082953.62">/// this is part of the garbage collection system. keep is the top level nid to keep.
/// seen gets marked true for every nid that is a dependency of keep.
/// TODO:: use a HashSet for 'seen' in markdeps()
fn markdeps(&self, keep:NID, seen:&mut Vec<bool>) {
if nid::is_lit(keep) { return }
if !nid::no_var(keep) { todo!("markdeps({:?})", keep) }
if !seen[nid::idx(keep)] {
seen[nid::idx(keep)] = true;
let mut f = |x:&NID| { self.markdeps(*x, seen) };
for op in self.bits[nid::idx(keep)].to_rpn() { if !op.is_fun() { f(op) }}}}
</t>
<t tx="tangentstorm.20220203082953.63">/// Construct a copy of the base, with the nodes reordered according to
/// permutation vector pv. That is, pv is a vector of unique node indices
/// that we want to keep, in the order we want them. (It might actually be
/// shorter than bits.len() and thus not technically a permutation vector,
/// but I don't have a better name for this concept.)
pub fn permute(&self, pv:&[usize])->RawASTBase {
// map each kept node in self.bits to Some(new position)
let new:Vec<Option<usize>> = {
let mut res = vec![None; self.bits.len()];
for (i,&n) in pv.iter().enumerate() { res[n] = Some(i) }
res };
let nn = |x:NID|{
if nid::is_lit(x) { x }
else {
let r = nid::ixn(new[nid::idx(x) as usize].expect("bad index in AST::permute") as u32);
if nid::is_inv(x) { !r } else { r }}};
let newbits = pv.iter().map(|&old| {
let new:Vec<NID> = self.bits[old].to_rpn().map(|&x| { if x.is_fun() { x } else { nn(x) }}).collect();
ops::rpn(&new) }).collect();
let mut newtags = HashMap::new();
for (key, &val) in &self.tags { newtags.insert(key.clone(), nn(val)); }
RawASTBase{ bits:newbits, tags:newtags, hash:HashMap::new() }}
</t>
<t tx="tangentstorm.20220203082953.64">/// Construct a new RawASTBase with only the nodes necessary to define the given nodes.
/// The relative order of the bits is preserved.
pub fn repack(&self, keep:Vec<NID>) -> (RawASTBase, Vec<NID>) {
// garbage collection: mark dependencies of the bits we want to keep
let mut deps = vec!(false;self.bits.len());
for &nid in keep.iter() { self.markdeps(nid, &mut deps) }
let mut new:Vec<Option<usize>> = vec![None; self.bits.len()];
let mut old:Vec<usize> = vec![];
for i in 0..self.bits.len() {
if deps[i] { new[i]=Some(old.len()); old.push(i); }}
(self.permute(&old), keep.iter().map(|&i|
nid::ixn(new[nid::idx(i) as usize].expect("?!") as u32)).collect()) }
</t>
<t tx="tangentstorm.20220203082953.65">pub fn get_ops(&self, n:NID)->&Ops {
if nid::no_var(n) { &self.bits[nid::idx(n)] } else { panic!("don't know how to op({:?})", n) }}
</t>
<t tx="tangentstorm.20220203082953.66">impl Base for RawASTBase {
@others
} // impl Base for RawASTBase
</t>
<t tx="tangentstorm.20220203082953.67">fn new()->Self { RawASTBase::empty() }
</t>
<t tx="tangentstorm.20220203082953.68">fn when_hi(&mut self, v:vid::VID, n:NID)->NID { self.when(v, nid::I, n) }
</t>
<t tx="tangentstorm.20220203082953.69">fn when_lo(&mut self, v:vid::VID, n:NID)->NID { self.when(v, nid::O, n) }
</t>
<t tx="tangentstorm.20220203082953.7">impl VID {
pub fn cmp_depth(&self, other: &Self) -> VidOrdering {
use self::VidOrdering::*;
match self.v {
T => if other.v == T { Level } else { Below },
NoV => match other.v {
T => Above,
NoV => Level,
_ => Below },
Var(x) => match other.v {
Vir(_) => Below,
Var(y) => cmp_depth_idx(x,&y),
NoV|T => Above },
Vir(x) => match other.v {
Var(_) => Above,
Vir(y) => cmp_depth_idx(x,&y),
NoV|T => Above }}}}
</t>
<t tx="tangentstorm.20220203082953.70">fn def(&mut self, s:String, v:vid::VID)->NID {
let nid = NID::from_vid(v);
self.tag(nid, format!("{}{:?}", s, v)) }
</t>
<t tx="tangentstorm.20220203082953.71">fn tag(&mut self, n:NID, s:String)->NID {
let n = n;
self.tags.insert(s, n); n }
</t>
<t tx="tangentstorm.20220203082953.72">fn and(&mut self, x:NID, y:NID)->NID {
if let Some(nid) = simp::and(x,y) { nid }
else {
let (lo, hi) = if x<y {(x,y)} else {(y,x)};
self.nid(ops::and(lo, hi)) }}
</t>
<t tx="tangentstorm.20220203082953.73">fn xor(&mut self, x:NID, y:NID)->NID {
if let Some(nid) = simp::xor(x,y) { nid }
else {
let (lo, hi) = if x<y {(x,y)} else {(y,x)};
self.nid(ops::xor(lo, hi)) }}
</t>
<t tx="tangentstorm.20220203082953.74">fn or(&mut self, x:NID, y:NID)->NID {
if let Some(nid) = simp::or(x,y) { nid }
else if x.is_inv() && y.is_inv() { !self.and(x, y) }
else {
let (lo, hi) = if x<y {(x,y)} else {(y,x)};
self.nid(ops::vel(lo, hi)) }}
</t>
<t tx="tangentstorm.20220203082953.75">fn sub(&mut self, _v:vid::VID, _n:NID, _ctx:NID)->NID { todo!("ast::sub") }
</t>
<t tx="tangentstorm.20220203082953.76">fn get(&self, s:&str)->Option<NID> { Some(*self.tags.get(s)?) }
</t>
<t tx="tangentstorm.20220203082953.77">fn save(&self, path:&str)->::std::io::Result<()> {
let s = bincode::serialize(&self).unwrap();
io::put(path, &s) }
</t>
<t tx="tangentstorm.20220203082953.78">// generate dot file (graphviz)
fn dot(&self, n:NID, wr: &mut dyn std::fmt::Write) {
macro_rules! w {
($x:expr $(,$xs:expr)*) => { writeln!(wr, $x $(,$xs)*).unwrap() }}
macro_rules! dotop {
($s:expr, $n:expr $(,$xs:expr)*) => {{
w!(" \"{}\"[label={}];", nid::raw($n), $s); // draw the node
$({ if nid::is_inv($xs) { w!("edge[style=dashed];"); }
else { w!("edge[style=solid];"); }
w!(" \"{}\"->\"{}\";", nid::raw($xs), nid::raw($n)); })* }}}
w!("digraph bdd {{");
w!("rankdir=BT;"); // put root on top
w!("node[shape=circle];");
w!("edge[style=solid];");
self.walk(n, &mut |n| {
match n {
nid::O => w!(" \"{}\"[label=⊥];", n),
nid::I => w!(" \"{}\"[label=⊤];", n),
_ if n.is_vid() => w!("\"{}\"[label=\"{}\"];", nid::raw(n), n.vid()),
_ => {
let rpn: Vec<NID> = self.get_ops(n).to_rpn().cloned().collect();
let fun = rpn.last().unwrap();
if let Some(2) = fun.arity() {
let (x, y) = (rpn[0], rpn[1]);
match *fun {
ops::AND => dotop!("∧",n,x,y),
ops::XOR => dotop!("≠",n,x,y),
ops::VEL => dotop!("∨",n,x,y),
_ => panic!("unexpected op in dot(): {:?}", n) }}
else { panic!("can't dot arbitrary ops yet: {:?}", rpn) }}}});
w!("}}"); }
</t>
<t tx="tangentstorm.20220203082953.79">pub struct ASTBase { base: Simplify<RawASTBase> }
@others
</t>
<t tx="tangentstorm.20220203082953.8">pub fn topmost(x:VID, y:VID)->VID { if x.is_above(&y) { x } else { y }}
</t>
<t tx="tangentstorm.20220203082953.80">impl Base for ASTBase {
inherit![when_hi, when_lo, and, xor, or, def, tag, get, sub, save, dot ];
fn new()->Self { ASTBase{ base: Simplify{ base: <RawASTBase as Base>::new() }}}}
</t>
<t tx="tangentstorm.20220203082953.81">impl ASTBase {
pub fn empty()->Self { ASTBase { base: Simplify{ base: RawASTBase::empty() }}}
pub fn raw_ast(&self)->&RawASTBase { &self.base.base }}
</t>
<t tx="tangentstorm.20220203082953.82">test_base_consts!(ASTBase);
test_base_when!(ASTBase);
#[test]
fn ast_and(){
let mut b = ASTBase::empty();
let x0 = NID::var(0); let x1 = NID::var(1);
let x01 = b.and(x0,x1);
let x10 = b.and(x1,x0);
assert_eq!(x01, x10, "expect $0 & $1 == $1 & $0"); }
</t>
<t tx="tangentstorm.20220203082953.9">pub fn botmost(x:VID, y:VID)->VID { if x.is_below(&y) { x } else { y }}
</t>
</tnodes>
</leo_file>