summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-07 05:26:35 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-07 07:26:35 -0600
commit7add98ae1348d71e364d2407a18d40a007ce1f0b (patch)
treed4520ce4d4d537d776af5bb9597c2d84f833169f
parent10278e9ec588286705468d72d04bbf03513b3c88 (diff)
Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp30
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? */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback