cmake: Working build infrastructure.

TODO: cvc4autoconfig.h

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b93868feab4d298410cfc57bfe7cf290e5f6916f..2cb86b259bf3e786191495a8e20954e078187917 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -111,44 +111,17 @@ execute_process(
 
 #-----------------------------------------------------------------------------#
 
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/src/git_versioninfo.cpp.in
-  ${CMAKE_CURRENT_BINARY_DIR}/src/git_versioninfo.cpp)
+# CONFIGURATION (for now manual)
 
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/SmtEngine.3cvc_template.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/SmtEngine.3cvc_template)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/cvc4.1_template.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/cvc4.1_template)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/cvc4.5.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/cvc4.5)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4.3.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4.3)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4compat.3.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4compat.3)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4parser.3.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4parser.3)
-
-configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/doc/options.3cvc_template.in
-  ${CMAKE_CURRENT_BINARY_DIR}/doc/options.3cvc_template)
+# src/util/rational.h.in
+# src/util/integer.h.in
+set(CVC4_NEED_INT64_T_OVERLOADS 0)
+set(CVC4_USE_CLN_IMP 0)
+set(CVC4_USE_GMP_IMP 1)
+set(CVC4_USE_SYMFPU 0)
 
 #-----------------------------------------------------------------------------#
 
-add_subdirectory(src/base)
-add_subdirectory(src/expr)
-add_subdirectory(src/options)
-add_subdirectory(src/parser)
-add_subdirectory(src/theory)
+add_subdirectory(doc)
 add_subdirectory(proofs/signatures)
-include_directories(src ${CMAKE_CURRENT_BINARY_DIR}/src)
+add_subdirectory(src)

diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt
new file mode 100644 (file)
index 0000000..bbde816
--- /dev/null
+++ b/doc/CMakeLists.txt
@@ -0,0 +1,27 @@
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/SmtEngine.3cvc_template.in
+  ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc_template)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.1_template.in
+  ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1_template)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.5.in
+  ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4.3.in
+  ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4compat.3.in
+  ${CMAKE_CURRENT_BINARY_DIR}/libcvc4compat.3)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4parser.3.in
+  ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/options.3cvc_template.in
+  ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc_template)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 500900bb11c9a14c2d040573022703a95a48b5df..e1e03bd9743912411b638957550005ec919af5a6 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1,17 +1,603 @@
-#add_subdirectory(base)
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/git_versioninfo.cpp.in
+  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+)
+
+set(cvc4_src_files
+  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+  api/cvc4cpp.cpp
+  api/cvc4cpp.h
+  api/cvc4cppkind.h
+  context/backtrackable.h
+  context/cddense_set.h
+  context/cdhashmap.h
+  context/cdhashmap_forward.h
+  context/cdhashset.h
+  context/cdhashset_forward.h
+  context/cdinsert_hashmap.h
+  context/cdinsert_hashmap_forward.h
+  context/cdlist.h
+  context/cdlist_forward.h
+  context/cdmaybe.h
+  context/cdo.h
+  context/cdqueue.h
+  context/cdtrail_queue.h
+  context/context.cpp
+  context/context.h
+  context/context_mm.cpp
+  context/context_mm.h
+  decision/decision_attributes.h
+  decision/decision_engine.cpp
+  decision/decision_engine.h
+  decision/decision_strategy.h
+  decision/justification_heuristic.cpp
+  decision/justification_heuristic.h
+  preprocessing/passes/apply_substs.cpp
+  preprocessing/passes/apply_substs.h
+  preprocessing/passes/bool_to_bv.cpp
+  preprocessing/passes/bool_to_bv.h
+  preprocessing/passes/bv_abstraction.cpp
+  preprocessing/passes/bv_abstraction.h
+  preprocessing/passes/bv_ackermann.cpp
+  preprocessing/passes/bv_ackermann.h
+  preprocessing/passes/bv_gauss.cpp
+  preprocessing/passes/bv_gauss.h
+  preprocessing/passes/bv_intro_pow2.cpp
+  preprocessing/passes/bv_intro_pow2.h
+  preprocessing/passes/bv_to_bool.cpp
+  preprocessing/passes/bv_to_bool.h
+  preprocessing/passes/int_to_bv.cpp
+  preprocessing/passes/int_to_bv.h
+  preprocessing/passes/pseudo_boolean_processor.cpp
+  preprocessing/passes/pseudo_boolean_processor.h
+  preprocessing/passes/real_to_int.cpp
+  preprocessing/passes/real_to_int.h
+  preprocessing/passes/rewrite.cpp
+  preprocessing/passes/rewrite.h
+  preprocessing/passes/sep_skolem_emp.cpp
+  preprocessing/passes/sep_skolem_emp.h
+  preprocessing/passes/static_learning.cpp
+  preprocessing/passes/static_learning.h
+  preprocessing/passes/symmetry_breaker.cpp
+  preprocessing/passes/symmetry_breaker.h
+  preprocessing/passes/symmetry_detect.cpp
+  preprocessing/passes/symmetry_detect.h
+  preprocessing/passes/synth_rew_rules.cpp
+  preprocessing/passes/synth_rew_rules.h
+  preprocessing/preprocessing_pass.cpp
+  preprocessing/preprocessing_pass.h
+  preprocessing/preprocessing_pass_context.cpp
+  preprocessing/preprocessing_pass_context.h
+  preprocessing/preprocessing_pass_registry.cpp
+  preprocessing/preprocessing_pass_registry.h
+  printer/ast/ast_printer.cpp
+  printer/ast/ast_printer.h
+  printer/cvc/cvc_printer.cpp
+  printer/cvc/cvc_printer.h
+  printer/dagification_visitor.cpp
+  printer/dagification_visitor.h
+  printer/printer.cpp
+  printer/printer.h
+  printer/smt2/smt2_printer.cpp
+  printer/smt2/smt2_printer.h
+  printer/sygus_print_callback.cpp
+  printer/sygus_print_callback.h
+  printer/tptp/tptp_printer.cpp
+  printer/tptp/tptp_printer.h
+  proof/arith_proof.cpp
+  proof/arith_proof.h
+  proof/array_proof.cpp
+  proof/array_proof.h
+  proof/bitvector_proof.cpp
+  proof/bitvector_proof.h
+  proof/clause_id.h
+  proof/cnf_proof.cpp
+  proof/cnf_proof.h
+  proof/lemma_proof.cpp
+  proof/lemma_proof.h
+  proof/proof.h
+  proof/proof_manager.cpp
+  proof/proof_manager.h
+  proof/proof_output_channel.cpp
+  proof/proof_output_channel.h
+  proof/proof_utils.cpp
+  proof/proof_utils.h
+  proof/sat_proof.h
+  proof/sat_proof_implementation.h
+  proof/simplify_boolean_node.cpp
+  proof/simplify_boolean_node.h
+  proof/skolemization_manager.cpp
+  proof/skolemization_manager.h
+  proof/theory_proof.cpp
+  proof/theory_proof.h
+  proof/uf_proof.cpp
+  proof/uf_proof.h
+  proof/unsat_core.cpp
+  proof/unsat_core.h
+  prop/cadical.cpp
+  prop/cadical.h
+  prop/cnf_stream.cpp
+  prop/cnf_stream.h
+  prop/cryptominisat.cpp
+  prop/cryptominisat.h
+  prop/prop_engine.cpp
+  prop/prop_engine.h
+  prop/registrar.h
+  prop/sat_solver.h
+  prop/sat_solver_factory.cpp
+  prop/sat_solver_factory.h
+  prop/sat_solver_types.h
+  prop/theory_proxy.cpp
+  prop/theory_proxy.h
+  smt/command.cpp
+  smt/command.h
+  smt/command_list.cpp
+  smt/command_list.h
+  smt/dump.cpp
+  smt/dump.h
+  smt/logic_exception.h
+  smt/logic_request.cpp
+  smt/logic_request.h
+  smt/managed_ostreams.cpp
+  smt/managed_ostreams.h
+  smt/model.cpp
+  smt/model.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
+  smt/smt_statistics_registry.h
+  smt/term_formula_removal.cpp
+  smt/term_formula_removal.h
+  smt/update_ostream.h
+  theory/arith/approx_simplex.cpp
+  theory/arith/approx_simplex.h
+  theory/arith/arith_ite_utils.cpp
+  theory/arith/arith_ite_utils.h
+  theory/arith/arith_msum.cpp
+  theory/arith/arith_msum.h
+  theory/arith/arith_rewriter.cpp
+  theory/arith/arith_rewriter.h
+  theory/arith/arith_static_learner.cpp
+  theory/arith/arith_static_learner.h
+  theory/arith/arith_utilities.h
+  theory/arith/arithvar.cpp
+  theory/arith/arithvar.h
+  theory/arith/attempt_solution_simplex.cpp
+  theory/arith/attempt_solution_simplex.h
+  theory/arith/bound_counts.h
+  theory/arith/callbacks.cpp
+  theory/arith/callbacks.h
+  theory/arith/congruence_manager.cpp
+  theory/arith/congruence_manager.h
+  theory/arith/constraint.cpp
+  theory/arith/constraint.h
+  theory/arith/constraint_forward.h
+  theory/arith/cut_log.cpp
+  theory/arith/cut_log.h
+  theory/arith/delta_rational.cpp
+  theory/arith/delta_rational.h
+  theory/arith/dio_solver.cpp
+  theory/arith/dio_solver.h
+  theory/arith/dual_simplex.cpp
+  theory/arith/dual_simplex.h
+  theory/arith/error_set.cpp
+  theory/arith/error_set.h
+  theory/arith/fc_simplex.cpp
+  theory/arith/fc_simplex.h
+  theory/arith/infer_bounds.cpp
+  theory/arith/infer_bounds.h
+  theory/arith/linear_equality.cpp
+  theory/arith/linear_equality.h
+  theory/arith/matrix.cpp
+  theory/arith/matrix.h
+  theory/arith/nonlinear_extension.cpp
+  theory/arith/nonlinear_extension.h
+  theory/arith/normal_form.cpp
+  theory/arith/normal_form.h
+  theory/arith/partial_model.cpp
+  theory/arith/partial_model.h
+  theory/arith/simplex.cpp
+  theory/arith/simplex.h
+  theory/arith/simplex_update.cpp
+  theory/arith/simplex_update.h
+  theory/arith/soi_simplex.cpp
+  theory/arith/soi_simplex.h
+  theory/arith/tableau.cpp
+  theory/arith/tableau.h
+  theory/arith/tableau_sizes.cpp
+  theory/arith/tableau_sizes.h
+  theory/arith/theory_arith.cpp
+  theory/arith/theory_arith.h
+  theory/arith/theory_arith_private.cpp
+  theory/arith/theory_arith_private.h
+  theory/arith/theory_arith_private_forward.h
+  theory/arith/theory_arith_type_rules.h
+  theory/arith/type_enumerator.h
+  theory/arrays/array_info.cpp
+  theory/arrays/array_info.h
+  theory/arrays/array_proof_reconstruction.cpp
+  theory/arrays/array_proof_reconstruction.h
+  theory/arrays/static_fact_manager.cpp
+  theory/arrays/static_fact_manager.h
+  theory/arrays/theory_arrays.cpp
+  theory/arrays/theory_arrays.h
+  theory/arrays/theory_arrays_rewriter.cpp
+  theory/arrays/theory_arrays_rewriter.h
+  theory/arrays/theory_arrays_type_rules.h
+  theory/arrays/type_enumerator.h
+  theory/arrays/union_find.cpp
+  theory/arrays/union_find.h
+  theory/assertion.cpp
+  theory/assertion.h
+  theory/atom_requests.cpp
+  theory/atom_requests.h
+  theory/booleans/circuit_propagator.cpp
+  theory/booleans/circuit_propagator.h
+  theory/booleans/theory_bool.cpp
+  theory/booleans/theory_bool.h
+  theory/booleans/theory_bool_rewriter.cpp
+  theory/booleans/theory_bool_rewriter.h
+  theory/booleans/theory_bool_type_rules.h
+  theory/booleans/type_enumerator.h
+  theory/builtin/theory_builtin.cpp
+  theory/builtin/theory_builtin.h
+  theory/builtin/theory_builtin_rewriter.cpp
+  theory/builtin/theory_builtin_rewriter.h
+  theory/builtin/theory_builtin_type_rules.h
+  theory/builtin/type_enumerator.cpp
+  theory/builtin/type_enumerator.h
+  theory/bv/abstraction.cpp
+  theory/bv/abstraction.h
+  theory/bv/bitblast/aig_bitblaster.cpp
+  theory/bv/bitblast/aig_bitblaster.h
+  theory/bv/bitblast/bitblast_strategies_template.h
+  theory/bv/bitblast/bitblast_utils.h
+  theory/bv/bitblast/bitblaster.h
+  theory/bv/bitblast/eager_bitblaster.cpp
+  theory/bv/bitblast/eager_bitblaster.h
+  theory/bv/bitblast/lazy_bitblaster.cpp
+  theory/bv/bitblast/lazy_bitblaster.h
+  theory/bv/bv_eager_solver.cpp
+  theory/bv/bv_eager_solver.h
+  theory/bv/bv_inequality_graph.cpp
+  theory/bv/bv_inequality_graph.h
+  theory/bv/bv_quick_check.cpp
+  theory/bv/bv_quick_check.h
+  theory/bv/bv_subtheory.h
+  theory/bv/bv_subtheory_algebraic.cpp
+  theory/bv/bv_subtheory_algebraic.h
+  theory/bv/bv_subtheory_bitblast.cpp
+  theory/bv/bv_subtheory_bitblast.h
+  theory/bv/bv_subtheory_core.cpp
+  theory/bv/bv_subtheory_core.h
+  theory/bv/bv_subtheory_inequality.cpp
+  theory/bv/bv_subtheory_inequality.h
+  theory/bv/slicer.cpp
+  theory/bv/slicer.h
+  theory/bv/theory_bv.cpp
+  theory/bv/theory_bv.h
+  theory/bv/theory_bv_rewrite_rules.h
+  theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+  theory/bv/theory_bv_rewrite_rules_core.h
+  theory/bv/theory_bv_rewrite_rules_normalization.h
+  theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+  theory/bv/theory_bv_rewrite_rules_simplification.h
+  theory/bv/theory_bv_rewriter.cpp
+  theory/bv/theory_bv_rewriter.h
+  theory/bv/theory_bv_type_rules.h
+  theory/bv/theory_bv_utils.cpp
+  theory/bv/theory_bv_utils.h
+  theory/bv/type_enumerator.h
+  theory/care_graph.h
+  theory/datatypes/datatypes_rewriter.cpp
+  theory/datatypes/datatypes_rewriter.h
+  theory/datatypes/datatypes_sygus.cpp
+  theory/datatypes/datatypes_sygus.h
+  theory/datatypes/sygus_simple_sym.cpp
+  theory/datatypes/sygus_simple_sym.h
+  theory/datatypes/theory_datatypes.cpp
+  theory/datatypes/theory_datatypes.h
+  theory/datatypes/theory_datatypes_type_rules.h
+  theory/datatypes/type_enumerator.cpp
+  theory/datatypes/type_enumerator.h
+  theory/evaluator.cpp
+  theory/evaluator.h
+  theory/ext_theory.cpp
+  theory/ext_theory.h
+  theory/fp/fp_converter.cpp
+  theory/fp/fp_converter.h
+  theory/fp/theory_fp.cpp
+  theory/fp/theory_fp.h
+  theory/fp/theory_fp_rewriter.cpp
+  theory/fp/theory_fp_rewriter.h
+  theory/fp/theory_fp_type_rules.h
+  theory/fp/type_enumerator.h
+  theory/idl/idl_assertion.cpp
+  theory/idl/idl_assertion.h
+  theory/idl/idl_assertion_db.cpp
+  theory/idl/idl_assertion_db.h
+  theory/idl/idl_model.cpp
+  theory/idl/idl_model.h
+  theory/idl/theory_idl.cpp
+  theory/idl/theory_idl.h
+  theory/interrupted.h
+  theory/ite_utilities.cpp
+  theory/ite_utilities.h
+  theory/logic_info.cpp
+  theory/logic_info.h
+  theory/output_channel.h
+  theory/quantifiers/alpha_equivalence.cpp
+  theory/quantifiers/alpha_equivalence.h
+  theory/quantifiers/anti_skolem.cpp
+  theory/quantifiers/anti_skolem.h
+  theory/quantifiers/bv_inverter.cpp
+  theory/quantifiers/bv_inverter.h
+  theory/quantifiers/candidate_rewrite_database.cpp
+  theory/quantifiers/candidate_rewrite_database.h
+  theory/quantifiers/candidate_rewrite_filter.cpp
+  theory/quantifiers/candidate_rewrite_filter.h
+  theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+  theory/quantifiers/cegqi/ceg_arith_instantiator.h
+  theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+  theory/quantifiers/cegqi/ceg_bv_instantiator.h
+  theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+  theory/quantifiers/cegqi/ceg_dt_instantiator.h
+  theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
+  theory/quantifiers/cegqi/ceg_epr_instantiator.h
+  theory/quantifiers/cegqi/ceg_instantiator.cpp
+  theory/quantifiers/cegqi/ceg_instantiator.h
+  theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+  theory/quantifiers/cegqi/inst_strategy_cbqi.h
+  theory/quantifiers/conjecture_generator.cpp
+  theory/quantifiers/conjecture_generator.h
+  theory/quantifiers/dynamic_rewrite.cpp
+  theory/quantifiers/dynamic_rewrite.h
+  theory/quantifiers/ematching/candidate_generator.cpp
+  theory/quantifiers/ematching/candidate_generator.h
+  theory/quantifiers/ematching/ho_trigger.cpp
+  theory/quantifiers/ematching/ho_trigger.h
+  theory/quantifiers/ematching/inst_match_generator.cpp
+  theory/quantifiers/ematching/inst_match_generator.h
+  theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+  theory/quantifiers/ematching/inst_strategy_e_matching.h
+  theory/quantifiers/ematching/instantiation_engine.cpp
+  theory/quantifiers/ematching/instantiation_engine.h
+  theory/quantifiers/ematching/trigger.cpp
+  theory/quantifiers/ematching/trigger.h
+  theory/quantifiers/equality_infer.cpp
+  theory/quantifiers/equality_infer.h
+  theory/quantifiers/equality_query.cpp
+  theory/quantifiers/equality_query.h
+  theory/quantifiers/extended_rewrite.cpp
+  theory/quantifiers/extended_rewrite.h
+  theory/quantifiers/first_order_model.cpp
+  theory/quantifiers/first_order_model.h
+  theory/quantifiers/fmf/ambqi_builder.cpp
+  theory/quantifiers/fmf/ambqi_builder.h
+  theory/quantifiers/fmf/bounded_integers.cpp
+  theory/quantifiers/fmf/bounded_integers.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_builder.h
+  theory/quantifiers/fmf/model_engine.cpp
+  theory/quantifiers/fmf/model_engine.h
+  theory/quantifiers/fun_def_process.cpp
+  theory/quantifiers/fun_def_process.h
+  theory/quantifiers/global_negate.cpp
+  theory/quantifiers/global_negate.h
+  theory/quantifiers/inst_match.cpp
+  theory/quantifiers/inst_match.h
+  theory/quantifiers/inst_match_trie.cpp
+  theory/quantifiers/inst_match_trie.h
+  theory/quantifiers/inst_propagator.cpp
+  theory/quantifiers/inst_propagator.h
+  theory/quantifiers/inst_strategy_enumerative.cpp
+  theory/quantifiers/inst_strategy_enumerative.h
+  theory/quantifiers/instantiate.cpp
+  theory/quantifiers/instantiate.h
+  theory/quantifiers/lazy_trie.cpp
+  theory/quantifiers/lazy_trie.h
+  theory/quantifiers/local_theory_ext.cpp
+  theory/quantifiers/local_theory_ext.h
+  theory/quantifiers/macros.cpp
+  theory/quantifiers/macros.h
+  theory/quantifiers/quant_conflict_find.cpp
+  theory/quantifiers/quant_conflict_find.h
+  theory/quantifiers/quant_epr.cpp
+  theory/quantifiers/quant_epr.h
+  theory/quantifiers/quant_relevance.cpp
+  theory/quantifiers/quant_relevance.h
+  theory/quantifiers/quant_split.cpp
+  theory/quantifiers/quant_split.h
+  theory/quantifiers/quant_util.cpp
+  theory/quantifiers/quant_util.h
+  theory/quantifiers/quantifiers_attributes.cpp
+  theory/quantifiers/quantifiers_attributes.h
+  theory/quantifiers/quantifiers_rewriter.cpp
+  theory/quantifiers/quantifiers_rewriter.h
+  theory/quantifiers/relevant_domain.cpp
+  theory/quantifiers/relevant_domain.h
+  theory/quantifiers/rewrite_engine.cpp
+  theory/quantifiers/rewrite_engine.h
+  theory/quantifiers/single_inv_partition.cpp
+  theory/quantifiers/single_inv_partition.h
+  theory/quantifiers/skolemize.cpp
+  theory/quantifiers/skolemize.h
+  theory/quantifiers/sygus/ce_guided_conjecture.cpp
+  theory/quantifiers/sygus/ce_guided_conjecture.h
+  theory/quantifiers/sygus/ce_guided_instantiation.cpp
+  theory/quantifiers/sygus/ce_guided_instantiation.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_unif.cpp
+  theory/quantifiers/sygus/cegis_unif.h
+  theory/quantifiers/sygus/sygus_eval_unfold.cpp
+  theory/quantifiers/sygus/sygus_eval_unfold.h
+  theory/quantifiers/sygus/sygus_explain.cpp
+  theory/quantifiers/sygus/sygus_explain.h
+  theory/quantifiers/sygus/sygus_grammar_cons.cpp
+  theory/quantifiers/sygus/sygus_grammar_cons.h
+  theory/quantifiers/sygus/sygus_grammar_norm.cpp
+  theory/quantifiers/sygus/sygus_grammar_norm.h
+  theory/quantifiers/sygus/sygus_grammar_red.cpp
+  theory/quantifiers/sygus/sygus_grammar_red.h
+  theory/quantifiers/sygus/sygus_invariance.cpp
+  theory/quantifiers/sygus/sygus_invariance.h
+  theory/quantifiers/sygus/sygus_module.cpp
+  theory/quantifiers/sygus/sygus_module.h
+  theory/quantifiers/sygus/sygus_pbe.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_repair_const.cpp
+  theory/quantifiers/sygus/sygus_repair_const.h
+  theory/quantifiers/sygus/sygus_unif.cpp
+  theory/quantifiers/sygus/sygus_unif.h
+  theory/quantifiers/sygus/sygus_unif_io.cpp
+  theory/quantifiers/sygus/sygus_unif_io.h
+  theory/quantifiers/sygus/sygus_unif_rl.cpp
+  theory/quantifiers/sygus/sygus_unif_rl.h
+  theory/quantifiers/sygus/sygus_unif_strat.cpp
+  theory/quantifiers/sygus/sygus_unif_strat.h
+  theory/quantifiers/sygus/term_database_sygus.cpp
+  theory/quantifiers/sygus/term_database_sygus.h
+  theory/quantifiers/sygus_inference.cpp
+  theory/quantifiers/sygus_inference.h
+  theory/quantifiers/sygus_sampler.cpp
+  theory/quantifiers/sygus_sampler.h
+  theory/quantifiers/term_database.cpp
+  theory/quantifiers/term_database.h
+  theory/quantifiers/term_enumeration.cpp
+  theory/quantifiers/term_enumeration.h
+  theory/quantifiers/term_util.cpp
+  theory/quantifiers/term_util.h
+  theory/quantifiers/theory_quantifiers.cpp
+  theory/quantifiers/theory_quantifiers.h
+  theory/quantifiers/theory_quantifiers_type_rules.h
+  theory/quantifiers_engine.cpp
+  theory/quantifiers_engine.h
+  theory/rep_set.cpp
+  theory/rep_set.h
+  theory/rewriter.cpp
+  theory/rewriter.h
+  theory/rewriter_attributes.h
+  theory/sep/theory_sep.cpp
+  theory/sep/theory_sep.h
+  theory/sep/theory_sep_rewriter.cpp
+  theory/sep/theory_sep_rewriter.h
+  theory/sep/theory_sep_type_rules.h
+  theory/sets/normal_form.h
+  theory/sets/rels_utils.h
+  theory/sets/theory_sets.cpp
+  theory/sets/theory_sets.h
+  theory/sets/theory_sets_private.cpp
+  theory/sets/theory_sets_private.h
+  theory/sets/theory_sets_rels.cpp
+  theory/sets/theory_sets_rels.h
+  theory/sets/theory_sets_rewriter.cpp
+  theory/sets/theory_sets_rewriter.h
+  theory/sets/theory_sets_type_enumerator.h
+  theory/sets/theory_sets_type_rules.h
+  theory/shared_terms_database.cpp
+  theory/shared_terms_database.h
+  theory/sort_inference.cpp
+  theory/sort_inference.h
+  theory/strings/regexp_operation.cpp
+  theory/strings/regexp_operation.h
+  theory/strings/theory_strings.cpp
+  theory/strings/theory_strings.h
+  theory/strings/theory_strings_preprocess.cpp
+  theory/strings/theory_strings_preprocess.h
+  theory/strings/theory_strings_rewriter.cpp
+  theory/strings/theory_strings_rewriter.h
+  theory/strings/theory_strings_type_rules.h
+  theory/strings/type_enumerator.h
+  theory/substitutions.cpp
+  theory/substitutions.h
+  theory/term_registration_visitor.cpp
+  theory/term_registration_visitor.h
+  theory/theory.cpp
+  theory/theory.h
+  theory/theory_engine.cpp
+  theory/theory_engine.h
+  theory/theory_model.cpp
+  theory/theory_model.h
+  theory/theory_model_builder.cpp
+  theory/theory_model_builder.h
+  theory/theory_registrar.h
+  theory/theory_test_utils.h
+  theory/type_enumerator.h
+  theory/type_set.cpp
+  theory/type_set.h
+  theory/uf/equality_engine.cpp
+  theory/uf/equality_engine.h
+  theory/uf/equality_engine_types.h
+  theory/uf/symmetry_breaker.cpp
+  theory/uf/symmetry_breaker.h
+  theory/uf/theory_uf.cpp
+  theory/uf/theory_uf.h
+  theory/uf/theory_uf_model.cpp
+  theory/uf/theory_uf_model.h
+  theory/uf/theory_uf_rewriter.h
+  theory/uf/theory_uf_strong_solver.cpp
+  theory/uf/theory_uf_strong_solver.h
+  theory/uf/theory_uf_type_rules.h
+  theory/unconstrained_simplifier.cpp
+  theory/unconstrained_simplifier.h
+  theory/valuation.cpp
+  theory/valuation.h
+)
+
+# Generated in theory/
+set(cvc4_gen_src_files
+  theory/rewriter_tables.h
+  theory/theory_traits.h
+  theory/type_enumerator.cpp
+)
+# Since these files are generated in a different CMakeLists.txt we have to
+# tell cmake that the files are generated.
+set_source_files_properties(${cvc4_gen_src_files} PROPERTIES GENERATED TRUE)
+
+add_library(cvc4 SHARED ${cvc4_src_files} ${cvc4_gen_src_files})
+set_target_properties(cvc4
+  PROPERTIES
+    COMPILE_DEFINITIONS
+      __BUILDING_CVC4LIB
+      __STDC_LIMIT_MACROS
+      __STDC_FORMAT_MACROS
+)
+add_dependencies(cvc4 gen-theory-files)
+target_link_libraries(cvc4
+  base bvminisat expr minisat options smtutil util replacements
+  ${LIBRARIES}
+)
+
+# TODO: if proofs: libsignatures
+
+include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
+include_directories(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
+include_directories(include ${CMAKE_CURRENT_BINARY_DIR}/include)
+include_directories(options ${CMAKE_CURRENT_BINARY_DIR}/options)
+
+add_subdirectory(base)
 #add_subdirectory(bindings)
-#add_subdirectory(compat)
-#add_subdirectory(context)
-#add_subdirectory(decision)
-#add_subdirectory(expr)
-#add_subdirectory(lib)
-#add_subdirectory(main)
-#add_subdirectory(options)
-#add_subdirectory(parser)
-#add_subdirectory(printer)
-#add_subdirectory(proof)
-#add_subdirectory(prop)
-#add_subdirectory(smt)
-#add_subdirectory(smt_util)
-#add_subdirectory(theory)
-#add_subdirectory(util)
+add_subdirectory(compat)
+add_subdirectory(expr)
+add_subdirectory(lib)
+add_subdirectory(main)
+add_subdirectory(options)
+add_subdirectory(parser)
+add_subdirectory(prop/bvminisat)
+add_subdirectory(prop/minisat)
+add_subdirectory(smt_util)
+add_subdirectory(theory)
+add_subdirectory(util)
+

diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index cf4e554cc69cf14b5fac2927caae6f8f62ef4afa..810ffa2538af237556042b14299c24be3cf98710 100644 (file)
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -1,3 +1,26 @@
+set(base_src_files
+  configuration.cpp
+  configuration.h
+  configuration_private.h
+  cvc4_assert.cpp
+  cvc4_assert.h
+  cvc4_check.cpp
+  cvc4_check.h
+  exception.cpp
+  exception.h
+  listener.cpp
+  listener.h
+  modal_exception.h
+  output.cpp
+  output.h
+)
+
+add_library(base SHARED ${base_src_files})
+set_target_properties(base PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)
+
+#
+# Generate code for debug/trace tags
+#
 set(mktags_script ${CMAKE_CURRENT_LIST_DIR}/mktags)
 set(mktagheaders_script ${CMAKE_CURRENT_LIST_DIR}/mktagheaders)
 file(GLOB_RECURSE source_files ${PROJECT_SOURCE_DIR}/src/*.cpp ${PROJECT_SOURCE_DIR}/src/*.cc ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.g)

diff --git a/src/compat/CMakeLists.txt b/src/compat/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..92b6aabfa3ab0ff71128d97685ddb616b9d1e887 100644 (file)
--- a/src/compat/CMakeLists.txt
+++ b/src/compat/CMakeLists.txt
@@ -0,0 +1,9 @@
+set(compat_src_files
+  cvc3_compat.cpp
+  cvc3_compat.h
+)
+
+add_library(cvc4compat SHARED ${compat_src_files})
+set_target_properties(cvc4compat
+  PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4COMPATLIB)
+target_link_libraries(cvc4compat cvc4)

diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
deleted file mode 100644 (file)
index e69de29..0000000

diff --git a/src/decision/CMakeLists.txt b/src/decision/CMakeLists.txt
deleted file mode 100644 (file)
index e69de29..0000000

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index c0f75d918f02501131a76aeb9e998b60e58478a0..a2e55f8748cdaadd52630b32a9898cb75122e9a7 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -1,3 +1,71 @@
+set(expr_src_files
+  array.h
+  array_store_all.cpp
+  array_store_all.h
+  ascription_type.h
+  attribute.h
+  attribute.cpp
+  attribute_internals.h
+  attribute_unique_id.h
+  chain.h
+  emptyset.cpp
+  emptyset.h
+  expr_iomanip.cpp
+  expr_iomanip.h
+  expr_manager_scope.h
+  expr_stream.h
+  kind_map.h
+  matcher.h
+  node.cpp
+  node.h
+  node_builder.h
+  node_manager.cpp
+  node_manager.h
+  node_manager_attributes.h
+  node_manager_listeners.cpp
+  node_manager_listeners.h
+  node_self_iterator.h
+  node_value.cpp
+  node_value.h
+  pickle_data.cpp
+  pickle_data.h
+  pickler.cpp
+  pickler.h
+  symbol_table.cpp
+  symbol_table.h
+  type.cpp
+  type.h
+  type_checker.h
+  type_node.cpp
+  type_node.h
+  variable_type_map.h
+  datatype.h
+  datatype.cpp
+  record.cpp
+  record.h
+  uninterpreted_constant.cpp
+  uninterpreted_constant.h
+)
+
+set(expr_gen_src_files
+  kind.cpp
+  kind.h
+  metakind.cpp
+  metakind.h
+  expr.cpp
+  expr.h
+  expr_manager.cpp
+  expr_manager.h
+  type_checker.cpp
+  type_properties.h
+)
+
+add_library(expr SHARED ${expr_src_files} ${expr_gen_src_files})
+set_target_properties(expr PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)
+
+#
+# Generate code for kinds.
+#
 file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
 
 set(mkkind_script ${CMAKE_CURRENT_LIST_DIR}/mkkind)
@@ -5,111 +73,101 @@ set(mkmetakind_script ${CMAKE_CURRENT_LIST_DIR}/mkmetakind)
 set(mkexpr_script ${CMAKE_CURRENT_LIST_DIR}/mkexpr)
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
-    DEPENDS mkkind kind_template.h
-    OUTPUT kind.h
-    COMMENT "Generating kind.h."
+  OUTPUT kind.h
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
+  DEPENDS mkkind kind_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
-    DEPENDS mkkind kind_template.cpp kind.h
-    OUTPUT kind.cpp
-    COMMENT "Generating kind.cpp."
+  OUTPUT kind.cpp
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
+  DEPENDS mkkind kind_template.cpp kind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
-    DEPENDS mkkind type_properties_template.h
-    OUTPUT type_properties.h
-    COMMENT "Generating type_properties.h."
+  OUTPUT type_properties.h
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
+  DEPENDS mkkind type_properties_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkmetakind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
-    DEPENDS mkmetakind metakind_template.h
-    OUTPUT metakind.h
-    COMMENT "Generating metakind.h."
+  OUTPUT metakind.h
+  COMMAND
+    ${mkmetakind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
+  DEPENDS mkmetakind metakind_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkmetakind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
-    DEPENDS mkmetakind metakind_template.cpp metakind.h
-    OUTPUT metakind.cpp
-    COMMENT "Generating metakind.cpp."
+  OUTPUT metakind.cpp
+  COMMAND
+    ${mkmetakind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
+  DEPENDS mkmetakind metakind_template.cpp metakind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
-    DEPENDS mkexpr expr_template.h kind.h
-    OUTPUT expr.h
-    COMMENT "Generating expr.h."
+  OUTPUT expr.h
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
+  DEPENDS mkexpr expr_template.h kind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
-    DEPENDS mkexpr expr_template.cpp expr.h
-    OUTPUT expr.cpp
-    COMMENT "Generating expr.cpp."
+  OUTPUT expr.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
+  DEPENDS mkexpr expr_template.cpp expr.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
-    DEPENDS mkexpr expr_manager_template.h expr.h
-    OUTPUT expr_manager.h
-    COMMENT "Generating expr_manager.h."
+  OUTPUT expr_manager.h
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
+  DEPENDS mkexpr expr_manager_template.h expr.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
-    DEPENDS mkexpr expr_manager_template.cpp expr_manager.h
-    OUTPUT expr_manager.cpp
-    COMMENT "Generating expr_manager.cpp."
+  OUTPUT expr_manager.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
+  DEPENDS mkexpr expr_manager_template.cpp expr_manager.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
-    DEPENDS mkexpr type_checker_template.cpp
-    OUTPUT type_checker.cpp
-    COMMENT "Generating type_checker.cpp."
+  OUTPUT type_checker.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
+  DEPENDS mkexpr type_checker_template.cpp
 )

diff --git a/src/lib/CMakeLists.txt b/src/lib/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..b56a0bb821c5dbd2e7c255efb7ad0e242cb60691 100644 (file)
--- a/src/lib/CMakeLists.txt
+++ b/src/lib/CMakeLists.txt
@@ -0,0 +1,12 @@
+set(replacements_src_files
+  clock_gettime.c
+  clock_gettime.h
+  ffs.c
+  ffs.h
+  replacements.h
+  strtok_r.c
+  strtok_r.h
+)
+
+add_library(replacements SHARED ${replacements_src_files})
+set_target_properties(replacements PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..1a586f8348533e9f7808f0beff2456ca8fbae8c7 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -0,0 +1,36 @@
+set(libmain_src_files
+  interactive_shell.cpp
+  interactive_shell.h
+  main.h
+  util.cpp
+)
+
+add_library(main SHARED ${libmain_src_files})
+set_target_properties(main PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4DRIVER)
+target_link_libraries(main cvc4 cvc4parser)
+
+set(cvc4main_src_files
+  command_executor.cpp
+  driver_unified.cpp
+  main.cpp
+)
+
+add_executable(cvc4-main ${cvc4main_src_files})
+set_target_properties(cvc4-main
+  PROPERTIES
+    OUTPUT_NAME cvc4
+    COMPILE_DEFINITIONS __BUILDING_CVC4DRIVER)
+target_link_libraries(cvc4-main main) #cvc4 cvc4parser replacements)
+
+#set(pcvc4_src_files
+#  main.cpp
+#  portfolio.cpp
+#  portfolio.h
+#  portfolio_util.cpp
+#  portfolio_util.h
+#  command_executor.cpp
+#  command_executor_portfolio.cpp
+#  command_executor.h
+#  command_executor_portfolio.h
+#  driver_unified.cpp
+#)

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 89f6ff16ef08da9bc69725e22e734233221ad3b9..5fcc22bd933cb8b579f05f13984d16e29f865344 100644 (file)
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -33,12 +33,13 @@ set(options_toml_files
   uf_options.toml
 )
 
-string(REPLACE "toml" "cpp;" options_cpp_files ${options_toml_files})
-string(REPLACE "toml" "h;"   options_h_files ${options_toml_files})
+string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
+string(REPLACE "toml" "h;"   options_gen_h_files ${options_toml_files})
 
 prepend_path(${options_toml_files})
 
 add_custom_command(
+    OUTPUT options.cpp options_holder.h ${options_gen_cpp_files} ${options_gen_h_files}
     COMMAND
       ${PYTHON_EXECUTABLE}
       ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py
@@ -46,9 +47,59 @@ add_custom_command(
       ${CMAKE_CURRENT_BINARY_DIR}/../../doc
       ${CMAKE_CURRENT_BINARY_DIR}
       ${PREPEND_PATH_SOURCES}
-    DEPENDS mkoptions.py ${options_toml_files}
-    OUTPUT ${options_cpp_files} ${options_h_files}
-    COMMENT "Generating code for options."
+    DEPENDS
+      mkoptions.py
+      ${options_toml_files}
+      module_template.h
+      module_template.cpp
+      options_holder_template.h
+      options_template.cpp
+      ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc4.1_template
+      ${CMAKE_CURRENT_BINARY_DIR}/../../doc/SmtEngine.3cvc_template
+      ${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template
 )
 
-#add_library(options STATIC ${options_cpp_files})
+set(options_src_files
+  argument_extender.h
+  argument_extender_implementation.cpp
+  argument_extender_implementation.h
+  arith_heuristic_pivot_rule.cpp
+  arith_heuristic_pivot_rule.h
+  arith_propagation_mode.cpp
+  arith_propagation_mode.h
+  arith_unate_lemma_mode.cpp
+  arith_unate_lemma_mode.h
+  base_handlers.h
+  bv_bitblast_mode.cpp
+  bv_bitblast_mode.h
+  datatypes_modes.h
+  decision_mode.cpp
+  decision_mode.h
+  decision_weight.h
+  didyoumean.cpp
+  didyoumean.h
+  language.cpp
+  language.h
+  open_ostream.cpp
+  open_ostream.h
+  option_exception.h
+  options.h
+  options_handler.cpp
+  options_handler.h
+  options_public_functions.cpp
+  printer_modes.cpp
+  printer_modes.h
+  quantifiers_modes.cpp
+  quantifiers_modes.h
+  set_language.cpp
+  set_language.h
+  simplification_mode.cpp
+  simplification_mode.h
+  sygus_out_mode.h
+  theoryof_mode.cpp
+  theoryof_mode.h
+  ufss_mode.h
+)
+
+add_library(options SHARED options.cpp ${options_gen_cpp_files} ${options_src_files})
+set_target_properties(options PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index f3a045e02a05a0b4798f7efb8bf9506c51ccb54f..8f801466c27a3b7823bd6e1aa341079e8027925a 100755 (executable)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -303,10 +303,8 @@ def write_file(directory, name, content):
         if os.path.isfile(fname):
             with open(fname, 'r') as file:
                 if content == file.read():
-                    print('{} is up-to-date'.format(name))
                     return
         with open(fname, 'w') as file:
-            print('generated {}'.format(name))
             file.write(content)
     except IOError:
         die("Could not write '{}'".format(fname))

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index dcb580d8f797b71d5d274103a9d34a7d5c191eed..8c0a65fa79422699f1a786d5f19044671e20cb9a 100644 (file)
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -1,3 +1,32 @@
+set(cvc4parser_src_files
+  antlr_input.cpp
+  antlr_input.h
+  antlr_input_imports.cpp
+  antlr_line_buffered_input.cpp
+  antlr_line_buffered_input.h
+  antlr_tracing.h
+  antlr_undefines.h
+  bounded_token_buffer.cpp
+  bounded_token_buffer.h
+  bounded_token_factory.cpp
+  bounded_token_factory.h
+  input.cpp
+  input.h
+  line_buffer.cpp
+  line_buffer.h
+  memory_mapped_input_buffer.cpp
+  memory_mapped_input_buffer.h
+  parser.cpp
+  parser.h
+  parser_builder.cpp
+  parser_builder.h
+  parser_exception.h
+)
+
+add_library(cvc4parser SHARED ${cvc4parser_src_files})
+set_target_properties(cvc4parser PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4PARSERLIB)
+target_link_libraries(cvc4parser parsercvc parsersmt1 parsersmt2 parsertptp cvc4)
+
 add_subdirectory(cvc)
 add_subdirectory(smt1)
 add_subdirectory(smt2)

diff --git a/src/parser/cvc/CMakeLists.txt b/src/parser/cvc/CMakeLists.txt
index 1f176cfb627186ae4f9abc170381395c902e0e02..8f27cbb2555e1cb16a064ca23bb783b2684e7d20 100644 (file)
--- a/src/parser/cvc/CMakeLists.txt
+++ b/src/parser/cvc/CMakeLists.txt
@@ -1,9 +1,25 @@
-add_custom_target(AntlrCvc
+set(parser_cvc_src_files
+  cvc_input.cpp
+  cvc_input.h
+)
+
+set(parser_cvc_gen_src_files
+  CvcLexer.c
+  CvcParser.c
+)
+
+add_custom_command(
+  OUTPUT ${parser_cvc_gen_src_files} CvcLexer.h CvcParser.h Cvc.tokens
   COMMAND
     ${ANTLR_BINARY}
       ${CMAKE_CURRENT_SOURCE_DIR}/Cvc.g
       -fo ${CMAKE_CURRENT_BINARY_DIR}
+      2> /dev/null # Ignore Antlr3 warnings
   DEPENDS
     Cvc.g
 )
-#add_dependencies(... AntlrCvc)
+
+add_library(parsercvc SHARED ${parser_cvc_src_files} ${parser_cvc_gen_src_files})
+set_target_properties(parsercvc PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4PARSERLIB)
+set_source_files_properties(${parser_cvc_gen_src_files} PROPERTIES LANGUAGE CXX)
+add_dependencies(parsercvc expr)

diff --git a/src/parser/smt1/CMakeLists.txt b/src/parser/smt1/CMakeLists.txt
index f219d85d923e6ed6e51bc3e3d055d37d6ea96ffa..89f440e8ed2edb51eca14425effc3ac6d01783bf 100644 (file)
--- a/src/parser/smt1/CMakeLists.txt
+++ b/src/parser/smt1/CMakeLists.txt
@@ -1,9 +1,27 @@
-add_custom_target(AntlrSmt1
+set(parser_smt1_src_files
+  smt1.cpp
+  smt1.h
+  smt1_input.cpp
+  smt1_input.h
+)
+
+set(parser_smt1_gen_src_files
+  Smt1Lexer.c
+  Smt1Parser.c
+)
+
+add_custom_command(
+  OUTPUT ${parser_smt1_gen_src_files} Smt1Lexer.h Smt1Parser.h Smt1.tokens
   COMMAND
     ${ANTLR_BINARY}
       ${CMAKE_CURRENT_SOURCE_DIR}/Smt1.g
       -fo ${CMAKE_CURRENT_BINARY_DIR}
+      2> /dev/null # Ignore Antlr3 warnings
   DEPENDS
     Smt1.g
 )
-#add_dependencies(... AntlrSmt1)
+
+add_library(parsersmt1 SHARED ${parser_smt1_src_files} ${parser_smt1_gen_src_files})
+set_target_properties(parsersmt1 PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4PARSERLIB)
+set_source_files_properties(${parser_smt1_gen_src_files} PROPERTIES LANGUAGE CXX)
+add_dependencies(parsersmt1 expr)

diff --git a/src/parser/smt2/CMakeLists.txt b/src/parser/smt2/CMakeLists.txt
index d35f500bb81affab5ff3d779ba758c207ee31e83..b046a6767b6bc787432c4ad798e00459d82b3be3 100644 (file)
--- a/src/parser/smt2/CMakeLists.txt
+++ b/src/parser/smt2/CMakeLists.txt
@@ -1,9 +1,29 @@
-add_custom_target(AntlrSmt2
+set(parser_smt2_src_files
+  smt2.cpp
+  smt2.h
+  smt2_input.cpp
+  smt2_input.h
+  sygus_input.cpp
+  sygus_input.h
+)
+
+set(parser_smt2_gen_src_files
+  Smt2Lexer.c
+  Smt2Parser.c
+)
+
+add_custom_command(
+  OUTPUT ${parser_smt2_gen_src_files} Smt2Lexer.h Smt2Parser.h Smt2.tokens
   COMMAND
     ${ANTLR_BINARY}
       ${CMAKE_CURRENT_SOURCE_DIR}/Smt2.g
       -fo ${CMAKE_CURRENT_BINARY_DIR}
+      2> /dev/null # Ignore Antlr3 warnings
   DEPENDS
     Smt2.g
 )
-#add_dependencies(... AntlrSmt2)
+
+add_library(parsersmt2 SHARED ${parser_smt2_src_files} ${parser_smt2_gen_src_files})
+set_target_properties(parsersmt2 PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4PARSERLIB)
+set_source_files_properties(${parser_smt2_gen_src_files} PROPERTIES LANGUAGE CXX)
+add_dependencies(parsersmt2 expr)

diff --git a/src/parser/tptp/CMakeLists.txt b/src/parser/tptp/CMakeLists.txt
index bee38ce87f944f8a7d41281465e035a355f99541..22593e7b2779d1271c3b2053bd7ed17696556adb 100644 (file)
--- a/src/parser/tptp/CMakeLists.txt
+++ b/src/parser/tptp/CMakeLists.txt
@@ -1,9 +1,27 @@
-add_custom_target(AntlrTptp
+set(parser_tptp_src_files
+  tptp.cpp
+  tptp.h
+  tptp_input.cpp
+  tptp_input.h
+)
+
+set(parser_tptp_gen_src_files
+  TptpLexer.c
+  TptpParser.c
+)
+
+add_custom_command(
+  OUTPUT ${parser_tptp_gen_src_files} TptpLexer.h TptpParser.h Tptp.tokens
   COMMAND
     ${ANTLR_BINARY}
       ${CMAKE_CURRENT_SOURCE_DIR}/Tptp.g
       -fo ${CMAKE_CURRENT_BINARY_DIR}
+      2> /dev/null # Ignore Antlr3 warnings
   DEPENDS
     Tptp.g
 )
-#add_dependencies(... AntlrTptp)
+
+add_library(parsertptp SHARED ${parser_tptp_src_files} ${parser_tptp_gen_src_files})
+set_target_properties(parsertptp PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4PARSERLIB)
+set_source_files_properties(${parser_tptp_gen_src_files} PROPERTIES LANGUAGE CXX)
+add_dependencies(parsertptp expr)

diff --git a/src/prop/bvminisat/CMakeLists.txt b/src/prop/bvminisat/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..f55d74c486ffb782ffe32e404b0a766ffc68cfb1 100644 (file)
--- a/src/prop/bvminisat/CMakeLists.txt
+++ b/src/prop/bvminisat/CMakeLists.txt
@@ -0,0 +1,31 @@
+set(bvminisat_src_files
+  bvminisat.cpp
+  bvminisat.h
+  core/Dimacs.h
+  core/Solver.cc
+  core/Solver.h
+  core/SolverTypes.h
+  mtl/Alg.h
+  mtl/Alloc.h
+  mtl/Heap.h
+  mtl/IntTypes.h
+  mtl/Map.h
+  mtl/Queue.h
+  mtl/Sort.h
+  mtl/Vec.h
+  mtl/XAlloc.h
+  simp/SimpSolver.cc
+  simp/SimpSolver.h
+  utils/Options.h
+)
+
+include_directories(.)
+add_library(bvminisat SHARED ${bvminisat_src_files})
+set_target_properties(bvminisat
+  PROPERTIES
+    COMPILE_DEFINITIONS
+      __BUILDING_CVC4LIB
+      __STDC_LIMIT_MACROS
+      __STDC_FORMAT_MACROS
+)
+add_dependencies(bvminisat expr)

diff --git a/src/prop/minisat/CMakeLists.txt b/src/prop/minisat/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..137b15766a8ae89653bb6aa1cc8fff0527f2a990 100644 (file)
--- a/src/prop/minisat/CMakeLists.txt
+++ b/src/prop/minisat/CMakeLists.txt
@@ -0,0 +1,31 @@
+set(minisat_src_files
+  core/Dimacs.h
+  core/Solver.cc
+  core/Solver.h
+  core/SolverTypes.h
+  minisat.cpp
+  minisat.h
+  mtl/Alg.h
+  mtl/Alloc.h
+  mtl/Heap.h
+  mtl/IntTypes.h
+  mtl/Map.h
+  mtl/Queue.h
+  mtl/Sort.h
+  mtl/Vec.h
+  mtl/XAlloc.h
+  simp/SimpSolver.cc
+  simp/SimpSolver.h
+  utils/Options.h
+)
+
+include_directories(.)
+add_library(minisat SHARED ${minisat_src_files})
+set_target_properties(minisat
+  PROPERTIES
+    COMPILE_DEFINITIONS
+      __BUILDING_CVC4LIB
+      __STDC_LIMIT_MACROS
+      __STDC_FORMAT_MACROS
+)
+add_dependencies(minisat expr)

diff --git a/src/smt_util/CMakeLists.txt b/src/smt_util/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..9934db3505d4b1e98c1bd39e5d2473b1eccb3946 100644 (file)
--- a/src/smt_util/CMakeLists.txt
+++ b/src/smt_util/CMakeLists.txt
@@ -0,0 +1,15 @@
+set(smtutil_src_files
+  boolean_simplification.cpp
+  boolean_simplification.h
+  lemma_channels.cpp
+  lemma_channels.h
+  lemma_input_channel.h
+  lemma_output_channel.h
+  nary_builder.cpp
+  nary_builder.h
+  node_visitor.h
+)
+
+add_library(smtutil SHARED ${smtutil_src_files})
+set_target_properties(smtutil PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)
+target_link_libraries(smtutil expr)

diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt
index 43592c48ba08cd0392b108c8b7447bbdcd9d67f2..ab6dd580fb3013be1500338c71e357c70edf5507 100644 (file)
--- a/src/theory/CMakeLists.txt
+++ b/src/theory/CMakeLists.txt
@@ -4,34 +4,36 @@ set(mktheorytraits_script ${CMAKE_CURRENT_LIST_DIR}/mktheorytraits)
 set(mkrewriter_script ${CMAKE_CURRENT_LIST_DIR}/mkrewriter)
 
 add_custom_command(
-    COMMAND
-      ${mkrewriter_script}
-      ${CMAKE_CURRENT_LIST_DIR}/rewriter_tables_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tables.h
-    DEPENDS mkrewriter rewriter_tables_template.h
-    OUTPUT rewriter_tables.h
-      COMMENT "Generating rewriter_tables.h."
+  OUTPUT rewriter_tables.h
+  COMMAND
+    ${mkrewriter_script}
+    ${CMAKE_CURRENT_LIST_DIR}/rewriter_tables_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tables.h
+  DEPENDS mkrewriter rewriter_tables_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mktheorytraits_script}
-      ${CMAKE_CURRENT_LIST_DIR}/theory_traits_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/theory_traits.h
-    DEPENDS mktheorytraits theory_traits_template.h
-    OUTPUT theory_traits.h
-    COMMENT "Generating theory_traits.h."
+  OUTPUT theory_traits.h
+  COMMAND
+    ${mktheorytraits_script}
+    ${CMAKE_CURRENT_LIST_DIR}/theory_traits_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/theory_traits.h
+  DEPENDS mktheorytraits theory_traits_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mktheorytraits_script}
-      ${CMAKE_CURRENT_LIST_DIR}/type_enumerator_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/type_enumerator.cpp
-    DEPENDS mktheorytraits type_enumerator_template.cpp
-    OUTPUT type_enumerator.cpp
-    COMMENT "Generating type_enumerator.cpp."
+  OUTPUT type_enumerator.cpp
+  COMMAND
+    ${mktheorytraits_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_enumerator_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_enumerator.cpp
+  DEPENDS mktheorytraits type_enumerator_template.cpp
+)
+
+add_custom_target(
+  gen-theory-files
+  DEPENDS type_enumerator.cpp theory_traits.h rewriter_tables.h
 )

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 5ea76962c2c797c2c616bf5b4ddd5dfda9d589e5..24022dd40a4cd3fa32ea93080373b471799afc2e 100644 (file)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,7 +1,77 @@
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/src/util/rational.h.in
-  ${CMAKE_CURRENT_BINARY_DIR}/src/util/rational.h)
+  ${CMAKE_CURRENT_SOURCE_DIR}/floatingpoint.h.in
+  ${CMAKE_CURRENT_BINARY_DIR}/floatingpoint.h)
 
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/src/util/integer.h.in
-  ${CMAKE_CURRENT_BINARY_DIR}/src/util/integer.h)
+  ${CMAKE_CURRENT_SOURCE_DIR}/rational.h.in
+  ${CMAKE_CURRENT_BINARY_DIR}/rational.h)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/integer.h.in
+  ${CMAKE_CURRENT_BINARY_DIR}/integer.h)
+
+set(util_src_files
+  abstract_value.cpp
+  abstract_value.h
+  bin_heap.h
+  bitvector.cpp
+  bitvector.h
+  bool.h
+  cardinality.cpp
+  cardinality.h
+  channel.h
+  debug.h
+  dense_map.h
+  divisible.cpp
+  divisible.h
+  dynamic_array.h
+  floatingpoint.cpp
+  gmp_util.h
+  hash.h
+  index.cpp
+  index.h
+  maybe.h
+  ntuple.h
+  ostream_util.cpp
+  ostream_util.h
+  proof.h
+  random.cpp
+  random.h
+  regexp.cpp
+  regexp.h
+  resource_manager.cpp
+  resource_manager.h
+  result.cpp
+  result.h
+  safe_print.cpp
+  safe_print.h
+  sampler.cpp
+  sampler.h
+  sexpr.cpp
+  sexpr.h
+  smt2_quote_string.cpp
+  smt2_quote_string.h
+  statistics.cpp
+  statistics.h
+  statistics_registry.cpp
+  statistics_registry.h
+  tuple.h
+  unsafe_interrupt_exception.h
+  utility.h
+)
+
+#TODO: if CVC4_CLN_IMP
+#list(APPEND util_src_files
+#  rational_cln_imp.cpp
+#  integer_cln_imp.cpp
+#)
+
+
+#TODO: if CVC4_GMP_IMP
+list(APPEND util_src_files
+  rational_gmp_imp.cpp
+  integer_gmp_imp.cpp
+)
+
+add_library(util SHARED ${util_src_files})
+set_target_properties(util PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)