summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2019-09-25 09:47:12 -0700
committerGitHub <noreply@github.com>2019-09-25 09:47:12 -0700
commit4f384b6fadd999324d83b4c4ea900de2a0e13dd7 (patch)
treed62683a66ede8c7a0ee04e8b67ee999aa71342ea
parentf892370a615ecadc011b49a98d2c4695fafa7f4f (diff)
Use separate CMake project for CVC4 examples. (#3196)
-rw-r--r--.travis.yml10
-rw-r--r--CMakeLists.txt18
-rw-r--r--cmake/CVC4Config.cmake.in5
-rw-r--r--examples/CMakeLists.txt96
-rw-r--r--examples/README.md (renamed from examples/README)45
-rw-r--r--examples/SimpleVC.java12
-rw-r--r--examples/api/CMakeLists.txt8
-rw-r--r--examples/api/bitvectors-new.cpp3
-rw-r--r--examples/api/bitvectors.cpp3
-rw-r--r--examples/api/bitvectors_and_arrays-new.cpp3
-rw-r--r--examples/api/bitvectors_and_arrays.cpp4
-rw-r--r--examples/api/combination-new.cpp3
-rw-r--r--examples/api/combination.cpp3
-rw-r--r--examples/api/datatypes-new.cpp3
-rw-r--r--examples/api/datatypes.cpp5
-rw-r--r--examples/api/extract-new.cpp3
-rw-r--r--examples/api/extract.cpp3
-rw-r--r--examples/api/helloworld-new.cpp3
-rw-r--r--examples/api/helloworld.cpp3
-rw-r--r--examples/api/java/CMakeLists.txt26
-rw-r--r--examples/api/linear_arith-new.cpp3
-rw-r--r--examples/api/linear_arith.cpp3
-rw-r--r--examples/api/sets-new.cpp3
-rw-r--r--examples/api/sets.cpp5
-rw-r--r--examples/api/strings-new.cpp3
-rw-r--r--examples/api/strings.cpp5
-rw-r--r--examples/hashsmt/CMakeLists.txt14
-rw-r--r--examples/hashsmt/sha1_collision.cpp7
-rw-r--r--examples/hashsmt/sha1_inversion.cpp8
-rw-r--r--examples/hashsmt/word.cpp8
-rw-r--r--examples/hashsmt/word.h4
-rw-r--r--examples/nra-translate/CMakeLists.txt4
-rw-r--r--examples/nra-translate/normalize.cpp14
-rw-r--r--examples/nra-translate/smt2info.cpp8
-rw-r--r--examples/nra-translate/smt2todreal.cpp12
-rw-r--r--examples/nra-translate/smt2toisat.cpp9
-rw-r--r--examples/nra-translate/smt2tomathematica.cpp8
-rw-r--r--examples/nra-translate/smt2toqepcad.cpp8
-rw-r--r--examples/nra-translate/smt2toredlog.cpp9
-rw-r--r--examples/sets-translate/CMakeLists.txt5
-rw-r--r--examples/sets-translate/sets_translate.cpp12
-rw-r--r--examples/simple_vc_cxx.cpp3
-rw-r--r--examples/simple_vc_quant_cxx.cpp3
-rw-r--r--examples/translator.cpp14
-rw-r--r--src/CMakeLists.txt30
-rw-r--r--src/bindings/java/CMakeLists.txt11
-rw-r--r--src/main/CMakeLists.txt7
-rw-r--r--src/parser/CMakeLists.txt2
-rw-r--r--test/CMakeLists.txt3
49 files changed, 211 insertions, 273 deletions
diff --git a/.travis.yml b/.travis.yml
index d4de3576c..64dd17c75 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -59,7 +59,13 @@ script:
makeCheck() {
cd build
make -j2 check ARGS='-LE regress[1-4]' CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED"
- ctest -j2 -L example || error "RUNNING EXAMPLES FAILED"
+ }
+ makeExamples() {
+ cd examples
+ mkdir build
+ cd build
+ cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake
+ ctest -j2 --output-on-failure || error "RUNNING EXAMPLES FAILED"
}
makeInstallCheck() {
cd build
@@ -78,7 +84,7 @@ script:
[ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker
[ -n "$TRAVIS_CVC4" ] && run configureCVC4
[ -n "$TRAVIS_CVC4" ] && run makeCheck
- [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck
+ [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck && run makeExamples
[ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration"
echo "travis_fold:end:load_script"
- echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}"
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b6bc5b452..706ef51f2 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -31,6 +31,14 @@ set(CMAKE_CXX_STANDARD 11)
# plugins.
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+#-----------------------------------------------------------------------------#
+
+set(INCLUDE_INSTALL_DIR include)
+set(LIBRARY_INSTALL_DIR lib)
+set(RUNTIME_INSTALL_DIR bin)
+
+#-----------------------------------------------------------------------------#
+
# Embed the installation prefix as an RPATH in the executable such that the
# linker can find our libraries (such as libcvc4parser) when executing the cvc4
# binary. This is for example useful when installing CVC4 with a custom prefix
@@ -40,7 +48,7 @@ set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
#
# More information on RPATH in CMake:
# https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
-set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
+set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${LIBRARY_INSTALL_DIR}")
#-----------------------------------------------------------------------------#
@@ -450,7 +458,6 @@ if(ENABLE_PROOFS)
endif()
add_subdirectory(doc)
-add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
add_subdirectory(src)
add_subdirectory(test)
@@ -468,12 +475,13 @@ include(CMakePackageConfigHelpers)
install(EXPORT cvc4-targets
FILE CVC4Targets.cmake
NAMESPACE CVC4::
- DESTINATION lib/cmake/CVC4)
+ DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4)
configure_package_config_file(
${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in
${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
- INSTALL_DESTINATION lib/cmake/CVC4
+ INSTALL_DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
+ PATH_VARS LIBRARY_INSTALL_DIR
)
write_basic_package_version_file(
@@ -485,7 +493,7 @@ write_basic_package_version_file(
install(FILES
${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
- DESTINATION lib/cmake/CVC4
+ DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
)
diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index f2eec75c6..86fbffff5 100644
--- a/cmake/CVC4Config.cmake.in
+++ b/cmake/CVC4Config.cmake.in
@@ -3,3 +3,8 @@
if(NOT TARGET CVC4::cvc4)
include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)
endif()
+
+if(NOT TARGET CVC4::cvc4jar)
+ set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@")
+ include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake)
+endif()
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index f81c68236..43f4109a3 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -1,40 +1,30 @@
-include_directories(${PROJECT_SOURCE_DIR}/src)
-include_directories(${PROJECT_SOURCE_DIR}/src/include)
-include_directories(${CMAKE_BINARY_DIR}/src)
+cmake_minimum_required(VERSION 3.2)
+
+project(cvc4-examples)
+
+enable_testing()
+
+# Find CVC4 package. If CVC4 is not installed into the default system location
+# use `cmake .. -DCMAKE_PREFIX_PATH=path/to/lib/cmake` to specify the location
+# of CVC4Config.cmake.
+find_package(CVC4)
# Some of the examples require boost. Enable these examples if boost is
# installed.
find_package(Boost 1.50.0)
-set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples)
-
-# Create target examples.
-#
-# Only builds the examples, but does not run them. To run and build all
-# examples, use target runexamples (below).
-# Use macro cvc4_add_example to add examples.
-add_custom_target(examples)
-
-# Create target runexamples.
-# Builds and runs all examples.
-add_custom_target(runexamples
- COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $$ARGS
- DEPENDS examples)
+set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin)
# Add example target and create test to run example with ctest.
#
# > name: The name of the example
# > src_files: The list of source files passed as string "src1 src2 ..."
# (alternative: "src1;src2;..."). If empty, <name>.cpp is assumed.
-# > libs: The list of libraries to link the example against, passed as either
-# - a list variable: set(<list name> <libs1> <libs2> ...) and pass
-# as "${<list name>}"
-# - a string: pass as "lib1 lib2 ..." (alternative: "lib1;lib2;...")
# > output_dir: Determines the examples subdirectory and is empty (passed as
# empty string) for the examples root directory (this)
# > ARGN: Any additional arguments passed to the macro are interpreted as
# as arguments to the test executable.
-macro(cvc4_add_example name src_files libs output_dir)
+macro(cvc4_add_example name src_files output_dir)
# The build target is created without the path prefix (not supported),
# e.g., for '<output_dir>/myexample.cpp'
# we create build target 'myexample'
@@ -45,56 +35,52 @@ macro(cvc4_add_example name src_files libs output_dir)
else()
string(REPLACE " " ";" src_files_list "${src_files}")
endif()
- add_executable(${name} EXCLUDE_FROM_ALL ${src_files_list})
- string(REPLACE " " ";" libs_list "${libs_list}")
- target_link_libraries(${name} ${libs})
- add_dependencies(examples ${name})
- # The test target is prefixed with test identifier 'example/' and the path,
+
+ add_executable(${name} ${src_files_list})
+ target_link_libraries(${name} CVC4::cvc4 CVC4::cvc4parser)
+
+ # The test target is prefixed with the path,
# e.g., for '<output_dir>/myexample.cpp'
- # we create test target 'example/<output_dir>/myexample'
- # and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+ # we create test target '<output_dir>/myexample'
+ # and run it with 'ctest -R "<output_dir>/myexample"'.
set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
if("${output_dir}" STREQUAL "")
- set(example_test example/${name})
+ set(example_test ${name})
else()
- set(example_test example/${output_dir}/${name})
+ set(example_test ${output_dir}/${name})
endif()
set_target_properties(${name}
PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${example_bin_dir})
add_test(${example_test} ${example_bin_dir}/${name} ${ARGN})
- set_tests_properties(${example_test} PROPERTIES LABELS "example")
endmacro()
-set(EXAMPLES_LINK_LIBS cvc4 cvc4parser)
-cvc4_add_example(simple_vc_cxx "" "${EXAMPLES_LINK_LIBS}" "")
-cvc4_add_example(simple_vc_quant_cxx "" "${EXAMPLES_LINK_LIBS}" "")
-cvc4_add_example(translator "" "${EXAMPLES_LINK_LIBS}" ""
+cvc4_add_example(simple_vc_cxx "" "")
+cvc4_add_example(simple_vc_quant_cxx "" "")
+cvc4_add_example(translator "" ""
# argument to binary (for testing)
${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
-if(BUILD_BINDINGS_JAVA)
+add_subdirectory(api)
+add_subdirectory(hashsmt)
+add_subdirectory(nra-translate)
+add_subdirectory(sets-translate)
+
+if(TARGET CVC4::cvc4jar)
find_package(Java REQUIRED)
- set(EXAMPLES_JAVA_CLASSPATH "${CMAKE_BINARY_DIR}/src/bindings/java/CVC4.jar")
- add_custom_target(SimpleVCjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/SimpleVC.java
- -d ${CMAKE_BINARY_DIR}/bin/examples
- DEPENDS cvc4jar)
- add_dependencies(examples SimpleVCjava)
+ include(UseJava)
+
+ get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
+
+ add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
+
add_test(
- NAME example/SimpleVCjava
+ NAME java/SimpleVC
COMMAND
${Java_JAVA_EXECUTABLE}
- -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
- -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/"
+ -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
+ -Djava.library.path=${CVC4_JNI_PATH}
SimpleVC
)
- set_tests_properties(example/SimpleVCjava PROPERTIES LABELS "example")
-endif()
-
-add_subdirectory(api)
-add_subdirectory(hashsmt)
-add_subdirectory(nra-translate)
-add_subdirectory(sets-translate)
+ add_subdirectory(api/java)
+endif()
diff --git a/examples/README b/examples/README.md
index cc3c23f26..18834719e 100644
--- a/examples/README
+++ b/examples/README.md
@@ -1,11 +1,37 @@
-Examples
---------
+# CVC4 API Examples
This directory contains usage examples of CVC4's different language
bindings, library APIs, and also tutorial examples from the tutorials
available at http://cvc4.cs.stanford.edu/wiki/Tutorials
-### SimpleVC*, simple_vc*
+## Building Examples
+
+The examples provided in this directory are not built by default.
+
+```
+ mkdir <build_dir>
+ cd <build_dir>
+ cmake ..
+ make # use -jN for parallel build with N threads
+
+ ctest # run all examples
+ ctest -R <example> # run specific example '<example>'
+
+ # Or just run the binaries in directory <build_dir>/bin/, for example:
+ bin/api/bitvectors
+```
+
+**Note:** If you installed CVC4 in a non-standard location you have to
+additionally specify `CMAKE_PREFIX_PATH` to point to the location of
+`CVC4Config.cmake` (usually `<your-install-prefix>/lib/cmake`) as follows:
+
+```
+ cmake .. -DCMAKE_PREFIX_PATH=<your-install-prefix>/lib/cmake
+```
+
+The examples binaries are built into `<build_dir>/bin`.
+
+## SimpleVC*, simple_vc*
These are examples of how to use CVC4 with each of its library
interfaces (APIs) and language bindings. They are essentially "hello
@@ -13,19 +39,8 @@ world" examples, and do not fully demonstrate the interfaces, but
function as a starting point to using simple expressions and solving
functionality through each library.
-### Targeted examples
+## Targeted examples
The "api" directory contains some more specifically-targeted
examples (for bitvectors, for arithmetic, etc.). The "api/java"
directory contains the same examples in Java.
-
-### Building Examples
-
-The examples provided in this directory are not built by default.
-
- make examples # build all examples
- make runexamples # build and run all examples
- make <example> # build examples/<subdir>/<example>.<ext>
- ctest example//<subdir>/<example> # run examples/<subdir>/<example>.<ext>
-
-The examples binaries are built into `<build_dir>/bin/examples`.
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 125b4f848..c84b040a3 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -17,18 +17,10 @@
** following:
**
** java \
- ** -classpath path/to/CVC4.jar \
- ** -Djava.library.path=/dir/containing/java/CVC4.so \
+ ** -cp path/to/CVC4.jar:SimpleVC.jar \
+ ** -Djava.library.path=/dir/containing/libcvc4jni.so \
** SimpleVC
**
- ** For example, if you are building CVC4 without specifying your own
- ** build directory, the build process puts everything in builds/, and
- ** you can run this example (after building it with "make") like this:
- **
- ** java \
- ** -classpath builds/examples:builds/src/bindings/CVC4.jar \
- ** -Djava.library.path=builds/src/bindings/java/.libs \
- ** SimpleVC
**/
import edu.nyu.acsys.CVC4.*;
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index c78c50466..b121c8833 100644
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -19,12 +19,6 @@ set(CVC4_EXAMPLES_API
strings-new
)
-set(EXAMPLES_API_LINK_LIBS cvc4 cvc4parser)
foreach(example ${CVC4_EXAMPLES_API})
- cvc4_add_example(${example}
- "" "${EXAMPLES_API_LINK_LIBS}" "api")
+ cvc4_add_example(${example} "" "api")
endforeach()
-
-if(BUILD_BINDINGS_JAVA)
- add_subdirectory(java)
-endif()
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index d0c26f134..58912a1bb 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 59257976d..259eb48ff 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp
index 955a83cff..44b5aa018 100644
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -17,8 +17,7 @@
#include <iostream>
#include <cmath>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index 983da71db..1820712bd 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/bitvectors_and_arrays.cpp
@@ -16,8 +16,8 @@
#include <iostream>
#include <cmath>
-// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index e78e8919f..5284a0119 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -18,8 +18,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 0d8ae0494..646e6b17a 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -18,8 +18,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 08918fc87..8c6257725 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace CVC4::api;
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 3bf1df12f..dabc1228f 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -15,9 +15,8 @@
**/
#include <iostream>
-#include "options/language.h" // for use with make examples
-#include "smt/smt_engine.h" // for use with make examples
-//#include <cvc4/cvc4.h> // To follow the wiki
+
+#include <cvc4/cvc4.h>
using namespace CVC4;
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index cb7d96fa5..0cb885b2c 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index c9240363e..a008ec718 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/extract.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
index a7fbe22e9..ab869f03c 100644
--- a/examples/api/helloworld-new.cpp
+++ b/examples/api/helloworld-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace CVC4::api;
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index 1235c4c55..befeaa7bd 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace CVC4;
int main() {
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index dd7d6566f..2b364c3d1 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -1,6 +1,3 @@
-set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_BIN_DIR}/api/java)
-file(MAKE_DIRECTORY ${EXAMPLES_API_JAVA_BIN_DIR})
-
set(EXAMPLES_API_JAVA
BitVectors
BitVectorsAndArrays
@@ -19,22 +16,19 @@ set(EXAMPLES_API_JAVA
)
foreach(example ${EXAMPLES_API_JAVA})
- add_custom_target(${example}
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/${example}.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
- add_dependencies(examples ${example})
- set(example_test example/api/java/${example})
+ add_jar(${example} ${example}.java
+ INCLUDE_JARS "${CVC4_JAR}"
+ OUTPUT_DIR "${CMAKE_BINARY_DIR}/bin/api/java")
+
+ set(EXAMPLE_TEST_NAME api/java/${example})
+
add_test(
- NAME ${example_test}
+ NAME ${EXAMPLE_TEST_NAME}
COMMAND
${Java_JAVA_EXECUTABLE}
- -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
- -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/api/java/"
+ -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/bin/api/java/${example}.jar"
+ -Djava.library.path=${CVC4_JNI_PATH}
${example}
)
- set_tests_properties(${example_test} PROPERTIES SKIP_RETURN_CODE 77)
- set_tests_properties(${example_test} PROPERTIES LABELS "example")
+ set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES SKIP_RETURN_CODE 77)
endforeach()
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index 2edcaf71e..a4ff9a2cc 100644
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -17,8 +17,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include "cvc4/api/cvc4cpp.h"
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 83a0064c9..f1c8b861c 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -17,8 +17,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 60df7a82f..2ca3db9d2 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace std;
using namespace CVC4::api;
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 3110c01e3..9fb342431 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -16,9 +16,8 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/options/set_language.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index 42630dc0e..e83ab89ff 100644
--- a/examples/api/strings-new.cpp
+++ b/examples/api/strings-new.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
-#include "api/cvc4cpp.h"
+#include <cvc4/api/cvc4cpp.h>
using namespace CVC4::api;
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 96f4dd400..661ae0e77 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -16,9 +16,8 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/options/set_language.h>
using namespace CVC4;
diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt
index ff696b403..39e503a81 100644
--- a/examples/hashsmt/CMakeLists.txt
+++ b/examples/hashsmt/CMakeLists.txt
@@ -1,13 +1,11 @@
-include_directories(.)
-
-set(EXAMPLES_HASHSMT_LINK_LIBS cvc4)
-
if(Boost_FOUND)
cvc4_add_example(sha1_inversion
- "sha1_inversion.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
- "a" "sha1_inversion.outfile") # arguments to binary (for testing)
+ "sha1_inversion.cpp word.cpp" "hashsmt"
+ # arguments to binary (for testing)
+ "a" "sha1_inversion.outfile")
endif()
cvc4_add_example(sha1_collision
- "sha1_collision.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
- "1" "1" "sha1_collision.outfile") # arguments to binary (for testing)
+ "sha1_collision.cpp word.cpp" "hashsmt"
+ # arguments to binary (for testing)
+ "1" "1" "sha1_collision.outfile")
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index e26b2623b..ea93db144 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -27,11 +27,10 @@
#include <sstream>
#include <string>
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
#include "sha1.hpp"
-#include "smt/command.h"
#include "word.h"
using namespace std;
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 667c3c4e0..b53f4b149 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -35,11 +35,11 @@
#include <string>
#include <vector>
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
+
#include "sha1.hpp"
-#include "smt/command.h"
#include "word.h"
using namespace std;
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 189eaf485..b26e3b4d3 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -26,10 +26,10 @@
#include <vector>
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/options.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/language.h>
+#include <cvc4/options/options.h>
using namespace std;
using namespace hashsmt;
diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h
index cbe53d549..ad08a63ae 100644
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -28,9 +28,7 @@
#include <string>
#include <iostream>
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "options/options.h"
+#include <cvc4/cvc4.h>
namespace hashsmt {
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;
diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt
index 1c34d3aaf..5487a2fcf 100644
--- a/examples/sets-translate/CMakeLists.txt
+++ b/examples/sets-translate/CMakeLists.txt
@@ -1,12 +1,11 @@
if(Boost_FOUND)
- set(EXAMPLES_SETS_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
cvc4_add_example(sets2arrays
- "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+ "sets_translate.cpp" "sets-translate"
# argument to binary (for testing)
${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
cvc4_add_example(sets2axioms
- "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+ "sets_translate.cpp" "sets-translate"
# argument to binary (for testing)
${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS)
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index f7513a401..0d263cb97 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -23,15 +23,9 @@
#include <unordered_map>
#include <vector>
-#include "api/cvc4cpp.h"
-#include "expr/expr.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 "theory/logic_info.h"
+#include <cvc4/api/cvc4cpp.h>
+#include <cvc4/cvc4.h>
+#include <cvc4/options/set_language.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index ad18ae5b7..25a05a1a7 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -18,8 +18,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index a8bbfe29a..11bbe01e0 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -16,8 +16,7 @@
#include <iostream>
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
+#include <cvc4/cvc4.h>
using namespace std;
using namespace CVC4;
diff --git a/examples/translator.cpp b/examples/translator.cpp
index b8b8fde38..741706070 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -22,16 +22,10 @@
#include <getopt.h>
#include <iostream>
-#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/src/CMakeLists.txt b/src/CMakeLists.txt
index d062e99c0..7289f650b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -761,8 +761,8 @@ target_include_directories(cvc4
install(TARGETS cvc4
EXPORT cvc4-targets
- LIBRARY DESTINATION lib
- ARCHIVE DESTINATION lib)
+ LIBRARY DESTINATION ${LIBRARY_INSTALL_DIR}
+ ARCHIVE DESTINATION ${LIBRARY_INSTALL_DIR})
set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
target_compile_definitions(cvc4
@@ -842,27 +842,27 @@ install(FILES
api/cvc4cpp.h
api/cvc4cppkind.h
DESTINATION
- include/cvc4/api)
+ ${INCLUDE_INSTALL_DIR}/cvc4/api)
install(FILES
base/configuration.h
base/exception.h
base/listener.h
base/modal_exception.h
DESTINATION
- include/cvc4/base)
+ ${INCLUDE_INSTALL_DIR}/cvc4/base)
install(FILES
context/cdhashmap_forward.h
context/cdhashset_forward.h
context/cdinsert_hashmap_forward.h
context/cdlist_forward.h
DESTINATION
- include/cvc4/context)
+ ${INCLUDE_INSTALL_DIR}/cvc4/context)
install(FILES
include/cvc4.h
include/cvc4_public.h
include/cvc4parser_public.h
DESTINATION
- include/cvc4)
+ ${INCLUDE_INSTALL_DIR}/cvc4)
install(FILES
expr/array.h
expr/array_store_all.h
@@ -881,7 +881,7 @@ install(FILES
${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
DESTINATION
- include/cvc4/expr)
+ ${INCLUDE_INSTALL_DIR}/cvc4/expr)
install(FILES
options/argument_extender.h
options/arith_heuristic_pivot_rule.h
@@ -898,38 +898,38 @@ install(FILES
options/sygus_out_mode.h
options/theoryof_mode.h
DESTINATION
- include/cvc4/options)
+ ${INCLUDE_INSTALL_DIR}/cvc4/options)
install(FILES
parser/input.h
parser/parser.h
parser/parser_builder.h
parser/parser_exception.h
DESTINATION
- include/cvc4/parser)
+ ${INCLUDE_INSTALL_DIR}/cvc4/parser)
install(FILES
printer/sygus_print_callback.h
DESTINATION
- include/cvc4/printer)
+ ${INCLUDE_INSTALL_DIR}/cvc4/printer)
install(FILES
proof/unsat_core.h
DESTINATION
- include/cvc4/proof)
+ ${INCLUDE_INSTALL_DIR}/cvc4/proof)
install(FILES
smt/command.h
smt/logic_exception.h
smt/smt_engine.h
DESTINATION
- include/cvc4/smt)
+ ${INCLUDE_INSTALL_DIR}/cvc4/smt)
install(FILES
smt_util/lemma_channels.h
smt_util/lemma_input_channel.h
smt_util/lemma_output_channel.h
DESTINATION
- include/cvc4/smt_util)
+ ${INCLUDE_INSTALL_DIR}/cvc4/smt_util)
install(FILES
theory/logic_info.h
DESTINATION
- include/cvc4/theory)
+ ${INCLUDE_INSTALL_DIR}/cvc4/theory)
install(FILES
util/abstract_value.h
util/bitvector.h
@@ -955,7 +955,7 @@ install(FILES
${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
DESTINATION
- include/cvc4/util)
+ ${INCLUDE_INSTALL_DIR}/cvc4/util)
# Fix include paths for all public headers.
# Note: This is a temporary fix until the new C++ API is in place.
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 3d1e0463b..b68a353ad 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -276,4 +276,13 @@ add_jar(cvc4jar
add_dependencies(cvc4jar cvc4jni)
install_jar(cvc4jar DESTINATION share/java/cvc4)
install_jni_symlink(cvc4jar DESTINATION share/java/cvc4)
-install(TARGETS cvc4jni DESTINATION lib)
+install(TARGETS cvc4jni
+ EXPORT cvc4-targets
+ DESTINATION ${LIBRARY_INSTALL_DIR})
+
+install_jar_exports(
+ TARGETS cvc4jar
+ NAMESPACE CVC4::
+ FILE CVC4JavaTargets.cmake
+ DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
+)
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 356b0e199..96e0078ed 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -47,9 +47,12 @@ set_target_properties(cvc4-bin
target_link_libraries(cvc4-bin cvc4 cvc4parser)
if(PROGRAM_PREFIX)
install(PROGRAMS
- $<TARGET_FILE:cvc4-bin> DESTINATION bin RENAME ${PROGRAM_PREFIX}cvc4)
+ $<TARGET_FILE:cvc4-bin>
+ DESTINATION ${RUNTIME_INSTALL_DIR}
+ RENAME ${PROGRAM_PREFIX}cvc4)
else()
- install(TARGETS cvc4-bin DESTINATION bin)
+ install(TARGETS cvc4-bin
+ DESTINATION ${RUNTIME_INSTALL_DIR})
endif()
# In order to get a fully static executable we have to make sure that we also
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 78ab82cb4..f2c1a6ef4 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -98,7 +98,7 @@ target_link_libraries(cvc4parser cvc4 ${ANTLR_LIBRARIES})
target_include_directories(cvc4parser PRIVATE ${ANTLR_INCLUDE_DIR})
install(TARGETS cvc4parser
EXPORT cvc4-targets
- DESTINATION lib)
+ DESTINATION ${LIBRARY_INSTALL_DIR})
# The generated lexer/parser files define some functions as
# __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index cd67c136e..447d4909f 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -5,9 +5,6 @@
# > system tests
add_custom_target(build-tests)
-# Since examples are also built and run for testing, we have to add examples
-# to the build test dependencies.
-add_dependencies(build-tests examples)
# Note: Do not add custom targets for running tests (regress, systemtests,
# units) as dependencies to other run targets. This will result in executing
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback