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/hashsmt | |
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/hashsmt')
-rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 14 | ||||
-rw-r--r-- | examples/hashsmt/sha1_inversion.cpp | 16 |
2 files changed, 13 insertions, 17 deletions
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; } } - - - |