@@ -4639,67 +4639,127 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
46394639 *
46404640 * Calculates per-stage metrics for data flow.
46414641 */
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+ }
47034763 }
47044764
47054765 private signature predicate flag ( ) ;
0 commit comments