diff options
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 46 |
1 files changed, 32 insertions, 14 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0124bf4f9..cff31dbcd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -88,6 +88,8 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h + preprocessing/passes/sygus_abduct.cpp + preprocessing/passes/sygus_abduct.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/symmetry_breaker.cpp @@ -139,6 +141,8 @@ libcvc4_add_sources( proof/dimacs_printer.h proof/drat/drat_proof.cpp proof/drat/drat_proof.h + proof/er/er_proof.cpp + proof/er/er_proof.h proof/lemma_proof.cpp proof/lemma_proof.h proof/lfsc_proof_printer.cpp @@ -235,7 +239,6 @@ libcvc4_add_sources( smt/model_core_builder.h smt/smt_engine.cpp smt/smt_engine.h - smt/smt_engine_check_proof.cpp smt/smt_engine_scope.cpp smt/smt_engine_scope.h smt/smt_statistics_registry.cpp @@ -622,10 +625,14 @@ libcvc4_add_sources( theory/shared_terms_database.h theory/sort_inference.cpp theory/sort_inference.h + theory/strings/normal_form.cpp + theory/strings/normal_form.h theory/strings/regexp_elim.cpp theory/strings/regexp_elim.h theory/strings/regexp_operation.cpp theory/strings/regexp_operation.h + theory/strings/regexp_solver.cpp + theory/strings/regexp_solver.h theory/strings/skolem_cache.cpp theory/strings/skolem_cache.h theory/strings/theory_strings.cpp @@ -768,6 +775,11 @@ endif() target_link_libraries(cvc4 ${GMP_LIBRARIES}) target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR}) +# Add rt library +# Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime). +# RT_LIBRARIES should be empty for glibc >= 2.17 +target_link_libraries(cvc4 ${RT_LIBRARIES}) + #-----------------------------------------------------------------------------# # Visit main subdirectory after creating target cvc4. For target main, we have # to manually add library dependencies since we can't use @@ -789,27 +801,27 @@ install(FILES api/cvc4cpp.h api/cvc4cppkind.h DESTINATION - include/api) + include/cvc4/api) install(FILES base/configuration.h base/exception.h base/listener.h base/modal_exception.h DESTINATION - include/base) + include/cvc4/base) install(FILES context/cdhashmap_forward.h context/cdhashset_forward.h context/cdinsert_hashmap_forward.h context/cdlist_forward.h DESTINATION - include/context) + include/cvc4/context) install(FILES include/cvc4.h include/cvc4_public.h include/cvc4parser_public.h DESTINATION - include) + include/cvc4) install(FILES expr/array.h expr/array_store_all.h @@ -829,7 +841,7 @@ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h DESTINATION - include/expr) + include/cvc4/expr) install(FILES options/argument_extender.h options/arith_heuristic_pivot_rule.h @@ -846,38 +858,38 @@ install(FILES options/sygus_out_mode.h options/theoryof_mode.h DESTINATION - include/options) + include/cvc4/options) install(FILES parser/input.h parser/parser.h parser/parser_builder.h parser/parser_exception.h DESTINATION - include/parser) + include/cvc4/parser) install(FILES printer/sygus_print_callback.h DESTINATION - include/printer) + include/cvc4/printer) install(FILES proof/unsat_core.h DESTINATION - include/proof) + include/cvc4/proof) install(FILES smt/command.h smt/logic_exception.h smt/smt_engine.h DESTINATION - include/smt) + include/cvc4/smt) install(FILES smt_util/lemma_channels.h smt_util/lemma_input_channel.h smt_util/lemma_output_channel.h DESTINATION - include/smt_util) + include/cvc4/smt_util) install(FILES theory/logic_info.h DESTINATION - include/theory) + include/cvc4/theory) install(FILES util/abstract_value.h util/bitvector.h @@ -904,4 +916,10 @@ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h DESTINATION - include/util) + include/cvc4/util) + +# Fix include paths for all public headers. +# Note: This is a temporary fix until the new C++ API is in place. +install(CODE "execute_process(COMMAND + ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh + ${CMAKE_INSTALL_PREFIX})") |