diff options
author | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
commit | 5f207ba01302c3245e169bfbe2ed91ad0cd659cd (patch) | |
tree | e1131e8c2891e283ab028fba6a7a677bb4ac9f5f /examples/sets-translate | |
parent | 7e4468ba0aa0b08eeb4ba1a86b1fdd839ae169d6 (diff) |
Modifying emptyset.h and sexpr. Adding SetLanguage.
- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.
Diffstat (limited to 'examples/sets-translate')
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index c33ccb367..7e17e68f4 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -23,7 +23,9 @@ #include <vector> #include "expr/expr.h" +#include "options/language.h" #include "options/options.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt_util/command.h" @@ -34,7 +36,7 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::options; -bool nonsense(char c) { return !isalnum(c); } +bool nonsense(char c) { return !isalnum(c); } #ifdef ENABLE_AXIOMS const bool enableAxioms = true; @@ -94,7 +96,7 @@ class Mapper { Type elementType = t.getElementType(); ostringstream oss_type; - oss_type << Expr::setlanguage(language::output::LANG_SMTLIB_V2) + oss_type << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType; string elementTypeAsString = oss_type.str(); elementTypeAsString.erase( @@ -103,7 +105,7 @@ class Mapper { // define-sort ostringstream oss_name; - oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2) + oss_name << language::SetLanguage(language::output::LANG_SMTLIB_V2) << "(Set " << elementType << ")"; string name = oss_name.str(); Type newt = em->mkArrayType(t.getElementType(), em->booleanType()); @@ -184,7 +186,8 @@ class Mapper { int N = sizeof(setaxioms) / sizeof(setaxioms[0]); for(int i = 0; i < N; ++i) { string s = setaxioms[i]; - ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType; + ostringstream oss; + oss << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType; boost::replace_all(s, "HOLDA", elementTypeAsString); boost::replace_all(s, "HOLDB", oss.str()); if( s == "" ) continue; @@ -207,7 +210,7 @@ class Mapper { public: Mapper(ExprManager* e) : em(e),depth(0) { - sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + sout << language::SetLanguage(language::output::LANG_SMTLIB_V2); } void defineSetSort() { @@ -259,17 +262,17 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.set(inputLanguage, language::input::LANG_SMTLIB_V2); - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); // cout << Expr::dag(0); ExprManager exprManager(options); Mapper m(&exprManager); - + // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); if(input == "<stdin>") parserBuilder.withStreamInput(cin); Parser* parser = parserBuilder.build(); - + // Variables and assertions vector<string> variables; vector<string> info_tags; |