diff options
| -rw-r--r-- | CMakeLists.txt | 45 | ||||
| -rw-r--r-- | doc/CMakeLists.txt | 27 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 618 | ||||
| -rw-r--r-- | src/base/CMakeLists.txt | 23 | ||||
| -rw-r--r-- | src/compat/CMakeLists.txt | 9 | ||||
| -rw-r--r-- | src/context/CMakeLists.txt | 0 | ||||
| -rw-r--r-- | src/decision/CMakeLists.txt | 0 | ||||
| -rw-r--r-- | src/expr/CMakeLists.txt | 218 | ||||
| -rw-r--r-- | src/lib/CMakeLists.txt | 12 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 36 | ||||
| -rw-r--r-- | src/options/CMakeLists.txt | 63 | ||||
| -rwxr-xr-x | src/options/mkoptions.py | 2 | ||||
| -rw-r--r-- | src/parser/CMakeLists.txt | 29 | ||||
| -rw-r--r-- | src/parser/cvc/CMakeLists.txt | 20 | ||||
| -rw-r--r-- | src/parser/smt1/CMakeLists.txt | 22 | ||||
| -rw-r--r-- | src/parser/smt2/CMakeLists.txt | 24 | ||||
| -rw-r--r-- | src/parser/tptp/CMakeLists.txt | 22 | ||||
| -rw-r--r-- | src/prop/bvminisat/CMakeLists.txt | 31 | ||||
| -rw-r--r-- | src/prop/minisat/CMakeLists.txt | 31 | ||||
| -rw-r--r-- | src/smt_util/CMakeLists.txt | 15 | ||||
| -rw-r--r-- | src/theory/CMakeLists.txt | 50 | ||||
| -rw-r--r-- | src/util/CMakeLists.txt | 78 |
22 files changed, 1199 insertions, 176 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index b93868fea..2cb86b259 100644 --- 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 index 000000000..bbde816e4 --- /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 500900bb1..e1e03bd97 100644 --- 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 cf4e554cc..810ffa253 100644 --- 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 e69de29bb..92b6aabfa 100644 --- 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 index e69de29bb..000000000 --- a/src/context/CMakeLists.txt +++ /dev/null diff --git a/src/decision/CMakeLists.txt b/src/decision/CMakeLists.txt deleted file mode 100644 index e69de29bb..000000000 --- a/src/decision/CMakeLists.txt +++ /dev/null diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index c0f75d918..a2e55f874 100644 --- 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 e69de29bb..b56a0bb82 100644 --- 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 e69de29bb..1a586f834 100644 --- 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 89f6ff16e..5fcc22bd9 100644 --- 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 f3a045e02..8f801466c 100755 --- 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 dcb580d8f..8c0a65fa7 100644 --- 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 1f176cfb6..8f27cbb25 100644 --- 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 f219d85d9..89f440e8e 100644 --- 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 d35f500bb..b046a6767 100644 --- 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 bee38ce87..22593e7b2 100644 --- 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 e69de29bb..f55d74c48 100644 --- 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 e69de29bb..137b15766 100644 --- 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 e69de29bb..9934db350 100644 --- 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 43592c48b..ab6dd580f 100644 --- 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 5ea76962c..24022dd40 100644 --- 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) |