diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-04 06:25:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-04 06:25:36 +0000 |
commit | 070b3f89d4bc9940fb87e86108152144b187c891 (patch) | |
tree | e3df02ffccc39cc9dd6bf4a9e3b17187c02fb9dc /src | |
parent | 4c5a38bef4d9daefef4531e6148b4314c049d505 (diff) |
compat layer cleanup
Diffstat (limited to 'src')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 96 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 3 | ||||
-rw-r--r-- | src/parser/parser.h | 3 |
3 files changed, 56 insertions, 46 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 6db6b440e..7b748a2d3 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -680,6 +680,7 @@ ValidityChecker::ValidityChecker() : setUpOptions(d_options, *d_clflags); d_em = new CVC4::ExprManager(d_options); d_smt = new CVC4::SmtEngine(d_em); + d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::ValidityChecker(const CLFlags& clflags) : @@ -688,9 +689,11 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) : setUpOptions(d_options, *d_clflags); d_em = new CVC4::ExprManager(d_options); d_smt = new CVC4::SmtEngine(d_em); + d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::~ValidityChecker() { + delete d_parserContext; delete d_clflags; } @@ -948,11 +951,11 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Subranges not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::tupleType(const Type& type0, const Type& type1) { @@ -977,23 +980,23 @@ Type ValidityChecker::tupleType(const std::vector<Type>& types) { } Type ValidityChecker::recordType(const std::string& field, const Type& type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1, const std::string& field2, const Type& type2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::vector<std::string>& fields, const std::vector<Type>& types) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::dataType(const std::string& name, @@ -1042,11 +1045,11 @@ Type ValidityChecker::createType(const std::string& typeName) { } Type ValidityChecker::createType(const std::string& typeName, const Type& def) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + d_parserContext->defineType(typeName, def); } Type ValidityChecker::lookupType(const std::string& typeName) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_parserContext->getSort(typeName); } ExprManager* ValidityChecker::getEM() { @@ -1054,16 +1057,17 @@ ExprManager* ValidityChecker::getEM() { } Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { - return d_em->mkVar(name, type); + return d_parserContext->mkVar(name, type); } Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + FatalAssert(def.getType() == type, "expected types to match"); + d_parserContext->defineVar(name, def); } Expr ValidityChecker::lookupVar(const std::string& name, Type* type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_parserContext->getVariable(name); } Type ValidityChecker::getType(const Expr& e) { @@ -1138,7 +1142,7 @@ void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { } Expr ValidityChecker::parseExpr(const Expr& e) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return e; } Type ValidityChecker::parseType(const Expr& e) { @@ -1167,14 +1171,11 @@ Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) { } CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "<internal>").withStringInput(s).withInputLanguage(lang).build(); - Expr dummy = p->nextExpression(); - if( dummy.isNull() ) { + p->useDeclarationsFrom(d_parserContext); + Expr e = p->nextExpression(); + if( e.isNull() ) { throw CVC4::parser::ParserException("Parser result is null: '" + s + "'"); } - //DebugAssert(dummy.getKind() == RAW_LIST, "Expected list expression"); - //DebugAssert(dummy.arity() == 2, "Expected two children"); - - Expr e = parseExpr(dummy[1]); delete p; @@ -1237,7 +1238,7 @@ Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { } Op ValidityChecker::createOp(const std::string& name, const Type& type) { - return d_em->mkVar(name, type); + return d_parserContext->mkVar(name, type); } Op ValidityChecker::createOp(const std::string& name, const Type& type, @@ -1246,7 +1247,9 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type, } Op ValidityChecker::lookupOp(const std::string& name, Type* type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Op op = d_parserContext->getFunction(name); + *type = op.getType(); + return op; } Expr ValidityChecker::funExpr(const Op& op, const Expr& child) { @@ -1333,32 +1336,32 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1, const std::string& field2, const Expr& expr2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields, const std::vector<Expr>& exprs) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, const Expr& newValue) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) { @@ -1657,12 +1660,12 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { @@ -1679,50 +1682,50 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid, const Type& type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, const Expr& trigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, const std::vector<Expr>& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body, const std::vector<std::vector<Expr> >& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTriggers(const Expr& e, const std::vector<Expr>& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::existsExpr(const std::vector<Expr>& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Op ValidityChecker::lambdaExpr(const std::vector<Expr>& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Lambda expressions not supported by CVC4 yet (sorry!)"); } Op ValidityChecker::transClosure(const Op& op) { @@ -1951,9 +1954,10 @@ void ValidityChecker::loadFile(const std::string& fileName, opts.interactive = interactive; opts.interactiveSetByUser = true; CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); - CVC4::parser::Parser* parser = parserBuilder.build(); - doCommands(parser, d_smt, opts); - delete parser; + CVC4::parser::Parser* p = parserBuilder.build(); + p->useDeclarationsFrom(d_parserContext); + doCommands(p, d_smt, opts); + delete p; } void ValidityChecker::loadFile(std::istream& is, @@ -1964,9 +1968,11 @@ void ValidityChecker::loadFile(std::istream& is, opts.interactive = interactive; opts.interactiveSetByUser = true; CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); - CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build(); - doCommands(parser, d_smt, opts); - delete parser; + CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); + d_parserContext = p; + p->useDeclarationsFrom(d_parserContext); + doCommands(p, d_smt, opts); + delete p; } Statistics& ValidityChecker::getStatistics() { diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index b4c9cba3e..1e4511ba5 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -60,6 +60,8 @@ #include "util/exception.h" #include "util/hash.h" +#include "parser/parser.h" + #include <stdlib.h> #include <map> #include <utility> @@ -462,6 +464,7 @@ class CVC4_PUBLIC ValidityChecker { CVC4::Options d_options; CVC4::ExprManager* d_em; CVC4::SmtEngine* d_smt; + CVC4::parser::Parser* d_parserContext; ValidityChecker(const CLFlags& clflags); diff --git a/src/parser/parser.h b/src/parser/parser.h index 46544559a..70bd45c31 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -473,7 +473,8 @@ public: * This feature is useful when e.g. reading out-of-band expression data: * 1. Parsing --replay log files produced with --replay-log. * 2. Perhaps a multi-query benchmark file is being single-stepped - * with intervening queries on stdin that must reference + * with intervening queries on stdin that must reference the same + * declaration scope(s). * * However, the feature must be used carefully. Pushes and pops * should be performed with the correct current declaration scope. |