| [12] | 1 | # FileName [ Makefile.in ] |
|---|
| 2 | # |
|---|
| 3 | # PackageName [ CUSP ] |
|---|
| 4 | # |
|---|
| 5 | # Synopsis [ Package-wide Makefile ] |
|---|
| 6 | # |
|---|
| 7 | # Description [ This file requires GNU's make program. |
|---|
| 8 | # Run "configure" to generate the Makefile, or use |
|---|
| 9 | # "config.status" (created by configure) to regenerate the |
|---|
| 10 | # Makefile after modifying this file. |
|---|
| 11 | # |
|---|
| 12 | # Type "gmake help" for help about valid targets. |
|---|
| 13 | # ] |
|---|
| 14 | # |
|---|
| 15 | # |
|---|
| 16 | # Author [ HoonSang Jin <jinh@colorado.edu> ] |
|---|
| 17 | # |
|---|
| 18 | # Copyright [ |
|---|
| 19 | # Copyright (c) 2002-2008, Regents of the University of Colorado |
|---|
| 20 | |
|---|
| 21 | # All rights reserved. |
|---|
| 22 | |
|---|
| 23 | # Redistribution and use in source and binary forms, with or without |
|---|
| 24 | # modification, are permitted provided that the following conditions |
|---|
| 25 | # are met: |
|---|
| 26 | |
|---|
| 27 | # Redistributions of source code must retain the above copyright |
|---|
| 28 | # notice, this list of conditions and the following disclaimer. |
|---|
| 29 | |
|---|
| 30 | # Redistributions in binary form must reproduce the above copyright |
|---|
| 31 | # notice, this list of conditions and the following disclaimer in the |
|---|
| 32 | # documentation and/or other materials provided with the distribution. |
|---|
| 33 | |
|---|
| 34 | # Neither the name of the University of Colorado nor the names of its |
|---|
| 35 | # contributors may be used to endorse or promote products derived from |
|---|
| 36 | # this software without specific prior written permission. |
|---|
| 37 | |
|---|
| 38 | # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
|---|
| 39 | # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
|---|
| 40 | # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
|---|
| 41 | # FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
|---|
| 42 | # COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
|---|
| 43 | # INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
|---|
| 44 | # BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
|---|
| 45 | # LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
|---|
| 46 | # CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
|---|
| 47 | # LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
|---|
| 48 | # ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
|---|
| 49 | # POSSIBILITY OF SUCH DAMAGE. |
|---|
| 50 | # ] |
|---|
| 51 | # |
|---|
| 52 | # Revision [$Id: Makefile.in,v 1.18 2009-04-14 02:36:20 hhhan Exp $] |
|---|
| 53 | |
|---|
| 54 | .PHONY : default |
|---|
| 55 | |
|---|
| 56 | default : all |
|---|
| 57 | |
|---|
| 58 | |
|---|
| 59 | PKGS = sat smt aig util st array |
|---|
| 60 | |
|---|
| 61 | #---------------------------------------------------------------------- |
|---|
| 62 | # For safety |
|---|
| 63 | #---------------------------------------------------------------------- |
|---|
| 64 | |
|---|
| 65 | SHELL = /bin/sh |
|---|
| 66 | .SUFFIXES: |
|---|
| 67 | |
|---|
| 68 | #---------------------------------------------------------------------- |
|---|
| 69 | # The name of the product and its version |
|---|
| 70 | #---------------------------------------------------------------------- |
|---|
| 71 | |
|---|
| 72 | PRODUCT = cusp |
|---|
| 73 | VERSION = 1.1 |
|---|
| 74 | |
|---|
| 75 | # Compile and version information |
|---|
| 76 | # |
|---|
| 77 | # CUR_DATE and CUR_VER are strings surrounded by double quotes that contain |
|---|
| 78 | # spaces, e.g., "vis release 2.0" |
|---|
| 79 | |
|---|
| 80 | VERDATE := -DCUR_DATE="\"$(shell date)\"" -DCUR_VER="\"$(PRODUCT) release $(VERSION)\"" |
|---|
| 81 | |
|---|
| 82 | #---------------------------------------------------------------------- |
|---|
| 83 | # Source directories |
|---|
| 84 | #---------------------------------------------------------------------- |
|---|
| 85 | |
|---|
| 86 | # Directory containing master source files. This directory is searched |
|---|
| 87 | # for packages NOT listed in the PKGS variable. Defaults to "." |
|---|
| 88 | # Override with ./configure --srcdir= |
|---|
| 89 | master_srcdir = @srcdir@ |
|---|
| 90 | |
|---|
| 91 | # Directory containing local source files. This directory is searched |
|---|
| 92 | # for packages listed in the PKGS variable. Defaults to the master source |
|---|
| 93 | # directory (see above). |
|---|
| 94 | # Override with ./configure --with-local-srcdir= |
|---|
| 95 | local_srcdir = @local_srcdir@ |
|---|
| 96 | |
|---|
| 97 | # Directory where object files will be placed during the build |
|---|
| 98 | objectdir = obj |
|---|
| 99 | |
|---|
| 100 | # Directory where links to header files will be placed during the build |
|---|
| 101 | headerdir = $(master_srcdir)/include |
|---|
| 102 | |
|---|
| 103 | # hsjin : -DCirCUsALLSAT is compile option for SAT package |
|---|
| 104 | AC_FLAGS = @DEFS@ -DCirCUsALLSAT |
|---|
| 105 | LIBDIRS = @LIBDIRS@ |
|---|
| 106 | RANLIB = @RANLIB@ |
|---|
| 107 | CC = @CC@ |
|---|
| 108 | LINKER = @LINKER@ |
|---|
| 109 | LDFLAGS = @LDFLAGS@ |
|---|
| 110 | # |
|---|
| 111 | # Define the linker for the executable with "memory_profile" activated |
|---|
| 112 | # |
|---|
| 113 | PLINKER = @PLINKER@ |
|---|
| 114 | CFLAGS = @CFLAGS@ -Wall |
|---|
| 115 | OTHERLIBS = -lm @LIBS@ @LEXLIB@ |
|---|
| 116 | YACC = @YACC@ |
|---|
| 117 | LEX = @LEX@ |
|---|
| 118 | NAWK = @AWK@ |
|---|
| 119 | INSTALL = @INSTALL@ |
|---|
| 120 | INSTALL_PROGRAM = @INSTALL_PROGRAM@ |
|---|
| 121 | INSTALL_DATA = @INSTALL_DATA@ |
|---|
| 122 | AR = @AR@ |
|---|
| 123 | |
|---|
| 124 | #---------------------------------------------------------------------- |
|---|
| 125 | # Installation names and directories |
|---|
| 126 | #---------------------------------------------------------------------- |
|---|
| 127 | |
|---|
| 128 | # Name of the library to create |
|---|
| 129 | LIBRARY = lib$(PRODUCT).a |
|---|
| 130 | |
|---|
| 131 | # Directory in which to install architecture-independent files |
|---|
| 132 | # Set by ./configure --prefix=... |
|---|
| 133 | prefix = @prefix@ |
|---|
| 134 | |
|---|
| 135 | # Directory in which to install architecture-dependent files |
|---|
| 136 | # Set by ./configure --exec-prefix=... |
|---|
| 137 | exec_prefix = @exec_prefix@ |
|---|
| 138 | |
|---|
| 139 | # Directory in which to install binaries |
|---|
| 140 | bindir = $(exec_prefix)/bin |
|---|
| 141 | |
|---|
| 142 | # Directory in which to install libraries |
|---|
| 143 | libdir = $(exec_prefix)/lib |
|---|
| 144 | |
|---|
| 145 | # Directory in which to install headers |
|---|
| 146 | includedir = $(prefix)/include |
|---|
| 147 | |
|---|
| 148 | |
|---|
| 149 | #---------------------------------------------------------------------- |
|---|
| 150 | # Include the make templates from all the packages |
|---|
| 151 | # |
|---|
| 152 | # Each of these templates (e.g., array/array.make) should contains lines |
|---|
| 153 | # of the form |
|---|
| 154 | # |
|---|
| 155 | # CSRC += source1.c source2.c |
|---|
| 156 | # HEADERS += header1.h header2.h |
|---|
| 157 | # LEXSRC += file1.l |
|---|
| 158 | # YACCSRC += file2.y |
|---|
| 159 | # GENERATEDCSRC += smtLex.c smtRead.c |
|---|
| 160 | #---------------------------------------------------------------------- |
|---|
| 161 | |
|---|
| 162 | MAKEINCLUDES = $(foreach package, $(PKGS), \ |
|---|
| 163 | $(master_srcdir)/src/$(package)/$(package).make) |
|---|
| 164 | |
|---|
| 165 | include $(MAKEINCLUDES) |
|---|
| 166 | |
|---|
| 167 | OBJECTS = $(addprefix $(objectdir)/,$(GENERATEDCSRC:.c=.o) $(CSRC:.c=.o)) |
|---|
| 168 | |
|---|
| 169 | #---------------------------------------------------------------------- |
|---|
| 170 | # Include the dependency files from each package directory. |
|---|
| 171 | # A missing dependency file does not produce an error. |
|---|
| 172 | #---------------------------------------------------------------------- |
|---|
| 173 | |
|---|
| 174 | DEPENDENCIES = $(foreach package, $(PKGS), \ |
|---|
| 175 | $(master_srcdir)/src/$(package)/$(package).d) |
|---|
| 176 | |
|---|
| 177 | -include $(DEPENDENCIES) |
|---|
| 178 | |
|---|
| 179 | INCLUDEDIRS = \ |
|---|
| 180 | $(foreach package, $(PKGS), -I$(master_srcdir)/src/$(package)) \ |
|---|
| 181 | -I$(objectdir) |
|---|
| 182 | |
|---|
| 183 | LIBRARYDIRS = $(LIBDIRS) |
|---|
| 184 | |
|---|
| 185 | LIBS = $(OTHERLIBS) |
|---|
| 186 | |
|---|
| 187 | VPATH = $(master_srcdir): \ |
|---|
| 188 | $(addprefix :$(master_srcdir)/src/,$(PKGS)): \ |
|---|
| 189 | $(objectdir): |
|---|
| 190 | |
|---|
| 191 | #GMPLIBS = -lgmp |
|---|
| 192 | |
|---|
| 193 | #gmplibdir = /usr/lib/ |
|---|
| 194 | |
|---|
| 195 | #---------------------------------------------------------------------- |
|---|
| 196 | # Examples included in the distribution |
|---|
| 197 | #---------------------------------------------------------------------- |
|---|
| 198 | |
|---|
| 199 | # Each example is declared only once. If some checking through is done |
|---|
| 200 | # make check, then it is declared in one of CHECK_CNF_EXAMPLES, |
|---|
| 201 | # CHECK_SMT_EXAMPLES. If the example |
|---|
| 202 | # is just being added to the examples directory in VIS, then add it here. |
|---|
| 203 | |
|---|
| 204 | EXAMPLES = $(CHECK_CNF_EXAMPLES) $(CHECK_SMT_EXAMPLES) |
|---|
| 205 | |
|---|
| 206 | # The "interesting" example files are anything in the examples subdirectories |
|---|
| 207 | # except the RCS subdirectories |
|---|
| 208 | # |
|---|
| 209 | # This is a rather messy way to look for filenames in the local_srcdir, |
|---|
| 210 | # then remove the local_srcdir prefix |
|---|
| 211 | |
|---|
| 212 | EXAMPLEFILES = $(patsubst $(local_srcdir)/%, %, \ |
|---|
| 213 | $(filter-out %RCS, $(foreach example, $(EXAMPLES), \ |
|---|
| 214 | $(wildcard $(local_srcdir)/examples/$(example)/*)))) |
|---|
| 215 | |
|---|
| 216 | #---------------------------------------------------------------------- |
|---|
| 217 | # Definitions for the distribution file |
|---|
| 218 | #---------------------------------------------------------------------- |
|---|
| 219 | |
|---|
| 220 | DISTRIBUTION = $(PRODUCT)-$(VERSION) |
|---|
| 221 | |
|---|
| 222 | # Directories to include in the distribution file |
|---|
| 223 | |
|---|
| 224 | DISTDIRS = src helpers share share/help obj doc examples \ |
|---|
| 225 | $(addprefix examples/,$(EXAMPLES)) $(addprefix src/,$(PKGS)) |
|---|
| 226 | |
|---|
| 227 | # Build/install helper files |
|---|
| 228 | |
|---|
| 229 | HELPERS = $(addprefix helpers/, \ |
|---|
| 230 | install-sh mkinstalldirs config.guess config.sub dependency.make) |
|---|
| 231 | |
|---|
| 232 | # Files to include in the distribution file |
|---|
| 233 | |
|---|
| 234 | DISTFILES = \ |
|---|
| 235 | configure configure.in Makefile.in README $(HELPERS) \ |
|---|
| 236 | $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES) \ |
|---|
| 237 | $(EXAMPLEFILES) \ |
|---|
| 238 | $(addprefix doc/,$(DOCUMENTATION)) \ |
|---|
| 239 | $(addprefix share/,$(SHAREFILES)) \ |
|---|
| 240 | $(addprefix share/help/,$(HELPFILES)) |
|---|
| 241 | |
|---|
| 242 | #---------------------------------------------------------------------- |
|---|
| 243 | # Implicit rules |
|---|
| 244 | #---------------------------------------------------------------------- |
|---|
| 245 | |
|---|
| 246 | ALLCFLAGS = $(CFLAGS) $(AC_FLAGS) -DBDDcu $(VERDATE) \ |
|---|
| 247 | -DNAWK=\"$(NAWK)\" -DLIBRARY=\"$(datadir)\" |
|---|
| 248 | |
|---|
| 249 | # For compiling a source file into the object directory |
|---|
| 250 | |
|---|
| 251 | $(objectdir)/%.o : %.c |
|---|
| 252 | umask 2 ; $(CC) -c $(ALLCFLAGS) $(INCLUDEDIRS) -o $@ $< |
|---|
| 253 | |
|---|
| 254 | # Place object files into an archive |
|---|
| 255 | |
|---|
| 256 | %.a : |
|---|
| 257 | rm -f $@ |
|---|
| 258 | umask 2; $(AR) cq $@ $^ |
|---|
| 259 | $(RANLIB) $@ |
|---|
| 260 | |
|---|
| 261 | ###################################################################### |
|---|
| 262 | # RULES # |
|---|
| 263 | ###################################################################### |
|---|
| 264 | |
|---|
| 265 | #: |
|---|
| 266 | #: Useful targets: |
|---|
| 267 | #: |
|---|
| 268 | |
|---|
| 269 | #---------------------------------------------------------------------- |
|---|
| 270 | # Rule for getting help |
|---|
| 271 | #---------------------------------------------------------------------- |
|---|
| 272 | |
|---|
| 273 | .PHONY : help |
|---|
| 274 | |
|---|
| 275 | #: help -- Print a list of targets |
|---|
| 276 | |
|---|
| 277 | # This prints all lines in this Makefile that begin with #: |
|---|
| 278 | |
|---|
| 279 | help : |
|---|
| 280 | @sed -n "s/^#://p" Makefile |
|---|
| 281 | |
|---|
| 282 | #---------------------------------------------------------------------- |
|---|
| 283 | # Always executed once when the Makefile is run |
|---|
| 284 | #---------------------------------------------------------------------- |
|---|
| 285 | |
|---|
| 286 | # Make sure the directory in which to place the objects exists |
|---|
| 287 | |
|---|
| 288 | ignored := $(shell umask 2; test -d $(objectdir) || mkdir $(objectdir)) |
|---|
| 289 | |
|---|
| 290 | #---------------------------------------------------------------------- |
|---|
| 291 | # Rules to compile and build libraries and executables |
|---|
| 292 | #---------------------------------------------------------------------- |
|---|
| 293 | |
|---|
| 294 | .PHONY : all library compile-version delete-version |
|---|
| 295 | |
|---|
| 296 | #: |
|---|
| 297 | #: all (the default) -- Compile the main executable |
|---|
| 298 | # (force the version to be recompiled) |
|---|
| 299 | |
|---|
| 300 | all : compile-version $(PRODUCT) |
|---|
| 301 | |
|---|
| 302 | # Create the main executable |
|---|
| 303 | |
|---|
| 304 | $(PRODUCT) : $(OBJECTS) |
|---|
| 305 | umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \ |
|---|
| 306 | $(OBJECTS) $(LIBRARYDIRS) $(LIBS) -ldl |
|---|
| 307 | |
|---|
| 308 | #$(PRODUCT) : $(OBJECTS) $(gmplibdir)/libgmp.la |
|---|
| 309 | # umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \ |
|---|
| 310 | # $(OBJECTS) $(LIBRARYDIRS) $(LIBS) -ldl $(GMPLIBS) |
|---|
| 311 | |
|---|
| 312 | # Force the "version" information to be recompiled |
|---|
| 313 | |
|---|
| 314 | compile-version : delete-version $(objectdir)/main.o |
|---|
| 315 | |
|---|
| 316 | # Delete the object file related to the version |
|---|
| 317 | |
|---|
| 318 | delete-version : |
|---|
| 319 | rm -f $(objectdir)/main.o |
|---|
| 320 | |
|---|
| 321 | # Build a library containing all the objects |
|---|
| 322 | |
|---|
| 323 | #: library -- Create a library of all the objects (useful in a central area) |
|---|
| 324 | |
|---|
| 325 | library : $(LIBRARY) |
|---|
| 326 | |
|---|
| 327 | $(LIBRARY) : $(OBJECTS) |
|---|
| 328 | |
|---|
| 329 | #---------------------------------------------------------------------- |
|---|
| 330 | # Rules for checking the build |
|---|
| 331 | #---------------------------------------------------------------------- |
|---|
| 332 | .PHONY : check check-examples |
|---|
| 333 | |
|---|
| 334 | # This is a lengthy sed command used to filter out the irrelevant CUSP |
|---|
| 335 | # output that appears when the examples are running. |
|---|
| 336 | # |
|---|
| 337 | # Sed does not permit space between the trailing p ("print matching |
|---|
| 338 | # lines") and the semicolon (end of command). Hashes are escaped -- |
|---|
| 339 | # otherwise they are Makefile comments. This was once a long egrep |
|---|
| 340 | # expression, but the string was too long for Ultrix's egrep. |
|---|
| 341 | |
|---|
| 342 | SED_CMD = \ |
|---|
| 343 | /^UNSATISFIABLE/p; \ |
|---|
| 344 | /^SATISFIABLE/p; \ |
|---|
| 345 | /^unsat/p; \ |
|---|
| 346 | /^sat/p; \ |
|---|
| 347 | /;.*;/p; |
|---|
| 348 | |
|---|
| 349 | # List of all examples to check (A subset of EXAMPLES) |
|---|
| 350 | |
|---|
| 351 | CHECK_CNF_EXAMPLES = arbiter daio 3blocks bw_large.a hanoi4 rot |
|---|
| 352 | |
|---|
| 353 | CHECK_SMT_EXAMPLES = 2ba bignum_idl1 bignum_idl2 bignum_rdl1 bignum_rdl2 \ |
|---|
| 354 | BinarySearch_live_blmc000 CELAR6_SUB0 ckt_PROP14_tf_9 \ |
|---|
| 355 | diamonds.10.2.i.a.u DTP_k2_n35_c175_s1 FISCHER3-4-ninc fischer3-mutex-5 \ |
|---|
| 356 | inf-bakery-mutex-1 int_incompleteness1 jobshop4-2-2-2-4-4-12 plan-5.cvc |
|---|
| 357 | |
|---|
| 358 | CHECK_EXAMPLES = $(CHECK_SMT_EXAMPLES) $(CHECK_CNF_EXAMPLES) |
|---|
| 359 | |
|---|
| 360 | # Determine the absolute executable path |
|---|
| 361 | # |
|---|
| 362 | # Starting from the current directory, change directory to the directory |
|---|
| 363 | # part of the product name, then tack on the filename part of EXECUTABLE |
|---|
| 364 | |
|---|
| 365 | EXECUTABLE = $(PRODUCT) |
|---|
| 366 | |
|---|
| 367 | EXECUTABLEPATH := \ |
|---|
| 368 | $(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE)) |
|---|
| 369 | |
|---|
| 370 | EXECUTABLEPATH := \ |
|---|
| 371 | $(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE)) |
|---|
| 372 | |
|---|
| 373 | # Determine the rootname of the examples |
|---|
| 374 | # |
|---|
| 375 | |
|---|
| 376 | EXAMPLEPATH = $(master_srcdir)/examples |
|---|
| 377 | |
|---|
| 378 | FULLEXAMPLEPATH := $(shell cd $(EXAMPLEPATH) ; pwd) |
|---|
| 379 | |
|---|
| 380 | #: |
|---|
| 381 | #: check -- Test the locally-built executable (runs check-examples) |
|---|
| 382 | #: Include check-cnf-simp-examples to check the cnf solver |
|---|
| 383 | #: with its preprocessors. For example, |
|---|
| 384 | # |
|---|
| 385 | # check : check-cnf-examples check-cnf-simp-examples check-smt-examples |
|---|
| 386 | # |
|---|
| 387 | check : check-cnf-examples check-smt-examples |
|---|
| 388 | |
|---|
| 389 | #: check-examples -- Test each of the examples listed in CHECK_EXAMPLES |
|---|
| 390 | #: You may want to invoke this with |
|---|
| 391 | #: gmake "CHECK_EXAMPLES=abp bakery" check-examples |
|---|
| 392 | #: gmake EXECUTABLE=cusp check-smt-examples |
|---|
| 393 | |
|---|
| 394 | # For each example, |
|---|
| 395 | # |
|---|
| 396 | # 1) create the directory checkresults/<example> |
|---|
| 397 | # 2) enter that directory |
|---|
| 398 | # 3) run CUSP for the example producing "result.raw" |
|---|
| 399 | # 5) filter out relevant lines in the result, producing "result.filtered" |
|---|
| 400 | # and compare this with the "check_result" file in the master source |
|---|
| 401 | # directory. Differences are written to "result.differences" |
|---|
| 402 | check-cnf-examples : |
|---|
| 403 | @test -d checkresults || mkdir checkresults |
|---|
| 404 | @echo "Checking examples. Results will be in checkresults/<example>/result.raw" |
|---|
| 405 | @echo "Running executable $(EXECUTABLEPATH) for CNFs " |
|---|
| 406 | @echo " (change with EXECUTABLE=...)" |
|---|
| 407 | @echo "Taking examples from $(FULLEXAMPLEPATH)" |
|---|
| 408 | @echo " (change with EXAMPLEPATH=...)" |
|---|
| 409 | @cwd=`pwd` ; \ |
|---|
| 410 | for example in $(CHECK_CNF_EXAMPLES) ; \ |
|---|
| 411 | do \ |
|---|
| 412 | echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \ |
|---|
| 413 | cd $$cwd ; \ |
|---|
| 414 | test -d checkresults/$$example || \ |
|---|
| 415 | mkdir checkresults/$$example ; \ |
|---|
| 416 | cd checkresults/$$example ; \ |
|---|
| 417 | $(EXECUTABLEPATH) -cnf $(FULLEXAMPLEPATH)/$$example/$$example.cnf > result.raw 2> result.stderr ; \ |
|---|
| 418 | sed -n '$(SED_CMD)' result.raw > result.filtered ; \ |
|---|
| 419 | if diff result.filtered \ |
|---|
| 420 | $(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \ |
|---|
| 421 | then \ |
|---|
| 422 | echo "passed" ; \ |
|---|
| 423 | rm result.differences ; \ |
|---|
| 424 | else \ |
|---|
| 425 | echo "failed (more checkresults/$$example/result.differences)" ; \ |
|---|
| 426 | fi ; \ |
|---|
| 427 | done |
|---|
| 428 | |
|---|
| 429 | check-cnf-simp-examples : |
|---|
| 430 | @test -d checkresults || mkdir checkresults |
|---|
| 431 | @echo "Checking examples. Results will be in checkresults/<example>/result.raw" |
|---|
| 432 | @echo "Running executable $(EXECUTABLEPATH) for CNFs " |
|---|
| 433 | @echo " (change with EXECUTABLE=...)" |
|---|
| 434 | @echo "Taking examples from $(FULLEXAMPLEPATH)" |
|---|
| 435 | @echo " (change with EXAMPLEPATH=...)" |
|---|
| 436 | @cwd=`pwd` ; \ |
|---|
| 437 | for example in $(CHECK_CNF_EXAMPLES) ; \ |
|---|
| 438 | do \ |
|---|
| 439 | echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \ |
|---|
| 440 | cd $$cwd ; \ |
|---|
| 441 | test -d checkresults/$$example || \ |
|---|
| 442 | mkdir checkresults/$$example ; \ |
|---|
| 443 | cd checkresults/$$example ; \ |
|---|
| 444 | $(EXECUTABLEPATH) -cnf $(FULLEXAMPLEPATH)/$$example/$$example.cnf -velim -distill > result.raw 2> result.stderr ; \ |
|---|
| 445 | sed -n '$(SED_CMD)' result.raw > result.filtered ; \ |
|---|
| 446 | if diff result.filtered \ |
|---|
| 447 | $(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \ |
|---|
| 448 | then \ |
|---|
| 449 | echo "passed" ; \ |
|---|
| 450 | rm result.differences ; \ |
|---|
| 451 | else \ |
|---|
| 452 | echo "failed (more checkresults/$$example/result.differences)" ; \ |
|---|
| 453 | fi ; \ |
|---|
| 454 | done |
|---|
| 455 | |
|---|
| 456 | check-smt-examples : |
|---|
| 457 | @test -d checkresults || mkdir checkresults |
|---|
| 458 | @echo "Checking examples. Results will be in checkresults/<example>/result.raw" |
|---|
| 459 | @echo "Running executable $(EXECUTABLEPATH) for SMTs " |
|---|
| 460 | @echo " (change with EXECUTABLE=...)" |
|---|
| 461 | @echo "Taking examples from $(FULLEXAMPLEPATH)" |
|---|
| 462 | @echo " (change with EXAMPLEPATH=...)" |
|---|
| 463 | @cwd=`pwd` ; \ |
|---|
| 464 | for example in $(CHECK_SMT_EXAMPLES) ; \ |
|---|
| 465 | do \ |
|---|
| 466 | echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \ |
|---|
| 467 | cd $$cwd ; \ |
|---|
| 468 | test -d checkresults/$$example || \ |
|---|
| 469 | mkdir checkresults/$$example ; \ |
|---|
| 470 | cd checkresults/$$example ; \ |
|---|
| 471 | $(EXECUTABLEPATH) $(FULLEXAMPLEPATH)/$$example/$$example.smt > result.raw 2> result.stderr ; \ |
|---|
| 472 | sed -n '$(SED_CMD)' result.raw > result.filtered ; \ |
|---|
| 473 | if diff result.filtered \ |
|---|
| 474 | $(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \ |
|---|
| 475 | then \ |
|---|
| 476 | echo "passed" ; \ |
|---|
| 477 | rm result.differences ; \ |
|---|
| 478 | else \ |
|---|
| 479 | awk '/read CNF file/ { print "Warning : CUSP for SMT is not built!"}' result.stderr; \ |
|---|
| 480 | awk '!/read CNF file/ { print "failed (more checkresults/$$example/result.differences)"}' result.stderr; \ |
|---|
| 481 | fi ; \ |
|---|
| 482 | done |
|---|
| 483 | |
|---|
| 484 | |
|---|
| 485 | #---------------------------------------------------------------------- |
|---|
| 486 | # Rules for installation |
|---|
| 487 | #---------------------------------------------------------------------- |
|---|
| 488 | |
|---|
| 489 | .PHONY : install uninstall installdirs |
|---|
| 490 | |
|---|
| 491 | #: |
|---|
| 492 | #: install -- Install the product and libraries in bindir, libdir, |
|---|
| 493 | #: datadir, etc. |
|---|
| 494 | |
|---|
| 495 | install : $(PRODUCT) $(LIBRARY) installdirs |
|---|
| 496 | @echo "Installing $(bindir)/$(PRODUCT)" |
|---|
| 497 | @$(INSTALL_PROGRAM) $(PRODUCT) $(bindir)/$(PRODUCT) |
|---|
| 498 | @echo "Installing $(libdir)/$(LIBRARY)" |
|---|
| 499 | @$(INSTALL_DATA) $(LIBRARY) $(libdir)/$(LIBRARY) |
|---|
| 500 | @for file in $(SHAREFILES) ; do \ |
|---|
| 501 | echo "Installing $(datadir)/$$file"; \ |
|---|
| 502 | $(INSTALL_DATA) $(master_srcdir)/share/$$file \ |
|---|
| 503 | $(datadir)/$$file; \ |
|---|
| 504 | done |
|---|
| 505 | @for file in $(HELPFILES) ; do \ |
|---|
| 506 | echo "Installing $(datadir)/help/$$file"; \ |
|---|
| 507 | $(INSTALL_DATA) $(master_srcdir)/share/help/$$file \ |
|---|
| 508 | $(datadir)/help/$$file; \ |
|---|
| 509 | done |
|---|
| 510 | @for header in $(HEADERS); do \ |
|---|
| 511 | echo "Installing $(includedir)/$$header"; \ |
|---|
| 512 | $(INSTALL_DATA) $(master_srcdir)/src/*/$$header \ |
|---|
| 513 | $(includedir)/$$header; \ |
|---|
| 514 | done |
|---|
| 515 | |
|---|
| 516 | #: uninstall -- Reverse the effects of "install" |
|---|
| 517 | |
|---|
| 518 | uninstall : |
|---|
| 519 | rm -f $(bindir)/$(PRODUCT) |
|---|
| 520 | rm -f $(libdir)/$(LIBRARY) |
|---|
| 521 | @for file in $(SHAREFILES) ; \ |
|---|
| 522 | do \ |
|---|
| 523 | echo "Removing $(datadir)/$$file"; \ |
|---|
| 524 | rm -f $(datadir)/$$file; \ |
|---|
| 525 | done |
|---|
| 526 | @for file in $(HELPFILES) ; \ |
|---|
| 527 | do \ |
|---|
| 528 | echo "Removing $(datadir)/help/$$file"; \ |
|---|
| 529 | rm -f $(datadir)/help/$$file; \ |
|---|
| 530 | done |
|---|
| 531 | @for header in $(HEADERS); \ |
|---|
| 532 | do \ |
|---|
| 533 | echo "Removing $(includedir)/$$header"; \ |
|---|
| 534 | rm -f $(includedir)/$$header; \ |
|---|
| 535 | done |
|---|
| 536 | |
|---|
| 537 | installdirs : |
|---|
| 538 | $(master_srcdir)/helpers/mkinstalldirs \ |
|---|
| 539 | $(bindir) $(libdir) $(includedir) $(datadir) $(datadir)/help \ |
|---|
| 540 | $(mandir) |
|---|
| 541 | |
|---|
| 542 | #---------------------------------------------------------------------- |
|---|
| 543 | # Rules for cleaning |
|---|
| 544 | #---------------------------------------------------------------------- |
|---|
| 545 | |
|---|
| 546 | .PHONY : clean mostlyclean distclean |
|---|
| 547 | |
|---|
| 548 | #: |
|---|
| 549 | #: clean -- Remove every file created by building |
|---|
| 550 | |
|---|
| 551 | clean mostlyclean : |
|---|
| 552 | rm -rf $(objectdir)/* $(PRODUCT) include |
|---|
| 553 | |
|---|
| 554 | #: distclean -- Remove every file created by building or configuring |
|---|
| 555 | |
|---|
| 556 | distclean : clean cleandependencies |
|---|
| 557 | rm -f Makefile config.status config.cache config.log |
|---|
| 558 | |
|---|
| 559 | #---------------------------------------------------------------------- |
|---|
| 560 | # Rule for performing a lint-like check on the source code |
|---|
| 561 | # |
|---|
| 562 | # Note: This requires gcc or g++ |
|---|
| 563 | #---------------------------------------------------------------------- |
|---|
| 564 | |
|---|
| 565 | .PHONY : check-code |
|---|
| 566 | |
|---|
| 567 | #: |
|---|
| 568 | #: check-code -- Run a lint-like check on the source code. |
|---|
| 569 | #: (useful for development) |
|---|
| 570 | |
|---|
| 571 | CHECK_FLAGS := -Wall -pedantic -Wmissing-declarations |
|---|
| 572 | ifeq ($(CC),gcc) |
|---|
| 573 | CHECK_FLAGS := $(CHECK_FLAGS) -Wstrict-prototypes -Wmissing-prototypes |
|---|
| 574 | endif |
|---|
| 575 | |
|---|
| 576 | check-code : $(CSRC) |
|---|
| 577 | ifneq ($(findstring <$(CC)>,<gcc> <g++>),) |
|---|
| 578 | @rm -f *.o_checkcode |
|---|
| 579 | @for file in $^; \ |
|---|
| 580 | do \ |
|---|
| 581 | echo "------------------------ Checking $$file"; \ |
|---|
| 582 | $(CC) -c $(CFLAGS) $(AC_FLAGS) $(CHECK_FLAGS) \ |
|---|
| 583 | $(VERDATE) $(INCLUDEDIRS) \ |
|---|
| 584 | -o $(objectdir)/checkcode_output.o $$file; \ |
|---|
| 585 | rm -f $(objectdir)/checkcode_output.o; \ |
|---|
| 586 | done |
|---|
| 587 | @rm -f *.o_checkcode |
|---|
| 588 | else |
|---|
| 589 | @echo "check-code requires gcc or g++" |
|---|
| 590 | @echo "Reconfigure with gcc or g++" |
|---|
| 591 | endif |
|---|
| 592 | |
|---|
| 593 | #---------------------------------------------------------------------- |
|---|
| 594 | # Rules that produce/delete the dependency file for every package |
|---|
| 595 | #---------------------------------------------------------------------- |
|---|
| 596 | |
|---|
| 597 | .PHONY : dependencies cleandependencies |
|---|
| 598 | |
|---|
| 599 | #: |
|---|
| 600 | #: dependencies -- Create a list of dependency files. |
|---|
| 601 | #: Useful when modifying header files. |
|---|
| 602 | |
|---|
| 603 | # Invoke the "dependency.make" Makefile on each package subdirectory, |
|---|
| 604 | # passing the path, etc. to it. |
|---|
| 605 | # |
|---|
| 606 | # There's a strange feature in autoconf where lines of the form " VPATH=" |
|---|
| 607 | # are removed from the Makefile. Thus, a flag is placed before the |
|---|
| 608 | # VPATH= argument below. |
|---|
| 609 | |
|---|
| 610 | dependencies: |
|---|
| 611 | ifneq ($(findstring <$(CC)>,<gcc> <g++>),) |
|---|
| 612 | for pkg in $(PKGS) ; \ |
|---|
| 613 | do \ |
|---|
| 614 | $(MAKE) --no-print-directory \ |
|---|
| 615 | -f $(master_srcdir)/helpers/dependency.make \ |
|---|
| 616 | CC="$(CC)" \ |
|---|
| 617 | CFLAGS="$(CFLAGS)" VPATH="$(local_srcdir)/src/$$pkg" \ |
|---|
| 618 | AC_FLAGS="$(AC_FLAGS)" \ |
|---|
| 619 | INCLUDEDIRS="$(INCLUDEDIRS)" objectdir=$(objectdir) \ |
|---|
| 620 | PKGNAME=$(local_srcdir)/src/$$pkg/$$pkg \ |
|---|
| 621 | $(local_srcdir)/src/$$pkg/$$pkg.d ; \ |
|---|
| 622 | done |
|---|
| 623 | else |
|---|
| 624 | @echo "dependency requires gcc or g++" |
|---|
| 625 | @echo "Reconfigure with gcc or g++" |
|---|
| 626 | endif |
|---|
| 627 | |
|---|
| 628 | cleandependencies: |
|---|
| 629 | rm -f $(local_srcdir)/src/*/*.d |
|---|
| 630 | |
|---|
| 631 | #---------------------------------------------------------------------- |
|---|
| 632 | # Rules for making a distribution file |
|---|
| 633 | #---------------------------------------------------------------------- |
|---|
| 634 | |
|---|
| 635 | .PHONY : dist |
|---|
| 636 | |
|---|
| 637 | #: |
|---|
| 638 | #: dist -- Create a tarred, gzipped distribution file |
|---|
| 639 | |
|---|
| 640 | # Warning: "tar" under Digital Unix (on DEC Alphas) writes directories |
|---|
| 641 | # that don't work under SunOS tar |
|---|
| 642 | |
|---|
| 643 | dist : $(DISTRIBUTION).tar.gz |
|---|
| 644 | |
|---|
| 645 | $(DISTRIBUTION).tar.gz : $(DISTFILES) |
|---|
| 646 | ifeq ($(strip $(FULL_MISSING_PKGS)),) |
|---|
| 647 | rm -rf $(DISTRIBUTION) |
|---|
| 648 | umask 022; mkdir $(DISTRIBUTION) |
|---|
| 649 | for dir in $(DISTDIRS); \ |
|---|
| 650 | do \ |
|---|
| 651 | umask 022; mkdir $(DISTRIBUTION)/$$dir; \ |
|---|
| 652 | done |
|---|
| 653 | @echo "Copying distribution files" |
|---|
| 654 | @for file in $(patsubst $(local_srcdir)/%, %, $^); \ |
|---|
| 655 | do \ |
|---|
| 656 | echo " $$file"; \ |
|---|
| 657 | cp -p $(local_srcdir)/$$file $(DISTRIBUTION)/$$file; \ |
|---|
| 658 | done |
|---|
| 659 | - chmod -R a+r $(DISTRIBUTION) |
|---|
| 660 | - chmod -R u+w $(DISTRIBUTION) |
|---|
| 661 | tar cf - $(DISTRIBUTION) | gzip -9 > $(DISTRIBUTION).tar.gz |
|---|
| 662 | rm -rf $(DISTRIBUTION) |
|---|
| 663 | else |
|---|
| 664 | @echo "Missing packages: $(FULL_MISSING_PKGS)" |
|---|
| 665 | @echo "Make sure PKGS lists all the packages" |
|---|
| 666 | @exit 1 |
|---|
| 667 | endif |
|---|
| 668 | |
|---|
| 669 | |
|---|
| 670 | #---------------------------------------------------------------------- |
|---|
| 671 | # Rules for debugging the Makefile |
|---|
| 672 | #---------------------------------------------------------------------- |
|---|
| 673 | |
|---|
| 674 | .PHONY : debug-make |
|---|
| 675 | |
|---|
| 676 | DEBUG_VARS = PKGS \ |
|---|
| 677 | VPATH \ |
|---|
| 678 | INCLUDEDIRS \ |
|---|
| 679 | CSRC \ |
|---|
| 680 | OBJECTS \ |
|---|
| 681 | HEADERS \ |
|---|
| 682 | MAKEINCLUDES \ |
|---|
| 683 | CFLAGS \ |
|---|
| 684 | AC_FLAGS \ |
|---|
| 685 | master_srcdir \ |
|---|
| 686 | LIBS |
|---|
| 687 | |
|---|
| 688 | #: |
|---|
| 689 | #: debug-make -- Print a list of Makefile variables |
|---|
| 690 | |
|---|
| 691 | debug-make: |
|---|
| 692 | @$(foreach var, $(DEBUG_VARS), echo $(var)=$($(var)) ; ) |
|---|