@@ -4639,67 +4639,127 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4639
4639
*
4640
4640
* Calculates per-stage metrics for data flow.
4641
4641
*/
4642
- predicate stageStats (
4643
- int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4644
- int calledges , int tfnodes , int tftuples
4645
- ) {
4646
- stage = "1 Fwd" and
4647
- n = 10 and
4648
- Stage1:: stats ( true , nodes , fields , conscand , states , tuples , calledges ) and
4649
- tfnodes = - 1 and
4650
- tftuples = - 1
4651
- or
4652
- stage = "1 Rev" and
4653
- n = 15 and
4654
- Stage1:: stats ( false , nodes , fields , conscand , states , tuples , calledges ) and
4655
- tfnodes = - 1 and
4656
- tftuples = - 1
4657
- or
4658
- stage = "2 Fwd" and
4659
- n = 20 and
4660
- Stage2:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4661
- or
4662
- stage = "2 Rev" and
4663
- n = 25 and
4664
- Stage2:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4665
- or
4666
- stage = "3 Fwd" and
4667
- n = 30 and
4668
- Stage3:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4669
- or
4670
- stage = "3 Rev" and
4671
- n = 35 and
4672
- Stage3:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4673
- or
4674
- stage = "4 Fwd" and
4675
- n = 40 and
4676
- Stage4:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4677
- or
4678
- stage = "4 Rev" and
4679
- n = 45 and
4680
- Stage4:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4681
- or
4682
- stage = "5 Fwd" and
4683
- n = 50 and
4684
- Stage5:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4685
- or
4686
- stage = "5 Rev" and
4687
- n = 55 and
4688
- Stage5:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4689
- or
4690
- stage = "6 Fwd" and
4691
- n = 60 and
4692
- finalStats ( true , nodes , fields , conscand , states , tuples ) and
4693
- calledges = - 1 and
4694
- tfnodes = - 1 and
4695
- tftuples = - 1
4696
- or
4697
- stage = "6 Rev" and
4698
- n = 65 and
4699
- finalStats ( false , nodes , fields , conscand , states , tuples ) and
4700
- calledges = - 1 and
4701
- tfnodes = - 1 and
4702
- tftuples = - 1
4642
+ predicate stageStats = Debug:: stageStats / 10 ;
4643
+
4644
+ private module Stage2alias = Stage2;
4645
+
4646
+ private module Stage3alias = Stage3;
4647
+
4648
+ private module Stage4alias = Stage4;
4649
+
4650
+ private module Stage5alias = Stage5;
4651
+
4652
+ /**
4653
+ * INTERNAL: Only for debugging.
4654
+ *
4655
+ * Contains references to individual pruning stages.
4656
+ */
4657
+ module Debug {
4658
+ module Stage2 = Stage2alias;
4659
+
4660
+ module Stage3 = Stage3alias;
4661
+
4662
+ module Stage4 = Stage4alias;
4663
+
4664
+ module Stage5 = Stage5alias;
4665
+
4666
+ predicate stageStats1 (
4667
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4668
+ int calledges , int tfnodes , int tftuples
4669
+ ) {
4670
+ stage = "1 Fwd" and
4671
+ n = 10 and
4672
+ Stage1:: stats ( true , nodes , fields , conscand , states , tuples , calledges ) and
4673
+ tfnodes = - 1 and
4674
+ tftuples = - 1
4675
+ or
4676
+ stage = "1 Rev" and
4677
+ n = 15 and
4678
+ Stage1:: stats ( false , nodes , fields , conscand , states , tuples , calledges ) and
4679
+ tfnodes = - 1 and
4680
+ tftuples = - 1
4681
+ }
4682
+
4683
+ predicate stageStats2 (
4684
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4685
+ int calledges , int tfnodes , int tftuples
4686
+ ) {
4687
+ stageStats1 ( n , stage , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4688
+ or
4689
+ stage = "2 Fwd" and
4690
+ n = 20 and
4691
+ Stage2:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4692
+ or
4693
+ stage = "2 Rev" and
4694
+ n = 25 and
4695
+ Stage2:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4696
+ }
4697
+
4698
+ predicate stageStats3 (
4699
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4700
+ int calledges , int tfnodes , int tftuples
4701
+ ) {
4702
+ stageStats2 ( n , stage , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4703
+ or
4704
+ stage = "3 Fwd" and
4705
+ n = 30 and
4706
+ Stage3:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4707
+ or
4708
+ stage = "3 Rev" and
4709
+ n = 35 and
4710
+ Stage3:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4711
+ }
4712
+
4713
+ predicate stageStats4 (
4714
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4715
+ int calledges , int tfnodes , int tftuples
4716
+ ) {
4717
+ stageStats3 ( n , stage , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4718
+ or
4719
+ stage = "4 Fwd" and
4720
+ n = 40 and
4721
+ Stage4:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4722
+ or
4723
+ stage = "4 Rev" and
4724
+ n = 45 and
4725
+ Stage4:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4726
+ }
4727
+
4728
+ predicate stageStats5 (
4729
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4730
+ int calledges , int tfnodes , int tftuples
4731
+ ) {
4732
+ stageStats4 ( n , stage , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4733
+ or
4734
+ stage = "5 Fwd" and
4735
+ n = 50 and
4736
+ Stage5:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4737
+ or
4738
+ stage = "5 Rev" and
4739
+ n = 55 and
4740
+ Stage5:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4741
+ }
4742
+
4743
+ predicate stageStats (
4744
+ int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
4745
+ int calledges , int tfnodes , int tftuples
4746
+ ) {
4747
+ stageStats5 ( n , stage , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
4748
+ or
4749
+ stage = "6 Fwd" and
4750
+ n = 60 and
4751
+ finalStats ( true , nodes , fields , conscand , states , tuples ) and
4752
+ calledges = - 1 and
4753
+ tfnodes = - 1 and
4754
+ tftuples = - 1
4755
+ or
4756
+ stage = "6 Rev" and
4757
+ n = 65 and
4758
+ finalStats ( false , nodes , fields , conscand , states , tuples ) and
4759
+ calledges = - 1 and
4760
+ tfnodes = - 1 and
4761
+ tftuples = - 1
4762
+ }
4703
4763
}
4704
4764
4705
4765
private signature predicate flag ( ) ;
0 commit comments