diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-07 05:26:35 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-07 07:26:35 -0600 |
commit | 7add98ae1348d71e364d2407a18d40a007ce1f0b (patch) | |
tree | d4520ce4d4d537d776af5bb9597c2d84f833169f | |
parent | 10278e9ec588286705468d72d04bbf03513b3c88 (diff) |
Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 30 |
1 files changed, 15 insertions, 15 deletions
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? */ |