diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-08 19:21:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-08 19:21:47 -0700 |
commit | 91d85704313de6be9fd382833f5cedd39e24a6fa (patch) | |
tree | 057adfdad9d586428482d9bd58e9c8124bddc47b /src | |
parent | b4d4006d08a32b107257b0edaba95679d0b0c65b (diff) |
Plug solver API object into parser. (#2240)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 69 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 156 | ||||
-rw-r--r-- | src/compat/cvc3_compat.cpp | 91 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 6 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 35 | ||||
-rw-r--r-- | src/main/command_executor.h | 52 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 34 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 7 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 7 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 1 | ||||
-rw-r--r-- | src/parser/parser.cpp | 53 | ||||
-rw-r--r-- | src/parser/parser.h | 220 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 76 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 27 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 10 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h | 11 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 9 |
20 files changed, 548 insertions, 344 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 19d7840a8..bc696a057 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -95,6 +95,10 @@ std::string Result::getUnknownExplanation(void) const std::string Result::toString(void) const { return d_result->toString(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Result Result::getResult(void) const { return *d_result; } + std::ostream& operator<<(std::ostream& out, const Result& r) { out << r.toString(); @@ -801,6 +805,10 @@ std::string Sort::toString() const return d_type->toString(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Type Sort::getType(void) const { return *d_type; } + std::ostream& operator<<(std::ostream& out, const Sort& s) { out << s.toString(); @@ -942,6 +950,10 @@ Term::const_iterator Term::end() const return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end())); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Expr Term::getExpr(void) const { return *d_expr; } + std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); @@ -1029,6 +1041,10 @@ bool OpTerm::isNull() const { return d_expr->isNull(); } std::string OpTerm::toString() const { return d_expr->toString(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; } + std::ostream& operator<<(std::ostream& out, const OpTerm& t) { out << t.toString(); @@ -1097,6 +1113,14 @@ std::string DatatypeConstructorDecl::toString() const return ss.str(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor( + void) const +{ + return *d_ctor; +} + std::ostream& operator<<(std::ostream& out, const DatatypeConstructorDecl& ctordecl) { @@ -1146,6 +1170,10 @@ std::string DatatypeDecl::toString() const return ss.str(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; } + std::ostream& operator<<(std::ostream& out, const DatatypeSelectorDecl& stordecl) { @@ -1171,6 +1199,14 @@ std::string DatatypeSelector::toString() const return ss.str(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg( + void) const +{ + return *d_stor; +} + std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) { out << stor.toString(); @@ -1287,6 +1323,14 @@ std::string DatatypeConstructor::toString() const return ss.str(); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor( + void) const +{ + return *d_ctor; +} + std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) { out << ctor.toString(); @@ -1333,6 +1377,10 @@ Datatype::const_iterator Datatype::end() const return Datatype::const_iterator(*d_dtype, false); } +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; } + Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin) { @@ -1431,10 +1479,11 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { - d_exprMgr = std::unique_ptr<ExprManager>( - opts == nullptr ? new ExprManager(Options()) : new ExprManager(*opts)); - d_smtEngine = std::unique_ptr<SmtEngine>(new SmtEngine(d_exprMgr.get())); - d_rng = std::unique_ptr<Random>(new Random((*opts)[options::seed])); + Options* o = opts == nullptr ? new Options() : opts; + d_exprMgr.reset(new ExprManager(*o)); + d_smtEngine.reset(new SmtEngine(d_exprMgr.get())); + d_rng.reset(new Random((*o)[options::seed])); + if (opts == nullptr) delete o; } Solver::~Solver() {} @@ -2777,5 +2826,17 @@ void Solver::setOption(const std::string& option, d_smtEngine->setOption(option, value); } +/** + * !!! This is only temporarily available until the parser is fully migrated to + * the new API. !!! + */ +ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); } + +/** + * !!! This is only temporarily available until the parser is fully migrated to + * the new API. !!! + */ +SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } + } // namespace api } // namespace CVC4 diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 0d05c9b19..b1a1e2abd 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -56,6 +56,15 @@ class CVC4_PUBLIC Result friend class Solver; public: + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param r the internal result that is to be wrapped by this result + * @return the Result + */ + Result(const CVC4::Result& r); + /** * Return true if query was a satisfiable checkSat() or checkSatAssuming() * query. @@ -116,14 +125,11 @@ class CVC4_PUBLIC Result */ std::string toString() const; - private: - /** - * Constructor. - * @param r the internal result that is to be wrapped by this result - * @return the Result - */ - Result(const CVC4::Result& r); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Result getResult(void) const; + private: /** * The interal result wrapped by this result. * This is a shared_ptr rather than a unique_ptr since CVC4::Result is @@ -160,6 +166,15 @@ class CVC4_PUBLIC Sort friend class Term; public: + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param t the internal type that is to be wrapped by this sort + * @return the Sort + */ + Sort(const CVC4::Type& t); + /** * Destructor. */ @@ -313,14 +328,11 @@ class CVC4_PUBLIC Sort */ std::string toString() const; - private: - /** - * Constructor. - * @param t the internal type that is to be wrapped by this sort - * @return the Sort - */ - Sort(const CVC4::Type& t); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Type getType(void) const; + private: /** * The interal type wrapped by this sort. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -361,6 +373,15 @@ class CVC4_PUBLIC Term friend struct TermHashFunction; public: + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + Term(const CVC4::Expr& e); + /** * Constructor. */ @@ -545,14 +566,11 @@ class CVC4_PUBLIC Term */ const_iterator end() const; - private: - /** - * Constructor. - * @param e the internal expression that is to be wrapped by this term - * @return the Term - */ - Term(const CVC4::Expr& e); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Expr getExpr(void) const; + private: /** * The internal expression wrapped by this term. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -650,6 +668,15 @@ class CVC4_PUBLIC OpTerm */ OpTerm(); + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + OpTerm(const CVC4::Expr& e); + /** * Destructor. */ @@ -701,14 +728,11 @@ class CVC4_PUBLIC OpTerm */ std::string toString() const; - private: - /** - * Constructor. - * @param e the internal expression that is to be wrapped by this term - * @return the Term - */ - OpTerm(const CVC4::Expr& e); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Expr getExpr(void) const; + private: /** * The internal expression wrapped by this operator term. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -812,6 +836,10 @@ class CVC4_PUBLIC DatatypeConstructorDecl */ std::string toString() const; + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::DatatypeConstructor getDatatypeConstructor(void) const; + private: /** * The internal (intermediate) datatype constructor wrapped by this @@ -875,6 +903,10 @@ class CVC4_PUBLIC DatatypeDecl */ std::string toString() const; + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Datatype getDatatype(void) const; + private: /* The internal (intermediate) datatype wrapped by this datatype * declaration @@ -898,6 +930,15 @@ class CVC4_PUBLIC DatatypeSelector */ DatatypeSelector(); + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param stor the internal datatype selector to be wrapped + * @return the DatatypeSelector + */ + DatatypeSelector(const CVC4::DatatypeConstructorArg& stor); + /** * Destructor. */ @@ -908,14 +949,11 @@ class CVC4_PUBLIC DatatypeSelector */ std::string toString() const; - private: - /** - * Constructor. - * @param stor the internal datatype selector to be wrapped - * @return the DatatypeSelector - */ - DatatypeSelector(const CVC4::DatatypeConstructorArg& stor); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const; + private: /** * The internal datatype selector wrapped by this datatype selector. * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -938,6 +976,15 @@ class CVC4_PUBLIC DatatypeConstructor */ DatatypeConstructor(); + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param ctor the internal datatype constructor to be wrapped + * @return thte DatatypeConstructor + */ + DatatypeConstructor(const CVC4::DatatypeConstructor& ctor); + /** * Destructor. */ @@ -1048,14 +1095,11 @@ class CVC4_PUBLIC DatatypeConstructor */ const_iterator end() const; - private: - /** - * Constructor. - * @param ctor the internal datatype constructor to be wrapped - * @return thte DatatypeConstructor - */ - DatatypeConstructor(const CVC4::DatatypeConstructor& ctor); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::DatatypeConstructor getDatatypeConstructor(void) const; + private: /** * The internal datatype constructor wrapped by this datatype constructor. * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -1073,6 +1117,15 @@ class CVC4_PUBLIC Datatype friend class Sort; public: + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param dtype the internal datatype to be wrapped + * @return the Datatype + */ + Datatype(const CVC4::Datatype& dtype); + /** * Destructor. */ @@ -1181,14 +1234,11 @@ class CVC4_PUBLIC Datatype */ const_iterator end() const; - private: - /** - * Constructor. - * @param dtype the internal datatype to be wrapped - * @return the Datatype - */ - Datatype(const CVC4::Datatype& dtype); + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Datatype getDatatype(void) const; + private: /** * The internal datatype wrapped by this datatype. * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -2349,6 +2399,14 @@ class CVC4_PUBLIC Solver */ void setOption(const std::string& option, const std::string& value) const; + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + ExprManager* getExprManager(void) const; + + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + SmtEngine* getSmtEngine(void) const; + private: /* Helper to convert a vector of internal types to sorts. */ std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index ff65e944c..7944c51ce 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -22,6 +22,7 @@ #include <iterator> #include <sstream> +#include "api/cvc4cpp.h" #include "base/exception.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -944,42 +945,53 @@ void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflag } } -ValidityChecker::ValidityChecker() : - d_clflags(new CLFlags()), - d_options(), - d_em(NULL), - d_emmc(), - d_reverseEmmc(), - d_smt(NULL), - d_parserContext(NULL), - d_exprTypeMapRemove(), - d_stackLevel(0), - d_constructors(), - d_selectors() { - d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); +ValidityChecker::ValidityChecker() + : d_clflags(new CLFlags()), + d_options(), + d_em(NULL), + d_emmc(), + d_reverseEmmc(), + d_smt(NULL), + d_parserContext(NULL), + d_exprTypeMapRemove(), + d_stackLevel(0), + d_constructors(), + d_selectors() +{ + d_solver.reset(new CVC4::api::Solver(&d_options)); + d_smt = d_solver->getSmtEngine(); + d_em = reinterpret_cast<ExprManager*>(d_solver->getExprManager()); s_validityCheckers[d_em] = this; - d_smt = new CVC4::SmtEngine(d_em); setUpOptions(d_options, *d_clflags); - d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); -} - -ValidityChecker::ValidityChecker(const CLFlags& clflags) : - d_clflags(new CLFlags(clflags)), - d_options(), - d_em(NULL), - d_emmc(), - d_reverseEmmc(), - d_smt(NULL), - d_parserContext(NULL), - d_exprTypeMapRemove(), - d_stackLevel(0), - d_constructors(), - d_selectors() { - d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>") + .withInputLanguage(CVC4::language::input::LANG_CVC4) + .withStringInput("") + .build(); +} + +ValidityChecker::ValidityChecker(const CLFlags& clflags) + : d_clflags(new CLFlags(clflags)), + d_options(), + d_em(NULL), + d_emmc(), + d_reverseEmmc(), + d_smt(NULL), + d_parserContext(NULL), + d_exprTypeMapRemove(), + d_stackLevel(0), + d_constructors(), + d_selectors() +{ + d_solver.reset(new CVC4::api::Solver(&d_options)); + d_smt = d_solver->getSmtEngine(); + d_em = reinterpret_cast<ExprManager*>(d_solver->getExprManager()); s_validityCheckers[d_em] = this; d_smt = new CVC4::SmtEngine(d_em); setUpOptions(d_options, *d_clflags); - d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>") + .withInputLanguage(CVC4::language::input::LANG_CVC4) + .withStringInput("") + .build(); } ValidityChecker::~ValidityChecker() { @@ -989,14 +1001,12 @@ ValidityChecker::~ValidityChecker() { } d_exprTypeMapRemove.clear(); delete d_parserContext; - delete d_smt; d_emmc.clear(); for(set<ValidityChecker*>::iterator i = d_reverseEmmc.begin(); i != d_reverseEmmc.end(); ++i) { (*i)->d_emmc.erase(d_em); } d_reverseEmmc.clear(); s_validityCheckers.erase(d_em); - delete d_em; delete d_clflags; } @@ -1609,7 +1619,11 @@ Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) { throw Exception("Unsupported language in exprFromString: " + ss.str()); } - CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "<internal>").withStringInput(s).withInputLanguage(lang).build(); + CVC4::parser::Parser* p = + CVC4::parser::ParserBuilder(d_solver.get(), "<internal>") + .withStringInput(s) + .withInputLanguage(lang) + .build(); p->useDeclarationsFrom(d_parserContext); Expr e = p->nextExpression(); if( e.isNull() ) { @@ -2570,7 +2584,10 @@ void ValidityChecker::reset() { // reset everything, forget everything d_smt->reset(); delete d_parserContext; - d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>") + .withInputLanguage(CVC4::language::input::LANG_CVC4) + .withStringInput("") + .build(); s_typeToExpr.clear(); s_exprToType.clear(); } @@ -2600,7 +2617,7 @@ void ValidityChecker::loadFile(const std::string& fileName, langss << lang; d_smt->setOption("input-language", CVC4::SExpr(langss.str())); d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); - CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); + CVC4::parser::ParserBuilder parserBuilder(d_solver.get(), fileName, opts); CVC4::parser::Parser* p = parserBuilder.build(); p->useDeclarationsFrom(d_parserContext); doCommands(p, d_smt, opts); @@ -2617,7 +2634,7 @@ void ValidityChecker::loadFile(std::istream& is, langss << lang; d_smt->setOption("input-language", CVC4::SExpr(langss.str())); d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); - CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); + CVC4::parser::ParserBuilder parserBuilder(d_solver.get(), "[stream]", opts); CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); d_parserContext = p; p->useDeclarationsFrom(d_parserContext); diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 7120e01f2..c9bde2fa0 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -2,7 +2,7 @@ /*! \file cvc3_compat.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Francois Bobot + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -232,6 +232,9 @@ class CVC4_PUBLIC Context; class CVC4_PUBLIC Proof {}; class CVC4_PUBLIC Theorem {}; +namespace api { +class CVC4_PUBLIC Solver; +} using CVC4::InputLanguage; using CVC4::Integer; using CVC4::Rational; @@ -513,6 +516,7 @@ class CVC4_PUBLIC ValidityChecker { CLFlags* d_clflags; CVC4::Options d_options; + std::unique_ptr<CVC4::api::Solver> d_solver; CVC3::ExprManager* d_em; std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc; std::set<ValidityChecker*> d_reverseEmmc; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 0fd421b24..40c31de99 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,6 +24,7 @@ #include <string> #include <vector> +#include "api/cvc4cpp.h" #include "main/main.h" #include "smt/command.h" @@ -48,15 +49,29 @@ void setNoLimitCPU() { void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString); -CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : - d_exprMgr(exprMgr), - d_smtEngine(new SmtEngine(&exprMgr)), - d_options(options), - d_stats("driver"), - d_result(), - d_replayStream(NULL) +CommandExecutor::CommandExecutor(api::Solver* solver, Options& options) + : d_solver(solver), + d_smtEngine(d_solver->getSmtEngine()), + d_options(options), + d_stats("driver"), + d_result(), + d_replayStream(NULL) {} +void CommandExecutor::flushStatistics(std::ostream& out) const +{ + d_solver->getExprManager()->getStatistics().flushInformation(out); + d_smtEngine->getStatistics().flushInformation(out); + d_stats.flushInformation(out); +} + +void CommandExecutor::safeFlushStatistics(int fd) const +{ + d_solver->getExprManager()->safeFlushStatistics(fd); + d_smtEngine->safeFlushStatistics(fd); + d_stats.safeFlushInformation(fd); +} + void CommandExecutor::setReplayStream(ExprStream* replayStream) { assert(d_replayStream == NULL); d_replayStream = replayStream; @@ -92,11 +107,11 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - if(d_options.getStatistics()) { + if (d_options.getStatistics()) + { flushStatistics(*d_options.getErr()); } - delete d_smtEngine; - d_smtEngine = new SmtEngine(&d_exprMgr); + d_solver->reset(); } bool CommandExecutor::doCommandSingleton(Command* cmd) diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 31a604174..7e7202a5a 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -2,7 +2,7 @@ /*! \file command_executor.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Tim King + ** Kshitij Bansal, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -25,6 +25,11 @@ #include "util/statistics_registry.h" namespace CVC4 { + +namespace api { +class Solver; +} + namespace main { class CommandExecutor { @@ -32,21 +37,22 @@ private: std::string d_lastStatistics; protected: - ExprManager& d_exprMgr; - SmtEngine* d_smtEngine; - Options& d_options; - StatisticsRegistry d_stats; - Result d_result; - ExprStream* d_replayStream; + api::Solver* d_solver; + SmtEngine* d_smtEngine; + Options& d_options; + StatisticsRegistry d_stats; + Result d_result; + ExprStream* d_replayStream; public: - CommandExecutor(ExprManager &exprMgr, Options &options); - - virtual ~CommandExecutor() { - delete d_smtEngine; - if(d_replayStream != NULL){ - delete d_replayStream; - } + CommandExecutor(api::Solver* solver, Options& options); + + virtual ~CommandExecutor() + { + if (d_replayStream != NULL) + { + delete d_replayStream; + } } /** @@ -63,20 +69,16 @@ public: return d_stats; } - virtual void flushStatistics(std::ostream& out) const { - d_exprMgr.getStatistics().flushInformation(out); - d_smtEngine->getStatistics().flushInformation(out); - d_stats.flushInformation(out); - } + /** + * Flushes statistics to a file descriptor. + */ + virtual void flushStatistics(std::ostream& out) const; /** - * Flushes statistics to a file descriptor. Safe to use in a signal handler. + * Flushes statistics to a file descriptor. + * Safe to use in a signal handler. */ - void safeFlushStatistics(int fd) const { - d_exprMgr.safeFlushStatistics(fd); - d_smtEngine->safeFlushStatistics(fd); - d_stats.safeFlushInformation(fd); - } + void safeFlushStatistics(int fd) const; static void printStatsFilterZeros(std::ostream& out, const std::string& statsString); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index f97b037eb..c29212c4f 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,6 +26,7 @@ // This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" +#include "api/cvc4cpp.h" #include "base/configuration.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -200,10 +201,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage()); // Create the expression manager using appropriate options - ExprManager* exprMgr; + std::unique_ptr<api::Solver> solver; # ifndef PORTFOLIO_BUILD - exprMgr = new ExprManager(opts); - pExecutor = new CommandExecutor(*exprMgr, opts); + solver.reset(new api::Solver(&opts)); + pExecutor = new CommandExecutor(solver.get(), opts); # else OptionsList threadOpts; parseThreadSpecificOptions(threadOpts, opts); @@ -230,19 +231,23 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } // pick appropriate one - if(useParallelExecutor) { - exprMgr = new ExprManager(threadOpts[0]); - pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); - } else { - exprMgr = new ExprManager(opts); - pExecutor = new CommandExecutor(*exprMgr, opts); + if (useParallelExecutor) + { + solver.reset(&threadOpts[0]); + pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); + } + else + { + solver.reset(&opts); + pExecutor = new CommandExecutor(solver.get(), opts); } # endif std::unique_ptr<Parser> replayParser; - if( opts.getReplayInputFilename() != "" ) { + if (opts.getReplayInputFilename() != "") + { std::string replayFilename = opts.getReplayInputFilename(); - ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); + ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts); if( replayFilename == "-") { if( inputFromStdin ) { @@ -281,7 +286,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } #endif /* PORTFOLIO_BUILD */ - InteractiveShell shell(*exprMgr); + InteractiveShell shell(solver.get()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); @@ -334,7 +339,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // delete cmd; } - ParserBuilder parserBuilder(exprMgr, filename, opts); + ParserBuilder parserBuilder(solver.get(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -491,7 +496,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } - ParserBuilder parserBuilder(exprMgr, filename, opts); + ParserBuilder parserBuilder(solver.get(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -578,7 +583,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // need to be around in that case for main() to print statistics. delete pTotalTime; delete pExecutor; - delete exprMgr; pTotalTime = NULL; pExecutor = NULL; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 2cec42fbf..aeccd3a64 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -37,6 +37,7 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ +#include "api/cvc4cpp.h" #include "base/output.h" #include "options/language.h" #include "options/options.h" @@ -87,13 +88,13 @@ static set<string> s_declarations; #endif /* HAVE_LIBREADLINE */ -InteractiveShell::InteractiveShell(ExprManager& exprManager) - : d_options(exprManager.getOptions()), +InteractiveShell::InteractiveShell(api::Solver* solver) + : d_options(solver->getExprManager()->getOptions()), d_in(*d_options.getIn()), d_out(*d_options.getOutConst()), d_quit(false) { - ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options); + ParserBuilder parserBuilder(solver, 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 203dfb766..ac52a78c4 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -25,9 +25,12 @@ namespace CVC4 { class Command; -class ExprManager; class Options; +namespace api { +class Solver; +} + namespace parser { class Parser; }/* CVC4::parser namespace */ @@ -47,7 +50,7 @@ class CVC4_PUBLIC InteractiveShell static const unsigned s_historyLimit = 500; public: - InteractiveShell(ExprManager& exprManager); + InteractiveShell(api::Solver* solver); /** * Close out the interactive session. diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 4da6dbb81..d9a065fd5 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -29,7 +29,6 @@ namespace CVC4 { class Command; class Expr; -class ExprManager; namespace parser { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 47124a589..182abb89b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -25,6 +25,7 @@ #include <sstream> #include <unordered_set> +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" @@ -42,10 +43,12 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, +Parser::Parser(api::Solver* solver, + Input* input, + bool strictMode, bool parseOnly) - : d_exprManager(exprManager), - d_resourceManager(d_exprManager->getResourceManager()), + : d_solver(solver), + d_resourceManager(d_solver->getExprManager()->getResourceManager()), d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), @@ -58,7 +61,8 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, d_parseOnly(parseOnly), d_canIncludeFile(true), d_logicIsForced(false), - d_forcedLogic() { + d_forcedLogic() +{ d_input->setParser(*this); } @@ -72,6 +76,11 @@ Parser::~Parser() { delete d_input; } +ExprManager* Parser::getExprManager() const +{ + return d_solver->getExprManager(); +} + Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); @@ -120,12 +129,12 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { if(isDefinedFunction(expr)) { // defined functions/constants are wrapped in an APPLY so that they are // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions - expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr); + expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr); }else{ Type te = expr.getType(); if(te.isConstructor() && ConstructorType(te).getArity() == 0) { // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); + expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); } } return expr; @@ -210,14 +219,14 @@ Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bo flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type, flags); + Expr expr = getExprManager()->mkVar(name, type, flags); defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } Expr Parser::mkBoundVar(const std::string& name, const Type& type) { Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkBoundVar(name, type); + Expr expr = getExprManager()->mkBoundVar(name, type); defineVar(name, expr, false); return expr; } @@ -228,7 +237,7 @@ Expr Parser::mkFunction(const std::string& name, const Type& type, flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type, flags); + Expr expr = getExprManager()->mkVar(name, type, flags); defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } @@ -240,7 +249,7 @@ Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return d_exprManager->mkVar(name.str(), type, flags); + return getExprManager()->mkVar(name.str(), type, flags); } std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, @@ -318,7 +327,7 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "newSort(" << name << ")" << std::endl; - Type type = d_exprManager->mkSort(name, flags); + Type type = getExprManager()->mkSort(name, flags); defineType(name, type); return type; } @@ -330,7 +339,7 @@ SortConstructorType Parser::mkSortConstructor(const std::string& name, Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; SortConstructorType type = - d_exprManager->mkSortConstructor(name, arity, flags); + getExprManager()->mkSortConstructor(name, arity, flags); defineType(name, vector<Type>(arity), type); return type; } @@ -353,7 +362,7 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor( const std::string& name, const std::vector<Type>& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - SortConstructorType unresolved = d_exprManager->mkSortConstructor( + SortConstructorType unresolved = getExprManager()->mkSortConstructor( name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); Type t = getSort(name, params); @@ -372,7 +381,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( std::vector<Datatype>& datatypes, bool doOverload) { try { std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved); assert(datatypes.size() == types.size()); @@ -467,7 +476,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, // the introduced variable is internal (not parsable) std::stringstream ss; ss << "__flatten_var_" << i; - Expr v = d_exprManager->mkBoundVar(ss.str(), domainTypes[i]); + Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]); flattenVars.push_back(v); } range = static_cast<FunctionType>(range).getRangeType(); @@ -476,7 +485,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, { return range; } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) @@ -493,14 +502,14 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); range = static_cast<FunctionType>(range).getRangeType(); } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex) { for (unsigned i = startIndex; i < args.size(); i++) { - expr = d_exprManager->mkExpr(HO_APPLY, expr, args[i]); + expr = getExprManager()->mkExpr(HO_APPLY, expr, args[i]); } return expr; } @@ -573,8 +582,8 @@ void Parser::checkArity(Kind kind, unsigned numArgs) return; } - unsigned min = d_exprManager->minArity(kind); - unsigned max = d_exprManager->maxArity(kind); + unsigned min = getExprManager()->minArity(kind); + unsigned max = getExprManager()->maxArity(kind); if (numArgs < min || numArgs > max) { stringstream ss; @@ -630,7 +639,7 @@ Command* Parser::nextCommand() dynamic_cast<QuitCommand*>(cmd) == NULL) { // don't count set-option commands as to not get stuck in an infinite // loop of resourcing out - const Options& options = d_exprManager->getOptions(); + const Options& options = getExprManager()->getOptions(); d_resourceManager->spendResource(options.getParseStep()); } return cmd; @@ -639,7 +648,7 @@ Command* Parser::nextCommand() Expr Parser::nextExpression() { Debug("parser") << "nextExpression()" << std::endl; - const Options& options = d_exprManager->getOptions(); + const Options& options = getExprManager()->getOptions(); d_resourceManager->spendResource(options.getParseStep()); Expr result; if (!done()) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 78cbcaafb..b0519691c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,23 +24,25 @@ #include <list> #include <cassert> -#include "parser/input.h" -#include "parser/parser_exception.h" #include "expr/expr.h" -#include "expr/symbol_table.h" -#include "expr/kind.h" #include "expr/expr_stream.h" +#include "expr/kind.h" +#include "expr/symbol_table.h" +#include "parser/input.h" +#include "parser/parser_exception.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { // Forward declarations class BooleanType; -class ExprManager; class Command; class FunctionType; class Type; class ResourceManager; +namespace api { +class Solver; +} //for sygus gterm two-pass parsing class CVC4_PUBLIC SygusGTerm { @@ -135,135 +137,137 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { class CVC4_PUBLIC Parser { friend class ParserBuilder; private: - /** The expression manager */ - ExprManager *d_exprManager; - /** The resource manager associated with this expr manager */ - ResourceManager *d_resourceManager; + /** The API Solver object. */ + api::Solver* d_solver; - /** The input that we're parsing. */ - Input *d_input; + /** The resource manager associated with this expr manager */ + ResourceManager* d_resourceManager; - /** - * The declaration scope that is "owned" by this parser. May or - * may not be the current declaration scope in use. - */ - SymbolTable d_symtabAllocated; + /** The input that we're parsing. */ + Input* d_input; - /** - * 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(). - */ - SymbolTable* d_symtab; + /** + * The declaration scope that is "owned" by this parser. May or + * may not be the current declaration scope in use. + */ + SymbolTable d_symtabAllocated; - /** - * The level of the assertions in the declaration scope. Things declared - * after this level are bindings from e.g. a let, a quantifier, or a - * lambda. - */ - size_t d_assertionLevel; + /** + * 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(). + */ + SymbolTable* d_symtab; - /** - * Whether we're in global declarations mode (all definitions and - * declarations are global). - */ - bool d_globalDeclarations; + /** + * The level of the assertions in the declaration scope. Things declared + * after this level are bindings from e.g. a let, a quantifier, or a + * lambda. + */ + size_t d_assertionLevel; - /** - * Maintains a list of reserved symbols at the assertion level that might - * not occur in our symbol table. This is necessary to e.g. support the - * proper behavior of the :named annotation in SMT-LIBv2 when used under - * a let or a quantifier, since inside a let/quant body the declaration - * scope is that of the let/quant body, but the defined name should be - * reserved at the assertion level. - */ - std::set<std::string> d_reservedSymbols; + /** + * Whether we're in global declarations mode (all definitions and + * declarations are global). + */ + bool d_globalDeclarations; + + /** + * Maintains a list of reserved symbols at the assertion level that might + * not occur in our symbol table. This is necessary to e.g. support the + * proper behavior of the :named annotation in SMT-LIBv2 when used under + * a let or a quantifier, since inside a let/quant body the declaration + * scope is that of the let/quant body, but the defined name should be + * reserved at the assertion level. + */ + std::set<std::string> d_reservedSymbols; - /** How many anonymous functions we've created. */ - size_t d_anonymousFunctionCount; + /** How many anonymous functions we've created. */ + size_t d_anonymousFunctionCount; - /** Are we done */ - bool d_done; + /** Are we done */ + bool d_done; - /** Are semantic checks enabled during parsing? */ - bool d_checksEnabled; + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; - /** Are we parsing in strict mode? */ - bool d_strictMode; + /** Are we parsing in strict mode? */ + bool d_strictMode; - /** Are we only parsing? */ - bool d_parseOnly; + /** Are we only parsing? */ + bool d_parseOnly; - /** - * Can we include files? (Set to false for security purposes in - * e.g. the online version.) - */ - bool d_canIncludeFile; - - /** - * Whether the logic has been forced with --force-logic. - */ - bool d_logicIsForced; + /** + * Can we include files? (Set to false for security purposes in + * e.g. the online version.) + */ + bool d_canIncludeFile; - /** - * The logic, if d_logicIsForced == true. - */ - std::string d_forcedLogic; + /** + * Whether the logic has been forced with --force-logic. + */ + bool d_logicIsForced; - /** The set of operators available in the current logic. */ - std::set<Kind> d_logicOperators; + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; - /** The set of attributes already warned about. */ - std::set<std::string> d_attributesWarnedAbout; + /** The set of operators available in the current logic. */ + std::set<Kind> d_logicOperators; - /** - * The current set of unresolved types. We can get by with this NOT - * being on the scope, because we can only have one DATATYPE - * definition going on at one time. This is a bit hackish; we - * depend on mkMutualDatatypeTypes() to check everything and clear - * this out. - */ - std::set<Type> d_unresolved; + /** The set of attributes already warned about. */ + std::set<std::string> d_attributesWarnedAbout; - /** - * "Preemption commands": extra commands implied by subterms that - * should be issued before the currently-being-parsed command is - * issued. Used to support SMT-LIBv2 ":named" attribute on terms. - * - * Owns the memory of the Commands in the queue. - */ - std::list<Command*> d_commandQueue; + /** + * The current set of unresolved types. We can get by with this NOT + * being on the scope, because we can only have one DATATYPE + * definition going on at one time. This is a bit hackish; we + * depend on mkMutualDatatypeTypes() to check everything and clear + * this out. + */ + std::set<Type> d_unresolved; + + /** + * "Preemption commands": extra commands implied by subterms that + * should be issued before the currently-being-parsed command is + * issued. Used to support SMT-LIBv2 ":named" attribute on terms. + * + * Owns the memory of the Commands in the queue. + */ + std::list<Command*> d_commandQueue; - /** Lookup a symbol in the given namespace (as specified by the type). - * Only returns a symbol if it is not overloaded, returns null otherwise. - */ - Expr getSymbol(const std::string& var_name, SymbolType type); + /** Lookup a symbol in the given namespace (as specified by the type). + * Only returns a symbol if it is not overloaded, returns null otherwise. + */ + Expr getSymbol(const std::string& var_name, SymbolType type); protected: - /** - * Create a parser state. - * - * @attention The parser takes "ownership" of the given - * input and will delete it on destruction. - * - * @param exprManager the expression manager to use when creating expressions - * @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 - * need not be performed, like those about unimplemented features, @see - * unimplementedFeature()) - */ - Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + /** + * Create a parser state. + * + * @attention The parser takes "ownership" of the given + * input and will delete it on destruction. + * + * @param the solver API object + * @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 + * need not be performed, like those about unimplemented features, @see + * unimplementedFeature()) + */ + Parser(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: virtual ~Parser(); /** Get the associated <code>ExprManager</code>. */ - inline ExprManager* getExprManager() const { - return d_exprManager; - } + ExprManager* getExprManager() const; /** Get the associated input. */ inline Input* getInput() const { diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 4505c4f86..95a3a7840 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -2,7 +2,7 @@ /*! \file parser_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -21,10 +21,11 @@ #include <string> +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" +#include "options/options.h" #include "parser/input.h" #include "parser/parser.h" -#include "options/options.h" #include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" @@ -32,29 +33,28 @@ namespace CVC4 { namespace parser { -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename) : - d_filename(filename), - d_exprManager(exprManager) { - init(exprManager, filename); +ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename) + : d_filename(filename), d_solver(solver) +{ + init(solver, filename); } -ParserBuilder::ParserBuilder(ExprManager* exprManager, +ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename, - const Options& options) : - d_filename(filename), - d_exprManager(exprManager) { - init(exprManager, filename); + const Options& options) + : d_filename(filename), d_solver(solver) +{ + init(solver, filename); withOptions(options); } -void ParserBuilder::init(ExprManager* exprManager, - const std::string& filename) { +void ParserBuilder::init(api::Solver* solver, const std::string& filename) +{ d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; d_filename = filename; d_streamInput = NULL; - d_exprManager = exprManager; + d_solver = solver; d_checksEnabled = true; d_strictMode = false; d_canIncludeFile = true; @@ -87,26 +87,27 @@ Parser* ParserBuilder::build() assert(input != NULL); Parser* parser = NULL; - switch(d_lang) { - case language::input::LANG_SMTLIB_V1: - parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); - break; - case language::input::LANG_SYGUS: - parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); - break; - case language::input::LANG_TPTP: - parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); - break; - default: - if (language::isInputLang_smt2(d_lang)) - { - parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); - } - else - { - parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); - } - break; + switch (d_lang) + { + case language::input::LANG_SMTLIB_V1: + parser = new Smt1(d_solver, input, d_strictMode, d_parseOnly); + break; + case language::input::LANG_SYGUS: + parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); + break; + case language::input::LANG_TPTP: + parser = new Tptp(d_solver, input, d_strictMode, d_parseOnly); + break; + default: + if (language::isInputLang_smt2(d_lang)) + { + parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); + } + else + { + parser = new Parser(d_solver, input, d_strictMode, d_parseOnly); + } + break; } if( d_checksEnabled ) { @@ -133,8 +134,9 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withExprManager(ExprManager* exprManager) { - d_exprManager = exprManager; +ParserBuilder& ParserBuilder::withSolver(api::Solver* solver) +{ + d_solver = solver; return *this; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index c4c75aae5..3e14d715a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -2,7 +2,7 @@ /*! \file parser_builder.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -26,9 +26,12 @@ namespace CVC4 { -class ExprManager; class Options; +namespace api { +class Solver; +} + namespace parser { class Parser; @@ -61,8 +64,8 @@ class CVC4_PUBLIC ParserBuilder { /** The stream input, if any. */ std::istream* d_streamInput; - /** The expression manager */ - ExprManager* d_exprManager; + /** The API Solver object. */ + api::Solver* d_solver; /** Should semantic checks be enabled during parsing? */ bool d_checksEnabled; @@ -86,14 +89,14 @@ class CVC4_PUBLIC ParserBuilder { std::string d_forcedLogic; /** Initialize this parser builder */ - void init(ExprManager* exprManager, const std::string& filename); - -public: + void init(api::Solver* solver, const std::string& filename); - /** Create a parser builder using the given ExprManager and filename. */ - ParserBuilder(ExprManager* exprManager, const std::string& filename); + public: + /** Create a parser builder using the given Solver and filename. */ + ParserBuilder(api::Solver* solver, const std::string& filename); - ParserBuilder(ExprManager* exprManager, const std::string& filename, + ParserBuilder(api::Solver* solver, + const std::string& filename, const Options& options); /** Build the parser, using the current settings. */ @@ -102,8 +105,8 @@ public: /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); - /** Set the ExprManager to use with the parser. */ - ParserBuilder& withExprManager(ExprManager* exprManager); + /** Set the Solver to use with the parser. */ + ParserBuilder& withSolver(api::Solver* solver); /** Set the parser to read a file for its input. (Default) */ ParserBuilder& withFileInput(); diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 87da44c0e..544c6e85c 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -14,9 +14,10 @@ #include "parser/smt1/smt1.h" +#include "api/cvc4cpp.h" #include "expr/type.h" -#include "smt/command.h" #include "parser/parser.h" +#include "smt/command.h" namespace CVC4 { namespace parser { @@ -70,9 +71,9 @@ Smt1::Logic Smt1::toLogic(const std::string& name) { return logicMap[name]; } -Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, - bool parseOnly) - : Parser(exprManager, input, strictMode, parseOnly), d_logic(UNSET) { +Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET) +{ // Boolean symbols are always defined addOperator(kind::AND); addOperator(kind::EQUAL); @@ -81,7 +82,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, addOperator(kind::NOT); addOperator(kind::OR); addOperator(kind::XOR); - } void Smt1::addArithmeticOperators() { diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index 42b6a4157..fe177d21e 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -2,7 +2,7 @@ /*! \file smt1.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -26,6 +26,10 @@ namespace CVC4 { class SExpr; +namespace api { +class Solver; +} + namespace parser { class Smt1 : public Parser { @@ -93,7 +97,10 @@ private: Logic d_logic; protected: - Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt1(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: /** diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a0cc750b3..0a93beb2e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,6 +15,7 @@ **/ #include "parser/smt2/smt2.h" +#include "api/cvc4cpp.h" #include "expr/type.h" #include "options/options.h" #include "parser/antlr_input.h" @@ -34,10 +35,11 @@ namespace CVC4 { namespace parser { -Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : - Parser(exprManager,input,strictMode,parseOnly), - d_logicSet(false) { - if( !strictModeEnabled() ) { +Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_logicSet(false) +{ + if (!strictModeEnabled()) + { addTheory(Smt2::THEORY_CORE); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c9b224d39..64a957402 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -34,6 +34,10 @@ namespace CVC4 { class SExpr; +namespace api { +class Solver; +} + namespace parser { class Smt2 : public Parser { @@ -69,7 +73,10 @@ private: std::map< Expr, bool > d_sygusVarPrimed; protected: - Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt2(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: /** diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 0228fdeff..ee313a202 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -20,6 +20,7 @@ #include <algorithm> #include <set> +#include "api/cvc4cpp.h" #include "expr/type.h" #include "parser/parser.h" @@ -30,11 +31,9 @@ namespace CVC4 { namespace parser { -Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, - bool parseOnly) - : Parser(exprManager, input, strictMode, parseOnly), - d_cnf(false), - d_fof(false) { +Tptp::Tptp(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_cnf(false), d_fof(false) +{ addTheory(Tptp::THEORY_CORE); /* Try to find TPTP dir */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 3ce9668e0..eb5532247 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -30,6 +30,11 @@ #include "util/hash.h" namespace CVC4 { + +namespace api { +class Solver; +} + namespace parser { class Tptp : public Parser { @@ -81,7 +86,9 @@ class Tptp : public Parser { bool hasConjecture() const { return d_hasConjecture; } protected: - Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, + Tptp(api::Solver* solver, + Input* input, + bool strictMode = false, bool parseOnly = false); public: |