From: Tim King <taking@cs.nyu.edu>
Date: Tue, 7 Nov 2017 13:26:35 +0000 (-0800)
Subject: Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)
X-Git-Tag: cvc5-1.0.0~5504
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7add98ae1348d71e364d2407a18d40a007ce1f0b;p=cvc5.git

Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)
---

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index f27a852d9..cca475d57 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -756,26 +756,26 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool
 */
 class EquivSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
 public:
-  EquivSygusInvarianceTest(){}
-  ~EquivSygusInvarianceTest(){}
-  /** initialize this invariance test
+ EquivSygusInvarianceTest() : d_conj(nullptr) {}
+ ~EquivSygusInvarianceTest() {}
+ /** initialize this invariance test
   * tn is the sygus type for e
   * aconj/e are used for conjecture-specific symmetry breaking
   * bvr is the builtin version of the right hand side of the rewrite that we are
   * checking for invariance
   */
-  void init(quantifiers::TermDbSygus* tds, TypeNode tn,
-            quantifiers::CegConjecture* aconj, Node e, Node bvr) {
-    //compute the current examples
-    d_bvr = bvr;
-    if (aconj->getPbe()->hasExamples(e)) {
-      d_conj = aconj;
-      d_enum = e;
-      unsigned nex = aconj->getPbe()->getNumExamples(e);
-      for( unsigned i=0; i<nex; i++ ){
-        d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
-      }
-    }
+ void init(quantifiers::TermDbSygus* tds, TypeNode tn,
+           quantifiers::CegConjecture* aconj, Node e, Node bvr) {
+   // compute the current examples
+   d_bvr = bvr;
+   if (aconj->getPbe()->hasExamples(e)) {
+     d_conj = aconj;
+     d_enum = e;
+     unsigned nex = aconj->getPbe()->getNumExamples(e);
+     for (unsigned i = 0; i < nex; i++) {
+       d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
+     }
+   }
   }
 protected:
  /** does nvn still rewrite to d_bvr? */