From 2d42e02067084617b3efb06a80c2c8003f8797c3 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 8 Feb 2018 13:52:36 -0800 Subject: [PATCH] Adding virtual destructors on classes with virtual functions. (#1583) --- src/theory/quantifiers/bv_inverter.h | 2 +- src/theory/quantifiers/ceg_instantiator.h | 2 ++ src/theory/quantifiers/sygus_invariance.h | 10 ++++++---- src/theory/quantifiers/sygus_sampler.h | 4 +++- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 10ef6ab4c..59dc543ae 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -37,7 +37,7 @@ class BvInverterQuery { public: BvInverterQuery() {} - ~BvInverterQuery() {} + virtual ~BvInverterQuery() {} /** returns the current model value of n */ virtual Node getModelValue(Node n) = 0; /** returns a bound variable of type tn */ diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index a0137abde..03983fe1a 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -52,6 +52,8 @@ class InstantiatorPreprocess; class TermProperties { public: TermProperties() : d_type(0) {} + virtual ~TermProperties() {} + // type of property for a term // for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound) int d_type; diff --git a/src/theory/quantifiers/sygus_invariance.h b/src/theory/quantifiers/sygus_invariance.h index bf3c56572..1cc43fb7d 100644 --- a/src/theory/quantifiers/sygus_invariance.h +++ b/src/theory/quantifiers/sygus_invariance.h @@ -43,6 +43,8 @@ class CegConjecture; class SygusInvarianceTest { public: + virtual ~SygusInvarianceTest(){} + /** Is nvn invariant with respect to this test ? * * - nvn is the term to check whether it is invariant. @@ -96,7 +98,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest { public: EvalSygusInvarianceTest() {} - ~EvalSygusInvarianceTest() {} + /** initialize this invariance test * This sets d_conj/d_var/d_result, where * we are checking whether: @@ -156,7 +158,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest { public: 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 @@ -197,7 +199,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest { public: DivByZeroSygusInvarianceTest() {} - ~DivByZeroSygusInvarianceTest() {} + protected: /** checks whether nvn involves division by zero. */ bool invariant(TermDbSygus* tds, Node nvn, Node x); @@ -233,7 +235,7 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest { public: NegContainsSygusInvarianceTest() : d_conj(nullptr) {} - ~NegContainsSygusInvarianceTest() {} + /** initialize this invariance test * cpbe is the conjecture utility. * e is the enumerator which we are reasoning about (associated with a synth diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index d8f2244c7..8ed4bc783 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -31,6 +31,7 @@ namespace quantifiers { class LazyTrieEvaluator { public: + virtual ~LazyTrieEvaluator() {} virtual Node evaluate(Node n, unsigned index) = 0; }; @@ -134,7 +135,8 @@ class SygusSampler : public LazyTrieEvaluator { public: SygusSampler(); - virtual ~SygusSampler() {} + ~SygusSampler() override {} + /** initialize * * tn : the return type of terms we will be testing with this class -- 2.30.2