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 | |
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')
-rw-r--r-- | examples/api/sets.cpp | 5 | ||||
-rw-r--r-- | examples/api/strings.cpp | 5 | ||||
-rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 14 | ||||
-rw-r--r-- | examples/hashsmt/sha1_inversion.cpp | 16 | ||||
-rw-r--r-- | examples/nra-translate/normalize.cpp | 16 | ||||
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 19 | ||||
-rw-r--r-- | examples/translator.cpp | 3 |
7 files changed, 41 insertions, 37 deletions
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 7390eefe0..68de230fe 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -18,6 +18,7 @@ //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed #include "smt/smt_engine.h" +#include "options/set_language.h" using namespace std; using namespace CVC4; @@ -34,8 +35,8 @@ int main() { smt.setOption("produce-models", true); // Set output language to SMTLIB2 - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); - + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + Type integer = em.integerType(); Type set = em.mkSetType(integer); diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 14ab0e64d..2e5d467d3 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -18,6 +18,7 @@ //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed #include "smt/smt_engine.h" +#include "options/set_language.h" using namespace CVC4; @@ -35,8 +36,8 @@ int main() { smt.setOption("strings-exp", true); // Set output language to SMTLIB2 - std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); - + std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + // String type Type string = em.stringType(); diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index e23be29bf..9ed4424ba 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -22,16 +22,17 @@ * Author: dejan */ -#include <string> +#include <boost/uuid/sha1.hpp> #include <fstream> #include <iostream> #include <sstream> +#include <string> -#include "word.h" +#include "options/language.h" +#include "options/set_language.h" #include "sha1.hpp" #include "smt_util/command.h" - -#include <boost/uuid/sha1.hpp> +#include "word.h" using namespace std; using namespace CVC4; @@ -69,7 +70,7 @@ int main(int argc, char* argv[]) { // The output ofstream output(argv[3]); - output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); output << SetBenchmarkLogicCommand("QF_BV") << endl; output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl; @@ -103,6 +104,3 @@ int main(int argc, char* argv[]) { cerr << e << endl; } } - - - diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index fadc6ecb9..15c7d8728 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -22,16 +22,17 @@ * Author: dejan */ -#include <string> +#include <boost/uuid/sha1.hpp> #include <fstream> #include <iostream> #include <sstream> +#include <string> -#include "word.h" +#include "options/language.h" +#include "options/set_language.h" #include "sha1.hpp" #include "smt_util/command.h" - -#include <boost/uuid/sha1.hpp> +#include "word.h" using namespace std; using namespace CVC4; @@ -50,7 +51,7 @@ int main(int argc, char* argv[]) { string msg = argv[1]; unsigned msgSize = msg.size(); ofstream output(argv[2]); - output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); output << SetBenchmarkLogicCommand("QF_BV") << endl; output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl; @@ -58,7 +59,7 @@ int main(int argc, char* argv[]) { hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize]; for (unsigned i = 0; i < msgSize; ++ i) { stringstream ss; - ss << "x" << i; + ss << "x" << i; cvc4input[i] = hashsmt::cvc4_uchar8(ss.str()); output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; @@ -102,6 +103,3 @@ int main(int argc, char* argv[]) { cerr << e << endl; } } - - - diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index d4aecbba9..db76390a7 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.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/smt_engine.h" @@ -35,18 +37,19 @@ using namespace CVC4::parser; using namespace CVC4::options; using namespace CVC4::theory; -int main(int argc, char* argv[]) +int main(int argc, char* argv[]) { - // Get the filename + // Get the filename string input(argv[1]); // Create the expression manager Options options; options.set(inputLanguage, language::input::LANG_SMTLIB_V2); ExprManager exprManager(options); - - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1); + + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2) + << Expr::setdepth(-1); // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); @@ -76,12 +79,11 @@ int main(int argc, char* argv[]) } cout << *cmd << endl; - delete cmd; + delete cmd; } cout << "(check-sat)" << endl; - + // Get rid of the parser delete parser; } - 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; diff --git a/examples/translator.cpp b/examples/translator.cpp index 522d88573..7d5e912e7 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -24,6 +24,7 @@ #include "expr/expr.h" #include "options/language.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" @@ -97,7 +98,7 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag toLang = toOutputLanguage(fromLang); } - *out << Expr::setlanguage(toLang); + *out << language::SetLanguage(toLang); Options opts; opts.set(options::inputLanguage, fromLang); |