From 4f384b6fadd999324d83b4c4ea900de2a0e13dd7 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 25 Sep 2019 09:47:12 -0700 Subject: [PATCH] Use separate CMake project for CVC4 examples. (#3196) --- .travis.yml | 10 +- CMakeLists.txt | 18 +++- cmake/CVC4Config.cmake.in | 5 + examples/CMakeLists.txt | 96 +++++++++----------- examples/{README => README.md} | 45 ++++++--- examples/SimpleVC.java | 12 +-- examples/api/CMakeLists.txt | 8 +- examples/api/bitvectors-new.cpp | 3 +- examples/api/bitvectors.cpp | 3 +- examples/api/bitvectors_and_arrays-new.cpp | 3 +- examples/api/bitvectors_and_arrays.cpp | 4 +- examples/api/combination-new.cpp | 3 +- examples/api/combination.cpp | 3 +- examples/api/datatypes-new.cpp | 3 +- examples/api/datatypes.cpp | 5 +- examples/api/extract-new.cpp | 3 +- examples/api/extract.cpp | 3 +- examples/api/helloworld-new.cpp | 3 +- examples/api/helloworld.cpp | 3 +- examples/api/java/CMakeLists.txt | 26 ++---- examples/api/linear_arith-new.cpp | 3 +- examples/api/linear_arith.cpp | 3 +- examples/api/sets-new.cpp | 3 +- examples/api/sets.cpp | 5 +- examples/api/strings-new.cpp | 3 +- examples/api/strings.cpp | 5 +- examples/hashsmt/CMakeLists.txt | 14 ++- examples/hashsmt/sha1_collision.cpp | 7 +- examples/hashsmt/sha1_inversion.cpp | 8 +- examples/hashsmt/word.cpp | 8 +- examples/hashsmt/word.h | 4 +- examples/nra-translate/CMakeLists.txt | 4 +- examples/nra-translate/normalize.cpp | 14 +-- examples/nra-translate/smt2info.cpp | 8 +- examples/nra-translate/smt2todreal.cpp | 12 +-- examples/nra-translate/smt2toisat.cpp | 9 +- examples/nra-translate/smt2tomathematica.cpp | 8 +- examples/nra-translate/smt2toqepcad.cpp | 8 +- examples/nra-translate/smt2toredlog.cpp | 9 +- examples/sets-translate/CMakeLists.txt | 5 +- examples/sets-translate/sets_translate.cpp | 12 +-- examples/simple_vc_cxx.cpp | 3 +- examples/simple_vc_quant_cxx.cpp | 3 +- examples/translator.cpp | 14 +-- src/CMakeLists.txt | 30 +++--- src/bindings/java/CMakeLists.txt | 11 ++- src/main/CMakeLists.txt | 7 +- src/parser/CMakeLists.txt | 2 +- test/CMakeLists.txt | 3 - 49 files changed, 211 insertions(+), 273 deletions(-) rename examples/{README => README.md} (50%) 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, .cpp is assumed. -# > libs: The list of libraries to link the example against, passed as either -# - a list variable: set( ...) and pass -# as "${}" -# - 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 '/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 '/myexample.cpp' - # we create test target 'example//myexample' - # and run it with 'ctest -R "example//myunittest"'. + # we create test target '/myexample' + # and run it with 'ctest -R "/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 similarity index 50% rename from examples/README rename to 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 + cd + cmake .. + make # use -jN for parallel build with N threads + + ctest # run all examples + ctest -R # run specific example '' + + # Or just run the binaries in directory /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 `/lib/cmake`) as follows: + +``` + cmake .. -DCMAKE_PREFIX_PATH=/lib/cmake +``` + +The examples binaries are built into `/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 # build examples//. - ctest example/// # run examples//. - -The examples binaries are built into `/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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 #include -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 #include -// #include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" + +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -#include "options/language.h" // for use with make examples -#include "smt/smt_engine.h" // for use with make examples -//#include // To follow the wiki + +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 -// #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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" -#include "options/set_language.h" +#include +#include 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 -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" -#include "options/set_language.h" +#include +#include 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 #include -#include "expr/expr_iomanip.h" -#include "options/language.h" -#include "options/set_language.h" +#include +#include +#include #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 #include -#include "expr/expr_iomanip.h" -#include "options/language.h" -#include "options/set_language.h" +#include +#include +#include + #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 -#include "expr/expr.h" -#include "expr/expr_iomanip.h" -#include "options/language.h" -#include "options/options.h" +#include +#include +#include +#include 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 #include -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "options/options.h" +#include 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 #include -#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 +#include +#include +#include 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 #include -#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 +#include 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 #include -#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 +#include +#include +#include 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 #include -#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 +#include 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 #include -#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 +#include 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 #include -#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 +#include 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 #include -#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 +#include 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 #include -#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 +#include +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 -//#include // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include 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 #include -#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 +#include +#include +#include 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 - $ DESTINATION bin RENAME ${PROGRAM_PREFIX}cvc4) + $ + 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 -- 2.30.2