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 \
/*! \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.
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
#include "options/language.h"
#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;
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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<Expr> assertions;
AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
if (assert) {
- Expr normalized = engine.simplify(assert->getExpr());
+ Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr());
cout << "(assert " << normalized << ")" << endl;
delete cmd;
continue;
/*! \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.
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/options.h"
#include "parser/parser.h"
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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
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;
/*! \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.
#include <typeinfo>
#include <vector>
+#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;
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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<Expr, unsigned> variables;
vector<string> info_tags;
/*! \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.
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/options.h"
#include "parser/parser.h"
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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<Expr, unsigned> variables;
vector<string> info_tags;
AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
if (assert) {
- assertions.push_back(engine.simplify(assert->getExpr()));
+ assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr()));
delete cmd;
continue;
}
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/options.h"
#include "parser/parser.h"
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/options.h"
#include "parser/parser.h"
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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
/*! \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.
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/options.h"
#include "parser/parser.h"
// Create the expression manager
Options options;
options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- ExprManager exprManager(options);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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<Expr, unsigned> variables;
vector<string> info_tags;
AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
if (assert) {
- assertions.push_back(engine.simplify(assert->getExpr()));
+ assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr()));
delete cmd;
continue;
}
/*! \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.
#include <unordered_map>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "options/language.h"
#include "options/options.h"
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<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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 == "<stdin>") parserBuilder.withStreamInput(cin);
Parser* parser = parserBuilder.build();
/*! \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.
#include <getopt.h>
#include <iostream>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
#include "options/language.h"
Options opts;
opts.setInputLanguage(fromLang);
ExprManager exprMgr(opts);
- ParserBuilder parserBuilder(&exprMgr, filename, opts);
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(new api::Solver(&opts));
+ ParserBuilder parserBuilder(solver.get(), filename, opts);
if(!strcmp(filename, "-")) {
parserBuilder.withFilename("<stdin>");
parserBuilder.withLineBufferedStreamInput(cin);
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();
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();
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();
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();
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)
{
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)
{
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();
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();
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)
{
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() {}
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
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.
*/
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
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.
*/
*/
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
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.
*/
*/
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
*/
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.
*/
*/
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
*/
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
*/
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
*/
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.
*/
*/
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
*/
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.
*/
*/
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
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.
*/
*/
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
*/
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;
#include <iterator>
#include <sstream>
+#include "api/cvc4cpp.h"
#include "base/exception.h"
#include "base/output.h"
#include "expr/expr_iomanip.h"
}
}
-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() {
}
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;
}
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() ) {
// 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();
}
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);
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);
/*! \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.
class CVC4_PUBLIC Proof {};
class CVC4_PUBLIC Theorem {};
+namespace api {
+class CVC4_PUBLIC Solver;
+}
using CVC4::InputLanguage;
using CVC4::Integer;
using CVC4::Rational;
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;
#include <string>
#include <vector>
+#include "api/cvc4cpp.h"
#include "main/main.h"
#include "smt/command.h"
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;
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)
/*! \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.
#include "util/statistics_registry.h"
namespace CVC4 {
+
+namespace api {
+class Solver;
+}
+
namespace main {
class CommandExecutor {
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;
+ }
}
/**
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);
// 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"
(*(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);
}
}
// 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 ) {
delete cmd;
}
#endif /* PORTFOLIO_BUILD */
- InteractiveShell shell(*exprMgr);
+ InteractiveShell shell(solver.get());
if(opts.getInteractivePrompt()) {
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
// 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)
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)
// need to be around in that case for main() to print statistics.
delete pTotalTime;
delete pExecutor;
- delete exprMgr;
pTotalTime = NULL;
pExecutor = NULL;
# 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"
#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()) {
namespace CVC4 {
class Command;
-class ExprManager;
class Options;
+namespace api {
+class Solver;
+}
+
namespace parser {
class Parser;
}/* CVC4::parser namespace */
static const unsigned s_historyLimit = 500;
public:
- InteractiveShell(ExprManager& exprManager);
+ InteractiveShell(api::Solver* solver);
/**
* Close out the interactive session.
class Command;
class Expr;
-class ExprManager;
namespace parser {
#include <sstream>
#include <unordered_set>
+#include "api/cvc4cpp.h"
#include "base/output.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
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),
d_parseOnly(parseOnly),
d_canIncludeFile(true),
d_logicIsForced(false),
- d_forcedLogic() {
+ d_forcedLogic()
+{
d_input->setParser(*this);
}
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));
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;
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;
}
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;
}
}
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,
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;
}
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;
}
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);
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());
// 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();
{
return range;
}
- return d_exprManager->mkFunctionType(sorts, range);
+ return getExprManager()->mkFunctionType(sorts, range);
}
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;
}
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;
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;
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()) {
#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 {
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 {
/*! \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.
#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"
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;
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 ) {
return *this;
}
-ParserBuilder& ParserBuilder::withExprManager(ExprManager* exprManager) {
- d_exprManager = exprManager;
+ParserBuilder& ParserBuilder::withSolver(api::Solver* solver)
+{
+ d_solver = solver;
return *this;
}
/*! \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.
namespace CVC4 {
-class ExprManager;
class Options;
+namespace api {
+class Solver;
+}
+
namespace parser {
class Parser;
/** 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;
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. */
/** 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();
#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 {
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);
addOperator(kind::NOT);
addOperator(kind::OR);
addOperator(kind::XOR);
-
}
void Smt1::addArithmeticOperators() {
/*! \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.
class SExpr;
+namespace api {
+class Solver;
+}
+
namespace parser {
class Smt1 : public Parser {
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:
/**
**/
#include "parser/smt2/smt2.h"
+#include "api/cvc4cpp.h"
#include "expr/type.h"
#include "options/options.h"
#include "parser/antlr_input.h"
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);
}
}
class SExpr;
+namespace api {
+class Solver;
+}
+
namespace parser {
class Smt2 : public Parser {
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:
/**
#include <algorithm>
#include <set>
+#include "api/cvc4cpp.h"
#include "expr/type.h"
#include "parser/parser.h"
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 */
#include "util/hash.h"
namespace CVC4 {
+
+namespace api {
+class Solver;
+}
+
namespace parser {
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:
/*! \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.
#include <sstream>
#include <string>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
#include "options/set_language.h"
int runTest() {
- ExprManager em;
- psr =
- ParserBuilder(&em, "internal-buffer")
- .withStringInput(declarations)
- .withInputLanguage(input::LANG_SMTLIB_V2)
- .build();
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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
/*! \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.
#include <iostream>
#include <sstream>
+#include "api/cvc4cpp.h"
#include "expr/expr_manager.h"
#include "options/options.h"
#include "options/set_language.h"
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<api::Solver> solver =
+ std::unique_ptr<api::Solver>(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(), "<internal>",
- smt.getExprManager()->getOptions());
+void testGetInfo(api::Solver* solver, const char* s)
+{
+ ParserBuilder pb(
+ solver, "<internal>", 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;
/*! \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.
#include <vector>
#include <sstream>
+#include "api/cvc4cpp.h"
#include "expr/expr_manager.h"
#include "main/interactive_shell.h"
#include "options/base_options.h"
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... */
}
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();
}
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<api::Solver> 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);
+ }
};
/*! \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.
#include <cxxtest/TestSuite.h>
#include <sstream>
+#include "api/cvc4cpp.h"
#include "base/output.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
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)
TS_ASSERT_THROWS(
{
Command* cmd;
- while ((cmd = parser->nextCommand()) != NULL) {
+ while ((cmd = parser->nextCommand()) != NULL)
+ {
Debug("parser") << "Parsed command: " << (*cmd) << endl;
delete cmd;
}
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
* 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<api::Solver> d_solver;
+
+}; /* class ParserBlack */
class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
/*! \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.
#include <fstream>
#include <iostream>
+#include "api/cvc4cpp.h"
#include "options/language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
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);
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<api::Solver> d_solver;
}; // class ParserBuilderBlack
projects / cvc5.git / commitdiff