Fix warnings and enable -Wnon-virtual-dtor warning (#2079)

This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.

9 files changed, 12 insertions, 8 deletions

diff --git a/configure.ac b/configure.ac
index 81e3f1fdc..48ef9c7f8 100644
--- a/configure.ac
+++ b/configure.ac
@@ -988,6 +988,7 @@ CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
+CVC4_CXX_OPTION([-Wnon-virtual-dtor], [W_NON_VIRTUAL_DTOR])
 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 AC_SUBST([WERROR])
 AC_SUBST([WNO_CONVERSION_NULL])
@@ -996,9 +997,11 @@ AC_SUBST([WNO_PARENTHESES])
 AC_SUBST([WNO_UNINITIALIZED])
 AC_SUBST([WNO_UNUSED_VARIABLE])
 AC_SUBST([W_SUGGEST_OVERRIDE])
+AC_SUBST([W_NON_VIRTUAL_DTOR])
 AC_SUBST([FNO_STRICT_ALIASING])
 
 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
+CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_NON_VIRTUAL_DTOR}"
 
 # On Mac, we have to fix the visibility of standard library symbols.
 # Otherwise, exported template instantiations---even though explicitly
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index f0c1d5488..938e0f2a6 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -667,7 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
   }
 
   if (signature.getNumChildren() == 0) {
-    Assert(signature.getKind() != kind::metakind::VARIABLE);
+    Assert(signature.getMetaKind() != kind::metakind::VARIABLE);
     seen[signature] = signature;
     return signature;
   }
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 00e527aba..27f36cbf3 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -24,8 +24,7 @@ namespace theory {
 namespace quantifiers {
 
 DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
-    : d_qe(qe),
-      d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
+    : d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
       d_rewrites(qe->getUserContext())
 {
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 56f591470..9d80ebe57 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -65,8 +65,6 @@ class DynamicRewriter
   bool areEqual(Node a, Node b);
 
  private:
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** index over argument types to function skolems
    *
    * The purpose of this trie is to associate a class of interpreted operator
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 856219b73..6330bbd30 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -42,7 +42,7 @@ class Cegis : public SygusModule
 {
  public:
   Cegis(QuantifiersEngine* qe, CegConjecture* p);
-  ~Cegis() {}
+  ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node n,
                           const std::vector<Node>& candidates,
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ec338a8b2..c0f860975 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -200,7 +200,7 @@ class CegisUnif : public Cegis
 {
  public:
   CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegisUnif();
+  ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
    * Non-unification candidates have themselves as enumerators, while for
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index b01f8e1d0..fb2821e20 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -49,7 +49,7 @@ class SygusModule
 {
  public:
   SygusModule(QuantifiersEngine* qe, CegConjecture* p);
-  ~SygusModule() {}
+  virtual ~SygusModule() {}
   /** initialize
    *
    * n is the "base instantiation" of the deep-embedding version of the
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index cbce5e70c..db0ff4afb 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -93,6 +93,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st);
 class UnifContext
 {
  public:
+  virtual ~UnifContext() {}
+
   /** Get the current role
    *
    * In a particular context when constructing solutions in synthesis by
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 5e0a24dd2..1b4d3aedd 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -278,6 +278,8 @@ class SygusSampler : public LazyTrieEvaluator
 class NotifyMatch
 {
  public:
+  virtual ~NotifyMatch() {}
+
   /**
    * A notification that s is equal to n * { vars -> subs }. This function
    * should return false if we do not wish to be notified of further matches.