1######################################################################### 2# 3# This file is part of the Yices SMT Solver. 4# Copyright (C) 2017 SRI International. 5# 6# Yices is free software: you can redistribute it and/or modify 7# it under the terms of the GNU General Public License as published by 8# the Free Software Foundation, either version 3 of the License, or 9# (at your option) any later version. 10# 11# Yices is distributed in the hope that it will be useful, 12# but WITHOUT ANY WARRANTY; without even the implied warranty of 13# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 14# GNU General Public License for more details. 15# 16# You should have received a copy of the GNU General Public License 17# along with Yices. If not, see <http://www.gnu.org/licenses/>. 18# 19######################################################################### 20 21# 22# src/Makefile 23# 24# Must be invoked with the following variables set 25# 26# YICES_TOP_DIR = top-level directory for Yices 27# YICES_MODE = build mode 28# YICES_MAKE_INCLUDE = configuration file to include 29# YICES_VERSION = full version 30# MAJOR = major version number 31# MINOR = minor version number 32# PATCH_LEVEL = patch level 33# ARCH = architecture (e.g, i686-pc-linux-gnu) 34# POSIXOS = OS (e.g., linux) 35# BUILD = target build director (normally build/$(ARCH)-$(YICES_MODE)) 36# 37# Config variables are imported by including the file 38# $(YICES_TOP_DIR)/$(YICES_MAKE_INCLUDE) 39# 40 41SHELL=/bin/sh 42 43ifeq (,$(YICES_TOP_DIR)) 44 $(error "YICES_TOP_DIR is undefined") 45endif 46 47ifeq (,$(YICES_MAKE_INCLUDE)) 48 $(error "YICES_MAKE_INCLUDE is undefined") 49endif 50 51conf=$(YICES_TOP_DIR)/$(YICES_MAKE_INCLUDE) 52 53include $(conf) 54 55# 56# Build subdirectories 57# -------------------- 58# build/obj: object files, in a form suitable for the dynamic libraries 59# (e.g., compiled with option -fPIC) 60# build/static_obj: object files compiled in a form suitable for libyices.a 61# (e.g., compiled without -fPIC) 62# 63# build/lib: libraries (GMP not included) 64# build/bin: binaries (GMP not included) 65# 66# build/static_lib: libraries (GMP included) 67# build/static_bin: binaries linked statically with GMP (and other libraries if possible) 68# 69# For cygiwn and mingw: we use a third subdirectory to build objects for the 70# dll that includes libgmp.a 71# build/static_dll_obj 72# 73objdir := $(BUILD)/obj 74libdir := $(BUILD)/lib 75bindir := $(BUILD)/bin 76 77static_objdir := $(BUILD)/static_obj 78static_libdir := $(BUILD)/static_lib 79static_bindir := $(BUILD)/static_bin 80 81static_dll_objdir := $(BUILD)/static_dll_obj 82 83# 84# Distribution subdirectory: tarfiles are constructed 85# via make binary-distribution or make smt-distribution 86# 87# In this makefile, we just copy what needs to be included 88# in the distribution tarfiles in $(BUILD)/dist or $(BUILD)/static_dist 89# 90distdir := $(BUILD)/dist 91static_distdir := $(BUILD)/static_dist 92smt_distdir := $(BUILD)/smt_dist 93static_smt_distdir := $(BUILD)/static_smt_dist 94 95 96 97# 98# SOURCE FILES 99# 100 101# 102# Source files for the dynamic library (libyices.so) 103# 104core_src_c := \ 105 api/context_config.c \ 106 api/search_parameters.c \ 107 api/smt_logic_codes.c \ 108 api/yices_api.c \ 109 api/yices_error.c \ 110 api/yices_error_report.c \ 111 api/yval.c \ 112 context/assumption_stack.c \ 113 context/common_conjuncts.c \ 114 context/conditional_definitions.c \ 115 context/context.c \ 116 context/context_simplifier.c \ 117 context/context_solver.c \ 118 context/context_statistics.c \ 119 context/context_utils.c \ 120 context/divmod_table.c \ 121 context/eq_abstraction.c \ 122 context/eq_learner.c \ 123 context/internalization_table.c \ 124 context/ite_flattener.c \ 125 context/pseudo_subst.c \ 126 context/shared_terms.c \ 127 context/symmetry_breaking.c \ 128 exists_forall/ef_client.c \ 129 exists_forall/ef_analyze.c \ 130 exists_forall/ef_parameters.c \ 131 exists_forall/ef_problem.c \ 132 exists_forall/efsolver.c \ 133 frontend/smt2/attribute_values.c \ 134 frontend/yices/yices_lexer.c \ 135 frontend/yices/yices_parser.c \ 136 io/concrete_value_printer.c \ 137 io/model_printer.c \ 138 io/pretty_printer.c \ 139 io/reader.c \ 140 io/simple_printf.c \ 141 io/term_printer.c \ 142 io/tracer.c \ 143 io/type_printer.c \ 144 io/yices_pp.c \ 145 io/writer.c \ 146 model/abstract_values.c \ 147 model/arith_projection.c \ 148 model/concrete_values.c \ 149 model/fresh_value_maker.c \ 150 model/fun_maps.c \ 151 model/fun_trees.c \ 152 model/generalization.c \ 153 model/literal_collector.c \ 154 model/map_to_model.c \ 155 model/model_eval.c \ 156 model/model_queries.c \ 157 model/model_support.c \ 158 model/models.c \ 159 model/presburger.c \ 160 model/projection.c \ 161 model/term_to_val.c \ 162 model/val_to_term.c \ 163 mt/yices_locks.c \ 164 parser_utils/lexer.c \ 165 parser_utils/parser.c \ 166 parser_utils/term_stack2.c \ 167 parser_utils/term_stack_error.c \ 168 solvers/bv/bit_blaster.c \ 169 solvers/bv/bv64_intervals.c \ 170 solvers/bv/bv_atomtable.c \ 171 solvers/bv/bvconst_hmap.c \ 172 solvers/bv/bvexp_table.c \ 173 solvers/bv/bv_intervals.c \ 174 solvers/bv/bvpoly_compiler.c \ 175 solvers/bv/bvpoly_dag.c \ 176 solvers/bv/bvsolver.c \ 177 solvers/bv/bv_vartable.c \ 178 solvers/bv/dimacs_printer.c \ 179 solvers/bv/merge_table.c \ 180 solvers/bv/remap_table.c \ 181 solvers/cdcl/delegate.c \ 182 solvers/cdcl/gates_hash_table.c \ 183 solvers/cdcl/gates_manager.c \ 184 solvers/cdcl/new_gates.c \ 185 solvers/cdcl/new_gate_hash_map.c \ 186 solvers/cdcl/new_gate_hash_map2.c \ 187 solvers/cdcl/new_sat_solver.c \ 188 solvers/cdcl/smt_core.c \ 189 solvers/cdcl/truth_tables.c \ 190 solvers/cdcl/wide_truth_tables.c \ 191 solvers/egraph/composites.c \ 192 solvers/egraph/diseq_stacks.c \ 193 solvers/egraph/egraph_assertion_queues.c \ 194 solvers/egraph/egraph.c \ 195 solvers/egraph/egraph_explanations.c \ 196 solvers/egraph/egraph_utils.c \ 197 solvers/egraph/theory_explanations.c \ 198 solvers/floyd_warshall/dl_vartable.c \ 199 solvers/floyd_warshall/idl_floyd_warshall.c \ 200 solvers/floyd_warshall/rdl_floyd_warshall.c \ 201 solvers/funs/fun_solver.c \ 202 solvers/simplex/arith_atomtable.c \ 203 solvers/simplex/arith_vartable.c \ 204 solvers/simplex/diophantine_systems.c \ 205 solvers/simplex/gomory_cuts.c \ 206 solvers/simplex/integrality_constraints.c \ 207 solvers/simplex/matrices.c \ 208 solvers/simplex/offset_equalities.c \ 209 solvers/simplex/simplex.c \ 210 terms/balanced_arith_buffers.c \ 211 terms/bit_expr.c \ 212 terms/bit_term_conversion.c \ 213 terms/bv64_interval_abstraction.c \ 214 terms/bv64_constants.c \ 215 terms/bv64_polynomials.c \ 216 terms/bvarith64_buffers.c \ 217 terms/bvarith64_buffer_terms.c \ 218 terms/bvarith_buffers.c \ 219 terms/bvarith_buffer_terms.c \ 220 terms/bv_constants.c \ 221 terms/bvfactor_buffers.c \ 222 terms/bvlogic_buffers.c \ 223 terms/bvpoly_buffers.c \ 224 terms/bv_polynomials.c \ 225 terms/bv_slices.c \ 226 terms/conditionals.c \ 227 terms/elim_subst.c \ 228 terms/extended_rationals.c \ 229 terms/free_var_collector.c \ 230 terms/full_subst.c \ 231 terms/int_rational_hash_maps.c \ 232 terms/ite_stack.c \ 233 terms/mpq_aux.c \ 234 terms/mpq_stores.c \ 235 terms/poly_buffer.c \ 236 terms/poly_buffer_terms.c \ 237 terms/polynomials.c \ 238 terms/power_products.c \ 239 terms/pprod_table.c \ 240 terms/rational_hash_maps.c \ 241 terms/rationals.c \ 242 terms/rba_buffer_terms.c \ 243 terms/renaming_context.c \ 244 terms/subst_cache.c \ 245 terms/subst_context.c \ 246 terms/term_explorer.c \ 247 terms/term_manager.c \ 248 terms/terms.c \ 249 terms/term_sets.c \ 250 terms/term_substitution.c \ 251 terms/term_utils.c \ 252 terms/types.c \ 253 terms/variable_renaming.c \ 254 utils/arena.c \ 255 utils/backtrack_arrays.c \ 256 utils/backtrack_int_hash_map.c \ 257 utils/cache.c \ 258 utils/csets.c \ 259 utils/cputime.c \ 260 utils/dep_tables.c \ 261 utils/gcd.c \ 262 utils/generic_heap.c \ 263 utils/hash_functions.c \ 264 utils/index_vectors.c \ 265 utils/int_array_hsets.c \ 266 utils/int_array_sort2.c \ 267 utils/int_array_sort.c \ 268 utils/int_bags.c \ 269 utils/int_bv_sets.c \ 270 utils/int_harray_store.c \ 271 utils/int_hash_classes.c \ 272 utils/int_hash_map2.c \ 273 utils/int_hash_map.c \ 274 utils/int_hash_sets.c \ 275 utils/int_hash_tables.c \ 276 utils/int_heap2.c \ 277 utils/int_heap.c \ 278 utils/int_partitions.c \ 279 utils/int_powers.c \ 280 utils/int_queues.c \ 281 utils/int_stack.c \ 282 utils/int_vectors.c \ 283 utils/mark_vectors.c \ 284 utils/memalloc.c \ 285 utils/object_stores.c \ 286 utils/pair_hash_map.c \ 287 utils/pair_hash_map2.c \ 288 utils/pointer_vectors.c \ 289 utils/ptr_array_sort2.c \ 290 utils/ptr_array_sort.c \ 291 utils/ptr_hash_classes.c \ 292 utils/ptr_hash_map.c \ 293 utils/ptr_heap.c \ 294 utils/ptr_partitions.c \ 295 utils/ptr_queues.c \ 296 utils/ptr_sets.c \ 297 utils/ptr_sets2.c \ 298 utils/ptr_stack.c \ 299 utils/ptr_vectors.c \ 300 utils/refcount_int_arrays.c \ 301 utils/refcount_strings.c \ 302 utils/resize_arrays.c \ 303 utils/simple_cache.c \ 304 utils/simple_int_stack.c \ 305 utils/sparse_arrays.c \ 306 utils/stable_sort.c \ 307 utils/string_buffers.c \ 308 utils/string_utils.c \ 309 utils/symbol_tables.c \ 310 utils/tag_map.c \ 311 utils/tuple_hash_map.c \ 312 utils/uint_array_sort.c \ 313 utils/uint_array_sort2.c \ 314 utils/uint_rbtrees.c \ 315 utils/use_vectors.c \ 316 utils/vector_hash_map.c 317 318# 319# Optional: mcsat solver 320# 321mcsat_src_c := \ 322 mcsat/tracing.c \ 323 mcsat/solver.c \ 324 mcsat/variable_db.c \ 325 mcsat/variable_queue.c \ 326 mcsat/value.c \ 327 mcsat/model.c \ 328 mcsat/trail.c \ 329 mcsat/conflict.c \ 330 mcsat/gc.c \ 331 mcsat/eq/equality_graph.c \ 332 mcsat/eq/merge_queue.c \ 333 mcsat/utils/int_mset.c \ 334 mcsat/utils/int_lset.c \ 335 mcsat/utils/value_hash_map.c \ 336 mcsat/utils/value_vector.c \ 337 mcsat/utils/scope_holder.c \ 338 mcsat/utils/statistics.c \ 339 mcsat/utils/substitution.c \ 340 mcsat/uf/uf_plugin.c \ 341 mcsat/bool/clause_db.c \ 342 mcsat/bool/cnf.c \ 343 mcsat/bool/bcp_watch_manager.c \ 344 mcsat/bool/bool_plugin.c \ 345 mcsat/nra/nra_plugin.c \ 346 mcsat/nra/nra_plugin_internal.c \ 347 mcsat/nra/nra_plugin_explain.c \ 348 mcsat/nra/libpoly_utils.c \ 349 mcsat/nra/poly_constraint.c \ 350 mcsat/nra/feasible_set_db.c \ 351 mcsat/ite/ite_plugin.c \ 352 mcsat/bv/bv_plugin.c \ 353 mcsat/bv/bv_bdd_manager.c \ 354 mcsat/bv/bv_evaluator.c \ 355 mcsat/bv/bv_explainer.c \ 356 mcsat/bv/bv_feasible_set_db.c \ 357 mcsat/bv/bdd_computation.c \ 358 mcsat/bv/explain/arith_utils.c \ 359 mcsat/bv/explain/arith_norm.c \ 360 mcsat/bv/explain/arith_intervals.c \ 361 mcsat/bv/explain/arith.c \ 362 mcsat/bv/explain/eq_ext_con.c \ 363 mcsat/bv/explain/full_bv_sat.c \ 364 mcsat/bv/explain/full_bv_trivial.c \ 365 mcsat/watch_list_manager.c \ 366 mcsat/preprocessor.c \ 367 mcsat/options.c 368 369 370 371# 372# Fake mcsat module: do nothing. Used to make the compilation go through. 373# 374no_mcsat_src_c := \ 375 mcsat/no_mcsat.c \ 376 mcsat/options.c 377 378 379# 380# Other source files for libyices.a 381# That's all the code needed by the main binaries 382# + experimental/unfinished modules 383# + functions for printing/debugging 384# + old stuff not needed anymore (except for tests) 385# 386extra_src_c := \ 387 context/context_parameters.c \ 388 context/context_printer.c \ 389 context/dump_context.c \ 390 context/internalization_printer.c \ 391 frontend/common/assumptions_and_core.c \ 392 frontend/common/assumption_table.c \ 393 frontend/common/bug_report.c \ 394 frontend/common/named_term_stacks.c \ 395 frontend/common/parameters.c \ 396 frontend/common/tables.c \ 397 frontend/smt1/smt_lexer.c \ 398 frontend/smt1/smt_parser.c \ 399 frontend/smt1/smt_term_stack.c \ 400 frontend/smt2/parenthesized_expr.c \ 401 frontend/smt2/smt2_commands.c \ 402 frontend/smt2/smt2_expressions.c \ 403 frontend/smt2/smt2_lexer.c \ 404 frontend/smt2/smt2_model_printer.c \ 405 frontend/smt2/smt2_parser.c \ 406 frontend/smt2/smt2_printer.c \ 407 frontend/smt2/smt2_symbol_printer.c \ 408 frontend/smt2/smt2_term_stack.c \ 409 frontend/smt2/smt2_type_printer.c \ 410 frontend/yices/arith_solver_codes.c \ 411 frontend/yices/labeled_assertions.c \ 412 frontend/yices/yices_help.c \ 413 frontend/yices/yices_reval.c \ 414 model/large_bvsets.c \ 415 model/rb_bvsets.c \ 416 model/small_bvsets.c \ 417 scratch/booleq_table.c \ 418 scratch/bool_vartable.c \ 419 scratch/update_graph.c \ 420 solvers/bv/bvsolver_printer.c \ 421 solvers/cdcl/clause_pool.c \ 422 solvers/cdcl/gates_printer.c \ 423 solvers/cdcl/sat_solver.c \ 424 solvers/cdcl/smt_core_printer.c \ 425 solvers/egraph/egraph_printer.c \ 426 solvers/floyd_warshall/idl_fw_printer.c \ 427 solvers/floyd_warshall/rdl_fw_printer.c \ 428 solvers/funs/fun_solver_printer.c \ 429 solvers/simplex/dsolver_printer.c \ 430 solvers/simplex/int_constraint_printer.c \ 431 solvers/simplex/simplex_printer.c \ 432 solvers/simplex/simplex_prop_table.c \ 433 terms/arith_buffers.c \ 434 utils/command_line.c \ 435 utils/memsize.c \ 436 utils/pair_hash_sets.c \ 437 utils/string_hash_map.c \ 438 utils/timeout.c \ 439 utils/union_find.c 440 441 442# 443# Optional for libyices.a: support for launching threads 444# and testing multi-threaded code 445# 446extra_thread_src_c := \ 447 mt/threads.c 448 449 450# 451# base: core + mcsat if MCSAT is enabled or core + fake mcsat 452# 453ifeq ($(ENABLE_MCSAT),yes) 454base_src_c := $(core_src_c) $(mcsat_src_c) 455else 456base_src_c := $(core_src_c) $(no_mcsat_src_c) 457endif 458 459# 460# all sources: base + extra 461# 462src_c := $(base_src_c) $(extra_src_c) 463ifeq ($(THREAD_SAFE),1) 464src_c := $(src_c) $(extra_thread_src_c) 465endif 466 467# 468# additional source files for the binaries 469# 470bin_src_c := \ 471 frontend/yices.c \ 472 frontend/yices_sat.c \ 473 frontend/yices_sat_new.c \ 474 frontend/yices_smt.c \ 475 frontend/yices_smt2.c \ 476 frontend/yices_smt2_mt.c \ 477 frontend/yices_smtcomp.c \ 478 479# 480# Auto-generated version file 481# 482version_c := api/yices_$(YICES_MODE)_version.c 483 484# 485# All auto-generated files 486# 487auto_generated := \ 488 $(version_c) \ 489 frontend/yices/yices_hash_keywords.h \ 490 frontend/smt1/smt_hash_keywords.h \ 491 frontend/smt2/smt2_hash_tokens.h \ 492 frontend/smt2/smt2_hash_keywords.h \ 493 frontend/smt2/smt2_hash_symbols.h 494 495# 496# Dependencies and object files 497# 498obj := $(src_c:%.c=$(objdir)/%.o) 499dep := $(src_c:%.c=$(objdir)/%.d) 500static_obj := $(src_c:%.c=$(static_objdir)/%.o) 501static_dep := $(src_c:%.c=$(static_objdir)/%.d) 502 503bin_obj := $(bin_src_c:%.c=$(objdir)/%.o) 504bin_dep := $(bin_src_c:%.c=$(objdir)/%.d) 505static_bin_obj = $(bin_src_c:%.c=$(static_objdir)/%.o) 506static_bin_dep = $(bin_src_c:%.c=$(static_objdir)/%.d) 507 508version_obj := $(objdir)/api/yices_version.o 509version_dep := $(version_c:%.c=$(objdir)/%.d) 510static_version_obj := $(static_objdir)/api/yices_version.o 511static_version_dep := $(version_c:%.c=$(static_objdir)/%.d) 512 513# extras for mingw and cygwin 514static_dll_obj := $(src_c:%.c=$(static_dll_objdir)/%.o) 515static_dll_dep := $(src_c:%.c=$(static_dll_objdir)/%.d) 516static_dll_version_obj := $(static_dll_objdir)/api/yices_version.o 517static_dll_version_dep := $(version_c:%.c=$(static_dll_objdir)/%.d) 518 519 520# 521# Static libraries 522# 523libyices := $(libdir)/libyices.a 524static_libyices := $(static_libdir)/libyices.a 525 526 527# 528# Binaries 529# 530# binaries := $(bin_src_c:%.c=$(bindir)/%$(EXEEXT)) 531# static_binaries := $(bin_src_c:%.c=$(static_bindir)/%$(EXEEXT)) 532binaries := $(addprefix $(bindir)/,$(notdir $(bin_src_c:%.c=%$(EXEEXT)))) 533static_binaries := $(addprefix $(static_bindir)/,$(notdir $(bin_src_c:%.c=%$(EXEEXT)))) 534 535 536# 537# DYNAMIC LIBRARIES 538# 539 540# 541# Linux/Solaris/FreeBSD 542# the library has full versioned name libyices.so.2.X.Y 543# soname: libyices.so.2.X 544# 545# For Free BSD: the convention seems to be libyices.so.2.X 546# 547ifeq ($(POSIXOS),dragonfly) 548libyices_so := libyices.so.$(MAJOR).$(MINOR) 549else 550libyices_so := libyices.so.$(YICES_VERSION) 551endif 552 553libyices_soname := libyices.so.$(MAJOR).$(MINOR) 554 555 556# 557# Darwin 558# library name: libyices.2.dylib 559# version and compatibility numbers for Darwin 560# install name: /usr/local/lib/libyices.2.dylib 561# 562# 2014/10/22: changed install name to use the $(prefix) 563# set by configure. 564# 565# TODO?: we should use $(libdir) instead of $(prefix)/lib but 566# this clashes with the $(libdir) set at the beginning of this 567# Makefile. 568# 569libyices_dylib := libyices.$(MAJOR).dylib 570libyices_curr_version := $(MAJOR).$(MINOR).$(PATCH_LEVEL) 571libyices_compat_version := $(MAJOR).$(MINOR).0 572libyices_install_name := $(prefix)/lib/libyices.$(MAJOR).dylib 573 574# 575# Cygwin and mingw: 576# the DLL is called cygyices.dll on cygwin 577# and libyices.dll on mingw 578# both systems use an import library called libyices.dll.a 579# 580# On mingw, we also produce libyices.def, which can be 581# used to produce an import library compatible with the Microsoft 582# compilation tools (and Visual Studio). 583# 584libyices_dll := cygyices.dll 585libyices_mingw_dll := libyices.dll 586 587libyices_implib=libyices.dll.a 588libyices_def=libyices.def 589 590 591 592 593########################### 594# COMPILATION FLAGS # 595########################### 596 597# 598# Whether we are building for a big endian architecture 599# 600ifeq ($(WORDS_BIGENDIAN),yes) 601 CPPFLAGS += -DWORDS_BIGENDIAN 602endif 603 604# 605# Whether we have support for mcsat 606# 607ifeq ($(ENABLE_MCSAT),yes) 608 CPPFLAGS += -DHAVE_MCSAT 609endif 610 611# 612# Whether we have thread safety 613# If so on Unix systems, we must add -pthread to CFLAGS 614# 615PTRHEAD= 616ifeq ($(THREAD_SAFE),1) 617 CPPFLAGS += -DTHREAD_SAFE 618 PTHREAD= -pthread 619endif 620 621 622# 623# OS-dependent compilation flags + which dynamic libraries to build 624# libyices_dynamic = dynamic library for make lib 625# static_libyices_dynamic = dynamic library for make static-lib 626# 627# -fPIC: PIC is the default on Darwin/Cygwin/Mingw (and causes 628# compilation warning on the latter two if present) 629# 630# -static: is not supported by Darwin or our Solaris2.10 machine 631# 632# BIN_LDFLAGS: LDFLAGS used when building executables 633# this is used to increase the stack size on cygwin/mingw (to 8Mbytes) 634# 635ifeq ($(POSIXOS),cygwin) 636 CPPFLAGS := $(CPPFLAGS) -DCYGWIN 637 PIC= 638 STATIC=-static -static-libgcc 639 BIN_LDFLAGS= -Wl,--stack,8388608 640 libyices_dynamic=$(bindir)/$(libyices_dll) 641 static_libyices_dynamic=$(static_bindir)/$(libyices_dll) 642else 643ifeq ($(POSIXOS),mingw) 644 CPPFLAGS := $(CPPFLAGS) -DMINGW -D__USE_MINGW_ANSI_STDIO 645 PIC= 646 STATIC=-static -static-libgcc 647 BIN_LDFLAGS= -Wl,--stack,8388608 648 libyices_dynamic=$(bindir)/$(libyices_mingw_dll) 649 static_libyices_dynamic=$(static_bindir)/$(libyices_mingw_dll) 650else 651ifeq ($(POSIXOS),darwin) 652 CPPFLAGS := $(CPPFLAGS) -DMACOSX 653 CFLAGS += -fvisibility=hidden $(PTHREAD) 654 PIC=-fPIC 655 STATIC= 656 BIN_LDFLAGS= 657 libyices_dynamic=$(libdir)/$(libyices_dylib) 658 static_libyices_dynamic=$(static_libdir)/$(libyices_dylib) 659 660 # 661 # To stop a clang warning when we compile with -pthread, 662 # we add option -Qunused-arguments 663 # 664 # Detect clang-disguised-as-gcc vs. GNU GCC 665 # 666 ifeq ($(THREAD_SAFE),1) 667 ifeq ($(shell $(CC) -v 2>&1 | grep -c "clang version"), 1) 668 CFLAGS += -Qunused-arguments 669 endif 670 endif 671else 672ifeq ($(POSIXOS),sunos) 673 PIC=-fPIC 674 STATIC= 675 CPPFLAGS := $(CPPFLAGS) -DSOLARIS 676 CFLAGS += -fvisibility=hidden $(PTHREAD) 677 BIN_LDFLAGS= 678 libyices_dynamic=$(libdir)/$(libyices_so) 679 static_libyices_dynamic=$(static_libdir)/$(libyices_so) 680else 681ifeq ($(POSIXOS),linux) 682 PIC=-fPIC 683 STATIC=-static 684 CPPFLAGS := $(CPPFLAGS) -DLINUX -U_FORTIFY_SOURCE 685 CFLAGS += -fvisibility=hidden $(PTHREAD) 686 BIN_LDFLAGS= $(PTHREAD) 687 libyices_dynamic=$(libdir)/$(libyices_so) 688 static_libyices_dynamic=$(static_libdir)/$(libyices_so) 689else 690ifeq ($(POSIXOS),dragonfly) 691 PIC=-fPIC 692 STATIC=-static 693 CPPFLAGS := $(CPPFLAGS) -DFREEBSD 694 CFLAGS += -fvisibility=hidden $(PTHREAD) 695 BIN_LDFLAGS= 696 libyices_dynamic=$(libdir)/$(libyices_so) 697 static_libyices_dynamic=$(static_libdir)/$(libyices_so) 698 699else 700ifeq ($(POSIXOS),netbsd) 701 PIC=-fPIC 702 STATIC=-static 703 CPPFLAGS := $(CPPFLAGS) -DNETBSD 704 CFLAGS += -fvisibility=hidden $(PTHREAD) 705 BIN_LDFLAGS= 706 libyices_dynamic=$(libdir)/$(libyices_so) 707 static_libyices_dynamic=$(static_libdir)/$(libyices_so) 708 709else 710ifeq ($(POSIXOS),unix) 711 PIC=-fPIC 712 STATIC=-static 713 CPPFLAGS := $(CPPFLAGS) -DLINUX 714 CFLAGS += -fvisibility=hidden $(PTHREAD) 715 BIN_LDFLAGS= 716 libyices_dynamic=$(libdir)/$(libyices_so) 717 static_libyices_dynamic=$(static_libdir)/$(libyices_so) 718else 719 $(error "Don't know how to compile on $(POSIXOS)") 720endif 721endif 722endif 723endif 724endif 725endif 726endif 727endif 728 729# 730# include dirs: we want -I. first 731# 732CPPFLAGS := -I. -Iinclude $(CPPFLAGS) 733 734# 735# Warning levels: dropped the flag -Winiline in all build modes. 736# Can't keep up with gcc/clang. 737# 738CFLAGS += -Wall -Wredundant-decls 739 740# 741# Format string issues on Windows/mingw 742# 743ifeq ($(POSIXOS),mingw) 744 CFLAGS += -Wno-format 745endif 746 747 748 749 750# 751# Compilation flags dependent on MODE 752# 753# Option -fomit-frame-pointer confuses the Mac OS profiling tools 754# (don't use it if MODE=profile). 755# 756# Option -fno-stack-protector is useful on Ubuntu (and probably other 757# Linux distributions). On these distributions, gcc has 758# -fstack-protector enabled by default. This can cause link-time 759# errors on the user's systems: 760# undefined reference to '__stack_chk_fail'. 761# However this option is not supported by older versions of GCC (before gcc-4.1?) 762# 763# Update: 02/16/2012: we check whether -fno-stack-protector is supported 764# in the configure script. The script sets variable $(NO_STACK_PROTECTOR) 765# properly. 766# 767# Related issue reported by Richard Corden (January 18, 2016) 768# Ubuntu sets -D_FORTIFY_SOURCE=2 by default (to detect buffer overflows 769# and other security issues). This causes link-time issues again: 770# undefined reference to __longjmp_chk. 771# The fix is to add -U_FORTIFY_SOURCE when we compile on linux 772# 773# To link with google gperftools: 774# on Linux we add the flag -Wl,--no-as-needed otherwise the profiler 775# library may not be linked with the binaries. (Because some 776# Linux distributions set -Wl,--as-needed by default). 777# 778# 779ifeq ($(YICES_MODE),release) 780CFLAGS := $(CFLAGS) -O3 -fomit-frame-pointer $(NO_STACK_PROTECTOR) 781CPPFLAGS := $(CPPFLAGS) -DNDEBUG 782else 783ifeq ($(YICES_MODE),devel) 784CFLAGS := $(CFLAGS) -O3 -g -fomit-frame-pointer $(NO_STACK_PROTECTOR) 785CPPFLAGS := $(CPPFLAGS) 786else 787ifeq ($(YICES_MODE),profile) 788CFLAGS := $(CFLAGS) -O3 -pg 789CPPFLAGS := $(CPPFLAGS) -DNDEBUG 790else 791ifeq ($(YICES_MODE),gcov) 792CFLAGS := $(CFLAGS) -fprofile-arcs -ftest-coverage -g -O0 793CPPFLAGS := $(CPPFLAGS) -DNDEBUG 794else 795ifeq ($(findstring $(YICES_MODE),valgrind quantify purify),$(YICES_MODE)) 796CFLAGS := $(CFLAGS) -O3 -g 797CPPFLAGS := $(CPPFLAGS) -DNDEBUG 798else 799ifeq ($(YICES_MODE),gperftools) 800CFLAGS := $(CFLAGS) -O3 -g 801CPPFLAGS := $(CPPFLAGS) -DNDEBUG 802ifeq ($(POSIXOS),linux) 803 LIBS += -Wl,--no-as-needed -lprofiler 804else 805 LIBS += -lprofiler 806endif 807else 808# 809# debug mode 810# 811CFLAGS := $(CFLAGS) -g 812endif 813endif 814endif 815endif 816endif 817endif 818 819 820# 821# Object files to include in the dynamic libraries 822# 823ifeq ($(YICES_MODE),release) 824base_obj := $(base_src_c:%.c=$(objdir)/%.o) 825static_base_obj := $(base_src_c:%.c=$(static_objdir)/%.o) 826static_dll_base_obj := $(base_src_c:%.c=$(static_dll_objdir)/%.o) 827else 828base_obj := $(obj) 829static_base_obj := $(static_obj) 830static_dll_base_obj := $(static_dll_obj) 831endif 832 833 834# 835# Link command for purify/quantify 836# 837ifeq ($(POSIXOS),sunos) 838ifeq ($(YICES_MODE),purify) 839LNK := purify $(CC) 840else 841ifeq ($(YICES_MODE),quantify) 842LNK := quantify $(CC) 843else 844LNK := $(CC) 845endif 846endif 847else 848LNK := $(CC) 849endif 850 851 852# 853# More CPPFLAGS for compiling static objects 854# 855ifneq ($(STATIC_GMP_INCLUDE_DIR),) 856 STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) 857endif 858 859ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) 860 STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) 861endif 862 863STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) 864 865# 866# For building dll linked statically with libgmp.a 867# we use the STATIC_CPPFLAGS (so that we use the right version of gmp.h) 868# For building the binaries linked statically with libgmp.a, 869# we also add the NOYICES_DLL flag. 870# 871ifeq ($(POSIXOS),cygwin) 872 STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) 873 STATIC_CPPFLAGS += -DNOYICES_DLL 874else 875ifeq ($(POSIXOS),mingw) 876 STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) 877 STATIC_CPPFLAGS += -DNOYICES_DLL 878endif 879endif 880 881 882# 883# LIBS for compiling in static mode 884# 885# We need to remove -lgmp and -lpoly from LIBS in static mode, otherwise adding 886# $(STATIC_GMP) does not work on Darwin and cygwin 887# We also use $(NOGMP_LIBS) to build yices_sat. 888# 889# Important: make sure the GMP library is last (if some 890# archives/libraries in NOGMP_LIBS depend on GMP). 891# 892NOGMP_LIBS := $(subst -lpoly,,$(subst -lgmp,,$(LIBS))) 893STATIC_LIBS := $(NOGMP_LIBS) $(STATIC_LIBPOLY) $(STATIC_GMP) 894PIC_LIBS := $(NOGMP_LIBS) $(PIC_LIBPOLY) $(PIC_GMP) 895 896 897 898################# 899# BUILD RULES # 900################# 901 902# 903# Dependency files 904# 905$(objdir)/%.d: %.c 906 @set -e; echo Building dependency file $@ ; \ 907 $(CC) -MM -MG -MT $*.o $(CFLAGS) $(CPPFLAGS) $< > $@.$$$$ ; \ 908 $(SED) 's,\($*\).o[ :]*,$(objdir)/\1.o $@ : , g' < $@.$$$$ > $@ ; \ 909 rm -f $@.$$$$ 910 911$(static_objdir)/%.d: %.c 912 @set -e; echo Building dependency file $@ ; \ 913 $(CC) -MM -MG -MT $*.o $(CFLAGS) $(STATIC_CPPFLAGS) $< > $@.$$$$ ; \ 914 $(SED) 's,\($*\).o[ :]*,$(static_objdir)/\1.o $@ : , g' < $@.$$$$ > $@ ; \ 915 rm -f $@.$$$$ 916 917$(static_dll_objdir)/%.d: %.c 918 @set -e; echo Building dependency file $@ ; \ 919 $(CC) -MM -MG -MT $*.o $(CFLAGS) $(STATIC_DLL_CPPFLAGS) $< > $@.$$$$ ; \ 920 $(SED) 's,\($*\).o[ :]*,$(static_dll_objdir)/\1.o $@ : , g' < $@.$$$$ > $@ ; \ 921 rm -f $@.$$$$ 922 923ifneq ($(MAKECMDGOALS),clean) 924 925static_goals := $(filter static-%,$(MAKECMDGOALS)) 926dyn_goals := $(filter-out static-%,$(MAKECMDGOALS)) 927 928ifneq ($(dyn_goals),) 929 include $(dep) 930 include $(bin_dep) 931 include $(version_dep) 932endif 933 934ifneq ($(static_goals),) 935 include $(static_dep) 936 include $(static_bin_dep) 937 include $(static_version_dep) 938 ifeq ($(POSIXOS),mingw) 939 include $(static_dll_dep) 940 include $(static_dll_version_dep) 941 else 942 ifeq ($(POSIXOS),cygwin) 943 include $(static_dll_dep) 944 include $(static_dll_version_dep) 945 endif 946 endif 947endif 948 949endif 950 951# 952# Gperf generated tables 953# - we need to give different names to the yices and smt lookup functions 954# 955frontend/yices/yices_hash_keywords.h: frontend/yices/yices_keywords.txt 956 $(GPERF) -C -L ANSI-C -W yices_kw --output-file=frontend/yices/yices_hash_keywords.h \ 957 --lookup-function-name=in_yices_kw frontend/yices/yices_keywords.txt 958 959frontend/smt1/smt_hash_keywords.h: frontend/smt1/smt_keywords.txt 960 $(GPERF) -C -L ANSI-C -W smt_kw --output-file=frontend/smt1/smt_hash_keywords.h \ 961 --lookup-function-name=in_smt_kw frontend/smt1/smt_keywords.txt 962 963# 964# Tables for SMT2: 965# - we want to include three hash functions in the same file (smt2_lexer.c) 966# - for this to work, 967# we need to give different names to the hash function (option -H ...) 968# we can't use -G and we must give -E 969# 970frontend/smt2/smt2_hash_tokens.h: frontend/smt2/smt2_tokens.txt 971 $(GPERF) -C -L ANSI-C -W smt2_tk -H hash_tk -E --output-file=frontend/smt2/smt2_hash_tokens.h \ 972 --lookup-function-name=in_smt2_tk frontend/smt2/smt2_tokens.txt 973 974frontend/smt2/smt2_hash_keywords.h: frontend/smt2/smt2_keywords.txt 975 $(GPERF) -C -L ANSI-C -W smt2_kw -H hash_kw -E --output-file=frontend/smt2/smt2_hash_keywords.h \ 976 --lookup-function-name=in_smt2_kw frontend/smt2/smt2_keywords.txt 977 978frontend/smt2/smt2_hash_symbols.h: frontend/smt2/smt2_symbols.txt 979 $(GPERF) -C -L ANSI-C -W smt2_sym -H hash_sym -E --output-file=frontend/smt2/smt2_hash_symbols.h \ 980 --lookup-function-name=in_smt2_sym frontend/smt2/smt2_symbols.txt 981 982# 983# Object files 984# 985$(version_obj): $(version_c) 986 $(CC) $(CPPFLAGS) $(CFLAGS) $(PIC) -c $(version_c) -o $(version_obj) 987 988$(objdir)/%.o: %.c 989 $(CC) $(CPPFLAGS) $(CFLAGS) $(PIC) -c $< -o $@ 990 991$(static_version_obj): $(version_c) 992 $(CC) -DYICES_STATIC $(STATIC_CPPFLAGS) $(CFLAGS) -c $(version_c) -o $(static_version_obj) 993 994$(static_dll_version_obj): $(version_c) 995 $(CC) -DYICES_STATIC $(STATIC_DLL_CPPFLAGS) $(CFLAGS) -c $(version_c) -o $(static_dll_version_obj) 996 997$(static_objdir)/%.o: %.c 998 $(CC) $(STATIC_CPPFLAGS) $(CFLAGS) -c $< -o $@ 999 1000$(static_dll_objdir)/%.o: %.c 1001 $(CC) $(STATIC_DLL_CPPFLAGS) $(CFLAGS) -c $< -o $@ 1002 1003# 1004# Static libraries 1005# 1006$(libyices): $(obj) $(version_obj) 1007 @ rm -f $(libyices) 1008 $(AR) cr $(libyices) $(obj) $(version_obj) 1009 $(RANLIB) $(libyices) 1010 1011$(static_libyices): $(static_obj) $(static_version_obj) 1012 @ rm -f $(static_libyices) 1013 $(AR) cr $(static_libyices) $(static_obj) $(static_version_obj) 1014 $(RANLIB) $(static_libyices) 1015 1016 1017# 1018# Executables 1019# 1020 1021# for yices_sat: we don't need gmp 1022$(bindir)/yices_sat$(EXEEXT): $(objdir)/frontend/yices_sat.o $(libyices) 1023 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) \ 1024 -o $@ $< $(libyices) $(NOGMP_LIBS) 1025 1026$(static_bindir)/yices_sat$(EXEEXT): $(static_objdir)/frontend/yices_sat.o $(static_libyices) 1027 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) $(STATIC) \ 1028 -o $@ $< $(static_libyices) $(NOGMP_LIBS) 1029 1030$(bindir)/yices_sat_new$(EXEEXT): $(objdir)/frontend/yices_sat_new.o $(libyices) 1031 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) \ 1032 -o $@ $< $(libyices) $(NOGMP_LIBS) 1033 1034$(static_bindir)/yices_sat_new$(EXEEXT): $(static_objdir)/frontend/yices_sat_new.o $(static_libyices) 1035 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) $(STATIC) \ 1036 -o $@ $< $(static_libyices) $(NOGMP_LIBS) 1037 1038 1039# for all other executables 1040$(bindir)/%$(EXEEXT): $(objdir)/frontend/%.o $(libyices) 1041 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) \ 1042 -o $@ $< $(libyices) $(LIBS) 1043 1044$(static_bindir)/%$(EXEEXT): $(static_objdir)/frontend/%.o $(static_libyices) 1045 $(LNK) $(CFLAGS) $(LDFLAGS) $(BIN_LDFLAGS) $(STATIC) \ 1046 -o $@ $< $(static_libyices) $(STATIC_LIBS) 1047 1048 1049# 1050# For dynamic libraries, the rules are platform-dependent. 1051# 1052 1053# 1054# linux + solaris + FreeBSD 1055# 1056# NOTE: by passing flag --no-undefined to ld, we should 1057# get an error if something is missing in the base_obj 1058# list. This flag causes problems on our Solaris 2.10 1059# machine, unless we also give -lc. 1060# 1061$(libdir)/$(libyices_so): $(base_obj) $(version_obj) 1062 $(CC) $(CFLAGS) $(LDFLAGS) -shared -o $@ \ 1063 -Wl,-soname,$(libyices_soname) -Wl,--no-undefined \ 1064 $(base_obj) $(version_obj) $(LIBS) -lc 1065ifeq ($(YICES_MODE),release) 1066 $(STRIP) -x $@ 1067endif 1068 1069$(static_libdir)/$(libyices_so): $(base_obj) $(version_obj) 1070 $(CC) $(CFLAGS) $(LDFLAGS) -shared -o $@ \ 1071 -Wl,-soname,$(libyices_soname) -Wl,--no-undefined \ 1072 $(base_obj) $(version_obj) $(PIC_LIBS) -lc 1073ifeq ($(YICES_MODE),release) 1074 $(STRIP) -x $@ 1075endif 1076 1077# 1078# DLL on cygwin 1079# the DLL is called cygyices.dll 1080# the linker creates libyices.dll.a (import library) 1081# 1082# To use these files on cygwin 1083# copy libyices.dll.a in /lib (or /usr/lib) 1084# copy cygyices.dll in /bin (or /usr/bin) 1085# link the code using the flags -lyices -lgmp 1086# 1087# Change: 2012/07/12 (following e-mail from Dave Vitek, Grammatech): 1088# build the DLLs in bindir or static_bindir, instead of libdir and 1089# static_libdir. 1090# 1091$(bindir)/$(libyices_dll): $(base_obj) $(version_obj) 1092 $(CC) $(CFLAGS) $(LDFLAGS) -shared -o $@ \ 1093 -Wl,--out-implib=$(libdir)/$(libyices_implib) \ 1094 -Wl,--no-undefined \ 1095 $(base_obj) $(version_obj) $(LIBS) 1096ifeq ($(YICES_MODE),release) 1097 $(STRIP) $@ 1098endif 1099 1100$(static_bindir)/$(libyices_dll): $(static_dll_base_obj) $(static_dll_version_obj) 1101 $(CC) $(CFLAGS) $(LDFLAGS) -shared -o $@ \ 1102 -Wl,--out-implib=$(static_libdir)/$(libyices_implib) \ 1103 -Wl,--no-undefined \ 1104 $(static_dll_base_obj) $(static_dll_version_obj) $(PIC_LIBS) 1105ifeq ($(YICES_MODE),release) 1106 $(STRIP) -x $@ 1107endif 1108 1109 1110# 1111# DLL on mingw: more-or-less like cygwin 1112# the DLL is called libyices.dll 1113# the linker creates libyices.dll.a (import library) and libyices.def 1114# 1115# To use libyices.dll on windows 1116# construct libyices.lib from libyices.def using the Microsoft lib tool 1117# lib /machine:i386 /def:libyices.def 1118# 1119# Change: 2012/07/12 as above: build DLLs in bin directories. 1120# Change: 2013/07/12: added -static-libgcc (otherwise the DLLs 1121# depend on libgcc_s_sjlj-1.dll) 1122# 1123$(bindir)/$(libyices_mingw_dll): $(base_obj) $(version_obj) 1124 $(CC) $(CFLAGS) $(LDFLAGS) -shared -static-libgcc -o $@ \ 1125 -Wl,--out-implib=$(libdir)/$(libyices_implib) \ 1126 -Wl,--output-def,$(libdir)/$(libyices_def) \ 1127 -Wl,--no-undefined \ 1128 $(base_obj) $(version_obj) $(LIBS) 1129ifeq ($(YICES_MODE),release) 1130 $(STRIP) $@ 1131endif 1132 1133$(static_bindir)/$(libyices_mingw_dll): $(static_dll_base_obj) $(static_dll_version_obj) 1134 $(CC) $(CFLAGS) $(LDFLAGS) -shared -static-libgcc -o $@ \ 1135 -Wl,--out-implib=$(static_libdir)/$(libyices_implib) \ 1136 -Wl,--output-def,$(static_libdir)/$(libyices_def) \ 1137 -Wl,--no-undefined \ 1138 $(static_dll_base_obj) $(static_dll_version_obj) $(PIC_LIBS) 1139ifeq ($(YICES_MODE),release) 1140 $(STRIP) -x $@ 1141endif 1142 1143 1144# 1145# Special dynamic tricks for Mac OS X: 1146# - the compatibility version is MAJOR.MINOR.0 1147# - the current version is MAJOR.MINOR.PATCH_LEVEL 1148# - install name: /usr/local/lib/libyices.MAJOR.dylib 1149# - option -headerpad_max_install_names allows users to 1150# safely change the install name using install_name_tool. 1151# 1152$(libdir)/$(libyices_dylib): $(base_obj) $(version_obj) 1153 $(CC) $(CFLAGS) $(LDFLAGS) -dynamiclib -o $@ \ 1154 -current_version $(libyices_curr_version) \ 1155 -compatibility_version $(libyices_compat_version) \ 1156 -Wl,-install_name,$(libyices_install_name) \ 1157 -Wl,-headerpad_max_install_names \ 1158 -Wl,-dead_strip \ 1159 $(base_obj) $(version_obj) $(LIBS) 1160ifeq ($(YICES_MODE),release) 1161 $(STRIP) -x $@ 1162endif 1163 1164$(static_libdir)/$(libyices_dylib): $(static_base_obj) $(static_version_obj) 1165 $(CC) $(CFLAGS) $(LDFLAGS) -dynamiclib -o $@ \ 1166 -current_version $(libyices_curr_version) \ 1167 -compatibility_version $(libyices_compat_version) \ 1168 -Wl,-install_name,$(libyices_install_name) \ 1169 -Wl,-headerpad_max_install_names \ 1170 -Wl,-dead_strip \ 1171 $(static_base_obj) $(static_version_obj) $(PIC_LIBS) 1172ifeq ($(YICES_MODE),release) 1173 $(STRIP) -x $@ 1174endif 1175 1176# All objects 1177obj: $(obj) $(bin_obj) 1178 1179static-obj: $(static_obj) $(static_bin_obj) 1180 1181# Binaries 1182bin: $(binaries) 1183 1184static-bin: $(static_binaries) 1185 1186# Libraries 1187lib: $(libyices) $(libyices_dynamic) 1188 1189static-lib: $(static_libyices) $(static_libyices_dynamic) 1190 1191 1192.PHONY: obj static-obj bin static-bin lib static-lib 1193 1194 1195 1196 1197########################## 1198# BINARY DISTRIBUTIONS # 1199########################## 1200 1201# 1202# OS-dependent flags for strip 1203# TODO: adjust this depending on OS 1204# 1205STRIPFLAGS= 1206 1207# 1208# Just copy the required binaries, libraries, include files into 1209# distdir. On cygwin/mingw, it makes sense to copy the dll 1210# into the bin directory. 1211# 1212dist: bin lib 1213 rm -r -f $(distdir)/* 1214 mkdir $(distdir)/include 1215 cp include/*.h $(distdir)/include 1216 mkdir $(distdir)/bin 1217 cp $(bindir)/yices$(EXEEXT) $(distdir)/bin/yices$(EXEEXT) 1218 cp $(bindir)/yices_smtcomp$(EXEEXT) $(distdir)/bin/yices-smt$(EXEEXT) 1219 cp $(bindir)/yices_smt2$(EXEEXT) $(distdir)/bin/yices-smt2$(EXEEXT) 1220 cp $(bindir)/yices_sat$(EXEEXT) $(distdir)/bin/yices-sat$(EXEEXT) 1221 cp $(bindir)/*.dll $(distdir)/bin || true 1222 mkdir $(distdir)/lib 1223 cp $(libdir)/* $(distdir)/lib 1224ifneq ($(YICES_MODE),debug) 1225 $(STRIP) $(STRIPFLAGS) $(distdir)/bin/yices$(EXEEXT) 1226 $(STRIP) $(STRIPFLAGS) $(distdir)/bin/yices-smt$(EXEEXT) 1227 $(STRIP) $(STRIPFLAGS) $(distdir)/bin/yices-smt2$(EXEEXT) 1228 $(STRIP) $(STRIPFLAGS) $(distdir)/bin/yices-sat$(EXEEXT) 1229endif 1230 1231static-dist: static-bin static-lib 1232 rm -r -f $(static_distdir)/* 1233 mkdir $(static_distdir)/include 1234 cp include/*.h $(static_distdir)/include 1235 mkdir $(static_distdir)/bin 1236 cp $(static_bindir)/yices$(EXEEXT) $(static_distdir)/bin/yices$(EXEEXT) 1237 cp $(static_bindir)/yices_smtcomp$(EXEEXT) $(static_distdir)/bin/yices-smt$(EXEEXT) 1238 cp $(static_bindir)/yices_smt2$(EXEEXT) $(static_distdir)/bin/yices-smt2$(EXEEXT) 1239 cp $(static_bindir)/yices_sat$(EXEEXT) $(static_distdir)/bin/yices-sat$(EXEEXT) 1240 cp $(static_bindir)/*.dll $(static_distdir)/bin || true 1241 mkdir $(static_distdir)/lib 1242 cp $(static_libdir)/* $(static_distdir)/lib 1243ifneq ($(YICES_MODE),debug) 1244 $(STRIP) $(STRIPFLAGS) $(static_distdir)/bin/yices$(EXEEXT) 1245 $(STRIP) $(STRIPFLAGS) $(static_distdir)/bin/yices-smt$(EXEEXT) 1246 $(STRIP) $(STRIPFLAGS) $(static_distdir)/bin/yices-smt2$(EXEEXT) 1247 $(STRIP) $(STRIPFLAGS) $(static_distdir)/bin/yices-sat$(EXEEXT) 1248endif 1249 1250 1251.PHONY: dist static-dist 1252 1253 1254############ 1255# OTHERS # 1256############ 1257 1258# 1259# Clean: remove the generated source files 1260# 1261clean: 1262 rm -f $(auto_generated) 1263 1264.PHONY: clean 1265 1266 1267ifeq ($(MAKE_RESTARTS),) 1268# 1269# Rules to keep going if .h or .c files have been deleted. This 1270# allows Make to rebuild an out-of-date dependency file 'source.d' 1271# that refers to an 'oldstuff.h' that has been deleted. We want to 1272# fail on the next restart if 'oldstuff.h' is still referenced in some 1273# existing 'source.c'. 1274# 1275%.h: 1276 @ echo "*** Warning: header file $@ is missing ***" 1277 1278%.c: 1279 @ echo "*** Warning: source file $@ is missing ***" 1280 1281endif 1282 1283 1284# 1285# For debugging of Makefile and configuration: 1286# print the options as set by this Makefile 1287# 1288show-details: 1289 @ echo 1290 @ echo "*** src/Mafefile ***" 1291 @ echo 1292 @ echo "target is $@" 1293 @ echo 1294 @ echo "ARCH is $(ARCH)" 1295 @ echo "POSIXOS is $(POSIXOS)" 1296 @ echo "YICES_TOP_DIR is $(YICES_TOP_DIR)" 1297 @ echo "YICES_MAKE_INCLUDE is $(YICES_MAKE_INCLUDE)" 1298 @ echo "YICES_MODE is $(YICES_MODE)" 1299 @ echo "BUILD is $(BUILD)" 1300 @ echo 1301 @ echo "Configuration" 1302 @ echo " EXEEXT = $(EXEEXT)" 1303 @ echo " SED = $(SED)" 1304 @ echo " LN_S = $(LN_S)" 1305 @ echo " MKDIR_P = $(MKDIR_P)" 1306 @ echo " CC = $(CC)" 1307 @ echo " CPPFLAGS = $(CPPFLAGS)" 1308 @ echo " LIBS = $(LIBS)" 1309 @ echo " LDFLAGS = $(LDFLAGS)" 1310 @ echo " LD = $(LD)" 1311 @ echo " AR = $(AR)" 1312 @ echo " RANLIB = $(RANLIB)" 1313 @ echo " STRIP = $(STRIP)" 1314 @ echo " NO_STACK_PROTECTOR = $(NO_STACK_PROTECTOR)" 1315 @ echo " STATIC_GMP = $(STATIC_GMP)" 1316 @ echo " STATIC_GMP_INCLUDE_DIR = $(STATIC_GMP_INCLUDE_DIR)" 1317 @ echo " PIC_GMP = $(PIC_GMP)" 1318 @ echo " PIC_GMP_INCLUDE_DIR = $(PIC_GMP_INCLUDE_DIR)" 1319 @ echo " ENABLE_MCSAT = $(ENABLE_MCSAT)" 1320 @ echo " STATIC_LIBPOLY = $(STATIC_LIBPOLY)" 1321 @ echo " STATIC_LIBPOLY_INCLUDE_DIR = $(STATIC_LIBPOLY_INCLUDE_DIR)" 1322 @ echo " PIC_LIBPOLY = $(PIC_LIBPOLY)" 1323 @ echo " PIC_LIBPOLY_INCLUDE_DIR = $(PIC_LIBPOLY_INCLUDE_DIR)" 1324