diff options
-rw-r--r-- | src/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 1 | ||||
-rw-r--r-- | src/main/command_executor.h | 23 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 13 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 6 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 3 | ||||
-rw-r--r-- | src/parser/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/parser/cvc/cvc.h | 3 | ||||
-rw-r--r-- | src/parser/parser.cpp | 5 | ||||
-rw-r--r-- | src/parser/parser.h | 16 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 26 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 13 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 1 | ||||
-rw-r--r-- | src/parser/symbol_manager.cpp | 77 | ||||
-rw-r--r-- | src/parser/symbol_manager.h | 102 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 10 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 1 | ||||
-rw-r--r-- | test/api/ouroborous.cpp | 4 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 6 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.h | 16 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 23 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.h | 26 |
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 |