Use separate CMake project for CVC4 examples. (#3196)

8 files changed, 19 insertions, 53 deletions

diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
index b719ac2a4..e83825e24 100644
--- a/examples/nra-translate/CMakeLists.txt
+++ b/examples/nra-translate/CMakeLists.txt
@@ -10,10 +10,8 @@ set(CVC4_EXAMPLES_NRA_TRANSLATE
   smt2toredlog
 )
 
-set(EXAMPLES_NRA_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
 foreach(example ${CVC4_EXAMPLES_NRA_TRANSLATE})
-  cvc4_add_example(${example}
-    "" "${EXAMPLES_NRA_TRANSLATE_LINK_LIBS}" "nra-translate"
+  cvc4_add_example(${example} "" "nra-translate"
     # arguments to binary (for testing)
     # input file is required by all tests
     ${CMAKE_CURRENT_SOURCE_DIR}/nra-translate-example-input.smt2
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index 3ca09c5bf..2ad1ea84e 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -22,16 +22,10 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/options.h"
-#include "options/set_language.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/smt_engine.h"
+#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 CVC4;
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index 513b52a39..dfbde05f5 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -21,12 +21,8 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 11f5ad4f8..8ea3cf862 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -22,14 +22,10 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/smt_engine.h"
+#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 CVC4;
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 5992cd0dc..34745ad03 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -22,13 +22,8 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/smt_engine.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index 8f0764e92..c5c2f3af4 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -22,12 +22,8 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index 28e699b6f..cdc2e0878 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -22,12 +22,8 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 0629b5d1c..654a6a038 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -22,13 +22,8 @@
 #include <typeinfo>
 #include <vector>
 
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/smt_engine.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
 
 using namespace std;
 using namespace CVC4;