From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 30 Jan 2014 22:30:21 +0000 (-0600)
Subject: stats for eq/diseq splits
X-Git-Tag: cvc5-1.0.0~7111
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab7aa25d496350be601f1fcf7befb01885c89433;p=cvc5.git

stats for eq/diseq splits
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 87283f2ef..d0876d983 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1103,6 +1103,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 
 									Node ant = mkExplain( antec );
 									sendLemma( ant, conc, "CST-SPLIT" );
+									++(d_statistics.d_eq_splits);
 									return true;
 								} else {
 									std::vector< Node > antec_new_lits;
@@ -1132,6 +1133,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 
 									Node ant = mkExplain( antec, antec_new_lits );
 									sendLemma( ant, conc, "VAR-SPLIT" );
+									++(d_statistics.d_eq_splits);
 									return true;
 								}
 							}
@@ -1436,13 +1438,13 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 											j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
 						
 						sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
+						++(d_statistics.d_deq_splits);
 						return true;
 					}else if( areEqual( li, lj ) ){
 						Assert( !areDisequal( i, j ) );
 						//splitting on demand : try to make them disequal
 						Node eq = i.eqNode( j );
 						sendSplit( i, j, "D-EQL-Split" );
-						++(d_statistics.d_deq_splits);
 						eq = Rewriter::rewrite( eq );
 						d_pending_req_phase[ eq ] = false;
 						return true;
@@ -1450,7 +1452,6 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 						//splitting on demand : try to make lengths equal
 						Node eq = li.eqNode( lj );
 						sendSplit( li, lj, "D-UNK-Split" );
-						++(d_statistics.d_deq_splits);
 						eq = Rewriter::rewrite( eq );
 						d_pending_req_phase[ eq ] = true;
 						return true;
@@ -2702,13 +2703,15 @@ int TheoryStrings::getMaxPossibleLength( Node x ) {
 
 // Stats
 TheoryStrings::Statistics::Statistics():
-  d_splits("TheoryStrings::NumOfSplits", 0),
+  d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
+  d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
   d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
   d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
   d_unroll_lemmas("TheoryStrings::NumOfUnrolls", 0),
   d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
 {
   StatisticsRegistry::registerStat(&d_splits);
+  StatisticsRegistry::registerStat(&d_eq_splits);
   StatisticsRegistry::registerStat(&d_deq_splits);
   StatisticsRegistry::registerStat(&d_loop_lemmas);
   StatisticsRegistry::registerStat(&d_unroll_lemmas);
@@ -2717,6 +2720,7 @@ TheoryStrings::Statistics::Statistics():
 
 TheoryStrings::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_splits);
+  StatisticsRegistry::unregisterStat(&d_eq_splits);
   StatisticsRegistry::unregisterStat(&d_deq_splits);
   StatisticsRegistry::unregisterStat(&d_loop_lemmas);
   StatisticsRegistry::unregisterStat(&d_unroll_lemmas);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index b7a660999..05e6ebf71 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -333,6 +333,7 @@ public:
   class Statistics {
   public:
     IntStat d_splits;
+    IntStat d_eq_splits;
     IntStat d_deq_splits;
     IntStat d_loop_lemmas;
     IntStat d_unroll_lemmas;