summaryrefslogtreecommitdiff
path: root/examples/api
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-04-05 19:31:28 -0700
committerGitHub <noreply@github.com>2021-04-05 19:31:28 -0700
commitd2e454e0dfc06e16fe0a4228168b21cf1311fc35 (patch)
tree65063161aa9e21348182b13251524c58b0ca49c5 /examples/api
parent00a20b53ce998f52b18303a7a680e6a00acc098c (diff)
New C++ Api: Rename and move headers. (#6292)
Diffstat (limited to 'examples/api')
-rw-r--r--examples/api/bitvectors.cpp4
-rw-r--r--examples/api/bitvectors_and_arrays.cpp6
-rw-r--r--examples/api/combination.cpp4
-rw-r--r--examples/api/datatypes.cpp4
-rw-r--r--examples/api/extract.cpp4
-rw-r--r--examples/api/helloworld.cpp4
-rw-r--r--examples/api/linear_arith.cpp2
-rw-r--r--examples/api/sequences.cpp2
-rw-r--r--examples/api/sets.cpp4
-rw-r--r--examples/api/strings.cpp4
-rw-r--r--examples/api/sygus-fun.cpp2
-rw-r--r--examples/api/sygus-grammar.cpp2
-rw-r--r--examples/api/sygus-inv.cpp2
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>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback