diff options
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; } } - - - |