diff options
Diffstat (limited to 'examples')
24 files changed, 51 insertions, 60 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 043bbf8aa..be9557c99 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -14,9 +14,9 @@ ** **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace std; using namespace cvc5::api; diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 2bca1eb4c..ca9869503 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -14,10 +14,10 @@ ** **/ -#include <iostream> -#include <cmath> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <cmath> +#include <iostream> using namespace std; using namespace cvc5::api; diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 9ea2f55ed..82c2978e6 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -16,9 +16,9 @@ ** The model is displayed using getValue(). **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace std; using namespace cvc5::api; diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 49253e466..f9a1484da 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -14,9 +14,9 @@ ** An example of using inductive datatypes in CVC4. **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace cvc5::api; diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index 760f5d0fe..d2f631d25 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -14,9 +14,9 @@ ** **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace std; using namespace cvc5::api; diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 092e2a79a..b5881f312 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -14,9 +14,9 @@ ** A very simple CVC4 tutorial example. **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace cvc5::api; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index b56982daa..ee9663455 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -17,7 +17,7 @@ #include <iostream> -#include "cvc4/api/cvc4cpp.h" +#include <cvc5/cvc5.h> using namespace std; using namespace cvc5::api; diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 3498b3275..39117c090 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -14,7 +14,7 @@ ** A simple demonstration of reasoning about sequences with CVC4 via C++ API. **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 59385896c..c8b8bcc9e 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -14,9 +14,9 @@ ** A simple demonstration of reasoning about sets with CVC4. **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace std; using namespace cvc5::api; diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 53352d266..548d25b81 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -14,9 +14,9 @@ ** A simple demonstration of reasoning about strings with CVC4 via C++ API. **/ -#include <iostream> +#include <cvc5/cvc5.h> -#include <cvc4/api/cvc4cpp.h> +#include <iostream> using namespace cvc5::api; diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index be4d3e8d5..44e276ddc 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -45,7 +45,7 @@ ** (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 61b00f6de..441cfa30c 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -42,7 +42,7 @@ ** (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 56b5a0aaa..5d6789759 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -33,7 +33,7 @@ ** (define-fun inv-f ((x Int)) Bool (not (>= x 11))) **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index ba495e1fd..635c369a0 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -15,6 +15,10 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> +#include <cvc4/expr/expr_iomanip.h> +#include <cvc4/options/set_language.h> + #include <cassert> #include <iostream> #include <map> @@ -22,11 +26,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/set_language.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 1eb4b3d4d..413601769 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -15,15 +15,14 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> + #include <cassert> #include <iostream> #include <string> #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 8139a4d91..62a1f4b5e 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -15,6 +15,10 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> +#include <cvc4/expr/expr_iomanip.h> +#include <cvc4/options/set_language.h> + #include <cassert> #include <iostream> #include <map> @@ -22,11 +26,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/set_language.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 09b0c69d8..5898e5cff 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> + #include <cassert> #include <iostream> #include <map> @@ -22,9 +24,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 6cb51f17c..b2c73d48e 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> + #include <cassert> #include <iostream> #include <map> @@ -22,9 +24,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index afd468d5d..760a7024c 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> + #include <cassert> #include <iostream> #include <map> @@ -22,9 +24,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index d9bd6012a..dd6fb9bb6 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include <cvc5/cvc5.h> + #include <cassert> #include <iostream> #include <map> @@ -22,9 +24,6 @@ #include <typeinfo> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index ec95b5f70..0f924072c 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -15,7 +15,10 @@ ** \todo document this file **/ -#include <boost/algorithm/string.hpp> // include Boost, a C++ library +#include <cvc5/cvc5.h> +#include <cvc4/options/set_language.h> + +#include <boost/algorithm/string.hpp> // include Boost, a C++ library #include <cassert> #include <iostream> #include <string> @@ -23,10 +26,6 @@ #include <unordered_map> #include <vector> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> -#include <cvc4/options/set_language.h> - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index b97b86bb8..4042e15cb 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -16,7 +16,7 @@ ** identical. **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 73dbfe34f..3d6a6e103 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -14,7 +14,7 @@ ** A simple demonstration of the C++ interface for quantifiers. **/ -#include <cvc4/api/cvc4cpp.h> +#include <cvc5/cvc5.h> #include <iostream> diff --git a/examples/translator.cpp b/examples/translator.cpp index 4838e06fb..bcdf2b2d2 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -15,18 +15,17 @@ ** CVC4's input languages to one of its output languages. **/ +#include <cvc5/cvc5.h> +#include <cvc4/expr/expr_iomanip.h> +#include <cvc4/options/set_language.h> +#include <getopt.h> + #include <cerrno> #include <cstdlib> #include <cstring> #include <fstream> -#include <getopt.h> #include <iostream> -#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/set_language.h> - using namespace std; using namespace cvc5; using namespace cvc5::language; |