diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-05 19:31:28 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-05 19:31:28 -0700 |
commit | d2e454e0dfc06e16fe0a4228168b21cf1311fc35 (patch) | |
tree | 65063161aa9e21348182b13251524c58b0ca49c5 /examples/api | |
parent | 00a20b53ce998f52b18303a7a680e6a00acc098c (diff) |
New C++ Api: Rename and move headers. (#6292)
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors.cpp | 4 | ||||
-rw-r--r-- | examples/api/bitvectors_and_arrays.cpp | 6 | ||||
-rw-r--r-- | examples/api/combination.cpp | 4 | ||||
-rw-r--r-- | examples/api/datatypes.cpp | 4 | ||||
-rw-r--r-- | examples/api/extract.cpp | 4 | ||||
-rw-r--r-- | examples/api/helloworld.cpp | 4 | ||||
-rw-r--r-- | examples/api/linear_arith.cpp | 2 | ||||
-rw-r--r-- | examples/api/sequences.cpp | 2 | ||||
-rw-r--r-- | examples/api/sets.cpp | 4 | ||||
-rw-r--r-- | examples/api/strings.cpp | 4 | ||||
-rw-r--r-- | examples/api/sygus-fun.cpp | 2 | ||||
-rw-r--r-- | examples/api/sygus-grammar.cpp | 2 | ||||
-rw-r--r-- | examples/api/sygus-inv.cpp | 2 |
13 files changed, 22 insertions, 22 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> |