diff options
Diffstat (limited to 'examples/sets-translate/sets_translate.cpp')
-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; |