From: Aina Niemetz Date: Thu, 9 Aug 2018 02:21:47 +0000 (-0700) Subject: Plug solver API object into parser. (#2240) X-Git-Tag: cvc5-1.0.0~4794 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91d85704313de6be9fd382833f5cedd39e24a6fa;p=cvc5.git Plug solver API object into parser. (#2240) --- diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am index d12f2877e..6ce35b300 100644 --- a/examples/api/java/Makefile.am +++ b/examples/api/java/Makefile.am @@ -2,7 +2,7 @@ noinst_DATA = if CVC4_LANGUAGE_BINDING_JAVA noinst_DATA += \ - CVC4Streams.class \ + #CVC4Streams.class \ ## disabled until bindings for the new API are in place (issue #2284) BitVectors.class \ BitVectorsAndArrays.class \ Combination.class \ diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index a9c18c3ae..a6c146622 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -2,7 +2,7 @@ /*! \file normalize.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters + ** Dejan Jovanovic, 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. @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "options/language.h" @@ -29,8 +30,8 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt/smt_engine.h" #include "smt/command.h" +#include "smt/smt_engine.h" using namespace std; using namespace CVC4; @@ -46,18 +47,16 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); cout << language::SetLanguage(language::output::LANG_SMTLIB_V2) << expr::ExprSetDepth(-1); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); - // Smt manager for simplifications - SmtEngine engine(&exprManager); - // Variables and assertions vector assertions; @@ -66,7 +65,7 @@ int main(int argc, char* argv[]) AssertCommand* assert = dynamic_cast(cmd); if (assert) { - Expr normalized = engine.simplify(assert->getExpr()); + Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr()); cout << "(assert " << normalized << ")" << endl; delete cmd; continue; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 1ece6a86d..55ddb0997 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -2,7 +2,7 @@ /*! \file smt2info.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters + ** Dejan Jovanovic, Aina Niemetz, Tim King ** 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,6 +21,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/options.h" #include "parser/parser.h" @@ -78,10 +79,11 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); // Variables and assertions @@ -122,7 +124,9 @@ int main(int argc, char* argv[]) unsigned total_degree = 0; for (unsigned i = 0; i < assertions.size(); ++ i) { - total_degree = std::max(total_degree, compute_degree(exprManager, assertions[i])); + total_degree = + std::max(total_degree, + compute_degree(*solver->getExprManager(), assertions[i])); } cout << "degree: " << total_degree << endl; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 94cb23a79..04a33624c 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -2,7 +2,7 @@ /*! \file smt2todreal.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters + ** Dejan Jovanovic, 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. @@ -22,13 +22,14 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt/smt_engine.h" #include "smt/command.h" +#include "smt/smt_engine.h" using namespace std; using namespace CVC4; @@ -45,17 +46,15 @@ int main(int argc, char* argv[]) Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); options.setOutputLanguage(language::output::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); cout << expr::ExprDag(0) << expr::ExprSetDepth(-1); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); - // Smt manager for simplifications - SmtEngine engine(&exprManager); - // Variables and assertions std::map variables; vector info_tags; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 767da1ffd..c4649dcae 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -2,7 +2,7 @@ /*! \file smt2toisat.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Andrew Reynolds + ** Dejan Jovanovic, 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. @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/options.h" #include "parser/parser.h" @@ -50,15 +51,13 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); - // Smt manager for simplifications - SmtEngine engine(&exprManager); - // Variables and assertions std::map variables; vector info_tags; @@ -88,7 +87,7 @@ int main(int argc, char* argv[]) AssertCommand* assert = dynamic_cast(cmd); if (assert) { - assertions.push_back(engine.simplify(assert->getExpr())); + assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); delete cmd; continue; } diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index b60c4824b..fd344caa9 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/options.h" #include "parser/parser.h" @@ -48,10 +49,11 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); // Variables and assertions diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index aea436383..acfd6bf97 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/options.h" #include "parser/parser.h" @@ -49,10 +50,11 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); // Variables and assertions diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index b7bbc5a75..feb5a583a 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -2,7 +2,7 @@ /*! \file smt2toredlog.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Andrew Reynolds + ** Dejan Jovanovic, 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. @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/options.h" #include "parser/parser.h" @@ -53,15 +54,13 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); Parser* parser = parserBuilder.build(); - // Smt manager for simplifications - SmtEngine engine(&exprManager); - // Variables and assertions std::map variables; vector info_tags; @@ -91,7 +90,7 @@ int main(int argc, char* argv[]) AssertCommand* assert = dynamic_cast(cmd); if (assert) { - assertions.push_back(engine.simplify(assert->getExpr())); + assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); delete cmd; continue; } diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index f5398f4df..452a874a8 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -2,7 +2,7 @@ /*! \file sets_translate.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Mathias Preiner + ** Kshitij Bansal, 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. @@ -23,6 +23,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "options/language.h" #include "options/options.h" @@ -268,12 +269,13 @@ int main(int argc, char* argv[]) options.setInputLanguage(language::input::LANG_SMTLIB_V2); cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); // cout << Expr::dag(0); - ExprManager exprManager(options); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&options)); - Mapper m(&exprManager); + Mapper m(solver->getExprManager()); // Create the parser - ParserBuilder parserBuilder(&exprManager, input, options); + ParserBuilder parserBuilder(solver.get(), input, options); if(input == "") parserBuilder.withStreamInput(cin); Parser* parser = parserBuilder.build(); diff --git a/examples/translator.cpp b/examples/translator.cpp index 1de05f65a..5be837e63 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -2,7 +2,7 @@ /*! \file translator.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** 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. @@ -22,6 +22,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "options/language.h" @@ -105,7 +106,9 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag Options opts; opts.setInputLanguage(fromLang); ExprManager exprMgr(opts); - ParserBuilder parserBuilder(&exprMgr, filename, opts); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&opts)); + ParserBuilder parserBuilder(solver.get(), filename, opts); if(!strcmp(filename, "-")) { parserBuilder.withFilename(""); parserBuilder.withLineBufferedStreamInput(cin); 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( - opts == nullptr ? new ExprManager(Options()) : new ExprManager(*opts)); - d_smtEngine = std::unique_ptr(new SmtEngine(d_exprMgr.get())); - d_rng = std::unique_ptr(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 sortVectorToTypes(const std::vector& 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 #include +#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(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(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, "").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(new CVC4::ExprManager(d_options)); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "") + .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(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, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "") + .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::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, "").withStringInput(s).withInputLanguage(lang).build(); + CVC4::parser::Parser* p = + CVC4::parser::ParserBuilder(d_solver.get(), "") + .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, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); + d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "") + .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 d_solver; CVC3::ExprManager* d_em; std::map d_emmc; std::set 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 #include +#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 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 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 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 #include +#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 Parser::mkVars(const std::vector 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(arity), type); return type; } @@ -353,7 +362,7 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor( const std::string& name, const std::vector& 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 Parser::mkMutualDatatypeTypes( std::vector& datatypes, bool doOverload) { try { std::vector 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& 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(range).getRangeType(); @@ -476,7 +485,7 @@ Type Parser::mkFlatFunctionType(std::vector& sorts, { return range; } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Type Parser::mkFlatFunctionType(std::vector& sorts, Type range) @@ -493,14 +502,14 @@ Type Parser::mkFlatFunctionType(std::vector& sorts, Type range) sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); range = static_cast(range).getRangeType(); } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Expr Parser::mkHoApply(Expr expr, std::vector& 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(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 #include -#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 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 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 d_logicOperators; + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; - /** The set of attributes already warned about. */ - std::set d_attributesWarnedAbout; + /** The set of operators available in the current logic. */ + std::set 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 d_unresolved; + /** The set of attributes already warned about. */ + std::set 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 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 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 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 ExprManager. */ - 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 +#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 #include +#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: diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index 1df405a17..a135e6c6c 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -2,7 +2,7 @@ /*! \file ouroborous.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** 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. @@ -28,6 +28,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "options/set_language.h" @@ -108,12 +109,12 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL int runTest() { - ExprManager em; - psr = - ParserBuilder(&em, "internal-buffer") - .withStringInput(declarations) - .withInputLanguage(input::LANG_SMTLIB_V2) - .build(); + std::unique_ptr solver = + std::unique_ptr(new api::Solver()); + psr = ParserBuilder(solver.get(), "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(input::LANG_SMTLIB_V2) + .build(); // we don't need to execute them, but we DO need to parse them to // get the declarations diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 134185dc4..8a14094d3 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -2,7 +2,7 @@ /*! \file smt2_compliance.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Aina Niemetz, Tim King ** 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. @@ -18,6 +18,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "options/options.h" #include "options/set_language.h" @@ -30,43 +31,45 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; -void testGetInfo(SmtEngine& smt, const char* s); +void testGetInfo(api::Solver* solver, const char* s); -int main() { +int main() +{ Options opts; opts.setInputLanguage(language::input::LANG_SMTLIB_V2); opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - ExprManager em(opts); - SmtEngine smt(&em); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&opts)); - testGetInfo(smt, ":error-behavior"); - testGetInfo(smt, ":name"); - testGetInfo(smt, ":authors"); - testGetInfo(smt, ":version"); - testGetInfo(smt, ":status"); - testGetInfo(smt, ":reason-unknown"); - testGetInfo(smt, ":arbitrary-undefined-keyword"); - testGetInfo(smt, ":56");// legal - testGetInfo(smt, ":<=");// legal - testGetInfo(smt, ":->");// legal - testGetInfo(smt, ":all-statistics"); + testGetInfo(solver.get(), ":error-behavior"); + testGetInfo(solver.get(), ":name"); + testGetInfo(solver.get(), ":authors"); + testGetInfo(solver.get(), ":version"); + testGetInfo(solver.get(), ":status"); + testGetInfo(solver.get(), ":reason-unknown"); + testGetInfo(solver.get(), ":arbitrary-undefined-keyword"); + testGetInfo(solver.get(), ":56"); // legal + testGetInfo(solver.get(), ":<="); // legal + testGetInfo(solver.get(), ":->"); // legal + testGetInfo(solver.get(), ":all-statistics"); return 0; } -void testGetInfo(SmtEngine& smt, const char* s) { - ParserBuilder pb(smt.getExprManager(), "", - smt.getExprManager()->getOptions()); +void testGetInfo(api::Solver* solver, const char* s) +{ + ParserBuilder pb( + solver, "", solver->getExprManager()->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); assert(p != NULL); Command* c = p->nextCommand(); assert(c != NULL); cout << c << endl; stringstream ss; - c->invoke(&smt, ss); + c->invoke(solver->getSmtEngine(), ss); assert(p->nextCommand() == NULL); delete p; delete c; diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index cf68b5465..44b3660c9 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -2,7 +2,7 @@ /*! \file interactive_shell_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Aina Niemetz, Morgan Deters ** 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. @@ -20,6 +20,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" @@ -31,64 +32,38 @@ using namespace CVC4; using namespace std; -class InteractiveShellBlack : public CxxTest::TestSuite { -private: - ExprManager* d_exprManager; - Options d_options; - stringstream* d_sin; - stringstream* d_sout; - - /** - * Read up to maxCommands+1 from the shell and throw an assertion error if - * it's fewer than minCommands and more than maxCommands. - * Note that an empty string followed by EOF may be returned as an empty - * command, and not NULL (subsequent calls to readCommand() should return - * NULL). E.g., "CHECKSAT;\n" may return two commands: the CHECKSAT, - * followed by an empty command, followed by NULL. - */ - void countCommands(InteractiveShell& shell, - int minCommands, - int maxCommands) { - Command* cmd; - int n = 0; - while( n <= maxCommands && (cmd = shell.readCommand()) != NULL ) { - ++n; - delete cmd; - } - TS_ASSERT( n <= maxCommands ); - TS_ASSERT( n >= minCommands ); - } - +class InteractiveShellBlack : public CxxTest::TestSuite +{ public: - void setUp() { + void setUp() + { d_sin = new stringstream; d_sout = new stringstream; d_options.set(options::in, d_sin); d_options.set(options::out, d_sout); d_options.set(options::inputLanguage, language::input::LANG_CVC4); - d_exprManager = new ExprManager(d_options); + d_solver.reset(new api::Solver(&d_options)); } void tearDown() { - delete d_exprManager; delete d_sin; delete d_sout; } void testAssertTrue() { *d_sin << "ASSERT TRUE;\n" << flush; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); countCommands( shell, 1, 1 ); } void testQueryFalse() { *d_sin << "QUERY FALSE;\n" << flush; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); countCommands( shell, 1, 1 ); } void testDefUse() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.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... */ @@ -96,7 +71,7 @@ private: } void testDefUse2() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); /* readCommand may return a sequence, see above. */ *d_sin << "x : REAL;\n" << flush; Command* tmp = shell.readCommand(); @@ -106,16 +81,42 @@ private: } void testEmptyLine() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); *d_sin << flush; countCommands(shell,0,0); } void testRepeatedEmptyLines() { *d_sin << "\n\n\n"; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); /* Might return up to four empties, might return nothing */ countCommands( shell, 0, 3 ); } + private: + std::unique_ptr d_solver; + Options d_options; + stringstream* d_sin; + stringstream* d_sout; + + /** + * Read up to maxCommands+1 from the shell and throw an assertion error if + * it's fewer than minCommands and more than maxCommands. Note that an empty + * string followed by EOF may be returned as an empty command, and not NULL + * (subsequent calls to readCommand() should return NULL). E.g., "CHECKSAT;\n" + * may return two commands: the CHECKSAT, followed by an empty command, + * followed by NULL. + */ + void countCommands(InteractiveShell& shell, int minCommands, int maxCommands) + { + Command* cmd; + int n = 0; + while (n <= maxCommands && (cmd = shell.readCommand()) != NULL) + { + ++n; + delete cmd; + } + TS_ASSERT(n <= maxCommands); + TS_ASSERT(n >= minCommands); + } }; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index b3c36e2c4..7b52e0662 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,7 +2,7 @@ /*! \file parser_black.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. @@ -19,6 +19,7 @@ #include #include +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -36,69 +37,71 @@ using namespace CVC4::parser; using namespace CVC4::language::input; using namespace std; -class ParserBlack { - InputLanguage d_lang; - ExprManager *d_exprManager; - -protected: +class ParserBlack +{ + protected: Options d_options; /* Set up declaration context for expr inputs */ virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ - parser.mkVar("a",d_exprManager->booleanType()); - parser.mkVar("b",d_exprManager->booleanType()); - parser.mkVar("c",d_exprManager->booleanType()); + parser.mkVar("a", d_solver->getExprManager()->booleanType()); + parser.mkVar("b", d_solver->getExprManager()->booleanType()); + parser.mkVar("c", d_solver->getExprManager()->booleanType()); /* t, u, v: TYPE */ Type t = parser.mkSort("t"); Type u = parser.mkSort("u"); Type v = parser.mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parser.mkVar("f", d_exprManager->mkFunctionType(t,u)); - parser.mkVar("g", d_exprManager->mkFunctionType(u,v)); - parser.mkVar("h", d_exprManager->mkFunctionType(v,t)); + parser.mkVar("f", d_solver->getExprManager()->mkFunctionType(t, u)); + parser.mkVar("g", d_solver->getExprManager()->mkFunctionType(u, v)); + parser.mkVar("h", d_solver->getExprManager()->mkFunctionType(v, t)); /* x:t; y:u; z:v; */ parser.mkVar("x",t); parser.mkVar("y",u); parser.mkVar("z",v); } - void tryGoodInput(const string goodInput) { - try { -// Debug.on("parser"); -// Debug.on("parser-extra"); -// cerr << "Testing good input: <<" << goodInput << ">>" << endl; -// istringstream stream(goodInputs[i]); - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(goodInput) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); - TS_ASSERT( !parser->done() ); - Command* cmd; - while((cmd = parser->nextCommand()) != NULL) { - Debug("parser") << "Parsed command: " << (*cmd) << endl; - delete cmd; - } - - TS_ASSERT( parser->done() ); - delete parser; -// Debug.off("parser"); -// Debug.off("parser-extra"); - } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInput << endl - << e << endl; -// Debug.off("parser"); - throw; + void tryGoodInput(const string goodInput) + { + try + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + // cerr << "Testing good input: <<" << goodInput << ">>" << endl; + // istringstream stream(goodInputs[i]); + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(goodInput) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build(); + TS_ASSERT(!parser->done()); + Command* cmd; + while ((cmd = parser->nextCommand()) != NULL) + { + Debug("parser") << "Parsed command: " << (*cmd) << endl; + delete cmd; } + + TS_ASSERT(parser->done()); + delete parser; + // Debug.off("parser"); + // Debug.off("parser-extra"); + } + catch (Exception& e) + { + cout << "\nGood input failed:\n" << goodInput << endl << e << endl; + // Debug.off("parser"); + throw; + } } - void tryBadInput(const string badInput, bool strictMode = false) { -// cerr << "Testing bad input: '" << badInput << "'\n"; -// Debug.on("parser"); + void tryBadInput(const string badInput, bool strictMode = false) + { + // cerr << "Testing bad input: '" << badInput << "'\n"; + // Debug.on("parser"); - Parser* parser = ParserBuilder(d_exprManager, "test") + Parser* parser = ParserBuilder(d_solver.get(), "test") .withStringInput(badInput) .withOptions(d_options) .withInputLanguage(d_lang) @@ -107,7 +110,8 @@ protected: TS_ASSERT_THROWS( { Command* cmd; - while ((cmd = parser->nextCommand()) != NULL) { + while ((cmd = parser->nextCommand()) != NULL) + { Debug("parser") << "Parsed command: " << (*cmd) << endl; delete cmd; } @@ -118,37 +122,40 @@ protected: delete parser; } - void tryGoodExpr(const string goodExpr) { -// Debug.on("parser"); -// Debug.on("parser-extra"); - try { -// cerr << "Testing good expr: '" << goodExpr << "'\n"; - // Debug.on("parser"); -// istringstream stream(context + goodBooleanExprs[i]); - - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(goodExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); - - TS_ASSERT( !parser->done() ); - setupContext(*parser); - TS_ASSERT( !parser->done() ); - Expr e = parser->nextExpression(); - TS_ASSERT( !e.isNull() ); - e = parser->nextExpression(); - TS_ASSERT( parser->done() ); - TS_ASSERT( e.isNull() ); - delete parser; - } catch (Exception& e) { - cout << endl - << "Good expr failed." << endl - << "Input: <<" << goodExpr << ">>" << endl - << "Output: <<" << e << ">>" << endl; - throw; - } + void tryGoodExpr(const string goodExpr) + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + try + { + // cerr << "Testing good expr: '" << goodExpr << "'\n"; + // Debug.on("parser"); + // istringstream stream(context + goodBooleanExprs[i]); + + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(goodExpr) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build(); + + TS_ASSERT(!parser->done()); + setupContext(*parser); + TS_ASSERT(!parser->done()); + Expr e = parser->nextExpression(); + TS_ASSERT(!e.isNull()); + e = parser->nextExpression(); + TS_ASSERT(parser->done()); + TS_ASSERT(e.isNull()); + delete parser; + } + catch (Exception& e) + { + cout << endl + << "Good expr failed." << endl + << "Input: <<" << goodExpr << ">>" << endl + << "Output: <<" << e << ">>" << endl; + throw; + } } /* NOTE: The check implemented here may fail if a bad expression @@ -159,44 +166,48 @@ protected: * input was consumed here, so just be careful to avoid valid * prefixes in tests. */ - void tryBadExpr(const string badExpr, bool strictMode = false) { -// Debug.on("parser"); -// Debug.on("parser-extra"); -// cout << "Testing bad expr: '" << badExpr << "'\n"; - - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(badExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build(); - setupContext(*parser); - TS_ASSERT( !parser->done() ); - TS_ASSERT_THROWS - ( Expr e = parser->nextExpression(); - cout << endl - << "Bad expr succeeded." << endl - << "Input: <<" << badExpr << ">>" << endl - << "Output: <<" << e << ">>" << endl;, - const ParserException& ); - delete parser; -// Debug.off("parser"); + void tryBadExpr(const string badExpr, bool strictMode = false) + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + // cout << "Testing bad expr: '" << badExpr << "'\n"; + + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(badExpr) + .withOptions(d_options) + .withInputLanguage(d_lang) + .withStrictMode(strictMode) + .build(); + setupContext(*parser); + TS_ASSERT(!parser->done()); + TS_ASSERT_THROWS(Expr e = parser->nextExpression(); + cout << endl + << "Bad expr succeeded." << endl + << "Input: <<" << badExpr << ">>" << endl + << "Output: <<" << e << ">>" << endl; + , const ParserException&); + delete parser; + // Debug.off("parser"); } ParserBlack(InputLanguage lang) : d_lang(lang) { } - void setUp() { - d_exprManager = new ExprManager; + void setUp() + { d_options.set(options::parseOnly, true); + d_solver.reset(new api::Solver(&d_options)); } void tearDown() { - delete d_exprManager; } -};/* class ParserBlack */ + + private: + InputLanguage d_lang; + std::unique_ptr d_solver; + +}; /* class ParserBlack */ class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 066c45fe1..45baf177f 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -2,7 +2,7 @@ /*! \file parser_builder_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters + ** Christopher L. Conway, Aina Niemetz, Tim King ** 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. @@ -24,6 +24,7 @@ #include #include +#include "api/cvc4cpp.h" #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -34,57 +35,19 @@ using namespace CVC4::parser; using namespace CVC4::language::input; using namespace std; -class ParserBuilderBlack : public CxxTest::TestSuite { +class ParserBuilderBlack : public CxxTest::TestSuite +{ + public: + void setUp() { d_solver.reset(new api::Solver()); } - ExprManager *d_exprManager; + void tearDown() {} - void checkEmptyInput(ParserBuilder& builder) { - Parser *parser = builder.build(); - TS_ASSERT( parser != NULL ); - - Expr e = parser->nextExpression(); - TS_ASSERT( e.isNull() ); - - delete parser; - } - - void checkTrueInput(ParserBuilder& builder) { - Parser *parser = builder.build(); - TS_ASSERT( parser != NULL ); - - Expr e = parser->nextExpression(); - TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) ); - - e = parser->nextExpression(); - TS_ASSERT( e.isNull() ); - delete parser; - } - - char* mkTemp() { - char *filename = strdup("/tmp/testinput.XXXXXX"); - int fd = mkstemp(filename); - TS_ASSERT( fd != -1 ); - close(fd); - return filename; - } - -public: - - void setUp() { - d_exprManager = new ExprManager; - } - - void tearDown() { - delete d_exprManager; - } - - void testEmptyFileInput() { + void testEmptyFileInput() + { char *filename = mkTemp(); checkEmptyInput( - ParserBuilder(d_exprManager,filename) - .withInputLanguage(LANG_CVC4) - ); + ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); remove(filename); free(filename); @@ -98,48 +61,72 @@ public: fs.close(); checkTrueInput( - ParserBuilder(d_exprManager,filename) - .withInputLanguage(LANG_CVC4) - ); + ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); remove(filename); free(filename); } void testEmptyStringInput() { - checkEmptyInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStringInput("") - ); + checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("")); } void testTrueStringInput() { - checkTrueInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStringInput("TRUE") - ); + checkTrueInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("TRUE")); } void testEmptyStreamInput() { stringstream ss( "", ios_base::in ); - checkEmptyInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStreamInput(ss) - ); + checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss)); } void testTrueStreamInput() { stringstream ss( "TRUE", ios_base::in ); - checkTrueInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStreamInput(ss) - ); + checkTrueInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss)); } + private: + void checkEmptyInput(ParserBuilder &builder) + { + Parser *parser = builder.build(); + TS_ASSERT(parser != NULL); + + Expr e = parser->nextExpression(); + TS_ASSERT(e.isNull()); + + delete parser; + } + + void checkTrueInput(ParserBuilder &builder) + { + Parser *parser = builder.build(); + TS_ASSERT(parser != NULL); + + Expr e = parser->nextExpression(); + TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true)); + + e = parser->nextExpression(); + TS_ASSERT(e.isNull()); + delete parser; + } + + char *mkTemp() + { + char *filename = strdup("/tmp/testinput.XXXXXX"); + int fd = mkstemp(filename); + TS_ASSERT(fd != -1); + close(fd); + return filename; + } + std::unique_ptr d_solver; }; // class ParserBuilderBlack