Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

22 files changed, 325 insertions, 323 deletions

diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index 4a08838fe..deefb02cf 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -45,7 +45,6 @@ namespace arrays {
 
 public:
   StaticFactManager() {}
-  ~StaticFactManager() throw() { }
 
   /**
    * Return a Node's union-find representative, doing path compression.
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index eb60f339b..3028eaf17 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -56,14 +56,12 @@ class UnionFind : context::ContextNotifyObj {
   /** Our current offset in the d_trace stack (context-dependent). */
   context::CDO<size_t> d_offset;
 
-public:
+ public:
   UnionFind(context::Context* ctxt) :
     context::ContextNotifyObj(ctxt),
     d_offset(ctxt, 0) {
   }
 
-  ~UnionFind() throw() { }
-
   /**
    * Return a Node's union-find representative, doing path compression.
    */
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 0e7614221..33dd4387e 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -180,7 +180,7 @@ public:
   bool hasBBAtom(TNode atom) const; 
 
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
-  ~TLazyBitblaster() throw();
+  ~TLazyBitblaster();
   /**
    * Pushes the assumption literal associated with node to the SAT
    * solver assumption queue. 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 831b767e0..d108a37f0 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -71,7 +71,8 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
   d_abstraction = abs;
 }
 
-TLazyBitblaster::~TLazyBitblaster() throw() {
+TLazyBitblaster::~TLazyBitblaster()
+{
   delete d_cnfStream;
   delete d_nullRegistrar;
   delete d_nullContext;
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index a27d3a64e..718121499 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -49,15 +49,13 @@ public:
     return utils::mkConst(d_size, d_bits);
   }
 
-  BitVectorEnumerator& operator++() throw() {
+  BitVectorEnumerator& operator++()
+  {
     d_bits += 1;
     return *this;
   }
 
-  bool isFinished() throw() {
-    return d_bits != d_bits.modByPow2(d_size);
-  }
-
+  bool isFinished() { return d_bits != d_bits.modByPow2(d_size); }
 };/* BitVectorEnumerator */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index cc8cee481..317795f0d 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -44,15 +44,13 @@ class LemmaStatus {
       : d_rewrittenLemma(rewrittenLemma), d_level(level) {}
 
   /** Get the T-rewritten form of the lemma. */
-  TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; }
-
+  TNode getRewrittenLemma() const { return d_rewrittenLemma; }
   /**
    * Get the user-level at which the lemma resides.  After this user level
    * is popped, the lemma is un-asserted from the SAT layer.  This level
    * will be 0 if the lemma didn't reach the SAT layer at all.
    */
-  unsigned getLevel() const throw() { return d_level; }
-
+  unsigned getLevel() const { return d_level; }
  private:
   Node d_rewrittenLemma;
   unsigned d_level;
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 89cd8b6a8..c451f0489 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -89,11 +89,13 @@ private:
   bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
 public:
   AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
-  ~AbsMbqiBuilder() throw() {}
+
   //process build model
-  bool processBuildModel(TheoryModel* m);
+  bool processBuildModel(TheoryModel* m) override;
   //do exhaustive instantiation
-  int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+  int doExhaustiveInstantiation(FirstOrderModel* fm,
+                                Node q,
+                                int effort) override;
 };
 
 }
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index dd71ef56e..4662d7c4c 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -61,25 +61,26 @@ public:
 
 /** candidate generator queue (for manual candidate generation) */
 class CandidateGeneratorQueue : public CandidateGenerator {
-private:
+ private:
   std::vector< Node > d_candidates;
   int d_candidate_index;
-public:
+
+ public:
   CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
-  ~CandidateGeneratorQueue() throw() {}
 
-  void addCandidate( Node n );
+  void addCandidate(Node n) override;
 
-  void resetInstantiationRound(){}
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override {}
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };/* class CandidateGeneratorQueue */
 
 //the default generator
 class CandidateGeneratorQE : public CandidateGenerator
 {
   friend class CandidateGeneratorQEDisequal;
-private:
+
+ private:
   //operator you are looking for
   Node d_op;
   //the equality class iterator
@@ -102,56 +103,56 @@ private:
   bool isLegalOpCandidate( Node n );
   Node d_n;
   std::map< Node, bool > d_exclude_eqc;
-public:
+
+ public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
-  ~CandidateGeneratorQE() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
   void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
   bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
 };
 
 class CandidateGeneratorQELitEq : public CandidateGenerator
 {
-private:
+ private:
   //the equality classes iterator
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
   Node d_match_pattern;
   Node d_match_gterm;
   bool d_do_mgt;
-public:
+
+ public:
   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitEq() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 class CandidateGeneratorQELitDeq : public CandidateGenerator
 {
-private:
+ private:
   //the equality class iterator for false
   eq::EqClassIterator d_eqc_false;
   //equality you are trying to match disequalities for
   Node d_match_pattern;
   //type of disequality
   TypeNode d_match_pattern_type;
-public:
+
+ public:
   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitDeq() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 class CandidateGeneratorQEAll : public CandidateGenerator
 {
-private:
+ private:
   //the equality classes iterator
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
@@ -162,13 +163,13 @@ private:
   unsigned d_index;
   //first time
   bool d_firstTime;
-public:
+
+ public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQEAll() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index fa74795c3..85a7d3eb4 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -399,7 +399,7 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 public:
   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
-  ~ConjectureGenerator() throw() {}
+
   /* needs check */
   bool needsCheck( Theory::Effort e );
   /* reset at a round */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 6749a8c0d..e7070b469 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -836,7 +836,8 @@ FirstOrderModel(qe, c, name){
 
 }
 
-FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
+FirstOrderModelFmc::~FirstOrderModelFmc()
+{
   for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
     delete (*i).second;
   }
@@ -1004,7 +1005,8 @@ FirstOrderModel(qe, c, name) {
 
 }
 
-FirstOrderModelAbs::~FirstOrderModelAbs() throw() {
+FirstOrderModelAbs::~FirstOrderModelAbs()
+{
   for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
     delete (*i).second;
   }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 57582a856..0c4b6b7a4 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -93,7 +93,7 @@ class FirstOrderModel : public TheoryModel
 {
  public:
   FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModel() throw() {}
+
   virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
   virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
@@ -214,7 +214,7 @@ private:
 //the following functions are for evaluating quantifier bodies
 public:
   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
-  ~FirstOrderModelIG() throw() {}
+
   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
@@ -257,7 +257,7 @@ private:
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModelFmc() throw();
+  ~FirstOrderModelFmc() override;
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
@@ -277,24 +277,26 @@ class AbsDef;
 
 class FirstOrderModelAbs : public FirstOrderModel
 {
-public:
+ public:
   std::map< Node, AbsDef * > d_models;
   std::map< Node, bool > d_models_valid;
   std::map< TNode, unsigned > d_rep_id;
   std::map< TypeNode, unsigned > d_domain;
   std::map< Node, std::vector< int > > d_var_order;
   std::map< Node, std::map< int, int > > d_var_index;
-private:
+
+ private:
   /** get current model value */
-  void processInitializeModelForTerm(Node n);
-  void processInitializeQuantifier( Node q );
+  void processInitializeModelForTerm(Node n) override;
+  void processInitializeQuantifier(Node q) override;
   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
   TNode getUsedRepresentative( TNode n );
-public:
+
+ public:
   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
-  ~FirstOrderModelAbs() throw();
-  FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
-  void processInitialize( bool ispre );
+  ~FirstOrderModelAbs() override;
+  FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; }
+  void processInitialize(bool ispre) override;
   unsigned getRepresentativeId( TNode n );
   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
   Node getFunctionValue(Node op, const char* argPrefix );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index c5d005969..f6d16dc03 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -134,7 +134,6 @@ private:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
-  ~FullModelChecker() throw() {}
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 884ed29f5..46ae8aa84 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -59,7 +59,8 @@ InstMatchGenerator::InstMatchGenerator() {
   d_independent_gen = false;
 }
 
-InstMatchGenerator::~InstMatchGenerator() throw() {
+InstMatchGenerator::~InstMatchGenerator()
+{
   for( unsigned i=0; i<d_children.size(); i++ ){
     delete d_children[i];
   }
@@ -692,10 +693,6 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
   }
 }
 
-InstMatchGeneratorMultiLinear::~InstMatchGeneratorMultiLinear() throw() {
-
-}
-
 int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
   for( unsigned i=0; i<d_children.size(); i++ ){
     if( !d_children[i]->reset( Node::null(), qe ) ){
@@ -814,7 +811,8 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
   }
 }
 
-InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
+{
   for( unsigned i=0; i<d_children.size(); i++ ){
     delete d_children[i];
   }
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 95faf0279..fc913c7cf 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -191,231 +191,231 @@ class CandidateGenerator;
 * ground terms not in the equivalence class of b.
 */
 class InstMatchGenerator : public IMGenerator {
-public:
- /** destructor */
- virtual ~InstMatchGenerator() throw();
+ public:
+  /** destructor */
+  ~InstMatchGenerator() override;
 
- /** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
- /** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
- /** Get the next match. */
- int getNextMatch(Node q,
-                  InstMatch& m,
-                  QuantifiersEngine* qe,
-                  Trigger* tparent) override;
- /** Add instantiations. */
- int addInstantiations(Node q,
-                       QuantifiersEngine* qe,
-                       Trigger* tparent) override;
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
+  /** Add instantiations. */
+  int addInstantiations(Node q,
+                        QuantifiersEngine* qe,
+                        Trigger* tparent) override;
 
- /** set active add flag (true by default)
-  *
- * If active add is true, we call sendInstantiation in calls to getNextMatch,
- * instead of returning the match. This is necessary so that we can ensure
- * policies that are dependent upon knowing when instantiations are
- * successfully added to the output channel through
- * Instantiate::addInstantiation(...).
- */
- void setActiveAdd(bool val);
- /** Get active score for this inst match generator
-  *
-  * See Trigger::getActiveScore for details.
+  /** set active add flag (true by default)
+   *
+  * If active add is true, we call sendInstantiation in calls to getNextMatch,
+  * instead of returning the match. This is necessary so that we can ensure
+  * policies that are dependent upon knowing when instantiations are
+  * successfully added to the output channel through
+  * Instantiate::addInstantiation(...).
   */
- int getActiveScore(QuantifiersEngine* qe);
- /** exclude match
-  *
-  * Exclude matching d_match_pattern with Node n on subsequent calls to
-  * getNextMatch.
+  void setActiveAdd(bool val);
+  /** Get active score for this inst match generator
+   *
+   * See Trigger::getActiveScore for details.
+   */
+  int getActiveScore(QuantifiersEngine* qe);
+  /** exclude match
+   *
+   * Exclude matching d_match_pattern with Node n on subsequent calls to
+   * getNextMatch.
+   */
+  void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
+  /** Get current match.
+   * Returns the term we are currently matching.
+   */
+  Node getCurrentMatch() { return d_curr_matched; }
+  /** set that this match generator is independent
+   *
+  * A match generator is indepndent when this generator fails to produce a
+  * match in a call to getNextMatch, the overall matching fails.
   */
- void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
- /** Get current match.
-  * Returns the term we are currently matching.
+  void setIndependent() { d_independent_gen = true; }
+  //-------------------------------construction of inst match generators
+  /** mkInstMatchGenerator for single triggers, calls the method below */
+  static InstMatchGenerator* mkInstMatchGenerator(Node q,
+                                                  Node pat,
+                                                  QuantifiersEngine* qe);
+  /** mkInstMatchGenerator for the multi trigger case
+  *
+  * This linked list of InstMatchGenerator classes with one
+  * InstMatchGeneratorMultiLinear at the head and a list of trailing
+  * InstMatchGenerators corresponding to each unique subterm of pats with
+  * free variables.
   */
- Node getCurrentMatch() { return d_curr_matched; }
- /** set that this match generator is independent
+  static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
+                                                       std::vector<Node>& pats,
+                                                       QuantifiersEngine* qe);
+  /** mkInstMatchGenerator
   *
- * A match generator is indepndent when this generator fails to produce a
- * match in a call to getNextMatch, the overall matching fails.
- */
- void setIndependent() { d_independent_gen = true; }
- //-------------------------------construction of inst match generators
- /** mkInstMatchGenerator for single triggers, calls the method below */
- static InstMatchGenerator* mkInstMatchGenerator(Node q,
-                                                 Node pat,
-                                                 QuantifiersEngine* qe);
- /** mkInstMatchGenerator for the multi trigger case
- *
- * This linked list of InstMatchGenerator classes with one
- * InstMatchGeneratorMultiLinear at the head and a list of trailing
- * InstMatchGenerators corresponding to each unique subterm of pats with
- * free variables.
- */
- static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
-                                                      std::vector<Node>& pats,
-                                                      QuantifiersEngine* qe);
- /** mkInstMatchGenerator
- *
- * This generates a linked list of InstMatchGenerators for each unique
- * subterm of pats with free variables.
- *
- * q is the quantified formula associated with the generator we are making
- * pats is a set of terms we are making InstMatchGenerator nodes for
- * qe is a pointer to the quantifiers engine (used for querying necessary
- * information during initialization) pat_map_init maps from terms to
- * generators we have already made for them.
- *
- * It calls initialize(...) for all InstMatchGenerators generated by this call.
- */
- static InstMatchGenerator* mkInstMatchGenerator(
-     Node q,
-     std::vector<Node>& pats,
-     QuantifiersEngine* qe,
-     std::map<Node, InstMatchGenerator*>& pat_map_init);
- //-------------------------------end construction of inst match generators
-
-protected:
- /** constructors
+  * This generates a linked list of InstMatchGenerators for each unique
+  * subterm of pats with free variables.
   *
- * These are intentionally private, and are called during linked list
- * construction in mkInstMatchGenerator.
- */
- InstMatchGenerator(Node pat);
- InstMatchGenerator();
- /** The pattern we are producing matches for.
+  * q is the quantified formula associated with the generator we are making
+  * pats is a set of terms we are making InstMatchGenerator nodes for
+  * qe is a pointer to the quantifiers engine (used for querying necessary
+  * information during initialization) pat_map_init maps from terms to
+  * generators we have already made for them.
   *
- * This term and d_match_pattern can be different since this
- * term may involve  information regarding phase and (dis)equality entailment,
- * or other special cases of Triggers.
- *
- * For example, for the trigger for P( x ) = false, which matches P( x ) with
- * P( t ) in the equivalence class of false,
- *   P( x ) = false is d_pattern
- *   P( x ) is d_match_pattern
- * Another example, for pure theory triggers like head( x ), we have
- *   head( x ) is d_pattern
- *   x is d_match_pattern
- * since head( x ) can match any (List) datatype term x.
- *
- * If null, this is a multi trigger that is merging matches from d_children,
- * which is used in InstMatchGeneratorMulti.
- */
- Node d_pattern;
- /** The match pattern
-  * This is the term that is matched against ground terms,
-  * see examples above.
-  */
- Node d_match_pattern;
- /** The current term we are matching. */
- Node d_curr_matched;
- /** do we need to call reset on this generator? */
- bool d_needsReset;
- /** candidate generator
-  * This is the back-end utility for InstMatchGenerator.
-  * It generates a stream of candidate terms to match against d_match_pattern
-  * below, dependending upon what kind of term we are matching
-  * (e.g. a matchable term, a variable, a relation, etc.).
+  * It calls initialize(...) for all InstMatchGenerators generated by this call.
   */
- CandidateGenerator* d_cg;
- /** children generators
-  * These match generators correspond to the children of the term
-  * we are matching with this generator.
-  * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
-  * in the example (EX1) above.
-  */
- std::vector<InstMatchGenerator*> d_children;
- /** for each child, the index in the term
-  * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
-  * in the example (EX1) above, indicating it is the 2nd child
-  * of the term.
+  static InstMatchGenerator* mkInstMatchGenerator(
+      Node q,
+      std::vector<Node>& pats,
+      QuantifiersEngine* qe,
+      std::map<Node, InstMatchGenerator*>& pat_map_init);
+  //-------------------------------end construction of inst match generators
+
+ protected:
+  /** constructors
+   *
+  * These are intentionally private, and are called during linked list
+  * construction in mkInstMatchGenerator.
   */
- std::vector<int> d_children_index;
- /** children types
+  InstMatchGenerator(Node pat);
+  InstMatchGenerator();
+  /** The pattern we are producing matches for.
+   *
+  * This term and d_match_pattern can be different since this
+  * term may involve  information regarding phase and (dis)equality entailment,
+  * or other special cases of Triggers.
   *
-  * If d_match_pattern is an instantiation constant, then this is a singleton
-  * vector containing the variable number of the d_match_pattern itself.
-  * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
-  * index i, d_children[i] stores the type of node ti is, where:
-  *   >= 0 : variable (indicates its number),
-  *   -1 : ground term,
-  *   -2 : child term.
-  */
- std::vector<int> d_children_types;
- /** The next generator in the linked list
-  * that this generator is a part of.
-  */
- InstMatchGenerator* d_next;
- /** The equivalence class we are currently matching in. */
- Node d_eq_class;
- /** If non-null, then this is a relational trigger of the form x ~
-  * d_eq_class_rel. */
- Node d_eq_class_rel;
- /** Excluded matches
- * Stores the terms we are not allowed to match.
- * These can for instance be specified by the smt2
- * extended syntax (! ... :no-pattern).
- */
- std::map<Node, bool> d_curr_exclude_match;
- /** Current first candidate
- * Used in a key fail-quickly optimization which generates
- * the first candidate term to match during reset().
- */
- Node d_curr_first_candidate;
- /** Indepdendent generate
- * If this flag is true, failures to match should be cached.
- */
- bool d_independent_gen;
- /** active add flag, described above. */
- bool d_active_add;
- /** cached value of d_match_pattern.getType() */
- TypeNode d_match_pattern_type;
- /** the match operator for d_match_pattern
+  * For example, for the trigger for P( x ) = false, which matches P( x ) with
+  * P( t ) in the equivalence class of false,
+  *   P( x ) = false is d_pattern
+  *   P( x ) is d_match_pattern
+  * Another example, for pure theory triggers like head( x ), we have
+  *   head( x ) is d_pattern
+  *   x is d_match_pattern
+  * since head( x ) can match any (List) datatype term x.
   *
-  * See TermDatabase::getMatchOperator for details on match operators.
+  * If null, this is a multi trigger that is merging matches from d_children,
+  * which is used in InstMatchGeneratorMulti.
   */
- Node d_match_pattern_op;
- /** get the match against ground term or formula t.
-  *
-  * d_match_pattern and t should have the same shape, that is,
-  * their match operator (see TermDatabase::getMatchOperator) is the same.
-  * only valid for use where !d_match_pattern.isNull().
+  Node d_pattern;
+  /** The match pattern
+   * This is the term that is matched against ground terms,
+   * see examples above.
+   */
+  Node d_match_pattern;
+  /** The current term we are matching. */
+  Node d_curr_matched;
+  /** do we need to call reset on this generator? */
+  bool d_needsReset;
+  /** candidate generator
+   * This is the back-end utility for InstMatchGenerator.
+   * It generates a stream of candidate terms to match against d_match_pattern
+   * below, dependending upon what kind of term we are matching
+   * (e.g. a matchable term, a variable, a relation, etc.).
+   */
+  CandidateGenerator* d_cg;
+  /** children generators
+   * These match generators correspond to the children of the term
+   * we are matching with this generator.
+   * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
+   * in the example (EX1) above.
+   */
+  std::vector<InstMatchGenerator*> d_children;
+  /** for each child, the index in the term
+   * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
+   * in the example (EX1) above, indicating it is the 2nd child
+   * of the term.
+   */
+  std::vector<int> d_children_index;
+  /** children types
+   *
+   * If d_match_pattern is an instantiation constant, then this is a singleton
+   * vector containing the variable number of the d_match_pattern itself.
+   * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
+   * index i, d_children[i] stores the type of node ti is, where:
+   *   >= 0 : variable (indicates its number),
+   *   -1 : ground term,
+   *   -2 : child term.
+   */
+  std::vector<int> d_children_types;
+  /** The next generator in the linked list
+   * that this generator is a part of.
+   */
+  InstMatchGenerator* d_next;
+  /** The equivalence class we are currently matching in. */
+  Node d_eq_class;
+  /** If non-null, then this is a relational trigger of the form x ~
+   * d_eq_class_rel. */
+  Node d_eq_class_rel;
+  /** Excluded matches
+  * Stores the terms we are not allowed to match.
+  * These can for instance be specified by the smt2
+  * extended syntax (! ... :no-pattern).
   */
- int getMatch(
-     Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
- /** Initialize this generator.
-  *
-  * q is the quantified formula associated with this generator.
-  *
-  * This constructs the appropriate information about what
-  * patterns we are matching and children generators.
-  *
-  * It may construct new (child) generators needed to implement
-  * the matching algorithm for this term. For each new generator
-  * constructed in this way, it adds them to gens.
+  std::map<Node, bool> d_curr_exclude_match;
+  /** Current first candidate
+  * Used in a key fail-quickly optimization which generates
+  * the first candidate term to match during reset().
   */
- void initialize(Node q,
-                 QuantifiersEngine* qe,
-                 std::vector<InstMatchGenerator*>& gens);
- /** Continue next match
-  *
- * This is called during getNextMatch when the current generator in the linked
- * list succesfully satisfies its matching constraint. This function either
- * calls getNextMatch of the next element in the linked list, or finalizes the
- * match (calling sendInstantiation(...) if active add is true, or returning a
- * value >0 if active add is false).  Its return value has the same semantics
- * as getNextMatch.
- */
- int continueNextMatch(Node q,
-                       InstMatch& m,
-                       QuantifiersEngine* qe,
-                       Trigger* tparent);
- /** Get inst match generator
-  *
-  * Gets the InstMatchGenerator that implements the
-  * appropriate matching algorithm for n within q
-  * within a linked list of InstMatchGenerators.
+  Node d_curr_first_candidate;
+  /** Indepdendent generate
+  * If this flag is true, failures to match should be cached.
   */
- static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
+  bool d_independent_gen;
+  /** active add flag, described above. */
+  bool d_active_add;
+  /** cached value of d_match_pattern.getType() */
+  TypeNode d_match_pattern_type;
+  /** the match operator for d_match_pattern
+   *
+   * See TermDatabase::getMatchOperator for details on match operators.
+   */
+  Node d_match_pattern_op;
+  /** get the match against ground term or formula t.
+   *
+   * d_match_pattern and t should have the same shape, that is,
+   * their match operator (see TermDatabase::getMatchOperator) is the same.
+   * only valid for use where !d_match_pattern.isNull().
+   */
+  int getMatch(
+      Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
+  /** Initialize this generator.
+   *
+   * q is the quantified formula associated with this generator.
+   *
+   * This constructs the appropriate information about what
+   * patterns we are matching and children generators.
+   *
+   * It may construct new (child) generators needed to implement
+   * the matching algorithm for this term. For each new generator
+   * constructed in this way, it adds them to gens.
+   */
+  void initialize(Node q,
+                  QuantifiersEngine* qe,
+                  std::vector<InstMatchGenerator*>& gens);
+  /** Continue next match
+   *
+  * This is called during getNextMatch when the current generator in the linked
+  * list succesfully satisfies its matching constraint. This function either
+  * calls getNextMatch of the next element in the linked list, or finalizes the
+  * match (calling sendInstantiation(...) if active add is true, or returning a
+  * value >0 if active add is false).  Its return value has the same semantics
+  * as getNextMatch.
+  */
+  int continueNextMatch(Node q,
+                        InstMatch& m,
+                        QuantifiersEngine* qe,
+                        Trigger* tparent);
+  /** Get inst match generator
+   *
+   * Gets the InstMatchGenerator that implements the
+   * appropriate matching algorithm for n within q
+   * within a linked list of InstMatchGenerators.
+   */
+  static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 };/* class InstMatchGenerator */
 
 /** match generator for Boolean term ITEs
@@ -424,7 +424,7 @@ protected:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
-  virtual ~VarMatchGeneratorBooleanTerm() throw() {}
+
   /** Reset */
   bool reset(Node eqc, QuantifiersEngine* qe) override
   {
@@ -451,7 +451,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
-  virtual ~VarMatchGeneratorTermSubs() throw() {}
+
   /** Reset */
   bool reset(Node eqc, QuantifiersEngine* qe) override
   {
@@ -515,9 +515,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator {
   friend class InstMatchGenerator;
 
  public:
-  /** destructor */
-  virtual ~InstMatchGeneratorMultiLinear() throw();
-
   /** Reset. */
   bool reset(Node eqc, QuantifiersEngine* qe) override;
   /** Get the next match. */
@@ -552,7 +549,7 @@ class InstMatchGeneratorMulti : public IMGenerator {
                           std::vector<Node>& pats,
                           QuantifiersEngine* qe);
   /** destructor */
-  virtual ~InstMatchGeneratorMulti() throw();
+  ~InstMatchGeneratorMulti() override;
 
   /** Reset instantiation round. */
   void resetInstantiationRound(QuantifiersEngine* qe) override;
@@ -641,8 +638,7 @@ class InstMatchGeneratorSimple : public IMGenerator {
  public:
   /** constructors */
   InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
-  /** destructor */
-  ~InstMatchGeneratorSimple() throw() {}
+
   /** Reset instantiation round. */
   void resetInstantiationRound(QuantifiersEngine* qe) override;
   /** Add instantiations. */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index bd2b8e78e..70dc9c4e9 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -48,8 +48,6 @@ d_nested_qe_waitlist_proc( qe->getUserContext() )
   d_qid_count = 0;
 }
 
-InstStrategyCbqi::~InstStrategyCbqi() throw(){}
-
 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
@@ -673,7 +671,8 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
   d_check_vts_lemma_lc = false;
 }
 
-InstStrategyCegqi::~InstStrategyCegqi() throw () {
+InstStrategyCegqi::~InstStrategyCegqi()
+{
   delete d_out;
 
   for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 0b23de10d..c2520a973 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -35,7 +35,8 @@ namespace quantifiers {
 class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-protected:
+
+ protected:
   bool d_cbqi_set_quant_inactive;
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
@@ -64,7 +65,8 @@ protected:
   /** process functions */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
-protected:
+
+ protected:
   //for identification
   uint64_t d_qid_count;
   //nested qe map
@@ -90,12 +92,14 @@ protected:
   NodeIntMap d_nested_qe_waitlist_size;
   NodeIntMap d_nested_qe_waitlist_proc;
   std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
-public:
+
+ public:
   //do nested quantifier elimination
   Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
-public:
+
+ public:
   InstStrategyCbqi( QuantifiersEngine * qe );
-  ~InstStrategyCbqi() throw();
+
   /** whether to do CBQI for quantifier q */
   bool doCbqi( Node q );
   /** process functions */
@@ -138,7 +142,7 @@ protected:
   void registerCounterexampleLemma( Node q, Node lem );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi() throw();
+  ~InstStrategyCegqi() override;
 
   bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 73e2937ab..511aebf3b 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -38,7 +38,7 @@ protected:
   unsigned d_triedLemmas;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilder() throw() {}
+
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
   // >0 : success
@@ -77,7 +77,8 @@ public:
 class QModelBuilderIG : public QModelBuilder
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-protected:
+
+ protected:
   BoolMap d_basisNoMatch;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
@@ -87,7 +88,8 @@ protected:
   bool d_didInstGen;
   /** process build model */
   virtual bool processBuildModel( TheoryModel* m );
-protected:
+
+ protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
   //initialize quantifiers, return number of lemmas produced
@@ -100,20 +102,23 @@ protected:
   virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
   //theory-specific build models
   virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
-protected:
+
+ protected:
   //map from quantifiers to if are SAT
   //std::map< Node, bool > d_quant_sat;
   //which quantifiers have been initialized
   std::map< Node, bool > d_quant_basis_match_added;
   //map from quantifiers to model basis match
   std::map< Node, InstMatch > d_quant_basis_match;
-protected:  //helper functions
+
+ protected:  // helper functions
   /** term has constant definition */
   bool hasConstantDefinition( Node n );
-public:
+
+ public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilderIG() throw() {}
-public:
+
+ public:
   /** statistics class */
   class Statistics {
   public:
@@ -152,8 +157,8 @@ public:
 
 class QModelBuilderDefault : public QModelBuilderIG
 {
-private:    ///information for (old) InstGen
-  //map from quantifiers to their selection literals
+ private:  /// information for (old) InstGen
+  // map from quantifiers to their selection literals
   std::map< Node, Node > d_quant_selection_lit;
   std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
   //map from quantifiers to their selection literal terms
@@ -164,20 +169,23 @@ private:    ///information for (old) InstGen
   std::map< Node, std::vector< Node > > d_op_selection_terms;
   //get selection score
   int getSelectionScore( std::vector< Node >& uf_terms );
-protected:
+
+ protected:
   //reset
-  void reset( FirstOrderModel* fm );
+  void reset(FirstOrderModel* fm) override;
   //analyze quantifier
-  void analyzeQuantifier( FirstOrderModel* fm, Node f );
+  void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
   //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen( FirstOrderModel* fm, Node f );
+  int doInstGen(FirstOrderModel* fm, Node f) override;
   //theory-specific build models
   void constructModelUf( FirstOrderModel* fm, Node op );
-protected:
+
+ protected:
   std::map< Node, QuantPhaseReq > d_phase_reqs;
-public:
+
+ public:
   QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-  ~QModelBuilderDefault() throw() {}
+
   //options
   bool optReconsiderFuncConstants() { return true; }
   //has inst gen
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index f4d0e8e43..3448e967b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -236,7 +236,7 @@ private:  //for equivalence classes
   bool areMatchDisequal( TNode n1, TNode n2 );
 public:
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
-  ~QuantConflictFind() throw() {}
+
   /** register quantifier */
   void registerQuantifier( Node q );
 public:
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index d2e9ec77b..47adddd9e 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -73,7 +73,6 @@ private:
   TNode getUnivRepresentativeInternal( TNode n );
 public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
-  virtual ~QuantEqualityEngine() throw (){}
 
   /* whether this module needs to check this round */
   bool needsCheck( Theory::Effort e );
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index d56e7c730..cfca96259 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -49,7 +49,6 @@ private:
   int checkRewriteRule( Node f, Theory::Effort e );
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
-  ~RewriteEngine() throw() {}
 
   bool needsCheck( Theory::Effort e );
   void check(Theory::Effort e, QEffort quant_e);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index ab844c6ec..934a09a8e 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -80,7 +80,7 @@ class TheoryModel : public Model
   friend class TheoryEngineModelBuilder;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
-  virtual ~TheoryModel() throw();
+  ~TheoryModel() override;
 
   /** reset the model */
   virtual void reset();
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 64ca41df2..bc729bcbf 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -154,17 +154,16 @@ private:
 
   Statistics d_stats;
 
-protected:
-
-  void contextNotifyPop() {
+ protected:
+  void contextNotifyPop() override
+  {
     Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
     clear();
   }
 
-public:
-
+ public:
   SymmetryBreaker(context::Context* context, std::string name = "");
-  ~SymmetryBreaker() throw() {}
+
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);