Changes needed to compile at Google, plus some bug fixes from Google.

13 files changed, 26 insertions, 16 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 44d327c5c..b2c49c8a3 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -89,6 +89,7 @@ private:
   bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
 public:
   AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
+  ~AbsMbqiBuilder() throw() {}
   //process build model
   void processBuildModel(TheoryModel* m, bool fullModel);
   //do exhaustive instantiation
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index c09527f89..dd241b15e 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -110,6 +110,7 @@ private:
   void addLiteralFromRange( Node lit, Node r );
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+  ~BoundedIntegers() throw() {}
 
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 7a959a70d..9d4035970 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -31,7 +31,7 @@ namespace inst {
 class CandidateGenerator {
 public:
   CandidateGenerator(){}
-  ~CandidateGenerator(){}
+  virtual ~CandidateGenerator(){}
 
   /** Get candidates functions.  These set up a context to get all match candidates.
       cg->reset( eqc );
@@ -60,7 +60,7 @@ private:
   int d_candidate_index;
 public:
   CandidateGeneratorQueue() : d_candidate_index( 0 ){}
-  ~CandidateGeneratorQueue(){}
+  ~CandidateGeneratorQueue() throw() {}
 
   void addCandidate( Node n );
 
@@ -94,7 +94,7 @@ private:
   Node d_n;
 public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
-  ~CandidateGeneratorQE(){}
+  ~CandidateGeneratorQE() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -112,7 +112,7 @@ private:
   QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitEq(){}
+  ~CandidateGeneratorQELitEq() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -130,7 +130,7 @@ private:
   QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitDeq(){}
+  ~CandidateGeneratorQELitDeq() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -154,7 +154,7 @@ private:
   bool d_firstTime;
 public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQEAll(){}
+  ~CandidateGeneratorQEAll() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index b5ebe3d7c..fc7481739 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -31,6 +31,7 @@ class CegConjecture;
 class CegqiOutput
 {
 public:
+  virtual ~CegqiOutput() {}
   virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
   virtual bool isEligibleForInstantiation( Node n ) = 0;
   virtual bool addLemma( Node lem ) = 0;
@@ -83,6 +84,7 @@ class CegqiOutputSingleInv : public CegqiOutput
 {
 public:
   CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
+  ~CegqiOutputSingleInv() {}
   CegConjectureSingleInv * d_out;
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 2d8e8e403..48694c99a 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -406,6 +406,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 eef354e75..88464bb9a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -585,7 +585,7 @@ FirstOrderModel(qe, c, name){
 
 }
 
-FirstOrderModelFmc::~FirstOrderModelFmc() {
+FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
   for(std::map<Node, Def*>::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 c2cd88e17..fbcaf938f 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -76,7 +76,7 @@ public: //for Theory Quantifiers:
   virtual void processInitializeQuantifier( Node q ) {}
 public:
   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
-  virtual ~FirstOrderModel() {}
+  virtual ~FirstOrderModel() throw() {}
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
@@ -181,7 +181,7 @@ private:
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModelFmc();
+  virtual ~FirstOrderModelFmc() throw();
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 372868ad7..9a7b05090 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -133,7 +133,7 @@ private:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
-  ~FullModelChecker(){}
+  ~FullModelChecker() throw() {}
 
   bool optBuildAtFullModel();
 
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 1be67caed..f9853ef54 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -33,6 +33,7 @@ namespace inst {
 /** base class for producing InstMatch objects */
 class IMGenerator {
 public:
+  virtual ~IMGenerator() {}
   /** reset instantiation round (call this at beginning of instantiation round) */
   virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
@@ -89,7 +90,7 @@ public:
   InstMatchGenerator( Node pat );
   InstMatchGenerator();
   /** destructor */
-  ~InstMatchGenerator(){}
+  ~InstMatchGenerator() throw() {}
   /** The pattern we are producing matches for.
       If null, this is a multi trigger that is merging matches from d_children.
   */
@@ -123,6 +124,7 @@ public:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
+  ~VarMatchGeneratorBooleanTerm() throw() {}
   Node d_comp;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -139,6 +141,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
+  ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
   Node d_subs;
   bool d_rm_prev;
@@ -186,7 +189,7 @@ public:
   /** constructors */
   InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
-  ~InstMatchGeneratorMulti(){}
+  ~InstMatchGeneratorMulti() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
@@ -218,7 +221,7 @@ public:
   /** constructors */
   InstMatchGeneratorSimple( Node f, Node pat );
   /** destructor */
-  ~InstMatchGeneratorSimple(){}
+  ~InstMatchGeneratorSimple() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9435fc97c..586cd492c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -75,7 +75,7 @@ private:
   int process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex(){}
+  ~InstStrategySimplex() throw() {}
   /** identify */
   std::string identify() const { return std::string("Simplex"); }
 };
@@ -107,7 +107,7 @@ private:
   int process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi(){}
+  ~InstStrategyCegqi() throw() {}
   
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );  
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 7679cf93f..47de4e581 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -35,7 +35,7 @@ protected:
   QuantifiersEngine* d_qe;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilder(){}
+  virtual ~QModelBuilder() throw() {}
   // is quantifier active?
   virtual bool isQuantifierActive( Node f );
   //do exhaustive instantiation
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index b2dc680f2..829b67777 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -203,6 +203,7 @@ public:
   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/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 1703a9bfc..2e2578af5 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -53,6 +53,7 @@ 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, unsigned quant_e );