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
[ -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}"
# 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
#
# 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}")
#-----------------------------------------------------------------------------#
endif()
add_subdirectory(doc)
-add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
add_subdirectory(src)
add_subdirectory(test)
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(
install(FILES
${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
- DESTINATION lib/cmake/CVC4
+ DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
)
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()
-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'
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()
+++ /dev/null
-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*
-
-These are examples of how to use CVC4 with each of its library
-interfaces (APIs) and language bindings. They are essentially "hello
-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
-
-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`.
--- /dev/null
+# 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
+
+## 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
+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
+
+The "api" directory contains some more specifically-targeted
+examples (for bitvectors, for arithmetic, etc.). The "api/java"
+directory contains the same examples in Java.
** 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.*;
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()
#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;
#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;
#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;
#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;
#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;
#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;
#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;
**/
#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;
#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;
#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;
#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;
#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() {
-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
)
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()
#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;
#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;
#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;
#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;
#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;
#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;
-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")
#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;
#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;
#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;
#include <string>
#include <iostream>
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "options/options.h"
+#include <cvc4/cvc4.h>
namespace hashsmt {
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
#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;
#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;
#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;
#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;
#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;
#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;
#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;
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)
#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;
#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;
#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;
#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;
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
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
${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
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
${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.
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
+)
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
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
# > 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
projects / cvc5.git / commitdiff