summaryrefslogtreecommitdiff
path: root/examples/nra-translate
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/nra-translate
parent00a20b53ce998f52b18303a7a680e6a00acc098c (diff)
New C++ Api: Rename and move headers. (#6292)
Diffstat (limited to 'examples/nra-translate')
-rw-r--r--examples/nra-translate/normalize.cpp9
-rw-r--r--examples/nra-translate/smt2info.cpp5
-rw-r--r--examples/nra-translate/smt2todreal.cpp9
-rw-r--r--examples/nra-translate/smt2toisat.cpp5
-rw-r--r--examples/nra-translate/smt2tomathematica.cpp5
-rw-r--r--examples/nra-translate/smt2toqepcad.cpp5
-rw-r--r--examples/nra-translate/smt2toredlog.cpp5
7 files changed, 18 insertions, 25 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback