From: Andres Noetzli Date: Mon, 17 Jul 2017 05:18:10 +0000 (-0400) Subject: Remove PtrCloser (#198) X-Git-Tag: cvc5-1.0.0~5716 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=efac53e969ccefc01bace1a5f095dfd3570c3767;p=cvc5.git Remove PtrCloser (#198) With C++11, we don't need PtrCloser anymore because we can just use std::unique_ptr. --- diff --git a/src/base/Makefile.am b/src/base/Makefile.am index bf919cd81..491baaa90 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -26,9 +26,7 @@ libbase_la_SOURCES = \ listener.h \ modal_exception.h \ output.cpp \ - output.h \ - ptr_closer.h - + output.h BUILT_SOURCES = \ diff --git a/src/base/ptr_closer.h b/src/base/ptr_closer.h deleted file mode 100644 index cd0c707b1..000000000 --- a/src/base/ptr_closer.h +++ /dev/null @@ -1,73 +0,0 @@ -/********************* */ -/*! \file ptr_closer.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class to close owned pointers in the destructor. - ** - ** A class to close owned pointers in the destructor. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__PTR_CLOSER_H -#define __CVC4__PTR_CLOSER_H - -namespace CVC4 { - -/** - * A class to close owned pointers in the destructor. This plays a similar role - * to unique_ptr, but without move semantics. This is designed to overcome the - * lack of having unique_ptr in C++05. - * - * This is a variant of unique_ptr that is not designed for move semantics. - * These are appropriate to own pointer allocations on the stack that should be - * deleted when an exception is thrown. These should be used with care within - * heap based data structures, and never as the return value of a function. - */ -template -class PtrCloser { - public: - PtrCloser() : d_pointer(NULL) {} - explicit PtrCloser(T* pointer) : d_pointer(pointer) {} - ~PtrCloser() { delete d_pointer; } - - /** Deletes the currently owned copy and takes ownership of pointer. */ - void reset(T* pointer = NULL) { - delete d_pointer; - d_pointer = pointer; - } - - /** Gives up ownership of the pointer to the caller. */ - T* release() { - T* copy = d_pointer; - d_pointer = NULL; - return copy; - } - - /** Returns the pointer. */ - T* get() const { return d_pointer; } - - /** Returns the pointer. Undefined if the pointer is null. */ - T* operator->() const { return d_pointer; } - - /** Returns true if the pointer is not-null. */ - operator bool() const { return d_pointer != NULL; } - - private: - PtrCloser(const PtrCloser*) CVC4_UNDEFINED; - PtrCloser& operator=(const PtrCloser&) CVC4_UNDEFINED; - - /** An owned pointer object allocated by `new`. Or NULL. */ - T* d_pointer; -}; /* class PtrCloser */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__PTR_CLOSER_H */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 8d8fba43c..57cfa0221 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -155,10 +155,11 @@ #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H -#include -#include #include +#include +#include #include +#include namespace CVC4 { static const unsigned default_nchild_thresh = 10; @@ -171,7 +172,6 @@ namespace CVC4 { #include "base/cvc4_assert.h" #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" @@ -890,14 +890,14 @@ template Node* NodeBuilder::constructNodePtr() { // maybeCheckType() can throw an exception. Make sure to call the destructor // on the exception branch. - PtrCloser np(new Node(constructNV())); + std::unique_ptr np(new Node(constructNV())); maybeCheckType(*np.get()); return np.release(); } template Node* NodeBuilder::constructNodePtr() const { - PtrCloser np(new Node(constructNV())); + std::unique_ptr np(new Node(constructNV())); maybeCheckType(*np.get()); return np.release(); } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 8b79e046c..697ce6642 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -20,6 +20,7 @@ #include #include #include +#include #include // This must come before PORTFOLIO_BUILD. @@ -27,7 +28,6 @@ #include "base/configuration.h" #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" #include "main/command_executor.h" @@ -249,7 +249,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } # endif - PtrCloser replayParser; + std::unique_ptr replayParser; if( opts.getReplayInputFilename() != "" ) { std::string replayFilename = opts.getReplayInputFilename(); ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); @@ -357,7 +357,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { vector< vector > allCommands; allCommands.push_back(vector()); - PtrCloser parser(parserBuilder.build()); + std::unique_ptr parser(parserBuilder.build()); if(replayParser) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser.get()); @@ -512,7 +512,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ } - PtrCloser parser(parserBuilder.build()); + std::unique_ptr parser(parserBuilder.build()); if(replayParser) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser.get()); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 171c6cab0..a2e9e6f47 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -531,10 +531,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" -#include #include +#include +#include -#include "base/ptr_closer.h" #include "options/set_language.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" @@ -595,7 +595,6 @@ namespace CVC4 { #include #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -659,7 +658,7 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser cmd; + std::unique_ptr cmd; } @after { cmd_return = cmd.release(); @@ -689,7 +688,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] * Matches a command of the input. If a declaration, it will return an empty * command. */ -command [CVC4::PtrCloser* cmd] +command [std::unique_ptr* cmd] : ( mainCommand[cmd] SEMICOLON | SEMICOLON | LET_TOK { PARSER_STATE->pushScope(); } @@ -716,7 +715,7 @@ options { backtrack = true; } : letDecl | typeLetDecl[check] ; -mainCommand[CVC4::PtrCloser* cmd] +mainCommand[std::unique_ptr* cmd] @init { Expr f; SExpr sexpr; @@ -934,7 +933,7 @@ symbolicExpr[CVC4::SExpr& sexpr] /** * Match a top-level declaration. */ -toplevelDeclaration[CVC4::PtrCloser* cmd] +toplevelDeclaration[std::unique_ptr* cmd] @init { std::vector ids; Type t; @@ -951,7 +950,7 @@ toplevelDeclaration[CVC4::PtrCloser* cmd] */ boundVarDecl[std::vector& ids, CVC4::Type& t] @init { - CVC4::PtrCloser local_cmd; + std::unique_ptr local_cmd; } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[&local_cmd,t,ids,false] @@ -1002,14 +1001,14 @@ boundVarDeclReturn[std::vector& terms, * because type declarations are always top-level, except for * type-lets, which don't use this rule. */ -declareTypes[CVC4::PtrCloser* cmd, +declareTypes[std::unique_ptr* cmd, const std::vector& idList] @init { Type t; } /* A sort declaration (e.g., "T : TYPE") */ : TYPE_TOK - { CVC4::PtrCloser seq(new DeclarationSequence()); + { std::unique_ptr seq(new DeclarationSequence()); for(std::vector::const_iterator i = idList.begin(); i != idList.end(); ++i) { // Don't allow a type variable to clash with a previously @@ -1044,7 +1043,7 @@ declareTypes[CVC4::PtrCloser* cmd, * permitted and "cmd" is output. If topLevel is false, bound vars * are created */ -declareVariables[CVC4::PtrCloser* cmd, CVC4::Type& t, +declareVariables[std::unique_ptr* cmd, CVC4::Type& t, const std::vector& idList, bool topLevel] @init { Expr f; @@ -1052,7 +1051,7 @@ declareVariables[CVC4::PtrCloser* cmd, CVC4::Type& t, } /* A variable declaration (or definition) */ : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? - { CVC4::PtrCloser seq; + { std::unique_ptr seq; if(topLevel) { seq.reset(new DeclarationSequence()); } @@ -2260,7 +2259,7 @@ datatypeDef[std::vector& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::PtrCloser ctor; + std::unique_ptr ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester @@ -2280,7 +2279,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::PtrCloser* ctor] +selector[std::unique_ptr* ctor] @init { std::string id; Type t, t2; diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 315ded475..b30922d58 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -71,9 +71,9 @@ options { // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" +#include #include -#include "base/ptr_closer.h" #include "smt/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" @@ -115,7 +115,6 @@ namespace CVC4 { #include #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -157,7 +156,7 @@ parseExpr returns [CVC4::parser::smt1::myExpr expr] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser cmd; + std::unique_ptr cmd; } @after { cmd_return = cmd.release(); @@ -177,7 +176,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] * Matches the whole SMT-LIB benchmark. * @return the sequence command containing the whole problem */ -benchmark [CVC4::PtrCloser* cmd] +benchmark [std::unique_ptr* cmd] : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK | EOF ; @@ -187,10 +186,10 @@ benchmark [CVC4::PtrCloser* cmd] * command sequence. * @return the command sequence */ -benchAttributes [CVC4::PtrCloser* cmd] +benchAttributes [std::unique_ptr* cmd] @init { - CVC4::PtrCloser cmd_seq(new CommandSequence()); - CVC4::PtrCloser attribute; + std::unique_ptr cmd_seq(new CommandSequence()); + std::unique_ptr attribute; } @after { cmd->reset(cmd_seq.release()); @@ -205,13 +204,13 @@ benchAttributes [CVC4::PtrCloser* cmd] * a corresponding command * @return a command corresponding to the attribute */ -benchAttribute [CVC4::PtrCloser* smt_command] +benchAttribute [std::unique_ptr* smt_command] @declarations { std::string name; BenchmarkStatus b_status; Expr expr; - CVC4::PtrCloser command_seq; - CVC4::PtrCloser declaration_command; + std::unique_ptr command_seq; + std::unique_ptr declaration_command; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); @@ -495,7 +494,7 @@ attribute[std::string& s] { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } ; -functionDeclaration[CVC4::PtrCloser* smt_command] +functionDeclaration[std::unique_ptr* smt_command] @declarations { std::string name; std::vector sorts; @@ -517,7 +516,7 @@ functionDeclaration[CVC4::PtrCloser* smt_command] /** * Matches the declaration of a predicate and declares it */ -predicateDeclaration[CVC4::PtrCloser* smt_command] +predicateDeclaration[std::unique_ptr* smt_command] @declarations { std::string name; std::vector p_sorts; @@ -534,7 +533,7 @@ predicateDeclaration[CVC4::PtrCloser* smt_command] } ; -sortDeclaration[CVC4::PtrCloser* smt_command] +sortDeclaration[std::unique_ptr* smt_command] @declarations { std::string name; } @@ -590,7 +589,7 @@ status[ CVC4::BenchmarkStatus& status ] * Matches an annotation, which is an attribute name, with an optional user * value. */ -annotation[CVC4::PtrCloser* smt_command] +annotation[std::unique_ptr* smt_command] @init { std::string key, value; std::vector pats; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5d24ec024..88709c29a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -85,7 +85,8 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" -#include "base/ptr_closer.h" +#include + #include "parser/parser.h" #include "parser/antlr_tracing.h" #include "smt/command.h" @@ -205,7 +206,7 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser cmd; + std::unique_ptr cmd; std::string name; } @after { @@ -241,7 +242,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] */ parseSygus returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser cmd; + std::unique_ptr cmd; std::string name; } @after { @@ -255,7 +256,7 @@ parseSygus returns [CVC4::Command* cmd_return = NULL] * Parse the internal portion of the command, ignoring the surrounding * parentheses. */ -command [CVC4::PtrCloser* cmd] +command [std::unique_ptr* cmd] @declarations { std::string name; std::vector names; @@ -455,7 +456,7 @@ command [CVC4::PtrCloser* cmd] PARSER_STATE->pushUnsatCoreNameScope(); cmd->reset(new PushCommand()); } else { - CVC4::PtrCloser seq(new CommandSequence()); + std::unique_ptr seq(new CommandSequence()); do { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); @@ -495,7 +496,7 @@ command [CVC4::PtrCloser* cmd] PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { - CVC4::PtrCloser seq(new CommandSequence()); + std::unique_ptr seq(new CommandSequence()); do { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); @@ -554,7 +555,7 @@ command [CVC4::PtrCloser* cmd] } ; -sygusCommand [CVC4::PtrCloser* cmd] +sygusCommand [std::unique_ptr* cmd] @declarations { std::string name, fun; std::vector names; @@ -565,7 +566,7 @@ sygusCommand [CVC4::PtrCloser* cmd] std::vector sygus_vars; std::vector > sortedVarNames; SExpr sexpr; - CVC4::PtrCloser seq; + std::unique_ptr seq; std::vector< std::vector< CVC4::SygusGTerm > > sgts; std::vector< CVC4::Datatype > datatypes; std::vector< std::vector > ops; @@ -1075,7 +1076,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] ; // Separate this into its own rule (can be invoked by set-info or meta-info) -metaInfoInternal[CVC4::PtrCloser* cmd] +metaInfoInternal[std::unique_ptr* cmd] @declarations { std::string name; SExpr sexpr; @@ -1105,7 +1106,7 @@ metaInfoInternal[CVC4::PtrCloser* cmd] } ; -setOptionInternal[CVC4::PtrCloser* cmd] +setOptionInternal[std::unique_ptr* cmd] @init { std::string name; SExpr sexpr; @@ -1122,7 +1123,7 @@ setOptionInternal[CVC4::PtrCloser* cmd] } ; -smt25Command[CVC4::PtrCloser* cmd] +smt25Command[std::unique_ptr* cmd] @declarations { std::string name; std::string fname; @@ -1136,7 +1137,7 @@ smt25Command[CVC4::PtrCloser* cmd] std::vector funcs; std::vector func_defs; Expr aexpr; - CVC4::PtrCloser seq; + std::unique_ptr seq; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -1330,7 +1331,7 @@ smt25Command[CVC4::PtrCloser* cmd] // GET_UNSAT_ASSUMPTIONS ; -extendedCommand[CVC4::PtrCloser* cmd] +extendedCommand[std::unique_ptr* cmd] @declarations { std::vector dts; Expr e, e2; @@ -1340,7 +1341,7 @@ extendedCommand[CVC4::PtrCloser* cmd] std::vector terms; std::vector sorts; std::vector > sortedVarNames; - CVC4::PtrCloser seq; + std::unique_ptr seq; } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -1495,7 +1496,7 @@ extendedCommand[CVC4::PtrCloser* cmd] ; -datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser* cmd] +datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] @declarations { std::vector dts; std::string name; @@ -1515,7 +1516,7 @@ datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser* cmd] } ; -datatypeDefCommand[bool isCo, CVC4::PtrCloser* cmd] +datatypeDefCommand[bool isCo, std::unique_ptr* cmd] @declarations { std::vector dts; std::string name; @@ -1530,7 +1531,7 @@ datatypeDefCommand[bool isCo, CVC4::PtrCloser* cmd] { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } ; -datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] +datatypesDefCommand[bool isCo, std::unique_ptr* cmd] @declarations { std::vector dts; std::string name; @@ -1593,7 +1594,7 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] } ; -rewriterulesCommand[CVC4::PtrCloser* cmd] +rewriterulesCommand[std::unique_ptr* cmd] @declarations { std::vector > sortedVarNames; std::vector args, guards, heads, triggers; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index fe4ea6f98..fbd3d8cfb 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -93,6 +93,8 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" +#include + #include "smt/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h"