From 544cf41c1a5c1a3c8514c21d426ad66e578e67b0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 10 Feb 2018 20:13:29 -0600
Subject: [PATCH] More minor improvements to synth-rr (#1597)

---
 src/theory/datatypes/datatypes_sygus.cpp          | 13 +++++++------
 src/theory/quantifiers/ce_guided_conjecture.cpp   |  3 +++
 .../quantifiers/ce_guided_instantiation.cpp       | 15 +++++++++++----
 src/theory/quantifiers/ce_guided_instantiation.h  |  2 ++
 4 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index c0f7f0ac2..91400479f 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -821,23 +821,24 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
               if (pt_index >= 0)
               {
                 Trace("sygus-rr-debug")
-                    << "; both ext-rewrite to : " << bvr << std::endl;
+                    << "; unsound: both ext-rewrite to : " << bvr << std::endl;
                 Trace("sygus-rr-debug")
-                    << "; but are not equivalent for : " << std::endl;
+                    << "; unsound: but are not equivalent for : " << std::endl;
                 std::vector<Node> vars;
                 std::vector<Node> pt;
                 its->second.getSamplePoint(pt_index, vars, pt);
                 Assert(vars.size() == pt.size());
                 for (unsigned i = 0, size = pt.size(); i < size; i++)
                 {
-                  Trace("sygus-rr-debug")
-                      << ";   " << vars[i] << " -> " << pt[i] << std::endl;
+                  Trace("sygus-rr-debug") << "; unsound:    " << vars[i]
+                                          << " -> " << pt[i] << std::endl;
                 }
                 Node bv_e = its->second.evaluate(bv, pt_index);
                 Node pbv_e = its->second.evaluate(prev_bv, pt_index);
                 Assert(bv_e != pbv_e);
-                Trace("sygus-rr-debug") << "; where they evaluate to " << pbv_e
-                                        << " and " << bv_e << std::endl;
+                Trace("sygus-rr-debug") << "; unsound: where they evaluate to "
+                                        << pbv_e << " and " << bv_e
+                                        << std::endl;
               }
               else
               {
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index b8f016a79..b6ba792df 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -20,6 +20,7 @@
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -622,6 +623,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
+      ++(d_qe->getCegInstantiation()->d_statistics.d_solutions);
 
       if (status != 0 && options::sygusRewSynth())
       {
@@ -643,6 +645,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
           // rewrite.
           out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
               << std::endl;
+          ++(d_qe->getCegInstantiation()->d_statistics.d_candidate_rewrites);
           // debugging information
           if (Trace.isOn("sygus-rr-debug"))
           {
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 38cfb9ba7..fbafb8b8c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -357,20 +357,27 @@ void CegInstantiation::preregisterAssertion( Node n ) {
   }
 }
 
-CegInstantiation::Statistics::Statistics():
-  d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
-  d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
-  d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0)
+CegInstantiation::Statistics::Statistics()
+    : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
+      d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
+      d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0),
+      d_solutions("CegConjecture::solutions", 0),
+      d_candidate_rewrites("CegConjecture::candidate_rewrites", 0)
+
 {
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_solutions);
+  smtStatisticsRegistry()->registerStat(&d_candidate_rewrites);
 }
 
 CegInstantiation::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_solutions);
+  smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites);
 }
 
 }/* namespace CVC4::theory::quantifiers */
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 691363311..644e5b3ef 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -74,6 +74,8 @@ public:
     IntStat d_cegqi_lemmas_ce;
     IntStat d_cegqi_lemmas_refine;
     IntStat d_cegqi_si_lemmas;
+    IntStat d_solutions;
+    IntStat d_candidate_rewrites;
     Statistics();
     ~Statistics();
   };/* class CegInstantiation::Statistics */
-- 
2.30.2