From d95fe7675e20eaee86b8e804469e6db83265a005 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 21 Apr 2015 16:34:15 -0700 Subject: [PATCH] Changes needed to compile at Google, plus some bug fixes from Google. --- proofs/lfsc_checker/check.h | 6 +++--- src/context/context.h | 2 +- src/decision/justification_heuristic.cpp | 2 +- src/decision/justification_heuristic.h | 2 +- src/expr/node.h | 8 ++++---- src/expr/node_manager.cpp | 4 ++-- src/expr/node_value.cpp | 4 +--- src/expr/node_value.h | 8 +++----- src/expr/pickler.h | 2 +- src/expr/type_node.cpp | 2 +- src/expr/type_node.h | 4 ++-- src/printer/printer.h | 1 + src/prop/bvminisat/mtl/Map.h | 9 +++++---- src/prop/minisat/core/SolverTypes.h | 1 + src/prop/minisat/mtl/Map.h | 9 +++++---- src/prop/sat_solver.h | 3 ++- src/smt/smt_engine.cpp | 2 +- src/theory/arith/bound_counts.h | 1 + src/theory/arith/callbacks.h | 5 +++++ src/theory/arith/linear_equality.h | 3 ++- src/theory/arith/matrix.h | 1 + src/theory/arith/simplex.h | 3 +-- src/theory/bv/bitblaster_template.h | 2 +- src/theory/bv/lazy_bitblaster.cpp | 2 +- src/theory/bv/theory_bv.cpp | 8 ++++---- src/theory/fp/theory_fp_rewriter.cpp | 4 ++-- src/theory/quantifiers/ambqi_builder.h | 1 + src/theory/quantifiers/bounded_integers.h | 1 + src/theory/quantifiers/candidate_generator.h | 12 ++++++------ src/theory/quantifiers/ce_guided_single_inv.h | 2 ++ src/theory/quantifiers/conjecture_generator.h | 1 + src/theory/quantifiers/first_order_model.cpp | 2 +- src/theory/quantifiers/first_order_model.h | 4 ++-- src/theory/quantifiers/full_model_check.h | 2 +- src/theory/quantifiers/inst_match_generator.h | 9 ++++++--- src/theory/quantifiers/inst_strategy_cbqi.h | 4 ++-- src/theory/quantifiers/model_builder.h | 2 +- src/theory/quantifiers/quant_conflict_find.h | 1 + src/theory/quantifiers/rewrite_engine.h | 1 + src/theory/strings/options | 2 +- src/theory/strings/regexp_operation.cpp | 4 ++-- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 2 +- src/util/didyoumean.cpp | 13 +++++++++++-- 45 files changed, 97 insertions(+), 70 deletions(-) diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h index a70599b0f..756bb4db6 100644 --- a/proofs/lfsc_checker/check.h +++ b/proofs/lfsc_checker/check.h @@ -80,7 +80,7 @@ inline char our_getc() { #endif colnum = 1; break; - case EOF: + case char(EOF): break; default: colnum++; @@ -95,7 +95,7 @@ inline char non_ws() { while(isspace(c = our_getc())); if (c == ';') { // comment to end of line - while((c = our_getc()) != '\n' && c != EOF); + while((c = our_getc()) != '\n' && c != char(EOF)); return non_ws(); } return c; @@ -115,7 +115,7 @@ extern char idbuf[]; inline const char *prefix_id() { int i = 0; char c = idbuf[i++] = non_ws(); - while (!isspace(c) && c != '(' && c != ')' && c != EOF) { + while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) { if (i == IDBUF_LEN) report_error("Identifier is too long"); diff --git a/src/context/context.h b/src/context/context.h index 02d82a6d3..9c631b202 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -613,7 +613,7 @@ public: /** * Destructor does nothing: subclass must explicitly call destroy() instead. */ - virtual ~ContextObj() {} + virtual ~ContextObj() throw(AssertionException) {} /** * If you want to allocate a ContextObj object on the heap, use this diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index c9a6b7e1b..082f3cdbf 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -55,7 +55,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, Trace("decision") << "Justification heuristic enabled" << std::endl; } -JustificationHeuristic::~JustificationHeuristic() { +JustificationHeuristic::~JustificationHeuristic() throw() { StatisticsRegistry::unregisterStat(&d_helfulness); StatisticsRegistry::unregisterStat(&d_giveup); StatisticsRegistry::unregisterStat(&d_timestat); diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 9177ba44d..e1ed431d1 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -114,7 +114,7 @@ public: context::UserContext *uc, context::Context *c); - ~JustificationHeuristic(); + ~JustificationHeuristic() throw(); prop::SatLiteral getNext(bool &stopSearch); diff --git a/src/expr/node.h b/src/expr/node.h index 080034e70..2a884d35a 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -261,7 +261,7 @@ public: std::hash_map& cache) const; /** Default constructor, makes a null expression. */ - NodeTemplate() : d_nv(&expr::NodeValue::s_null) { } + NodeTemplate() : d_nv(&expr::NodeValue::null()) { } /** * Conversion between nodes that are reference-counted and those that are @@ -322,7 +322,7 @@ public: */ bool isNull() const { assertTNodeNotExpired(); - return d_nv == &expr::NodeValue::s_null; + return d_nv == &expr::NodeValue::null(); } /** @@ -1026,7 +1026,7 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { } template -NodeTemplate NodeTemplate::s_null(&expr::NodeValue::s_null); +NodeTemplate NodeTemplate::s_null(&expr::NodeValue::null()); // FIXME: escape from type system convenient but is there a better // way? Nodes conceptually don't change their expr values but of @@ -1039,7 +1039,7 @@ NodeTemplate::NodeTemplate(const expr::NodeValue* ev) : if(ref_count) { d_nv->inc(); } else { - Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::s_null, + Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(), "TNode constructed from NodeValue with rc == 0"); } } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 48aacddf2..4eb5dd680 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -112,7 +112,7 @@ NodeManager::NodeManager(ExprManager* exprManager, } void NodeManager::init() { - poolInsert( &expr::NodeValue::s_null ); + poolInsert( &expr::NodeValue::null() ); for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { Kind k = Kind(i); @@ -163,7 +163,7 @@ NodeManager::~NodeManager() { reclaimZombies(); } - poolRemove( &expr::NodeValue::s_null ); + poolRemove( &expr::NodeValue::null() ); if(Debug.isOn("gc:leaks")) { Debug("gc:leaks") << "still in pool:" << endl; diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 8af056f62..6b48fd9b7 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -32,12 +32,10 @@ using namespace std; namespace CVC4 { namespace expr { -NodeValue NodeValue::s_null(0); - string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage(); toStream(ss, -1, false, false, outlang); return ss.str(); } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index a6e7a6053..785f8909f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -74,9 +74,6 @@ namespace expr { */ class NodeValue { - /** A convenient null-valued expression value */ - static NodeValue s_null; - static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID; @@ -278,8 +275,9 @@ public: return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } - static inline const NodeValue& null() { - return s_null; + static inline NodeValue& null() { + static NodeValue* s_null = new NodeValue(0); + return *s_null; } /** diff --git a/src/expr/pickler.h b/src/expr/pickler.h index f1cdd1c65..8c3da5f40 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -74,7 +74,7 @@ protected: public: Pickler(ExprManager* em); - ~Pickler(); + virtual ~Pickler(); /** * Constructs a new Pickle of the node n. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9dbcb628f..1f2963e18 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -24,7 +24,7 @@ using namespace std; namespace CVC4 { -TypeNode TypeNode::s_null( &expr::NodeValue::s_null ); +TypeNode TypeNode::s_null( &expr::NodeValue::null() ); TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement, diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5129b7581..4f9e497ea 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -107,7 +107,7 @@ private: public: /** Default constructor, makes a null expression. */ - TypeNode() : d_nv(&expr::NodeValue::s_null) { } + TypeNode() : d_nv(&expr::NodeValue::null()) { } /** Copy constructor */ TypeNode(const TypeNode& node); @@ -404,7 +404,7 @@ public: * @return true if null */ bool isNull() const { - return d_nv == &expr::NodeValue::s_null; + return d_nv == &expr::NodeValue::null(); } /** diff --git a/src/printer/printer.h b/src/printer/printer.h index e0b80ddfc..fcc0df93c 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -44,6 +44,7 @@ class Printer { protected: // derived classes can construct, but no one else. Printer() throw() {} + virtual ~Printer() {} /** write model response to command */ virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0; diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h index 8bd5659bc..4e61d6582 100644 --- a/src/prop/bvminisat/mtl/Map.h +++ b/src/prop/bvminisat/mtl/Map.h @@ -29,16 +29,17 @@ namespace BVMinisat { // Default hash/equals functions // +static inline uint32_t hash(uint32_t x){ return x; } +static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } +static inline uint32_t hash(int32_t x) { return (uint32_t)x; } +static inline uint32_t hash(int64_t x) { return (uint32_t)x; } + template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; -static inline uint32_t hash(uint32_t x){ return x; } -static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } -static inline uint32_t hash(int32_t x) { return (uint32_t)x; } -static inline uint32_t hash(int64_t x) { return (uint32_t)x; } //================================================================================================= diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index bc60542e7..46c2666c8 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -175,6 +175,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { namespace CVC4 { class ProofProxyAbstract { public: + virtual ~ProofProxyAbstract() {} virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; }; } diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index dda6c73d1..72563e6d3 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -29,16 +29,17 @@ namespace Minisat { // Default hash/equals functions // +static inline uint32_t hash(uint32_t x){ return x; } +static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } +static inline uint32_t hash(int32_t x) { return (uint32_t)x; } +static inline uint32_t hash(int64_t x) { return (uint32_t)x; } + template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; -static inline uint32_t hash(uint32_t x){ return x; } -static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } -static inline uint32_t hash(int32_t x) { return (uint32_t)x; } -static inline uint32_t hash(int64_t x) { return (uint32_t)x; } //================================================================================================= diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index b71844590..8effa8189 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -36,7 +36,7 @@ class SatSolver { public: /** Virtual destructor */ - virtual ~SatSolver() { } + virtual ~SatSolver() throw(AssertionException) { } /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; @@ -80,6 +80,7 @@ public: class BVSatSolverInterface: public SatSolver { public: + virtual ~BVSatSolverInterface() throw(AssertionException) {} /** Interface for notifications */ class Notify { public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 229cc7c7c..04af80281 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -474,7 +474,7 @@ public: d_resourceManager = NodeManager::currentResourceManager(); } - ~SmtEnginePrivate() { + ~SmtEnginePrivate() throw() { if(d_propagatorNeedsFinish) { d_propagator.finish(); d_propagatorNeedsFinish = false; 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::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::applies(res[1])) || - res[1].getKind() == kind::BITVECTOR_PLUS && - RewriteRule::applies(res[0]))) { + (res[1].getKind() == kind::BITVECTOR_PLUS && + RewriteRule::applies(res[0])))) { Node mult = RewriteRule::applies(res[0])? RewriteRule::run(res[0]) : RewriteRule::run(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::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 &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; diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp index 228fe721e..dd8941033 100644 --- a/src/util/didyoumean.cpp +++ b/src/util/didyoumean.cpp @@ -77,7 +77,12 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b) int len1 = a.size(); int len2 = b.size(); - int C[3][len2+1]; // cost + int* C[3]; + int ii; + for (ii = 0; ii < 3; ++ii) { + C[ii] = new int[len2+1]; + } + // int C[3][len2+1]; // cost for(int j = 0; j <= len2; ++j) { C[0][j] = j * addCost; @@ -123,7 +128,11 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b) } } - return C[len1%3][len2]; + int result = C[len1%3][len2]; + for (ii = 0; ii < 3; ++ii) { + delete [] C[ii]; + } + return result; } string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) { -- 2.30.2