## Top contributors (to current version):
## Mathias Preiner, Andrew Reynolds, Gereon Kremer
## This file is part of the CVC4 project.
-## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
## in the top-level source directory and their institutional affiliations.
## All rights reserved. See the file COPYING in the top-level source
## directory for licensing information.
# Collect libcvc4 source files
libcvc4_add_sources(
- api/cvc4cpp.cpp
- api/cvc4cpp.h
- api/cvc4cppkind.h
+ api/cpp/cvc5.cpp
+ api/cpp/cvc5.h
+ api/cpp/cvc5_checks.h
+ api/cpp/cvc5_kind.h
context/backtrackable.h
context/cddense_set.h
context/cdhashmap.h
lib/replacements.h
lib/strtok_r.c
lib/strtok_r.h
+ omt/bitvector_optimizer.cpp
+ omt/bitvector_optimizer.h
+ omt/integer_optimizer.cpp
+ omt/integer_optimizer.h
+ omt/omt_optimizer.cpp
+ omt/omt_optimizer.h
preprocessing/assertion_pipeline.cpp
preprocessing/assertion_pipeline.h
preprocessing/passes/ackermann.cpp
proof/clause_id.h
proof/cnf_proof.cpp
proof/cnf_proof.h
+ proof/dot/dot_printer.cpp
+ proof/dot/dot_printer.h
proof/proof_manager.cpp
proof/proof_manager.h
proof/sat_proof.h
prop/sat_solver_factory.h
prop/sat_solver_types.cpp
prop/sat_solver_types.h
+ prop/skolem_def_manager.cpp
+ prop/skolem_def_manager.h
prop/theory_proxy.cpp
prop/theory_proxy.h
smt/abduction_solver.cpp
smt/dump.h
smt/dump_manager.cpp
smt/dump_manager.h
+ smt/env.cpp
+ smt/env.h
smt/expand_definitions.cpp
smt/expand_definitions.h
smt/listeners.cpp
smt/listeners.h
smt/logic_exception.h
- smt/logic_request.cpp
- smt/logic_request.h
smt/interpolation_solver.cpp
smt/interpolation_solver.h
smt/managed_ostreams.cpp
smt/model_blocker.h
smt/node_command.cpp
smt/node_command.h
+ smt/optimization_solver.cpp
+ smt/optimization_solver.h
smt/options_manager.cpp
smt/options_manager.h
smt/output_manager.cpp
theory/arith/approx_simplex.h
theory/arith/arith_ite_utils.cpp
theory/arith/arith_ite_utils.h
- theory/arith/arith_lemma.cpp
- theory/arith/arith_lemma.h
theory/arith/arith_msum.cpp
theory/arith/arith_msum.h
theory/arith/arith_preprocess.cpp
theory/arith/fc_simplex.h
theory/arith/infer_bounds.cpp
theory/arith/infer_bounds.h
- theory/arith/inference_id.cpp
- theory/arith/inference_id.h
theory/arith/inference_manager.cpp
theory/arith/inference_manager.h
theory/arith/linear_equality.cpp
theory/arith/nl/cad/constraints.h
theory/arith/nl/cad/projections.cpp
theory/arith/nl/cad/projections.h
+ theory/arith/nl/cad/proof_checker.cpp
+ theory/arith/nl/cad/proof_checker.h
+ theory/arith/nl/cad/proof_generator.cpp
+ theory/arith/nl/cad/proof_generator.h
theory/arith/nl/cad/variable_ordering.cpp
theory/arith/nl/cad/variable_ordering.h
theory/arith/nl/ext/constraint.cpp
theory/bags/theory_bags_type_enumerator.cpp
theory/bags/theory_bags_type_enumerator.h
theory/bags/theory_bags_type_rules.h
+ theory/bags/theory_bags_type_rules.cpp
theory/booleans/circuit_propagator.cpp
theory/booleans/circuit_propagator.h
theory/booleans/proof_circuit_propagator.cpp
theory/bv/bitblast/eager_bitblaster.h
theory/bv/bitblast/lazy_bitblaster.cpp
theory/bv/bitblast/lazy_bitblaster.h
+ theory/bv/bitblast/proof_bitblaster.cpp
+ theory/bv/bitblast/proof_bitblaster.h
theory/bv/bitblast/simple_bitblaster.cpp
theory/bv/bitblast/simple_bitblaster.h
theory/bv/bv_eager_solver.cpp
theory/bv/bv_subtheory_core.h
theory/bv/bv_subtheory_inequality.cpp
theory/bv/bv_subtheory_inequality.h
+ theory/bv/int_blaster.h
theory/bv/proof_checker.cpp
theory/bv/proof_checker.h
theory/bv/slicer.cpp
theory/datatypes/theory_datatypes_type_rules.h
theory/datatypes/theory_datatypes_utils.cpp
theory/datatypes/theory_datatypes_utils.h
+ theory/datatypes/tuple_project_op.cpp
+ theory/datatypes/tuple_project_op.h
theory/datatypes/type_enumerator.cpp
theory/datatypes/type_enumerator.h
theory/decision_manager.cpp
theory/fp/theory_fp_rewriter.cpp
theory/fp/theory_fp_rewriter.h
theory/fp/theory_fp_type_rules.h
+ theory/fp/theory_fp_type_rules.cpp
theory/fp/type_enumerator.h
theory/interrupted.h
+ theory/incomplete_id.cpp
+ theory/incomplete_id.h
+ theory/inference_id.cpp
+ theory/inference_id.h
theory/inference_manager_buffered.cpp
theory/inference_manager_buffered.h
+ theory/lazy_tree_proof_generator.cpp
+ theory/lazy_tree_proof_generator.h
theory/logic_info.cpp
theory/logic_info.h
theory/model_manager.cpp
theory/quantifiers/ematching/candidate_generator.h
theory/quantifiers/ematching/ho_trigger.cpp
theory/quantifiers/ematching/ho_trigger.h
+ theory/quantifiers/ematching/im_generator.cpp
+ theory/quantifiers/ematching/im_generator.h
theory/quantifiers/ematching/inst_match_generator.cpp
theory/quantifiers/ematching/inst_match_generator.h
theory/quantifiers/ematching/inst_match_generator_multi.cpp
theory/quantifiers/ematching/inst_match_generator_multi_linear.h
theory/quantifiers/ematching/inst_match_generator_simple.cpp
theory/quantifiers/ematching/inst_match_generator_simple.h
+ theory/quantifiers/ematching/inst_strategy.cpp
theory/quantifiers/ematching/inst_strategy.h
theory/quantifiers/ematching/inst_strategy_e_matching.cpp
theory/quantifiers/ematching/inst_strategy_e_matching.h
theory/quantifiers/ematching/pattern_term_selector.h
theory/quantifiers/ematching/trigger.cpp
theory/quantifiers/ematching/trigger.h
+ theory/quantifiers/ematching/trigger_database.cpp
+ theory/quantifiers/ematching/trigger_database.h
theory/quantifiers/ematching/trigger_term_info.cpp
theory/quantifiers/ematching/trigger_term_info.h
theory/quantifiers/ematching/trigger_trie.cpp
theory/quantifiers/first_order_model.h
theory/quantifiers/fmf/bounded_integers.cpp
theory/quantifiers/fmf/bounded_integers.h
+ theory/quantifiers/fmf/first_order_model_fmc.cpp
+ theory/quantifiers/fmf/first_order_model_fmc.h
theory/quantifiers/fmf/full_model_check.cpp
theory/quantifiers/fmf/full_model_check.h
theory/quantifiers/fmf/model_builder.cpp
theory/quantifiers/fmf/model_engine.h
theory/quantifiers/fun_def_evaluator.cpp
theory/quantifiers/fun_def_evaluator.h
+ theory/quantifiers/index_trie.cpp
+ theory/quantifiers/index_trie.h
theory/quantifiers/inst_match.cpp
theory/quantifiers/inst_match.h
theory/quantifiers/inst_match_trie.cpp
theory/quantifiers/lazy_trie.h
theory/quantifiers/proof_checker.cpp
theory/quantifiers/proof_checker.h
+ theory/quantifiers/quant_bound_inference.cpp
+ theory/quantifiers/quant_bound_inference.h
theory/quantifiers/quant_conflict_find.cpp
theory/quantifiers/quant_conflict_find.h
theory/quantifiers/quant_relevance.cpp
theory/quantifiers/quant_split.h
theory/quantifiers/quant_util.cpp
theory/quantifiers/quant_util.h
+ theory/quantifiers/quant_module.cpp
+ theory/quantifiers/quant_module.h
theory/quantifiers/quantifiers_attributes.cpp
theory/quantifiers/quantifiers_attributes.h
theory/quantifiers/quantifiers_inference_manager.cpp
theory/quantifiers/quantifiers_rewriter.h
theory/quantifiers/quantifiers_state.cpp
theory/quantifiers/quantifiers_state.h
+ theory/quantifiers/quantifiers_statistics.cpp
+ theory/quantifiers/quantifiers_statistics.h
theory/quantifiers/query_generator.cpp
theory/quantifiers/query_generator.h
theory/quantifiers/relevant_domain.cpp
theory/quantifiers/skolemize.h
theory/quantifiers/solution_filter.cpp
theory/quantifiers/solution_filter.h
+ theory/quantifiers/term_pools.cpp
+ theory/quantifiers/term_pools.h
+ theory/quantifiers/term_tuple_enumerator.cpp
+ theory/quantifiers/term_tuple_enumerator.h
theory/quantifiers/sygus/ce_guided_single_inv.cpp
theory/quantifiers/sygus/ce_guided_single_inv.h
- theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
- theory/quantifiers/sygus/ce_guided_single_inv_sol.h
theory/quantifiers/sygus/cegis.cpp
theory/quantifiers/sygus/cegis.h
theory/quantifiers/sygus/cegis_core_connective.cpp
theory/quantifiers/sygus/example_infer.h
theory/quantifiers/sygus/example_min_eval.cpp
theory/quantifiers/sygus/example_min_eval.h
+ theory/quantifiers/sygus/rcons_obligation_info.cpp
+ theory/quantifiers/sygus/rcons_obligation_info.h
+ theory/quantifiers/sygus/rcons_type_info.cpp
+ theory/quantifiers/sygus/rcons_type_info.h
theory/quantifiers/sygus/sygus_abduct.cpp
theory/quantifiers/sygus/sygus_abduct.h
theory/quantifiers/sygus/sygus_enumerator.cpp
theory/quantifiers/sygus/sygus_pbe.h
theory/quantifiers/sygus/sygus_process_conj.cpp
theory/quantifiers/sygus/sygus_process_conj.h
+ theory/quantifiers/sygus/sygus_reconstruct.cpp
+ theory/quantifiers/sygus/sygus_reconstruct.h
theory/quantifiers/sygus/sygus_qe_preproc.cpp
theory/quantifiers/sygus/sygus_qe_preproc.h
theory/quantifiers/sygus/sygus_repair_const.cpp
theory/quantifiers/term_database.h
theory/quantifiers/term_enumeration.cpp
theory/quantifiers/term_enumeration.h
+ theory/quantifiers/term_registry.cpp
+ theory/quantifiers/term_registry.h
theory/quantifiers/term_util.cpp
theory/quantifiers/term_util.h
theory/quantifiers/theory_quantifiers.cpp
theory/shared_solver_distributed.h
theory/shared_terms_database.cpp
theory/shared_terms_database.h
+ theory/skolem_lemma.cpp
+ theory/skolem_lemma.h
theory/smt_engine_subsolver.cpp
theory/smt_engine_subsolver.h
theory/sort_inference.cpp
theory/theory_rewriter.h
theory/theory_state.cpp
theory/theory_state.h
- theory/theory_test_utils.h
theory/trust_node.cpp
theory/trust_node.h
theory/trust_substitutions.cpp
$<INSTALL_INTERFACE:include>
)
+include(GenerateExportHeader)
+generate_export_header(cvc4)
+
install(TARGETS cvc4
EXPORT cvc4-targets
LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR})
endif()
if(USE_ABC)
- target_link_libraries(cvc4 ${ABC_LIBRARIES})
+ target_link_libraries(cvc4 PRIVATE ${ABC_LIBRARIES})
target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR})
endif()
if(USE_CADICAL)
- target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR})
+ target_link_libraries(cvc4 PRIVATE CaDiCaL)
endif()
if(USE_CLN)
- target_link_libraries(cvc4 ${CLN_LIBRARIES})
- target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+ target_link_libraries(cvc4 PRIVATE CLN)
endif()
if(USE_CRYPTOMINISAT)
- target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
+ target_link_libraries(cvc4 PRIVATE CryptoMiniSat)
endif()
if(USE_KISSAT)
- target_link_libraries(cvc4 ${Kissat_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
-endif()
-if(USE_DRAT2ER)
- target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
+ target_link_libraries(cvc4 PRIVATE Kissat)
endif()
if(USE_GLPK)
- target_link_libraries(cvc4 ${GLPK_LIBRARIES})
+ target_link_libraries(cvc4 PRIVATE ${GLPK_LIBRARIES})
target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
endif()
-if(USE_LFSC)
- target_link_libraries(cvc4 ${LFSC_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
-endif()
if(USE_POLY)
- target_link_libraries(cvc4 ${POLY_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
+ target_link_libraries(cvc4 PRIVATE Polyxx)
endif()
if(USE_SYMFPU)
- target_include_directories(cvc4
- PUBLIC $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
+ target_link_libraries(cvc4 PRIVATE SymFPU)
endif()
# Note: When linked statically GMP needs to be linked after CLN since CLN
# depends on GMP.
-target_link_libraries(cvc4 ${GMP_LIBRARIES})
-target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(cvc4 PRIVATE GMP)
# 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})
+target_link_libraries(cvc4 PRIVATE ${RT_LIBRARIES})
#-----------------------------------------------------------------------------#
# Visit main subdirectory after creating target cvc4. For target main, we have
endif()
#-----------------------------------------------------------------------------#
-# Note:
-# We define all install commands for all public headers here in one
-# place so that we can easily remove them as soon as we enforce the new
-# C++ API.
-#
-# All (generated) headers that either include cvc4_public.h or
-# cvc4parser_public.h need to be listed explicitly here.
-#
-install(FILES
- api/cvc4cpp.h
- api/cvc4cppkind.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api)
-install(FILES
- base/configuration.h
- base/exception.h
- base/listener.h
- base/modal_exception.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/base)
-install(FILES
- context/cdhashmap_forward.h
- context/cdhashset_forward.h
- context/cdinsert_hashmap_forward.h
- context/cdlist_forward.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/context)
-install(FILES
- include/cvc4.h
- include/cvc4_public.h
- include/cvc4parser_public.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4)
-install(FILES
- expr/array_store_all.h
- expr/ascription_type.h
- expr/emptyset.h
- expr/expr_iomanip.h
- expr/record.h
- expr/sequence.h
- expr/symbol_manager.h
- expr/symbol_table.h
- expr/type.h
- expr/uninterpreted_constant.h
- expr/variable_type_map.h
- ${CMAKE_CURRENT_BINARY_DIR}/expr/expr.h
- ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
- ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/expr)
-install(FILES
- options/language.h
- options/option_exception.h
- options/options.h
- options/printer_modes.h
- options/set_language.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/options)
-install(FILES
- parser/input.h
- parser/parser.h
- parser/parser_builder.h
- parser/parser_exception.h
- parser/parse_op.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser)
-install(FILES
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/printer)
-install(FILES
- proof/unsat_core.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/proof)
-install(FILES
- smt/command.h
- smt/logic_exception.h
- smt/smt_engine.h
- DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/smt)
+# Install public API headers
+
install(FILES
- theory/logic_info.h
- theory/theory_id.h
+ api/cpp/cvc5.h
+ api/cpp/cvc5_kind.h
DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/theory)
+ ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/)
install(FILES
- util/abstract_value.h
- util/bitvector.h
- util/bool.h
- util/cardinality.h
- util/divisible.h
- util/gmp_util.h
- util/hash.h
- util/iand.h
- util/integer_cln_imp.h
- util/integer_gmp_imp.h
- util/maybe.h
- util/poly_util.h
- util/rational_cln_imp.h
- util/rational_gmp_imp.h
- util/real_algebraic_number_poly_imp.h
- util/regexp.h
- util/resource_manager.h
- util/result.h
- util/sexpr.h
- util/statistics.h
- util/string.h
- util/tuple.h
- util/unsafe_interrupt_exception.h
- ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
- ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
- ${CMAKE_CURRENT_BINARY_DIR}/util/real_algebraic_number.h
- ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint_literal_symfpu.h
+ ${CMAKE_CURRENT_BINARY_DIR}/cvc4_export.h
DESTINATION
- ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/util)
+ ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/)
# Fix include paths for all public headers.
# Note: This is a temporary fix until the new C++ API is in place.
projects / cvc5.git / blobdiff