More minor improvements to synth-rr (#1597)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index c0f7f0ac2c0f2677d776e9016a96bfda7db7a4f5..91400479f4ff9001707150079fbf61dc015b8590 100644 (file)
--- 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 b8f016a7965ed34e206836246c89f8c107c5d25a..b6ba792df633cbca584ea6f2ce34a2105817f63b 100644 (file)
--- 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 38cfb9ba701439da7ccdd7bfa8afebc32141d8ec..fbafb8b8ce1b0f70218064668cc0cc4c83cacb94 100644 (file)
--- 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 6913633118b9e6a646c0d0efa1e68fd34f9b177f..644e5b3ef3b0a5aa293995771d3aa7f618212023 100644 (file)
--- 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 */