summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/Makefile.am4
-rw-r--r--src/base/ptr_closer.h73
-rw-r--r--src/expr/node_builder.h10
-rw-r--r--src/main/driver_unified.cpp8
-rw-r--r--src/parser/cvc/Cvc.g27
-rw-r--r--src/parser/smt1/Smt1.g27
-rw-r--r--src/parser/smt2/Smt2.g37
-rw-r--r--src/parser/tptp/Tptp.g2
8 files changed, 57 insertions, 131 deletions
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 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 */
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 <iostream>
-#include <vector>
#include <cstdlib>
+#include <iostream>
+#include <memory>
#include <stdint.h>
+#include <vector>
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 <unsigned nchild_thresh>
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();
}
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 <cstring>
#include <fstream>
#include <iostream>
+#include <memory>
#include <new>
// 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<Parser> replayParser;
+ std::unique_ptr<Parser> 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<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());
@@ -512,7 +512,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
#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());
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback