Adding virtual destructors on classes with virtual functions. (#1583)

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 10ef6ab4ce231371b24c60a0167f3c277d13e60b..59dc543ae5b27831992631d55cda2f413fc1c2ba 100644 (file)
--- 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 a0137abde35453f438ae8416041e337f8d36eb8a..03983fe1a0ec61e7b7d895d3ff6f0cd3b0e40415 100644 (file)
--- 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 bf3c565727db03c7a219c71bbc277e7d79560778..1cc43fb7d2acf306a5eeef675c849056c9f49490 100644 (file)
--- 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 d8f2244c7dd2714f42048e256cfeb4b57cc4bcb0..8ed4bc783bb359b62e33979e99e319c5f73a41c6 100644 (file)
--- 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