diff options
Diffstat (limited to 'src/theory')
27 files changed, 51 insertions, 34 deletions
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 472eff883..c1f0ce545 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -226,6 +226,7 @@ inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){ } class BoundUpdateCallback { public: + virtual ~BoundUpdateCallback() {} virtual void operator()(ArithVar v, const BoundsInfo& up) = 0; }; diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index ad88aea86..734c605c6 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -36,6 +36,7 @@ namespace arith { */ class ArithVarCallBack { public: + virtual ~ArithVarCallBack() {} virtual void operator()(ArithVar x) = 0; }; @@ -45,22 +46,26 @@ public: */ class ArithVarMalloc { public: + virtual ~ArithVarMalloc() {} virtual ArithVar request() = 0; virtual void release(ArithVar v) = 0; }; class TNodeCallBack { public: + virtual ~TNodeCallBack() {} virtual void operator()(TNode n) = 0; }; class NodeCallBack { public: + virtual ~NodeCallBack() {} virtual void operator()(Node n) = 0; }; class RationalCallBack { public: + virtual ~RationalCallBack() {} virtual Rational operator()() const = 0; }; diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index f6717d141..99ec6e52c 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -159,7 +159,8 @@ public: } void dropNonZeroes(){ - std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero); + d_vec.erase(std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero), + d_vec.end()); } const Border& top() const { diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 73235d490..6c218eb0b 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -39,6 +39,7 @@ const RowIndex ROW_INDEX_SENTINEL = std::numeric_limits<RowIndex>::max(); class CoefficientChangeCallback { public: + virtual ~CoefficientChangeCallback() {} virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0; virtual void multiplyRow(RowIndex ridx, int Sgn) = 0; virtual bool canUseRow(RowIndex ridx) const = 0; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index ada9b5efd..2d7fc597a 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -135,7 +135,7 @@ protected: public: SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - ~SimplexDecisionProcedure(); + virtual ~SimplexDecisionProcedure(); /** * Tries to update the assignments of variables such that all of the @@ -217,4 +217,3 @@ protected: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 79434102e..d4d7bc04c 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -170,7 +170,7 @@ public: void storeBBAtom(TNode atom, Node atom_bb); bool hasBBAtom(TNode atom) const; TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); - ~TLazyBitblaster(); + ~TLazyBitblaster() throw(); /** * 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 fbebcd952..080f23143 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -62,7 +62,7 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { d_abstraction = abs; } -TLazyBitblaster::~TLazyBitblaster() { +TLazyBitblaster::~TLazyBitblaster() throw() { delete d_cnfStream; delete d_nullRegistrar; delete d_nullContext; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 08fe5f2e9..9dcd5ac62 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -576,8 +576,8 @@ Node TheoryBV::ppRewrite(TNode t) } else if( res.getKind() == kind::EQUAL && ((res[0].getKind() == kind::BITVECTOR_PLUS && RewriteRule<ConcatToMult>::applies(res[1])) || - res[1].getKind() == kind::BITVECTOR_PLUS && - RewriteRule<ConcatToMult>::applies(res[0]))) { + (res[1].getKind() == kind::BITVECTOR_PLUS && + RewriteRule<ConcatToMult>::applies(res[0])))) { Node mult = RewriteRule<ConcatToMult>::applies(res[0])? RewriteRule<ConcatToMult>::run<false>(res[0]) : RewriteRule<ConcatToMult>::run<true>(res[1]); @@ -747,8 +747,8 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { d_staticLearnCache.insert(in); if (in.getKind() == kind::EQUAL) { - if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL || - in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){ + if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) || + (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) { TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1]; TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 0c41e8ff7..ba9823541 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -202,10 +202,10 @@ namespace rewrite { // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder RewriteResponse compactMinMax (TNode node, bool isPreRewrite) { +#ifdef CVC4_ASSERTIONS Kind k = node.getKind(); - Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX)); - +#endif if (node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, node[0]); } else { 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 ); diff --git a/src/theory/strings/options b/src/theory/strings/options index 11156b5a4..a5b977121 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -8,7 +8,7 @@ module STRINGS "theory/strings/options.h" Strings theory option stringExp strings-exp --strings-exp bool :default false :read-write experimental features in the theory of strings -option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h" +option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h" the strategy of LB rule application: 0-lazy, 1-eager, 2-no option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate less_equal(2) :predicate-include "smt/smt_engine.h" diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 8d107d36a..cad1f3bf1 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1386,8 +1386,8 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pv bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) { for(std::set< PairNodes >::const_iterator itr = s.begin(); itr != s.end(); ++itr) { - if(itr->first == n1 && itr->second == n2 || - itr->first == n2 && itr->second == n1) { + if((itr->first == n1 && itr->second == n2) || + (itr->first == n2 && itr->second == n1)) { return true; } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5dc4d9408..d0a1eb696 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -962,8 +962,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); - if(! d_logicInfo.isTheoryEnabled(toTheoryId) && - toTheoryId != THEORY_SAT_SOLVER) { + if(toTheoryId != THEORY_SAT_SOLVER && + ! d_logicInfo.isTheoryEnabled(toTheoryId)) { stringstream ss; ss << "The logic was specified as " << d_logicInfo.getLogicString() << ", which doesn't include " << toTheoryId diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6a53cb3ab..072f579be 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -46,7 +46,7 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM d_eeContext->push(); } -TheoryModel::~TheoryModel() { +TheoryModel::~TheoryModel() throw() { d_eeContext->pop(); delete d_equalityEngine; delete d_eeContext; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index eeaf3c8da..4e5c84f42 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -38,7 +38,7 @@ protected: SubstitutionMap d_substitutions; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); - virtual ~TheoryModel(); + virtual ~TheoryModel() throw(); /** special local context for our equalityEngine so we can clear it independently of search context */ context::Context* d_eeContext; |