diff options
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/datatypes.cpp | 2 | ||||
-rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 2 | ||||
-rw-r--r-- | examples/hashsmt/sha1_inversion.cpp | 2 | ||||
-rw-r--r-- | examples/nra-translate/normalize.cpp | 11 | ||||
-rw-r--r-- | examples/nra-translate/smt2info.cpp | 9 | ||||
-rw-r--r-- | examples/nra-translate/smt2todreal.cpp | 10 | ||||
-rw-r--r-- | examples/nra-translate/smt2toisat.cpp | 11 | ||||
-rw-r--r-- | examples/nra-translate/smt2tomathematica.cpp | 11 | ||||
-rw-r--r-- | examples/nra-translate/smt2toqepcad.cpp | 10 | ||||
-rw-r--r-- | examples/nra-translate/smt2toredlog.cpp | 11 | ||||
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 13 | ||||
-rw-r--r-- | examples/translator.cpp | 17 |
12 files changed, 52 insertions, 57 deletions
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 463cf9534..3da8cfa4a 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -15,8 +15,8 @@ **/ #include <iostream> +#include "options/language.h" // for use with make examples #include "smt/smt_engine.h" // for use with make examples -#include "util/language.h" // for use with make examples //#include <cvc4/cvc4.h> // To follow the wiki using namespace CVC4; diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index ad3705a94..e23be29bf 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -29,7 +29,7 @@ #include "word.h" #include "sha1.hpp" -#include "expr/command.h" +#include "smt_util/command.h" #include <boost/uuid/sha1.hpp> diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 51267ba06..fadc6ecb9 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -29,7 +29,7 @@ #include "word.h" #include "sha1.hpp" -#include "expr/command.h" +#include "smt_util/command.h" #include <boost/uuid/sha1.hpp> diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 2dd450c4e..d4aecbba9 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index a2c12f05d..d59f9f4c4 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -15,18 +15,17 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 4413c480a..97c5c5d04 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -15,19 +15,19 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index eae77e1ce..9c94cdd43 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 3158243a5..86aaf786f 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -15,19 +15,18 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index cb4855a38..058fa8e0d 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -15,18 +15,18 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 71d7229af..1ebd6ea59 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include <string> +#include <cassert> #include <iostream> +#include <map> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <map> - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index acf0fcafe..c33ccb367 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include <string> +#include <boost/algorithm/string.hpp> // include Boost, a C++ library +#include <cassert> #include <iostream> +#include <string> #include <typeinfo> -#include <cassert> #include <vector> -#include <boost/algorithm/string.hpp> // include Boost, a C++ library - -#include "options/options.h" #include "expr/expr.h" -#include "theory/logic_info.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" +#include "theory/logic_info.h" using namespace std; using namespace CVC4; diff --git a/examples/translator.cpp b/examples/translator.cpp index 7aa969e06..522d88573 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -15,18 +15,19 @@ ** CVC4's input languages to one of its output languages. **/ -#include <iostream> +#include <cerrno> +#include <cstdlib> +#include <cstring> #include <fstream> #include <getopt.h> -#include <cstring> -#include <cstdlib> -#include <cerrno> -#include "smt/smt_engine.h" -#include "util/language.h" -#include "expr/command.h" +#include <iostream> + #include "expr/expr.h" -#include "parser/parser_builder.h" +#include "options/language.h" #include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; |