diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-07-17 01:18:10 -0400 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-17 01:18:10 -0400 |
commit | efac53e969ccefc01bace1a5f095dfd3570c3767 (patch) | |
tree | 0cfcf50944619bc0e7c452f9aa918a56ebd3d540 /src/parser | |
parent | 949e19cbc2881996e5c5eed613f4506264482039 (diff) |
Remove PtrCloser (#198)
With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 27 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 27 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 37 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 |
4 files changed, 47 insertions, 46 deletions
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 <stdint.h> #include <cassert> +#include <memory> +#include <stdint.h> -#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 <vector> #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<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> 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<CVC4::Command>* cmd] +command [std::unique_ptr<CVC4::Command>* cmd] : ( mainCommand[cmd] SEMICOLON | SEMICOLON | LET_TOK { PARSER_STATE->pushScope(); } @@ -716,7 +715,7 @@ options { backtrack = true; } : letDecl | typeLetDecl[check] ; -mainCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +mainCommand[std::unique_ptr<CVC4::Command>* cmd] @init { Expr f; SExpr sexpr; @@ -934,7 +933,7 @@ symbolicExpr[CVC4::SExpr& sexpr] /** * Match a top-level declaration. */ -toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd] +toplevelDeclaration[std::unique_ptr<CVC4::Command>* cmd] @init { std::vector<std::string> ids; Type t; @@ -951,7 +950,7 @@ toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd] */ boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t] @init { - CVC4::PtrCloser<Command> local_cmd; + std::unique_ptr<Command> local_cmd; } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[&local_cmd,t,ids,false] @@ -1002,14 +1001,14 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms, * because type declarations are always top-level, except for * type-lets, which don't use this rule. */ -declareTypes[CVC4::PtrCloser<CVC4::Command>* cmd, +declareTypes[std::unique_ptr<CVC4::Command>* cmd, const std::vector<std::string>& idList] @init { Type t; } /* A sort declaration (e.g., "T : TYPE") */ : TYPE_TOK - { CVC4::PtrCloser<DeclarationSequence> seq(new DeclarationSequence()); + { std::unique_ptr<DeclarationSequence> seq(new DeclarationSequence()); for(std::vector<std::string>::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<CVC4::Command>* cmd, * permitted and "cmd" is output. If topLevel is false, bound vars * are created */ -declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t, +declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel] @init { Expr f; @@ -1052,7 +1051,7 @@ declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t, } /* A variable declaration (or definition) */ : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? - { CVC4::PtrCloser<DeclarationSequence> seq; + { std::unique_ptr<DeclarationSequence> seq; if(topLevel) { seq.reset(new DeclarationSequence()); } @@ -2260,7 +2259,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::PtrCloser<CVC4::DatatypeConstructor> ctor; + std::unique_ptr<CVC4::DatatypeConstructor> ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester @@ -2280,7 +2279,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::PtrCloser<CVC4::DatatypeConstructor>* ctor] +selector[std::unique_ptr<CVC4::DatatypeConstructor>* 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 <memory> #include <stdint.h> -#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 <vector> #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<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> 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<CVC4::Command>* cmd] +benchmark [std::unique_ptr<CVC4::Command>* cmd] : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK | EOF ; @@ -187,10 +186,10 @@ benchmark [CVC4::PtrCloser<CVC4::Command>* cmd] * command sequence. * @return the command sequence */ -benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd] +benchAttributes [std::unique_ptr<CVC4::Command>* cmd] @init { - CVC4::PtrCloser<CVC4::CommandSequence> cmd_seq(new CommandSequence()); - CVC4::PtrCloser<CVC4::Command> attribute; + std::unique_ptr<CVC4::CommandSequence> cmd_seq(new CommandSequence()); + std::unique_ptr<CVC4::Command> attribute; } @after { cmd->reset(cmd_seq.release()); @@ -205,13 +204,13 @@ benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd] * a corresponding command * @return a command corresponding to the attribute */ -benchAttribute [CVC4::PtrCloser<CVC4::Command>* smt_command] +benchAttribute [std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; BenchmarkStatus b_status; Expr expr; - CVC4::PtrCloser<CVC4::CommandSequence> command_seq; - CVC4::PtrCloser<CVC4::Command> declaration_command; + std::unique_ptr<CVC4::CommandSequence> command_seq; + std::unique_ptr<CVC4::Command> 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<CVC4::Command>* smt_command] +functionDeclaration[std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; std::vector<Type> sorts; @@ -517,7 +516,7 @@ functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] /** * Matches the declaration of a predicate and declares it */ -predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] +predicateDeclaration[std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; std::vector<Type> p_sorts; @@ -534,7 +533,7 @@ predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] } ; -sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] +sortDeclaration[std::unique_ptr<CVC4::Command>* 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<CVC4::Command>* smt_command] +annotation[std::unique_ptr<CVC4::Command>* smt_command] @init { std::string key, value; std::vector<Expr> 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 <memory> + #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<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> 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<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> 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<CVC4::Command>* cmd] +command [std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::vector<std::string> names; @@ -455,7 +456,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] PARSER_STATE->pushUnsatCoreNameScope(); cmd->reset(new PushCommand()); } else { - CVC4::PtrCloser<CommandSequence> seq(new CommandSequence()); + std::unique_ptr<CommandSequence> seq(new CommandSequence()); do { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); @@ -495,7 +496,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { - CVC4::PtrCloser<CommandSequence> seq(new CommandSequence()); + std::unique_ptr<CommandSequence> seq(new CommandSequence()); do { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); @@ -554,7 +555,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] } ; -sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] +sygusCommand [std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name, fun; std::vector<std::string> names; @@ -565,7 +566,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> sygus_vars; std::vector<std::pair<std::string, Type> > sortedVarNames; SExpr sexpr; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; std::vector< std::vector< CVC4::SygusGTerm > > sgts; std::vector< CVC4::Datatype > datatypes; std::vector< std::vector<Expr> > 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<CVC4::Command>* cmd] +metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; SExpr sexpr; @@ -1105,7 +1106,7 @@ metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd] } ; -setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd] +setOptionInternal[std::unique_ptr<CVC4::Command>* cmd] @init { std::string name; SExpr sexpr; @@ -1122,7 +1123,7 @@ setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd] } ; -smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] +smt25Command[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::string fname; @@ -1136,7 +1137,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> funcs; std::vector<Expr> func_defs; Expr aexpr; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -1330,7 +1331,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] // GET_UNSAT_ASSUMPTIONS ; -extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; Expr e, e2; @@ -1340,7 +1341,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> terms; std::vector<Type> sorts; std::vector<std::pair<std::string, Type> > sortedVarNames; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -1495,7 +1496,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] ; -datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1515,7 +1516,7 @@ datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] } ; -datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1530,7 +1531,7 @@ datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } ; -datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1593,7 +1594,7 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] } ; -rewriterulesCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<std::pair<std::string, Type> > sortedVarNames; std::vector<Expr> 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 <memory> + #include "smt/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" |