summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/main/command_executor.cpp1
-rw-r--r--src/main/command_executor.h23
-rw-r--r--src/main/driver_unified.cpp13
-rw-r--r--src/main/interactive_shell.cpp6
-rw-r--r--src/main/interactive_shell.h3
-rw-r--r--src/parser/CMakeLists.txt2
-rw-r--r--src/parser/cvc/cvc.h3
-rw-r--r--src/parser/parser.cpp5
-rw-r--r--src/parser/parser.h16
-rw-r--r--src/parser/parser_builder.cpp26
-rw-r--r--src/parser/parser_builder.h13
-rw-r--r--src/parser/smt2/smt2.cpp8
-rw-r--r--src/parser/smt2/smt2.h1
-rw-r--r--src/parser/symbol_manager.cpp77
-rw-r--r--src/parser/symbol_manager.h102
-rw-r--r--src/parser/tptp/tptp.cpp10
-rw-r--r--src/parser/tptp/tptp.h1
-rw-r--r--test/api/ouroborous.cpp4
-rw-r--r--test/api/smt2_compliance.cpp6
-rw-r--r--test/unit/main/interactive_shell_black.h16
-rw-r--r--test/unit/parser/parser_black.h23
-rw-r--r--test/unit/parser/parser_builder_black.h26
23 files changed, 325 insertions, 61 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c6b41e94a..7f89b4de3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1150,6 +1150,7 @@ install(FILES
parser/parser_builder.h
parser/parser_exception.h
parser/parse_op.h
+ parser/symbol_manager.h
DESTINATION
${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser)
install(FILES
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index c91b0455c..a56210fb1 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,6 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
CommandExecutor::CommandExecutor(Options& options)
: d_solver(new api::Solver(&options)),
+ d_symman(new parser::SymbolManager(d_solver.get())),
d_smtEngine(d_solver->getSmtEngine()),
d_options(options),
d_stats("driver"),
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d7899020e..c3c310380 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -21,6 +21,7 @@
#include "api/cvc4cpp.h"
#include "expr/expr_manager.h"
#include "options/options.h"
+#include "parser/symbol_manager.h"
#include "smt/smt_engine.h"
#include "util/statistics_registry.h"
@@ -28,10 +29,6 @@ namespace CVC4 {
class Command;
-namespace api {
-class Solver;
-}
-
namespace main {
class CommandExecutor
@@ -40,7 +37,22 @@ class CommandExecutor
std::string d_lastStatistics;
protected:
+ /**
+ * The solver object, which is allocated by this class and is used for
+ * executing most commands (e.g. check-sat).
+ */
std::unique_ptr<api::Solver> d_solver;
+ /**
+ * The symbol manager, which is allocated by this class. This manages
+ * all things related to definitions of symbols and their impact on behaviors
+ * for commands (e.g. get-unsat-core, get-model, get-assignment), as well
+ * as tracking expression names. Note the symbol manager is independent from
+ * the parser, which uses this symbol manager given a text input.
+ *
+ * Certain commands (e.g. reset-assertions) have a specific impact on the
+ * symbol manager.
+ */
+ std::unique_ptr<parser::SymbolManager> d_symman;
SmtEngine* d_smtEngine;
Options& d_options;
StatisticsRegistry d_stats;
@@ -67,6 +79,9 @@ class CommandExecutor
/** Get a pointer to the solver object owned by this CommandExecutor. */
api::Solver* getSolver() { return d_solver.get(); }
+ /** Get a pointer to the symbol manager owned by this CommandExecutor */
+ parser::SymbolManager* getSymbolManager() { return d_symman.get(); }
+
api::Result getResult() const { return d_result; }
void reset();
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9fff51b93..673c5ddd9 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,7 +213,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
- InteractiveShell shell(pExecutor->getSolver());
+ InteractiveShell shell(pExecutor->getSolver(),
+ pExecutor->getSymbolManager());
if(opts.getInteractivePrompt()) {
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
@@ -258,7 +259,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
// pExecutor->doCommand(cmd);
}
- ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+ ParserBuilder parserBuilder(pExecutor->getSolver(),
+ pExecutor->getSymbolManager(),
+ filename,
+ opts);
if( inputFromStdin ) {
#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -411,7 +415,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
pExecutor->doCommand(cmd);
}
- ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+ ParserBuilder parserBuilder(pExecutor->getSolver(),
+ pExecutor->getSymbolManager(),
+ filename,
+ opts);
if( inputFromStdin ) {
#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b798d03ee..8d482b08e 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -43,6 +43,7 @@
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "parser/symbol_manager.h"
#include "smt/command.h"
#include "theory/logic_info.h"
@@ -83,13 +84,14 @@ static set<string> s_declarations;
#endif /* HAVE_LIBEDITLINE */
-InteractiveShell::InteractiveShell(api::Solver* solver)
+InteractiveShell::InteractiveShell(api::Solver* solver,
+ parser::SymbolManager* sm)
: d_options(solver->getOptions()),
d_in(*d_options.getIn()),
d_out(*d_options.getOutConst()),
d_quit(false)
{
- ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
+ ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options);
/* Create parser with bogus input. */
d_parser = parserBuilder.withStringInput("").build();
if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 36e6068a4..b00f8a8f4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -33,6 +33,7 @@ class Solver;
namespace parser {
class Parser;
+ class SymbolManager;
}/* CVC4::parser namespace */
class CVC4_PUBLIC InteractiveShell
@@ -50,7 +51,7 @@ class CVC4_PUBLIC InteractiveShell
static const unsigned s_historyLimit = 500;
public:
- InteractiveShell(api::Solver* solver);
+ InteractiveShell(api::Solver* solver, parser::SymbolManager* sm);
/**
* Close out the interactive session.
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 8e69da34b..7b55c0915 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -55,6 +55,8 @@ set(libcvc4parser_src_files
smt2/smt2_input.h
smt2/sygus_input.cpp
smt2/sygus_input.h
+ symbol_manager.cpp
+ symbol_manager.h
tptp/TptpLexer.c
tptp/TptpParser.c
tptp/tptp.cpp
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h
index c9e3345d7..7214b6455 100644
--- a/src/parser/cvc/cvc.h
+++ b/src/parser/cvc/cvc.h
@@ -38,10 +38,11 @@ class Cvc : public Parser
protected:
Cvc(api::Solver* solver,
+ SymbolManager* sm,
Input* input,
bool strictMode = false,
bool parseOnly = false)
- : Parser(solver, input, strictMode, parseOnly)
+ : Parser(solver, sm, input, strictMode, parseOnly)
{
}
};
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index af2faa505..710381f9b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -42,12 +42,13 @@ namespace CVC4 {
namespace parser {
Parser::Parser(api::Solver* solver,
+ SymbolManager* sm,
Input* input,
bool strictMode,
bool parseOnly)
: d_input(input),
- d_symtabAllocated(),
- d_symtab(&d_symtabAllocated),
+ d_symman(sm),
+ d_symtab(sm->getSymbolTable()),
d_assertionLevel(0),
d_globalDeclarations(false),
d_anonymousFunctionCount(0),
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 260ab33cf..405935165 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -30,6 +30,7 @@
#include "parser/input.h"
#include "parser/parse_op.h"
#include "parser/parser_exception.h"
+#include "parser/symbol_manager.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
@@ -109,16 +110,13 @@ private:
Input* d_input;
/**
- * The declaration scope that is "owned" by this parser. May or
- * may not be the current declaration scope in use.
+ * Reference to the symbol manager, which manages the symbol table used by
+ * this parser.
*/
- SymbolTable d_symtabAllocated;
+ SymbolManager* d_symman;
/**
- * This current symbol table used by this parser. Initially points
- * to d_symtabAllocated, but can be changed (making this parser
- * delegate its definitions and lookups to another parser).
- * See useDeclarationsFrom().
+ * This current symbol table used by this parser, from symbol manager.
*/
SymbolTable* d_symtab;
@@ -215,7 +213,8 @@ protected:
* @attention The parser takes "ownership" of the given
* input and will delete it on destruction.
*
- * @param the solver API object
+ * @param solver solver API object
+ * @param symm reference to the symbol manager
* @param input the parser input
* @param strictMode whether to incorporate strict(er) compliance checks
* @param parseOnly whether we are parsing only (and therefore certain checks
@@ -223,6 +222,7 @@ protected:
* unimplementedFeature())
*/
Parser(api::Solver* solver,
+ SymbolManager* sm,
Input* input,
bool strictMode = false,
bool parseOnly = false);
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ac8190a17..9adb46af1 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -33,28 +33,34 @@
namespace CVC4 {
namespace parser {
-ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename)
- : d_filename(filename), d_solver(solver)
+ParserBuilder::ParserBuilder(api::Solver* solver,
+ SymbolManager* sm,
+ const std::string& filename)
+ : d_filename(filename), d_solver(solver), d_symman(sm)
{
- init(solver, filename);
+ init(solver, sm, filename);
}
ParserBuilder::ParserBuilder(api::Solver* solver,
+ SymbolManager* sm,
const std::string& filename,
const Options& options)
- : d_filename(filename), d_solver(solver)
+ : d_filename(filename), d_solver(solver), d_symman(sm)
{
- init(solver, filename);
+ init(solver, sm, filename);
withOptions(options);
}
-void ParserBuilder::init(api::Solver* solver, const std::string& filename)
+void ParserBuilder::init(api::Solver* solver,
+ SymbolManager* sm,
+ const std::string& filename)
{
d_inputType = FILE_INPUT;
d_lang = language::input::LANG_AUTO;
d_filename = filename;
d_streamInput = NULL;
d_solver = solver;
+ d_symman = sm;
d_checksEnabled = true;
d_strictMode = false;
d_canIncludeFile = true;
@@ -90,19 +96,19 @@ Parser* ParserBuilder::build()
switch (d_lang)
{
case language::input::LANG_SYGUS_V2:
- parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+ parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
break;
case language::input::LANG_TPTP:
- parser = new Tptp(d_solver, input, d_strictMode, d_parseOnly);
+ parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly);
break;
default:
if (language::isInputLang_smt2(d_lang))
{
- parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+ parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
}
else
{
- parser = new Cvc(d_solver, input, d_strictMode, d_parseOnly);
+ parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly);
}
break;
}
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 7eab196b8..9d62c12a3 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -35,6 +35,7 @@ class Solver;
namespace parser {
class Parser;
+class SymbolManager;
/**
* A builder for input language parsers. <code>build()</code> can be
@@ -67,6 +68,9 @@ class CVC4_PUBLIC ParserBuilder {
/** The API Solver object. */
api::Solver* d_solver;
+ /** The symbol manager */
+ SymbolManager* d_symman;
+
/** Should semantic checks be enabled during parsing? */
bool d_checksEnabled;
@@ -89,13 +93,18 @@ class CVC4_PUBLIC ParserBuilder {
std::string d_forcedLogic;
/** Initialize this parser builder */
- void init(api::Solver* solver, const std::string& filename);
+ void init(api::Solver* solver,
+ SymbolManager* sm,
+ const std::string& filename);
public:
/** Create a parser builder using the given Solver and filename. */
- ParserBuilder(api::Solver* solver, const std::string& filename);
+ ParserBuilder(api::Solver* solver,
+ SymbolManager* sm,
+ const std::string& filename);
ParserBuilder(api::Solver* solver,
+ SymbolManager* sm,
const std::string& filename,
const Options& options);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a8a2eb27a..1decb3b1c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -32,8 +32,12 @@
namespace CVC4 {
namespace parser {
-Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
- : Parser(solver, input, strictMode, parseOnly),
+Smt2::Smt2(api::Solver* solver,
+ SymbolManager* sm,
+ Input* input,
+ bool strictMode,
+ bool parseOnly)
+ : Parser(solver, sm, input, strictMode, parseOnly),
d_logicSet(false),
d_seenSetLogic(false)
{
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1aa0ebac7..eeedbec55 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -68,6 +68,7 @@ class Smt2 : public Parser
protected:
Smt2(api::Solver* solver,
+ SymbolManager* sm,
Input* input,
bool strictMode = false,
bool parseOnly = false);
diff --git a/src/parser/symbol_manager.cpp b/src/parser/symbol_manager.cpp
new file mode 100644
index 000000000..32e17aea8
--- /dev/null
+++ b/src/parser/symbol_manager.cpp
@@ -0,0 +1,77 @@
+/********************* */
+/*! \file symbol_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 The symbol manager
+ **/
+
+#include "parser/symbol_manager.h"
+
+namespace CVC4 {
+namespace parser {
+
+SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
+
+SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
+
+bool SymbolManager::setExpressionName(api::Term t,
+ const std::string& name,
+ bool isAssertion)
+{
+ if (d_names.find(t) != d_names.end())
+ {
+ // already named assertion
+ return false;
+ }
+ if (isAssertion)
+ {
+ d_namedAsserts.insert(t);
+ }
+ d_names[t] = name;
+ return true;
+}
+
+bool SymbolManager::getExpressionName(api::Term t,
+ std::string& name,
+ bool isAssertion) const
+{
+ std::map<api::Term, std::string>::const_iterator it = d_names.find(t);
+ if (it == d_names.end())
+ {
+ return false;
+ }
+ if (isAssertion)
+ {
+ // must be an assertion name
+ if (d_namedAsserts.find(t) == d_namedAsserts.end())
+ {
+ return false;
+ }
+ }
+ name = it->second;
+ return true;
+}
+
+void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions) const
+{
+ for (const api::Term& t : ts)
+ {
+ std::string name;
+ if (getExpressionName(t, name, areAssertions))
+ {
+ names.push_back(name);
+ }
+ }
+}
+
+} // namespace parser
+} // namespace CVC4
diff --git a/src/parser/symbol_manager.h b/src/parser/symbol_manager.h
new file mode 100644
index 000000000..20b0c80e4
--- /dev/null
+++ b/src/parser/symbol_manager.h
@@ -0,0 +1,102 @@
+/********************* */
+/*! \file symbol_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 The symbol manager
+ **/
+
+#include "cvc4parser_public.h"
+
+#ifndef CVC4__PARSER__SYMBOL_MANAGER_H
+#define CVC4__PARSER__SYMBOL_MANAGER_H
+
+#include <map>
+#include <set>
+#include <string>
+
+#include "api/cvc4cpp.h"
+#include "expr/symbol_table.h"
+
+namespace CVC4 {
+namespace parser {
+
+/**
+ * Symbol manager, which manages:
+ * (1) The symbol table used by the parser,
+ * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
+ */
+class CVC4_PUBLIC SymbolManager
+{
+ public:
+ SymbolManager(api::Solver* s);
+ ~SymbolManager() {}
+ /** Get the underlying symbol table */
+ SymbolTable* getSymbolTable();
+ //---------------------------- named expressions
+ /** Set name of term t to name
+ *
+ * @param t The term to name
+ * @param name The given name
+ * @param isAssertion Whether t is being given a name in an assertion
+ * context. In particular, this is true if and only if there was an assertion
+ * command of the form (assert (! t :named name)).
+ * @return true if the name was set. This method may return false if t
+ * already has a name.
+ */
+ bool setExpressionName(api::Term t,
+ const std::string& name,
+ bool isAssertion = false);
+ /** Get name for term t
+ *
+ * @param t The term
+ * @param name The argument to update with the name of t
+ * @param isAssertion Whether we only wish to get the assertion name of t
+ * @return true if t has a name. If so, name is updated to that name.
+ * Otherwise, name is unchanged.
+ */
+ bool getExpressionName(api::Term t,
+ std::string& name,
+ bool isAssertion = false) const;
+ /**
+ * Convert list of terms to list of names. This adds to names the names of
+ * all terms in ts that has names. Terms that do not have names are not
+ * included.
+ *
+ * Notice that we do not distinguish what terms among those in ts have names.
+ * If the caller of this method wants more fine-grained information about what
+ * specific terms had names, then use the more fine grained interface above,
+ * per term.
+ *
+ * @param ts The terms
+ * @param names The name list
+ * @param areAssertions Whether we only wish to include assertion names
+ */
+ void getExpressionNames(const std::vector<api::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions = false) const;
+ //---------------------------- end named expressions
+
+ private:
+ /** The API Solver object. */
+ api::Solver* d_solver;
+ /**
+ * The declaration scope that is "owned" by this symbol manager.
+ */
+ SymbolTable d_symtabAllocated;
+ /** Map terms to names */
+ std::map<api::Term, std::string> d_names;
+ /** The set of terms with assertion names */
+ std::set<api::Term> d_namedAsserts;
+};
+
+} // namespace parser
+} // namespace CVC4
+
+#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 066970fe3..f80b9c3c8 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -33,8 +33,14 @@
namespace CVC4 {
namespace parser {
-Tptp::Tptp(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
- : Parser(solver, input, strictMode, parseOnly), d_cnf(false), d_fof(false)
+Tptp::Tptp(api::Solver* solver,
+ SymbolManager* sm,
+ Input* input,
+ bool strictMode,
+ bool parseOnly)
+ : Parser(solver, sm, input, strictMode, parseOnly),
+ d_cnf(false),
+ d_fof(false)
{
addTheory(Tptp::THEORY_CORE);
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 0cd45847c..ca4dd61bf 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -92,6 +92,7 @@ class Tptp : public Parser {
protected:
Tptp(api::Solver* solver,
+ SymbolManager* sm,
Input* input,
bool strictMode = false,
bool parseOnly = false);
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 5ddc3ec26..5ed240233 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -111,7 +111,9 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL
int runTest() {
std::unique_ptr<api::Solver> solver =
std::unique_ptr<api::Solver>(new api::Solver());
- psr = ParserBuilder(solver.get(), "internal-buffer")
+ std::unique_ptr<parser::SymbolManager> symman(
+ new parser::SymbolManager(solver.get()));
+ psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer")
.withStringInput(declarations)
.withInputLanguage(input::LANG_SMTLIB_V2)
.build();
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index e5781cfaa..7f9035636 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -43,7 +43,6 @@ int main()
std::unique_ptr<api::Solver> solver =
std::unique_ptr<api::Solver>(new api::Solver(&opts));
-
testGetInfo(solver.get(), ":error-behavior");
testGetInfo(solver.get(), ":name");
testGetInfo(solver.get(), ":authors");
@@ -61,7 +60,10 @@ int main()
void testGetInfo(api::Solver* solver, const char* s)
{
- ParserBuilder pb(solver, "<internal>", solver->getOptions());
+ std::unique_ptr<parser::SymbolManager> symman(
+ new parser::SymbolManager(solver));
+
+ ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
assert(p != NULL);
Command* c = p->nextCommand();
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 417cfa94d..af6960ff7 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -27,6 +27,7 @@
#include "options/language.h"
#include "options/options.h"
#include "parser/parser_builder.h"
+#include "parser/symbol_manager.h"
#include "smt/command.h"
using namespace CVC4;
@@ -42,7 +43,9 @@ class InteractiveShellBlack : public CxxTest::TestSuite
d_options.set(options::in, d_sin);
d_options.set(options::out, d_sout);
d_options.set(options::inputLanguage, language::input::LANG_CVC4);
+ d_symman.reset(nullptr);
d_solver.reset(new api::Solver(&d_options));
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
}
void tearDown() override
@@ -53,18 +56,18 @@ class InteractiveShellBlack : public CxxTest::TestSuite
void testAssertTrue() {
*d_sin << "ASSERT TRUE;\n" << flush;
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
countCommands( shell, 1, 1 );
}
void testQueryFalse() {
*d_sin << "QUERY FALSE;\n" << flush;
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
countCommands( shell, 1, 1 );
}
void testDefUse() {
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
*d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
/* readCommand may return a sequence, so we can't say for sure
whether it will return 1 or 2... */
@@ -72,7 +75,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite
}
void testDefUse2() {
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
/* readCommand may return a sequence, see above. */
*d_sin << "x : REAL;\n" << flush;
Command* tmp = shell.readCommand();
@@ -82,20 +85,21 @@ class InteractiveShellBlack : public CxxTest::TestSuite
}
void testEmptyLine() {
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
*d_sin << flush;
countCommands(shell,0,0);
}
void testRepeatedEmptyLines() {
*d_sin << "\n\n\n";
- InteractiveShell shell(d_solver.get());
+ InteractiveShell shell(d_solver.get(), d_symman.get());
/* Might return up to four empties, might return nothing */
countCommands( shell, 0, 3 );
}
private:
std::unique_ptr<api::Solver> d_solver;
+ std::unique_ptr<parser::SymbolManager> d_symman;
Options d_options;
stringstream* d_sin;
stringstream* d_sout;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index dfe2ee138..2bdd5c950 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -29,9 +29,9 @@
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
+#include "parser/symbol_manager.h"
#include "smt/command.h"
-
using namespace CVC4;
using namespace CVC4::parser;
using namespace CVC4::language::input;
@@ -70,7 +70,8 @@ class ParserBlack
// Debug.on("parser-extra");
// cerr << "Testing good input: <<" << goodInput << ">>" << endl;
// istringstream stream(goodInputs[i]);
- Parser* parser = ParserBuilder(d_solver.get(), "test")
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
.withStringInput(goodInput)
.withOptions(d_options)
.withInputLanguage(d_lang)
@@ -101,7 +102,8 @@ class ParserBlack
// cerr << "Testing bad input: '" << badInput << "'\n";
// Debug.on("parser");
- Parser* parser = ParserBuilder(d_solver.get(), "test")
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
.withStringInput(badInput)
.withOptions(d_options)
.withInputLanguage(d_lang)
@@ -132,7 +134,8 @@ class ParserBlack
// Debug.on("parser");
// istringstream stream(context + goodBooleanExprs[i]);
- Parser* parser = ParserBuilder(d_solver.get(), "test")
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
.withStringInput(goodExpr)
.withOptions(d_options)
.withInputLanguage(d_lang)
@@ -179,7 +182,8 @@ class ParserBlack
// Debug.on("parser-extra");
// cout << "Testing bad expr: '" << badExpr << "'\n";
- Parser* parser = ParserBuilder(d_solver.get(), "test")
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
.withStringInput(badExpr)
.withOptions(d_options)
.withInputLanguage(d_lang)
@@ -206,14 +210,21 @@ class ParserBlack
void setUp()
{
d_options.set(options::parseOnly, true);
+ // ensure the old symbol manager is deleted
+ d_symman.reset(nullptr);
d_solver.reset(new api::Solver(&d_options));
}
- void tearDown() { d_solver.reset(nullptr); }
+ void tearDown()
+ {
+ d_symman.reset(nullptr);
+ d_solver.reset(nullptr);
+ }
private:
InputLanguage d_lang;
std::unique_ptr<api::Solver> d_solver;
+ std::unique_ptr<parser::SymbolManager> d_symman;
}; /* class ParserBlack */
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 003424397..b8ec96836 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -28,6 +28,7 @@
#include "options/language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "parser/symbol_manager.h"
using namespace CVC4;
using namespace CVC4::parser;
@@ -37,7 +38,13 @@ using namespace std;
class ParserBuilderBlack : public CxxTest::TestSuite
{
public:
- void setUp() override { d_solver.reset(new api::Solver()); }
+ void setUp() override
+ {
+ // ensure the old symbol manager is deleted
+ d_symman.reset(nullptr);
+ d_solver.reset(new api::Solver());
+ d_symman.reset(new parser::SymbolManager(d_solver.get()));
+ }
void tearDown() override {}
@@ -45,8 +52,8 @@ class ParserBuilderBlack : public CxxTest::TestSuite
{
char *filename = mkTemp();
- checkEmptyInput(
- ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
+ checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), filename)
+ .withInputLanguage(LANG_CVC4));
remove(filename);
free(filename);
@@ -59,35 +66,35 @@ class ParserBuilderBlack : public CxxTest::TestSuite
fs << "TRUE" << std::endl;
fs.close();
- checkTrueInput(
- ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
+ checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), filename)
+ .withInputLanguage(LANG_CVC4));
remove(filename);
free(filename);
}
void testEmptyStringInput() {
- checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+ checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
.withInputLanguage(LANG_CVC4)
.withStringInput(""));
}
void testTrueStringInput() {
- checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+ checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
.withInputLanguage(LANG_CVC4)
.withStringInput("TRUE"));
}
void testEmptyStreamInput() {
stringstream ss( "", ios_base::in );
- checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+ checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
.withInputLanguage(LANG_CVC4)
.withStreamInput(ss));
}
void testTrueStreamInput() {
stringstream ss( "TRUE", ios_base::in );
- checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+ checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
.withInputLanguage(LANG_CVC4)
.withStreamInput(ss));
}
@@ -127,5 +134,6 @@ class ParserBuilderBlack : public CxxTest::TestSuite
}
std::unique_ptr<api::Solver> d_solver;
+ std::unique_ptr<parser::SymbolManager> d_symman;
}; // class ParserBuilderBlack
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback