diff options
Diffstat (limited to 'examples')
41 files changed, 154 insertions, 244 deletions
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; |