diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-10-19 14:45:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-19 14:45:42 -0700 |
commit | ce8c429281fd1f7e4ac4d2b7133152c1d370df0c (patch) | |
tree | 407400e728621cc9a5262e7112a93bd6acd0835a /src | |
parent | 7de0540252b62080ee9f98617f5718cb1ae08579 (diff) |
Remove autotools build system. (#2639)
Diffstat (limited to 'src')
41 files changed, 0 insertions, 2377 deletions
diff --git a/src/Makefile b/src/Makefile deleted file mode 100644 index dc23e2272..000000000 --- a/src/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = .. -srcdir = src - -include $(topdir)/Makefile.subdir diff --git a/src/Makefile.am b/src/Makefile.am deleted file mode 100644 index d29dcd172..000000000 --- a/src/Makefile.am +++ /dev/null @@ -1,864 +0,0 @@ -# LIBCVC4_VERSION (-version-info) is in the form current:revision:age -# -# current - -# increment if interfaces have been added, removed or changed -# revision - -# increment if source code has changed -# set to zero if current is incremented -# age - -# increment if interfaces have been added -# set to zero if interfaces have been removed -# or changed -# -LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@ -I@srcdir@/include -I@srcdir@ -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) - -SUBDIRS = lib base options util expr smt_util prop/minisat prop/bvminisat . parser bindings main -# The THEORIES list has been moved to Makefile.theories -include @top_srcdir@/src/Makefile.theories - -lib_LTLIBRARIES = libcvc4.la - -libcvc4_la_LDFLAGS = \ - -no-undefined \ - -version-info $(LIBCVC4_VERSION) - -# This "tricks" automake into linking us as a C++ library (rather than -# as a C library, which messes up exception handling support) -nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp -libcvc4_la_SOURCES = \ - git_versioninfo.cpp \ - api/cvc4cpp.h \ - api/cvc4cppkind.h \ - api/cvc4cpp.cpp \ - 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/assertion_pipeline.cpp \ - preprocessing/assertion_pipeline.h \ - preprocessing/passes/apply_substs.cpp \ - preprocessing/passes/apply_substs.h \ - preprocessing/passes/apply_to_const.cpp \ - preprocessing/passes/apply_to_const.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_eager_atoms.cpp \ - preprocessing/passes/bv_eager_atoms.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/extended_rewriter_pass.cpp \ - preprocessing/passes/extended_rewriter_pass.h \ - preprocessing/passes/global_negate.cpp \ - preprocessing/passes/global_negate.h \ - preprocessing/passes/int_to_bv.cpp \ - preprocessing/passes/int_to_bv.h \ - preprocessing/passes/ite_removal.cpp \ - preprocessing/passes/ite_removal.h \ - preprocessing/passes/ite_simp.cpp \ - preprocessing/passes/ite_simp.h \ - preprocessing/passes/non_clausal_simp.cpp \ - preprocessing/passes/non_clausal_simp.h \ - preprocessing/passes/nl_ext_purify.cpp \ - preprocessing/passes/nl_ext_purify.h \ - preprocessing/passes/pseudo_boolean_processor.cpp \ - preprocessing/passes/pseudo_boolean_processor.h \ - preprocessing/passes/miplib_trick.cpp \ - preprocessing/passes/miplib_trick.h \ - preprocessing/passes/quantifier_macros.cpp \ - preprocessing/passes/quantifier_macros.h \ - preprocessing/passes/quantifiers_preprocess.cpp \ - preprocessing/passes/quantifiers_preprocess.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/sort_infer.cpp \ - preprocessing/passes/sort_infer.h \ - preprocessing/passes/static_learning.cpp \ - preprocessing/passes/static_learning.h \ - preprocessing/passes/sygus_inference.cpp \ - preprocessing/passes/sygus_inference.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/passes/theory_preprocess.cpp \ - preprocessing/passes/theory_preprocess.h \ - preprocessing/passes/unconstrained_simplifier.cpp \ - preprocessing/passes/unconstrained_simplifier.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 \ - preprocessing/util/ite_utilities.cpp \ - preprocessing/util/ite_utilities.h \ - printer/dagification_visitor.cpp \ - printer/dagification_visitor.h \ - printer/printer.cpp \ - printer/printer.h \ - printer/sygus_print_callback.cpp \ - printer/sygus_print_callback.h \ - printer/ast/ast_printer.cpp \ - printer/ast/ast_printer.h \ - printer/cvc/cvc_printer.cpp \ - printer/cvc/cvc_printer.h \ - printer/smt2/smt2_printer.cpp \ - printer/smt2/smt2_printer.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/lfsc_proof_printer.cpp \ - proof/lfsc_proof_printer.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/model_core_builder.cpp \ - smt/model_core_builder.h \ - smt/smt_engine.cpp \ - smt/smt_engine.h \ - smt/smt_engine_check_proof.cpp \ - smt/smt_engine_scope.cpp \ - smt/smt_engine_scope.h \ - smt/smt_statistics_registry.cpp \ - smt/smt_statistics_registry.h \ - smt/term_formula_removal.cpp \ - smt/term_formula_removal.h \ - smt/update_ostream.h \ - theory/assertion.cpp \ - theory/assertion.h \ - theory/atom_requests.cpp \ - theory/atom_requests.h \ - theory/care_graph.h \ - theory/evaluator.cpp \ - theory/evaluator.h \ - theory/interrupted.h \ - theory/logic_info.cpp \ - theory/logic_info.h \ - theory/output_channel.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/shared_terms_database.cpp \ - theory/shared_terms_database.h \ - theory/sort_inference.cpp \ - theory/sort_inference.h \ - theory/substitutions.cpp \ - theory/substitutions.h \ - theory/subs_minimize.cpp \ - theory/subs_minimize.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/valuation.cpp \ - theory/valuation.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.h \ - theory/arith/nonlinear_extension.cpp \ - 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/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/datatypes/datatypes_rewriter.cpp \ - theory/datatypes/datatypes_rewriter.h \ - theory/datatypes/datatypes_sygus.cpp \ - theory/datatypes/datatypes_sygus.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/datatypes/sygus_simple_sym.cpp \ - theory/datatypes/sygus_simple_sym.h \ - theory/decision_manager.cpp \ - theory/decision_manager.h \ - theory/decision_strategy.cpp \ - theory/decision_strategy.h \ - theory/ext_theory.cpp \ - theory/ext_theory.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/fp/fp_converter.h \ - theory/fp/fp_converter.cpp \ - 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/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/bv_inverter_utils.cpp \ - theory/quantifiers/bv_inverter_utils.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_instantiator.cpp \ - theory/quantifiers/cegqi/ceg_instantiator.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_bv_instantiator_utils.cpp \ - theory/quantifiers/cegqi/ceg_bv_instantiator_utils.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/inst_strategy_cegqi.cpp \ - theory/quantifiers/cegqi/inst_strategy_cegqi.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_query.cpp \ - theory/quantifiers/equality_query.h \ - theory/quantifiers/equality_infer.cpp \ - theory/quantifiers/equality_infer.h \ - theory/quantifiers/expr_miner.cpp \ - theory/quantifiers/expr_miner.h \ - theory/quantifiers/expr_miner_manager.cpp \ - theory/quantifiers/expr_miner_manager.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/instantiate.cpp \ - theory/quantifiers/instantiate.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/lazy_trie.cpp \ - theory/quantifiers/lazy_trie.h \ - theory/quantifiers/local_theory_ext.cpp \ - theory/quantifiers/local_theory_ext.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/query_generator.cpp \ - theory/quantifiers/query_generator.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/cegis.cpp \ - theory/quantifiers/sygus/cegis.h \ - theory/quantifiers/sygus/cegis_unif.cpp \ - theory/quantifiers/sygus/cegis_unif.h \ - theory/quantifiers/sygus/ce_guided_single_inv.cpp \ - theory/quantifiers/sygus/ce_guided_single_inv.h \ - theory/quantifiers/sygus/enum_stream_substitution.cpp \ - theory/quantifiers/sygus/enum_stream_substitution.h \ - theory/quantifiers/sygus/sygus_pbe.cpp \ - theory/quantifiers/sygus/sygus_pbe.h \ - theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \ - theory/quantifiers/sygus/ce_guided_single_inv_sol.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_invariance.cpp \ - theory/quantifiers/sygus/sygus_invariance.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_module.cpp \ - theory/quantifiers/sygus/sygus_module.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/synth_conjecture.cpp \ - theory/quantifiers/sygus/synth_conjecture.h \ - theory/quantifiers/sygus/synth_engine.cpp \ - theory/quantifiers/sygus/synth_engine.h \ - theory/quantifiers/sygus/term_database_sygus.cpp \ - theory/quantifiers/sygus/term_database_sygus.h \ - theory/quantifiers/sygus_sampler.cpp \ - theory/quantifiers/sygus_sampler.h \ - theory/quantifiers/term_canonize.cpp \ - theory/quantifiers/term_canonize.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/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/strings/regexp_elim.cpp \ - theory/strings/regexp_elim.h \ - theory/strings/regexp_operation.cpp \ - theory/strings/regexp_operation.h \ - theory/strings/skolem_cache.cpp \ - theory/strings/skolem_cache.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/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 - -nodist_libcvc4_la_SOURCES = \ - theory/rewriter_tables.h \ - theory/theory_traits.h \ - theory/type_enumerator.cpp - -libcvc4_la_LIBADD = \ - @builddir@/base/libbase.la \ - @builddir@/options/liboptions.la \ - @builddir@/util/libutil.la \ - @builddir@/expr/libexpr.la \ - @builddir@/smt_util/libsmtutil.la \ - @builddir@/prop/minisat/libminisat.la \ - @builddir@/prop/bvminisat/libbvminisat.la -if CVC4_PROOF -libcvc4_la_LIBADD += \ - @top_builddir@/proofs/signatures/libsignatures.la -endif - -libcvc4_la_LIBADD += \ - @builddir@/lib/libreplacements.la - -if CVC4_USE_GLPK -libcvc4_la_LIBADD += $(GLPK_LIBS) -libcvc4_la_LDFLAGS += $(GLPK_LDFLAGS) -endif - -if CVC4_USE_ABC -libcvc4_la_LIBADD += $(ABC_LIBS) -libcvc4_la_LDFLAGS += $(ABC_LDFLAGS) -endif - -if CVC4_USE_CADICAL -libcvc4_la_LIBADD += $(CADICAL_LIBS) -libcvc4_la_LDFLAGS += $(CADICAL_LDFLAGS) -endif - -if CVC4_USE_CRYPTOMINISAT -libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS) -libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS) -endif - -if CVC4_USE_LFSC -libcvc4_la_LIBADD += $(LFSC_LIBS) -libcvc4_la_LDFLAGS += $(LFSC_LDFLAGS) -endif - - - -BUILT_SOURCES = \ - theory/rewriter_tables.h \ - theory/theory_traits.h \ - theory/type_enumerator.cpp \ - $(top_builddir)/src/.subdirs - -CLEANFILES = \ - git_versioninfo.cpp \ - gitinfo.tmp \ - gitinfo \ - theory/rewriter_tables.h \ - theory/theory_traits.h \ - theory/type_enumerator.cpp \ - $(top_builddir)/src/.subdirs - -EXTRA_DIST = \ - Makefile.theories \ - cvc4.i \ - include/cvc4.h \ - include/cvc4_private.h \ - include/cvc4_private_library.h \ - include/cvc4_public.h \ - include/cvc4parser_private.h \ - include/cvc4parser_public.h \ - mksubdirs \ - smt/command.i \ - smt/logic_exception.i \ - smt/smt_engine.i \ - proof/unsat_core.i \ - theory/arith/kinds \ - theory/arrays/kinds \ - theory/booleans/kinds \ - theory/builtin/kinds \ - theory/bv/kinds \ - theory/datatypes/kinds \ - theory/example/ecdata.cpp \ - theory/example/ecdata.h \ - theory/example/theory_uf_tim.cpp \ - theory/example/theory_uf_tim.h \ - theory/fp/kinds \ - theory/idl/kinds \ - theory/logic_info.i \ - theory/mkrewriter \ - theory/mktheorytraits \ - theory/quantifiers/kinds \ - theory/rewriter_tables_template.h \ - theory/sep/kinds \ - theory/sets/kinds \ - theory/strings/kinds \ - theory/theory_traits_template.h \ - theory/type_enumerator_template.cpp \ - theory/uf/kinds - -git_versioninfo.cpp: gitinfo - $(AM_V_GEN)( \ - if test -s gitinfo; then \ - isgit=true; \ - branch=`head -1 gitinfo`; \ - rev=`head -2 gitinfo | tail -1 | awk '{print$$1}'`; \ - mods=`grep '^Modifications: ' gitinfo | awk '{print$$2} END { if(!NR) print "false" }'`; \ - else \ - isgit=false; \ - branch=unknown; \ - rev=unknown; \ - mods=false; \ - fi; \ - echo "#include \"base/configuration.h\""; \ - echo "const bool ::CVC4::Configuration::IS_GIT_BUILD = $$isgit;"; \ - echo "const char* const ::CVC4::Configuration::GIT_BRANCH_NAME = \"$$branch\";"; \ - echo "const char* const ::CVC4::Configuration::GIT_COMMIT = \"$$rev\";"; \ - echo "const bool ::CVC4::Configuration::GIT_HAS_MODIFICATIONS = $$mods;"; \ - ) >"$@" -# This .tmp business is to keep from having to re-compile options.cpp -# (and then re-link the libraries) if nothing has changed. -gitinfo: gitinfo.tmp - $(AM_V_GEN)if diff -q gitinfo.tmp gitinfo &>/dev/null; then rm -f gitinfo.tmp; else mv gitinfo.tmp gitinfo; fi || true -# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) -.PHONY: gitinfo.tmp -gitinfo.tmp: - $(AM_V_GEN)(cd "$(top_srcdir)"; if test -e .git/HEAD; then if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`"; fi) >"$@" 2>/dev/null || true - -install-data-local: - (echo include/cvc4.h; \ - echo include/cvc4_public.h; \ - echo include/cvc4parser_public.h; \ - echo util/floatingpoint.h; \ - echo util/integer.h; \ - echo util/rational.h; \ - find * -name '*.h' | \ - xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ - (cd "$(srcdir)" && find * -name '*.h' | \ - xargs grep -l '^# *include *"cvc4.*_public\.h"')) | \ - while read f; do \ - if expr "$$f" : ".*_\(template\|private\|private_library\|test_utils\)\.h$$" &>/dev/null; then \ - continue; \ - fi; \ - d="$$(echo "$$f" | sed 's,^include/,,')"; \ - $(mkinstalldirs) "$$(dirname "$(DESTDIR)$(includedir)/cvc4/$$d")"; \ - if [ -e "$$f" ]; then \ - path="$$f"; \ - else \ - path="$(srcdir)/$$f"; \ - fi; \ - fixpath="$(top_builddir)/header_install.fix"; \ - sed 's,^\([ \t]*#[ \t]*include[ \t*]\)"\(.*\)"\([ \t]*\)$$,\1<cvc4/\2>\3,' "$$path" > "$$fixpath" || exit 1; \ - echo $(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d"; \ - if $(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d"; then \ - rm -f "$$fixpath"; \ - else \ - rm -f "$$fixpath"; \ - exit 1; \ - fi; \ - done - -uninstall-local: - -(echo include/cvc4.h; \ - echo include/cvc4_public.h; \ - echo include/cvc4parser_public.h; \ - echo util/floatingpoint.h; \ - echo util/integer.h; \ - echo util/rational.h; \ - find * -name '*.h' | \ - xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ - (cd "$(srcdir)" && find * -name '*.h' | \ - xargs grep -l '^# *include *"cvc4.*_public\.h"')) | \ - while read f; do \ - if expr "$$f" : ".*_\(template\|private\|private_library\|test_utils\)\.h$$" &>/dev/null; then \ - continue; \ - fi; \ - d="$$(echo "$$f" | sed 's,^include/,,')"; \ - rm -f "$(DESTDIR)$(includedir)/cvc4/$$d"; \ - done - -rmdir "$(DESTDIR)$(includedir)/cvc4/bindings" - -rmdir "$(DESTDIR)$(includedir)/cvc4" - -rmdir "$(DESTDIR)$(libdir)/ocaml/cvc4" - -# This rule is ugly. It's needed to ensure that automake's dependence -# includes are available during distclean, even though they come from -# directories that are cleaned first. Without this rule, "distclean" -# fails. -%.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" - -#include @top_srcdir@/src/theory/Makefile.subdirs -$(top_builddir)/src/.subdirs: $(top_srcdir)/src/Makefile.theories @top_srcdir@/src/mksubdirs - $(AM_V_at)test -d $(top_builddir)/src || mkdir $(top_builddir)/src - $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs - $(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/.subdirs.tmp - @if ! diff -q $(top_builddir)/src/.subdirs $(top_builddir)/src/.subdirs.tmp &>/dev/null; then \ - echo " GEN " $@; \ - $(am__mv) $(top_builddir)/src/.subdirs.tmp $(top_builddir)/src/.subdirs; \ - fi - -theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)test -d $(top_builddir)/src/theory || mkdir -p @top_builddir@/src/theory - $(AM_V_at)chmod +x @srcdir@/theory/mkrewriter - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/theory/mkrewriter \ - $< \ - `cat @top_builddir@/src/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)test -d $(top_builddir)/src/theory || mkdir -p @top_builddir@/src/theory - $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ - $< \ - `cat @top_builddir@/src/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)test -d $(top_builddir)/src/theory || mkdir -p @top_builddir@/src/theory - $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ - $< \ - `cat @top_builddir@/src/.subdirs` \ - > $@) || (rm -f $@ && exit 1) diff --git a/src/Makefile.theories b/src/Makefile.theories deleted file mode 100644 index 276663cc5..000000000 --- a/src/Makefile.theories +++ /dev/null @@ -1,3 +0,0 @@ - - -THEORIES = builtin booleans uf arith bv fp arrays datatypes sep sets strings quantifiers idl diff --git a/src/base/Makefile.am b/src/base/Makefile.am deleted file mode 100644 index 3706f57a3..000000000 --- a/src/base/Makefile.am +++ /dev/null @@ -1,77 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libbase.la - -# Do not list built sources here! -# Rather, list them under BUILT_SOURCES, and their .in versions under -# EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is -# no good---they belong in the configured builds/ directory. If they -# end up in the source directory, they build the cvc4 that was -# configured at the time of the "make dist", which (1) may not be the -# configuration that the user wants, and (2) might cause link errors. -libbase_la_SOURCES = \ - Makefile.am \ - Makefile.in \ - 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 \ - map_util.h \ - modal_exception.h \ - output.cpp \ - output.h - -# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES = \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.h \ - Trace_tags - -MOSTLYCLEANFILES = \ - Debug_tags \ - Trace_tags \ - Debug_tags.tmp \ - Trace_tags.tmp \ - Debug_tags.h \ - Trace_tags.h - -EXTRA_DIST = \ - configuration.i \ - exception.i \ - mktagheaders \ - mktags \ - modal_exception.i - -%_tags.h: %_tags mktagheaders - $(AM_V_at)chmod +x @srcdir@/mktagheaders - $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" - -# This .tmp business is to keep from having to re-compile options.cpp -# (and then re-link the libraries) if nothing has changed. -%_tags: %_tags.tmp - $(AM_V_GEN)\ - diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true -# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) -.PHONY: Debug_tags.tmp Trace_tags.tmp -# The "sed" invocation below is particularly obnoxious, but it works around -# inconsistencies in REs on different platforms, using only a basic regular -# expression (no |, no \<, ...). -Debug_tags.tmp Trace_tags.tmp: mktags - $(AM_V_at)chmod +x @srcdir@/mktags - $(AM_V_GEN)(@srcdir@/mktags \ - '$(@:_tags.tmp=)' \ - "$$(find @srcdir@/../ -name '*.cpp' -o -name '*.h' -o -name '*.cc' -o -name '*.g')") >"$@" diff --git a/src/bindings/Makefile b/src/bindings/Makefile deleted file mode 100644 index 419d3a1b4..000000000 --- a/src/bindings/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/bindings - -include $(topdir)/Makefile.subdir diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am deleted file mode 100644 index 9de484d1c..000000000 --- a/src/bindings/Makefile.am +++ /dev/null @@ -1,237 +0,0 @@ -# LIBCVC4BINDINGS_VERSION (-version-info) is in the form current:revision:age -# -# current - -# increment if interfaces have been added, removed or changed -# revision - -# increment if source code has changed -# set to zero if current is incremented -# age - -# increment if interfaces have been added -# set to zero if interfaces have been removed -# or changed -# -LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ - -AUTOMAKE_OPTIONS = subdir-objects - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4BINDINGSLIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall - -# any binding-specific flags to pass to swig -java_cpp_SWIGFLAGS = -package edu.nyu.acsys.CVC4 - -lib_LTLIBRARIES = -bin_PROGRAMS = -javadatadir = $(datadir)/java -javalibdir = $(libdir)/jni -ocamldatadir = $(libdir)/ocaml/cvc4 -ocamllibdir = $(libdir)/ocaml/cvc4 -perldatadir = $(datadir)/perl5 -perllibdir = $(libdir)/perl5 -phpdatadir = $(datadir)/php -phplibdir = $(libdir)/php -pythondatadir = $(datadir)/pyshared -pythonlibdir = $(libdir)/pyshared -csharpdatadir = $(datadir)/csharp -csharplibdir = $(libdir)/csharp -rubylibdir = $(libdir)/ruby -tcllibdir = $(libdir)/tcltk -javadata_DATA = -javalib_LTLIBRARIES= -ocamldata_DATA = -ocamllib_LTLIBRARIES= -perldata_DATA = -perllib_LTLIBRARIES = -phpdata_DATA = -phplib_LTLIBRARIES = -pythondata_DATA = -pythonlib_LTLIBRARIES = -csharpdata_DATA = -csharplib_LTLIBRARIES = -rubylib_LTLIBRARIES = -tcllib_LTLIBRARIES = -if CVC4_HAS_SWIG -if CVC4_LANGUAGE_BINDING_JAVA -javalib_LTLIBRARIES += java/libcvc4jni.la -javadata_DATA += CVC4.jar -java_libcvc4jni_la_LDFLAGS = \ - -no-undefined \ - -module \ - -shrext $(CVC4_JAVA_MODULE_EXT) \ - -version-info $(LIBCVC4BINDINGS_VERSION) -java_libcvc4jni_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -endif -if CVC4_LANGUAGE_BINDING_CSHARP -csharplib_LTLIBRARIES += csharp/CVC4.la -csharp_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -csharp_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -endif -if CVC4_LANGUAGE_BINDING_PERL -perllib_LTLIBRARIES += perl/CVC4.la -perl_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -perl_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -perldata_DATA += perl/CVC4.pm -endif -if CVC4_LANGUAGE_BINDING_PHP -phplib_LTLIBRARIES += php/CVC4.la -php_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -php_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -phpdata_DATA += php/CVC4.php -endif -if CVC4_LANGUAGE_BINDING_PYTHON -pythonlib_LTLIBRARIES += python/CVC4.la -python_CVC4_la_CXXFLAGS = $(PYTHON_CXXFLAGS) -python_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -python_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -pythondata_DATA += python/CVC4.py -endif -if CVC4_LANGUAGE_BINDING_OCAML -ocamllib_LTLIBRARIES += ocaml/CVC4.la -bin_PROGRAMS += cvc4_ocaml_top -# We provide a make rule below, but we have to tell automake to lay off, too, -# otherwise it tries (and fails) to package the nonexistent cvc4_ocaml_top.c! -cvc4_ocaml_top_SOURCES = -ocamldata_DATA += ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/swigp4.cmi ocaml/CVC4.cmo ocaml/CVC4.cmi -ocaml_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -ocaml_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -endif -if CVC4_LANGUAGE_BINDING_RUBY -rubylib_LTLIBRARIES += ruby/CVC4.la -ruby_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -ruby_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -endif -if CVC4_LANGUAGE_BINDING_TCL -tcllib_LTLIBRARIES += tcl/CVC4.la -tcl_CVC4_la_LDFLAGS = \ - -module \ - -version-info $(LIBCVC4BINDINGS_VERSION) -tcl_CVC4_la_LIBADD = \ - @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la -endif -# this endif matches the "if CVC4_HAS_SWIG" above -endif - -nodist_java_libcvc4jni_la_SOURCES = java.cpp -java_libcvc4jni_la_CXXFLAGS = -Wno-all @FNO_STRICT_ALIASING@ @WNO_UNUSED_VARIABLE@ @WNO_UNINITIALIZED@ -nodist_csharp_CVC4_la_SOURCES = csharp.cpp -nodist_perl_CVC4_la_SOURCES = perl.cpp -nodist_php_CVC4_la_SOURCES = php.cpp -nodist_python_CVC4_la_SOURCES = python.cpp -nodist_ocaml_CVC4_la_SOURCES = ocaml.cpp -nodist_ruby_CVC4_la_SOURCES = ruby.cpp -nodist_tcl_CVC4_la_SOURCES = tcl.cpp - -CLEANFILES = \ - java.cpp \ - csharp.cpp \ - perl.cpp \ - php.cpp \ - python.cpp \ - ocaml.cpp \ - ruby.cpp \ - tcl.cpp - -EXTRA_DIST = \ - swig.h \ - java_iterator_adapter.h \ - java_stream_adapters.h - -MOSTLYCLEANFILES = \ - .swig_deps \ - $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \ - CVC4.jar - -java_libcvc4jni_la-java.lo: java.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $< -java.lo: java.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $< -CVC4.jar: java.cpp - $(AM_V_GEN) \ - (cd java && \ - rm -fr classes && \ - mkdir -p classes && \ - $(JAVAC) -source 1.6 -target 1.6 -classpath . -d classes `find . -name '*.java'` && \ - cd classes) && \ - $(JAR) cf $@ -C java/classes . -#java.cpp:; -csharp.lo: csharp.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(CSHARP_CPPFLAGS) -o $@ $< -#csharp.cpp:; -perl.lo: perl.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $< -#perl.cpp:; -perl/CVC4.pm: perl.cpp -php.lo: php.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $< -#php.cpp:; -python.lo: python.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $< -ocaml.lo: ocaml.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(OCAML_CPPFLAGS) -o $@ $< -ocaml/swig.cmo: ocaml/swig.ml ocaml/swig.cmi; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $< -ocaml/swig.cmi: ocaml/swig.mli; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $< -ocaml/CVC4.cmo: ocaml/CVC4.ml ocaml/CVC4.cmi; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $< -ocaml/CVC4.cmi: ocaml/CVC4.mli; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $< -ocaml/swigp4.cmo: ocaml/swigp4.ml; $(AM_V_GEN)$(OCAMLFIND) ocamlc -package camlp4 -pp "$(CAMLP4O) pa_extend.cmo q_MLast.cmo" -o $@ -c $< -ocaml/swig.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.ml -ocaml/swig.mli:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.mli -ocaml/swigp4.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swigp4.ml -#ocaml.cpp:; -cvc4_ocaml_top$(EXEEXT): ocaml/CVC4.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi - $(AM_V_GEN)\ - $(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top$(EXEEXT) -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib ocaml/.libs/CVC4.so -cclib -lstdc++ -ruby.lo: ruby.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $< -tcl.lo: tcl.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $< -#tcl.cpp:; - -if CVC4_HAS_SWIG - -$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i - $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) - $(AM_V_GEN)$(SWIG) -Wall -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $< - -# Automake 1.16 is executing this target at configuration time. Because some -# generated source files do not exist at that time, we use the -ignoremissing -# option to not have SWIG complain about those missing files. -$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i - $(AM_V_GEN)$(SWIG) -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -c++ -$(patsubst %.d,%,$@) -ignoremissing -MM -o $(patsubst %.d,%.cpp,$@) $< -# .PHONY so they get rebuilt each time -.PHONY: .swig_deps $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) -.swig_deps: $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) - $(AM_V_GEN)cat $+ </dev/null >$@ -@mk_include@ .swig_deps - -endif - -clean-local:; rm -fr $(patsubst %.cpp,%,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) diff --git a/src/expr/.gitignore b/src/expr/.gitignore deleted file mode 100644 index 238db3ad3..000000000 --- a/src/expr/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -/kind.h -/metakind.h -/expr.cpp -/expr.h -/expr_manager.cpp -/expr_manager.h diff --git a/src/expr/Makefile b/src/expr/Makefile deleted file mode 100644 index eff3b332e..000000000 --- a/src/expr/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/expr - -include $(topdir)/Makefile.subdir diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am deleted file mode 100644 index f8f9dbd11..000000000 --- a/src/expr/Makefile.am +++ /dev/null @@ -1,228 +0,0 @@ -# if coverage is enabled: -# COVERAGE_ON = yes from configure.ac -# Using an inline conditional function to choose between absolute and -# relative paths for options files -# lcov does not support relative paths and src/options and src/expr -# in particular were breaking it -# Building with coverage will cause portability issues in some cases - -VPATH = $(if $(COVERAGE_ON), $(realpath @srcdir@), @srcdir@) - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - $(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libexpr.la - -# For some reason statistics were in libutil. No idea why though. -libexpr_la_SOURCES = \ - 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_algorithm.cpp \ - node_algorithm.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 - -nodist_libexpr_la_SOURCES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - type_properties.h \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp - -EXTRA_DIST = \ - array.i \ - chain.i \ - array_store_all.i \ - ascription_type.i \ - datatype.i \ - emptyset.i \ - kind_template.h \ - kind_template.cpp \ - metakind_template.h \ - metakind_template.cpp \ - type_properties_template.h \ - expr_manager_template.h \ - expr_manager_template.cpp \ - expr_template.h \ - expr_template.cpp \ - type_checker_template.cpp \ - mkkind \ - mkmetakind \ - mkexpr \ - expr_stream.i \ - expr_manager.i \ - symbol_table.i \ - type.i \ - kind.i \ - expr.i \ - record.i \ - variable_type_map.i \ - uninterpreted_constant.i - -BUILT_SOURCES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - type_properties.h \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp \ - $(top_builddir)/src/expr/.subdirs - -CLEANFILES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp \ - type_properties.h \ - $(top_builddir)/src/expr/.subdirs - -$(top_builddir)/src/expr/.subdirs: $(top_srcdir)/src/Makefile.theories @top_srcdir@/src/mksubdirs - $(AM_V_at)test -d $(top_builddir)/src/expr || mkdir $(top_builddir)/src/expr - $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs - $(AM_V_at)( @top_srcdir@/src/mksubdirs $(if $(COVERAGE_ON), "$(abs_top_srcdir)", "$(top_srcdir)")) > $(top_builddir)/src/expr/.subdirs.tmp - @if ! diff -q $(top_builddir)/src/expr/.subdirs $(top_builddir)/src/expr/.subdirs.tmp &>/dev/null; then \ - echo " GEN " $@; \ - $(am__mv) $(top_builddir)/src/expr/.subdirs.tmp $(top_builddir)/src/expr/.subdirs; \ - fi - -kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -kind.cpp: kind_template.cpp mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkmetakind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkmetakind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -metakind.cpp: metakind_template.cpp mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkmetakind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkmetakind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -.PHONY: builts -builts: $(BUILT_SOURCES) diff --git a/src/include/.gitignore b/src/include/.gitignore deleted file mode 100644 index 274bc504a..000000000 --- a/src/include/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -/Makefile - diff --git a/src/lib/Makefile b/src/lib/Makefile deleted file mode 100644 index 9811fec4f..000000000 --- a/src/lib/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/lib - -include $(topdir)/Makefile.subdir diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am deleted file mode 100644 index aec9fa634..000000000 --- a/src/lib/Makefile.am +++ /dev/null @@ -1,25 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -# This is a workaround for now to fix some warnings related to unsupported -# compiler flags since we are compiling C code here. CXXFLAGS is set via -# configure, however, we should actually set AM_CXXFLAGS. -CXXFLAGS = $(AM_CXXFLAGS) - -noinst_LTLIBRARIES = libreplacements.la - -libreplacements_la_SOURCES = - -libreplacements_la_LIBADD = \ - $(LTLIBOBJS) - -EXTRA_DIST = \ - replacements.h \ - clock_gettime.c \ - clock_gettime.h \ - strtok_r.c \ - strtok_r.h \ - ffs.c \ - ffs.h diff --git a/src/main/Makefile b/src/main/Makefile deleted file mode 100644 index 5e936ee06..000000000 --- a/src/main/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/main - -include $(topdir)/Makefile.subdir diff --git a/src/main/Makefile.am b/src/main/Makefile.am deleted file mode 100644 index 372e817f6..000000000 --- a/src/main/Makefile.am +++ /dev/null @@ -1,85 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4DRIVER \ - -I@builddir@/.. $(ANTLR_INCLUDES) -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas - -bin_PROGRAMS = cvc4 - -noinst_LIBRARIES = libmain.a - -libmain_a_SOURCES = \ - interactive_shell.h \ - interactive_shell.cpp \ - main.h \ - util.cpp - -if CVC4_BUILD_PCVC4 -bin_PROGRAMS += pcvc4 -pcvc4_SOURCES = \ - 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 -pcvc4_LDADD = \ - libmain.a \ - @builddir@/../parser/libcvc4parser.la \ - @builddir@/../libcvc4.la \ - $(READLINE_LIBS) \ - @builddir@/../lib/libreplacements.la - -pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD -pcvc4_LDADD += $(BOOST_THREAD_LIBS) -pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) - -if STATIC_BINARY -pcvc4_LINK = $(CXXLINK) -all-static $(pcvc4_LDFLAGS) -else -pcvc4_LINK = $(CXXLINK) $(pcvc4_LDFLAGS) -endif -endif - -cvc4_SOURCES = \ - main.cpp \ - command_executor.cpp \ - driver_unified.cpp -cvc4_LDADD = \ - libmain.a \ - @builddir@/../parser/libcvc4parser.la \ - @builddir@/../libcvc4.la \ - $(READLINE_LIBS) \ - @builddir@/../lib/libreplacements.la - -BUILT_SOURCES = \ - $(TOKENS_FILES) - -TOKENS_FILES = \ - cvc_tokens.h \ - smt1_tokens.h \ - smt2_tokens.h \ - tptp_tokens.h - -cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -smt1_tokens.h: @srcdir@/../parser/smt1/Smt1.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ - - -clean-local: - rm -f $(BUILT_SOURCES) - -if STATIC_BINARY -cvc4_LINK = $(CXXLINK) -all-static $(cvc4_LDFLAGS) -else -cvc4_LINK = $(CXXLINK) $(cvc4_LDFLAGS) -endif - diff --git a/src/mksubdirs b/src/mksubdirs deleted file mode 100755 index c96437caa..000000000 --- a/src/mksubdirs +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/bash -# -# The purpose of this file is to generate a .subdirs file in the build process. -# This file contains a file of relative paths to all of the theories relative -# to the current directory. Each Makefile.am should thus build its own .subdirs file. -# This assumes it is passed the equivalent of the $top_srcdir configure variable. -# -# Invocation: -# -# mksubdirs <top_srcdir> - -TOP_SRCDIR=$1 - -grep '^THEORIES = ' $TOP_SRCDIR/src/Makefile.theories | \ - cut -d' ' -f3- | tr ' ' "\n" | \ - xargs -I__D__ echo "$TOP_SRCDIR/src/theory/__D__/kinds" diff --git a/src/options/Makefile b/src/options/Makefile deleted file mode 100644 index 54a46191d..000000000 --- a/src/options/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/options - -include $(topdir)/Makefile.subdir diff --git a/src/options/Makefile.am b/src/options/Makefile.am deleted file mode 100644 index 498989c80..000000000 --- a/src/options/Makefile.am +++ /dev/null @@ -1,159 +0,0 @@ -# if coverage is enabled: -# COVERAGE_ON = yes from configure.ac -# Using an inline conditional function to choose between absolute and -# relative paths for options files -# lcov does not support relative paths and src/options and src/expr -# in particular were breaking it -# Building with coverage will cause portability issues in some cases - -VPATH = $(if $(COVERAGE_ON), $(realpath @srcdir@), @srcdir@) - -OPTIONS_CONFIG_FILES = \ - arith_options.toml \ - arrays_options.toml \ - base_options.toml \ - booleans_options.toml \ - builtin_options.toml \ - bv_options.toml \ - datatypes_options.toml \ - decision_options.toml \ - expr_options.toml \ - fp_options.toml \ - idl_options.toml \ - main_options.toml \ - parser_options.toml \ - printer_options.toml \ - proof_options.toml \ - prop_options.toml \ - quantifiers_options.toml \ - sep_options.toml \ - sets_options.toml \ - smt_options.toml \ - strings_options.toml \ - theory_options.toml \ - uf_options.toml - -OPTIONS_GEN_H = $(OPTIONS_CONFIG_FILES:.toml=.h) - -OPTIONS_GEN_CPP = $(OPTIONS_CONFIG_FILES:.toml=.cpp) - -CPP_TEMPLATE_FILES = \ - module_template.h \ - module_template.cpp \ - options_holder_template.h \ - options_template.cpp - -DOCUMENTATION_FILES = \ - ../../doc/cvc4.1 \ - ../../doc/SmtEngine.3cvc \ - ../../doc/options.3cvc - -DOCUMENTATION_TEMPLATE_FILES = \ - ../../doc/cvc4.1_template \ - ../../doc/SmtEngine.3cvc_template \ - ../../doc/options.3cvc_template - - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - $(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..) -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = liboptions.la - -liboptions_la_SOURCES = \ - 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 \ - argument_extender_implementation.cpp \ - argument_extender_implementation.h \ - argument_extender.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.cpp \ - 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 \ - smt_modes.cpp \ - smt_modes.h \ - sygus_out_mode.h \ - theoryof_mode.cpp \ - theoryof_mode.h \ - ufss_mode.h - - -nodist_liboptions_la_SOURCES = \ - options.cpp \ - options_holder.h \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_GEN_CPP) - - -BUILT_SOURCES = \ - options.cpp - - -CLEANFILES = \ - $(BUILT_SOURCES) \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_GEN_CPP) \ - $(DOCUMENTATION_FILES) \ - options_holder.h - - -EXTRA_DIST = \ - options.cpp \ - options_holder.h \ - $(OPTIONS_GEN_CPP) \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_CONFIG_FILES) \ - $(CPP_TEMPLATE_FILES) \ - $(DOCUMENTATION_FILES) \ - mkoptions.py \ - language.i \ - option_exception.i \ - options.i - - - -# Make sure the implicit rules never mistake a _template.cpp or _template.h -# file for source file. -$(CPP_TEMPLATE_FILES):; - -# All source/doc files are generated in one pass with rule options.cpp. Note -# that this is done incrementally since mkoptions.py checks if a generated file -# changed before writing to the file. No global re-compilation of all generated -# files happens if only individual files were modified. -$(OPTIONS_GEN_CPP) $(OPTIONS_GEN_H) options_holder.h $(DOCUMENTATION_FILES): options.cpp - -options.cpp: mkoptions.py $(CPP_TEMPLATE_FILES) $(OPTIONS_CONFIG_FILES) $(DOCUMENTATION_TEMPLATE_FILES) - $(PYTHON) @srcdir@/mkoptions.py @abs_srcdir@ ../../doc . $(addprefix @abs_srcdir@/, $(OPTIONS_CONFIG_FILES)) - -# This rule is ugly. It's needed to ensure that automake's dependence -# includes are available during distclean, even though they come from -# directories that are cleaned first. Without this rule, "distclean" -# fails. -%.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" diff --git a/src/parser/Makefile b/src/parser/Makefile deleted file mode 100644 index cef81750e..000000000 --- a/src/parser/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/parser - -include $(topdir)/Makefile.subdir diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am deleted file mode 100644 index 98b98ccaf..000000000 --- a/src/parser/Makefile.am +++ /dev/null @@ -1,76 +0,0 @@ -# LIBCVC4PARSER_VERSION (-version-info) is in the form current:revision:age -# -# current - -# increment if interfaces have been added, removed or changed -# revision - -# increment if source code has changed -# set to zero if current is incremented -# age - -# increment if interfaces have been added -# set to zero if interfaces have been removed -# or changed -# -LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@builddir@/.. $(ANTLR_INCLUDES) -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -SUBDIRS = smt1 smt2 cvc tptp - -lib_LTLIBRARIES = libcvc4parser.la - -libcvc4parser_la_LDFLAGS = \ - $(ANTLR_LDFLAGS) \ - -no-undefined \ - -version-info $(LIBCVC4PARSER_VERSION) - -if CVC4_WINDOWS_BUILD -# -Wl,--export-all-symbols makes sure that all symbols are exported when -# building a DLL. This option is on by default but gets disabled for the parser -# library because the generated lexer/parser files define some functions as -# __declspec(dllexport), which leads to lots of unresolved symbols when linking -# against libcvc4parser. -libcvc4parser_la_LDFLAGS += -Wl,--export-all-symbols -endif - -libcvc4parser_la_LIBADD = \ - @builddir@/smt1/libparsersmt1.la \ - @builddir@/smt2/libparsersmt2.la \ - @builddir@/tptp/libparsertptp.la \ - @builddir@/cvc/libparsercvc.la \ - @builddir@/../libcvc4.la \ - @builddir@/../lib/libreplacements.la - -libcvc4parser_la_SOURCES = \ - 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 - -EXTRA_DIST = \ - Makefile.antlr_tracing \ - cvc4parser.i \ - input.i \ - parser_builder.i \ - parser_exception.i \ - parser.i diff --git a/src/parser/Makefile.antlr_tracing b/src/parser/Makefile.antlr_tracing deleted file mode 100644 index fa79337b4..000000000 --- a/src/parser/Makefile.antlr_tracing +++ /dev/null @@ -1,22 +0,0 @@ -# -*-makefile-*- -# -# This makefile is included from parser directories in order to -# do antlr tracing. THIS IS VERY MUCH A HACK, and is only enabled -# if CVC4_TRACE_ANTLR is defined (and not 0). In ANTLR 3.2, we -# have to #define "println" and "System," etc., because the -# generator erroneously puts Java in C output! -# - -ifeq ($(CVC4_TRACE_ANTLR),) -else - -ifeq ($(CVC4_TRACE_ANTLR),0) -else - -AM_CPPFLAGS += -DCVC4_TRACE_ANTLR -ANTLR_OPTS += -trace - -endif - -endif - diff --git a/src/parser/cvc/Makefile b/src/parser/cvc/Makefile deleted file mode 100644 index cbcc0a493..000000000 --- a/src/parser/cvc/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/parser/cvc - -include $(topdir)/Makefile.subdir diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am deleted file mode 100644 index ff3308d89..000000000 --- a/src/parser/cvc/Makefile.am +++ /dev/null @@ -1,68 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_UNINITIALIZED) $(WNO_CONVERSION_NULL) - -# Compile generated C files using C++ compiler -AM_CFLAGS = $(AM_CXXFLAGS) -CFLAGS=$(CXXFLAGS) -CC=$(CXX) - -ANTLR_OPTS = - -# hide this included makefile from automake -@mk_include@ @srcdir@/../Makefile.antlr_tracing - -noinst_LTLIBRARIES = libparsercvc.la - -ANTLR_TOKEN_STUFF = \ - @builddir@/Cvc.tokens -ANTLR_LEXER_STUFF = \ - @builddir@/CvcLexer.h \ - @builddir@/CvcLexer.c \ - $(ANTLR_TOKEN_STUFF) -ANTLR_PARSER_STUFF = \ - @builddir@/CvcParser.h \ - @builddir@/CvcParser.c -ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) - -libparsercvc_la_SOURCES = \ - Cvc.g \ - cvc_input.h \ - cvc_input.cpp \ - $(ANTLR_STUFF) - -BUILT_SOURCES = \ - @builddir@/Cvc.tokens \ - @builddir@/CvcLexer.h \ - @builddir@/CvcLexer.c \ - @builddir@/CvcParser.h \ - @builddir@/CvcParser.c \ - stamp-generated - -EXTRA_DIST = \ - README \ - stamp-generated - -DISTCLEANFILES = $(ANTLR_STUFF) -distclean-local: - -$(AM_V_at)rmdir generated - -$(AM_V_at)rm -f stamp-generated - -stamp-generated: - $(AM_V_at)mkdir -p generated - $(AM_V_at)touch stamp-generated - -# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -@builddir@/CvcLexer.h: Cvc.g stamp-generated - -$(AM_V_at)rm -f $(ANTLR_STUFF) - @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@builddir@" "@srcdir@/Cvc.g" - -# These don't actually depend on CvcLexer.h, but if we're doing parallel -# make and the lexer needs to be rebuilt, we have to keep the rules -# from running in parallel (since the token files will be deleted & -# recreated) -@builddir@/CvcLexer.c @builddir@/CvcParser.h @builddir@/CvcParser.c $(ANTLR_TOKEN_STUFF): @builddir@/CvcLexer.h diff --git a/src/parser/smt1/Makefile b/src/parser/smt1/Makefile deleted file mode 100644 index 7e97ed357..000000000 --- a/src/parser/smt1/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/parser/smt - -include $(topdir)/Makefile.subdir diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am deleted file mode 100644 index f5320002d..000000000 --- a/src/parser/smt1/Makefile.am +++ /dev/null @@ -1,69 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable - -# Compile generated C files using C++ compiler -AM_CFLAGS = $(AM_CXXFLAGS) -CFLAGS=$(CXXFLAGS) -CC=$(CXX) - -ANTLR_OPTS = - -# hide this included makefile from automake -@mk_include@ @srcdir@/../Makefile.antlr_tracing - -noinst_LTLIBRARIES = libparsersmt1.la - -ANTLR_TOKEN_STUFF = \ - @builddir@/Smt1.tokens -ANTLR_LEXER_STUFF = \ - @builddir@/Smt1Lexer.h \ - @builddir@/Smt1Lexer.c \ - $(ANTLR_TOKEN_STUFF) -ANTLR_PARSER_STUFF = \ - @builddir@/Smt1Parser.h \ - @builddir@/Smt1Parser.c -ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) - -libparsersmt1_la_SOURCES = \ - Smt1.g \ - smt1.h \ - smt1.cpp \ - smt1_input.h \ - smt1_input.cpp \ - $(ANTLR_STUFF) - -BUILT_SOURCES = \ - @builddir@/Smt1.tokens \ - @builddir@/Smt1Lexer.h \ - @builddir@/Smt1Lexer.c \ - @builddir@/Smt1Parser.h \ - @builddir@/Smt1Parser.c \ - stamp-generated - -EXTRA_DIST = \ - stamp-generated - -DISTCLEANFILES = $(ANTLR_STUFF) -distclean-local: - -$(AM_V_at)rmdir generated - -$(AM_V_at)rm -f stamp-generated - -stamp-generated: - $(AM_V_at)mkdir -p generated - $(AM_V_at)touch stamp-generated - -# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -@builddir@/Smt1Lexer.h: Smt1.g stamp-generated - -$(AM_V_at)rm -f $(ANTLR_STUFF) - @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@builddir@" "@srcdir@/Smt1.g" - -# These don't actually depend on Smt1Lexer.h, but if we're doing parallel -# make and the lexer needs to be rebuilt, we have to keep the rules -# from running in parallel (since the token files will be deleted & -# recreated) -@builddir@/Smt1Lexer.c @builddir@/Smt1Parser.h @builddir@/Smt1Parser.c $(ANTLR_TOKEN_STUFF): @builddir@/Smt1Lexer.h diff --git a/src/parser/smt2/Makefile b/src/parser/smt2/Makefile deleted file mode 100644 index fc9cc6db2..000000000 --- a/src/parser/smt2/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/parser/smt2 - -include $(topdir)/Makefile.subdir diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am deleted file mode 100644 index 995e442e6..000000000 --- a/src/parser/smt2/Makefile.am +++ /dev/null @@ -1,71 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable - -# Compile generated C files using C++ compiler -AM_CFLAGS = $(AM_CXXFLAGS) -CFLAGS=$(CXXFLAGS) -CC=$(CXX) - -ANTLR_OPTS = - -# hide this included makefile from automake -@mk_include@ @srcdir@/../Makefile.antlr_tracing - -noinst_LTLIBRARIES = libparsersmt2.la - -ANTLR_TOKEN_STUFF = \ - @builddir@/Smt2.tokens -ANTLR_LEXER_STUFF = \ - @builddir@/Smt2Lexer.h \ - @builddir@/Smt2Lexer.c \ - $(ANTLR_TOKEN_STUFF) -ANTLR_PARSER_STUFF = \ - @builddir@/Smt2Parser.h \ - @builddir@/Smt2Parser.c -ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) - -libparsersmt2_la_SOURCES = \ - Smt2.g \ - smt2.h \ - smt2.cpp \ - smt2_input.h \ - smt2_input.cpp \ - sygus_input.h \ - sygus_input.cpp \ - $(ANTLR_STUFF) - -BUILT_SOURCES = \ - @builddir@/Smt2.tokens \ - @builddir@/Smt2Lexer.h \ - @builddir@/Smt2Lexer.c \ - @builddir@/Smt2Parser.h \ - @builddir@/Smt2Parser.c \ - stamp-generated - -EXTRA_DIST = \ - stamp-generated - -DISTCLEANFILES = $(ANTLR_STUFF) -distclean-local: - -$(AM_V_at)rmdir generated - -$(AM_V_at)rm -f stamp-generated - -stamp-generated: - $(AM_V_at)mkdir -p generated - $(AM_V_at)touch stamp-generated - -# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -@builddir@/Smt2Lexer.h: Smt2.g stamp-generated - -$(AM_V_at)rm -f $(ANTLR_STUFF) - @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@builddir@" "@srcdir@/Smt2.g" - -# These don't actually depend on SmtLexer.h, but if we're doing parallel -# make and the lexer needs to be rebuilt, we have to keep the rules -# from running in parallel (since the token files will be deleted & -# recreated) -@builddir@/Smt2Lexer.c @builddir@/Smt2Parser.h @builddir@/Smt2Parser.c $(ANTLR_TOKEN_STUFF): @builddir@/Smt2Lexer.h diff --git a/src/parser/tptp/Makefile b/src/parser/tptp/Makefile deleted file mode 100644 index 45cde5821..000000000 --- a/src/parser/tptp/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/parser/tptp - -include $(topdir)/Makefile.subdir diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am deleted file mode 100644 index 43bbc595d..000000000 --- a/src/parser/tptp/Makefile.am +++ /dev/null @@ -1,69 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable - -# Compile generated C files using C++ compiler -AM_CFLAGS = $(AM_CXXFLAGS) -CFLAGS=$(CXXFLAGS) -CC=$(CXX) - -ANTLR_OPTS = - -# hide this included makefile from automake -@mk_include@ @srcdir@/../Makefile.antlr_tracing - -noinst_LTLIBRARIES = libparsertptp.la - -ANTLR_TOKEN_STUFF = \ - @builddir@/Tptp.tokens -ANTLR_LEXER_STUFF = \ - @builddir@/TptpLexer.h \ - @builddir@/TptpLexer.c \ - $(ANTLR_TOKEN_STUFF) -ANTLR_PARSER_STUFF = \ - @builddir@/TptpParser.h \ - @builddir@/TptpParser.c -ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) - -libparsertptp_la_SOURCES = \ - Tptp.g \ - tptp.h \ - tptp.cpp \ - tptp_input.h \ - tptp_input.cpp \ - $(ANTLR_STUFF) - -BUILT_SOURCES = \ - @builddir@/Tptp.tokens \ - @builddir@/TptpLexer.h \ - @builddir@/TptpLexer.c \ - @builddir@/TptpParser.h \ - @builddir@/TptpParser.c \ - stamp-generated - -EXTRA_DIST = \ - stamp-generated - -DISTCLEANFILES = $(ANTLR_STUFF) -distclean-local: - -$(AM_V_at)rmdir generated - -$(AM_V_at)rm -f stamp-generated - -stamp-generated: - $(AM_V_at)mkdir -p generated - $(AM_V_at)touch stamp-generated - -# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -@builddir@/TptpLexer.h: Tptp.g stamp-generated - -$(AM_V_at)rm -f $(ANTLR_STUFF) - @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@builddir@" "@srcdir@/Tptp.g" - -# These don't actually depend on TptpLexer.h, but if we're doing parallel -# make and the lexer needs to be rebuilt, we have to keep the rules -# from running in parallel (since the token files will be deleted & -# recreated) -@builddir@/TptpLexer.c @builddir@/TptpParser.h @builddir@/TptpParser.c $(ANTLR_TOKEN_STUFF): @builddir@/TptpLexer.h diff --git a/src/prop/bvminisat/Makefile.am b/src/prop/bvminisat/Makefile.am deleted file mode 100644 index d34a4c12c..000000000 --- a/src/prop/bvminisat/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/ -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libbvminisat.la -libbvminisat_la_SOURCES = \ - core/Dimacs.h \ - core/Solver.cc \ - core/Solver.h \ - core/SolverTypes.h \ - simp/SimpSolver.cc \ - simp/SimpSolver.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 \ - utils/Options.h \ - bvminisat.h \ - bvminisat.cpp - -EXTRA_DIST = \ - core/Main.cc \ - core/Makefile \ - doc/ReleaseNotes-2.2.0.txt \ - simp/Main.cc \ - simp/Makefile \ - README \ - LICENSE \ - mtl/config.mk \ - mtl/template.mk \ - utils/Options.cc \ - utils/ParseUtils.h \ - utils/System.h \ - utils/System.cc \ - Makefile - diff --git a/src/prop/bvminisat/core/Makefile b/src/prop/bvminisat/core/Makefile deleted file mode 100644 index 5de1f7295..000000000 --- a/src/prop/bvminisat/core/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = minisat -DEPDIR = mtl utils - -include $(MROOT)/mtl/template.mk diff --git a/src/prop/bvminisat/simp/Makefile b/src/prop/bvminisat/simp/Makefile deleted file mode 100644 index 27b45f493..000000000 --- a/src/prop/bvminisat/simp/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = minisat -DEPDIR = mtl utils core - -include $(MROOT)/mtl/template.mk diff --git a/src/prop/bvminisat/utils/Makefile b/src/prop/bvminisat/utils/Makefile deleted file mode 100644 index 204cea541..000000000 --- a/src/prop/bvminisat/utils/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = system_test -DEPDIR = mtl - -include $(MROOT)/mtl/template.mk diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am deleted file mode 100644 index 4c110980d..000000000 --- a/src/prop/minisat/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/ -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libminisat.la -libminisat_la_SOURCES = \ - core/Dimacs.h \ - core/Solver.cc \ - core/Solver.h \ - core/SolverTypes.h \ - simp/SimpSolver.cc \ - simp/SimpSolver.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 \ - utils/Options.h \ - minisat.cpp \ - minisat.h - -EXTRA_DIST = \ - core/Main.cc \ - core/Makefile \ - doc/ReleaseNotes-2.2.0.txt \ - simp/Main.cc \ - simp/Makefile \ - README \ - LICENSE \ - mtl/config.mk \ - mtl/template.mk \ - utils/Options.cc \ - utils/ParseUtils.h \ - utils/System.h \ - utils/System.cc \ - Makefile - diff --git a/src/prop/minisat/core/Makefile b/src/prop/minisat/core/Makefile deleted file mode 100644 index 5de1f7295..000000000 --- a/src/prop/minisat/core/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = minisat -DEPDIR = mtl utils - -include $(MROOT)/mtl/template.mk diff --git a/src/prop/minisat/simp/Makefile b/src/prop/minisat/simp/Makefile deleted file mode 100644 index 27b45f493..000000000 --- a/src/prop/minisat/simp/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = minisat -DEPDIR = mtl utils core - -include $(MROOT)/mtl/template.mk diff --git a/src/prop/minisat/utils/Makefile b/src/prop/minisat/utils/Makefile deleted file mode 100644 index 204cea541..000000000 --- a/src/prop/minisat/utils/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -EXEC = system_test -DEPDIR = mtl - -include $(MROOT)/mtl/template.mk diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am deleted file mode 100644 index 46f6493a9..000000000 --- a/src/smt_util/Makefile.am +++ /dev/null @@ -1,20 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libsmtutil.la - -libsmtutil_la_SOURCES = \ - Makefile.am \ - Makefile.in \ - 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 - diff --git a/src/theory/.gitignore b/src/theory/.gitignore deleted file mode 100644 index 4d15f70c0..000000000 --- a/src/theory/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/theoryof_table.h diff --git a/src/theory/sets/.gitignore b/src/theory/sets/.gitignore deleted file mode 100644 index 4c83ffd6f..000000000 --- a/src/theory/sets/.gitignore +++ /dev/null @@ -1 +0,0 @@ -README.WHATS-NEXT diff --git a/src/util/Makefile b/src/util/Makefile deleted file mode 100644 index ea9087049..000000000 --- a/src/util/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/util - -include $(topdir)/Makefile.subdir diff --git a/src/util/Makefile.am b/src/util/Makefile.am deleted file mode 100644 index baa3286ab..000000000 --- a/src/util/Makefile.am +++ /dev/null @@ -1,118 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libutil.la - - -# Do not list built sources (like integer.h, rational.h) here! -# Rather, list them under BUILT_SOURCES, and their .in versions under -# EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is -# no good---they belong in the configured builds/ directory. If they -# end up in the source directory, they build the cvc4 that was -# configured at the time of the "make dist", which (1) may not be the -# configuration that the user wants, and (2) might cause link errors. -libutil_la_SOURCES = \ - Makefile.am \ - Makefile.in \ - 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 \ - floatingpoint.cpp \ - gmp_util.h \ - hash.h \ - index.cpp \ - index.h \ - maybe.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 - -BUILT_SOURCES = \ - floatingpoint.h \ - integer.h \ - rational.h - -if CVC4_CLN_IMP -libutil_la_SOURCES += \ - rational_cln_imp.cpp \ - integer_cln_imp.cpp -endif -if CVC4_GMP_IMP -libutil_la_SOURCES += \ - rational_gmp_imp.cpp \ - integer_gmp_imp.cpp -endif - - -EXTRA_DIST = \ - bitvector.i \ - bool.i \ - cardinality.i \ - divisible.i \ - floatingpoint.h.in \ - floatingpoint.i \ - hash.i \ - integer.h.in \ - integer.i \ - integer_cln_imp.cpp \ - integer_cln_imp.h \ - integer_gmp_imp.cpp \ - integer_gmp_imp.h \ - proof.i \ - rational.h.in \ - rational.i \ - rational_cln_imp.cpp \ - rational_cln_imp.h \ - rational_gmp_imp.cpp \ - rational_gmp_imp.h \ - regexp.i \ - resource_manager.i \ - result.i \ - sexpr.i \ - statistics.i \ - tuple.i \ - unsafe_interrupt_exception.i - - -DISTCLEANFILES = \ - floatingpoint.h.tmp \ - integer.h.tmp \ - rational.h.tmp \ - floatingpoint.h \ - integer.h \ - rational.h |