listener.h \
modal_exception.h \
output.cpp \
- output.h \
- ptr_closer.h
-
+ output.h
BUILT_SOURCES = \
+++ /dev/null
-/********************* */
-/*! \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 T>
-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 */
#ifndef __CVC4__NODE_BUILDER_H
#define __CVC4__NODE_BUILDER_H
-#include <iostream>
-#include <vector>
#include <cstdlib>
+#include <iostream>
+#include <memory>
#include <stdint.h>
+#include <vector>
namespace CVC4 {
static const unsigned default_nchild_thresh = 10;
#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"
Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
// maybeCheckType() can throw an exception. Make sure to call the destructor
// on the exception branch.
- PtrCloser<Node> np(new Node(constructNV()));
+ std::unique_ptr<Node> np(new Node(constructNV()));
maybeCheckType(*np.get());
return np.release();
}
template <unsigned nchild_thresh>
Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
- PtrCloser<Node> np(new Node(constructNV()));
+ std::unique_ptr<Node> np(new Node(constructNV()));
maybeCheckType(*np.get());
return np.release();
}
#include <cstring>
#include <fstream>
#include <iostream>
+#include <memory>
#include <new>
// This must come before PORTFOLIO_BUILD.
#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"
}
# endif
-
PtrCloser<Parser> replayParser;
+
std::unique_ptr<Parser> replayParser;
if( opts.getReplayInputFilename() != "" ) {
std::string replayFilename = opts.getReplayInputFilename();
ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
vector< vector<Command*> > allCommands;
allCommands.push_back(vector<Command*>());
-
PtrCloser<Parser> parser(parserBuilder.build());
+
std::unique_ptr<Parser> parser(parserBuilder.build());
if(replayParser) {
// have the replay parser use the file's declarations
replayParser->useDeclarationsFrom(parser.get());
#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
}
-
PtrCloser<Parser> parser(parserBuilder.build());
+
std::unique_ptr<Parser> parser(parserBuilder.build());
if(replayParser) {
// have the replay parser use the file's declarations
replayParser->useDeclarationsFrom(parser.get());
// 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"
#include <vector>
#include "base/output.h"
-#include "base/ptr_closer.h"
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
*/
parseCommand returns [CVC4::Command* cmd_return = NULL]
@declarations {
- CVC4::PtrCloser<CVC4::Command> cmd;
+ std::unique_ptr<CVC4::Command> cmd;
}
@after {
cmd_return = cmd.release();
* 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(); }
: letDecl | typeLetDecl[check]
;
-mainCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
+mainCommand[std::unique_ptr<CVC4::Command>* cmd]
@init {
Expr f;
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;
*/
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]
* 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
* 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;
}
/* 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());
}
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
}
;
-selector[CVC4::PtrCloser<CVC4::DatatypeConstructor>* ctor]
+selector[std::unique_ptr<CVC4::DatatypeConstructor>* ctor]
@init {
std::string id;
Type t, t2;
// 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"
#include <vector>
#include "base/output.h"
-#include "base/ptr_closer.h"
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
*/
parseCommand returns [CVC4::Command* cmd_return = NULL]
@declarations {
- CVC4::PtrCloser<CVC4::Command> cmd;
+ std::unique_ptr<CVC4::Command> cmd;
}
@after {
cmd_return = cmd.release();
* 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
;
* 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());
* 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));
{ 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;
/**
* 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;
}
;
-sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
+sortDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
@declarations {
std::string name;
}
* 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;
// 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"
*/
parseCommand returns [CVC4::Command* cmd_return = NULL]
@declarations {
- CVC4::PtrCloser<CVC4::Command> cmd;
+ std::unique_ptr<CVC4::Command> cmd;
std::string name;
}
@after {
*/
parseSygus returns [CVC4::Command* cmd_return = NULL]
@declarations {
- CVC4::PtrCloser<CVC4::Command> cmd;
+ std::unique_ptr<CVC4::Command> cmd;
std::string name;
}
@after {
* 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;
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();
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();
}
;
-sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
+sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::string name, fun;
std::vector<std::string> names;
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;
;
// 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;
}
;
-setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
+setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
@init {
std::string name;
SExpr sexpr;
}
;
-smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
+smt25Command[std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::string name;
std::string fname;
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]
// 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;
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. */
;
-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;
}
;
-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;
{ 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;
}
;
-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;
// 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"
projects / cvc5.git / commitdiff