# FileName	[ Makefile.in ]
#
# PackageName	[ CUSP ]
#
# Synopsis	[ Package-wide Makefile ]
#
# Description	[ This file requires GNU's make program.
#		  Run "configure" to generate the Makefile, or use
#		  "config.status" (created by configure) to regenerate the
#		  Makefile after modifying this file.
#
#		  Type "gmake help" for help about valid targets.
#		 ]
#
#
# Author	[ HoonSang Jin <jinh@colorado.edu> ]
#
# Copyright	[
#  Copyright (c) 2002-2008, Regents of the University of Colorado

#  All rights reserved.

#  Redistribution and use in source and binary forms, with or without
#  modification, are permitted provided that the following conditions
#  are met:

#  Redistributions of source code must retain the above copyright
#  notice, this list of conditions and the following disclaimer.

#  Redistributions in binary form must reproduce the above copyright
#  notice, this list of conditions and the following disclaimer in the
#  documentation and/or other materials provided with the distribution.

#  Neither the name of the University of Colorado nor the names of its
#  contributors may be used to endorse or promote products derived from
#  this software without specific prior written permission.

#  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
#  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
#  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
#  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
#  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
#  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
#  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
#  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
#  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
#  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
#  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
#  POSSIBILITY OF SUCH DAMAGE.
#  ]
#
# Revision	[$Id: Makefile.in,v 1.18 2009-04-14 02:36:20 hhhan Exp $]

.PHONY : default

default : all


PKGS = sat smt aig util st array

#----------------------------------------------------------------------
# For safety
#----------------------------------------------------------------------

SHELL = /bin/sh
.SUFFIXES:

#----------------------------------------------------------------------
# The name of the product and its version
#----------------------------------------------------------------------

PRODUCT = cusp
VERSION = 1.1

# Compile and version information
#
# CUR_DATE and CUR_VER are strings surrounded by double quotes that contain
# spaces, e.g., "vis release 2.0"

VERDATE := -DCUR_DATE="\"$(shell date)\"" -DCUR_VER="\"$(PRODUCT) release $(VERSION)\""

#----------------------------------------------------------------------
# Source directories
#----------------------------------------------------------------------

# Directory containing master source files.  This directory is searched
# for packages NOT listed in the PKGS variable.  Defaults to "."
# Override with  ./configure --srcdir=
master_srcdir = @srcdir@

# Directory containing local source files.  This directory is searched
# for packages listed in the PKGS variable.  Defaults to the master source
# directory (see above).
# Override with ./configure --with-local-srcdir=
local_srcdir =  @local_srcdir@

# Directory where object files will be placed during the build
objectdir =	obj

# Directory where links to header files will be placed during the build
headerdir =	$(master_srcdir)/include

# hsjin : -DCirCUsALLSAT is compile option for SAT package
AC_FLAGS =	@DEFS@ -DCirCUsALLSAT
LIBDIRS =	@LIBDIRS@
RANLIB =	@RANLIB@
CC =		@CC@
LINKER =	@LINKER@
LDFLAGS =	@LDFLAGS@
#
# Define the linker for the executable with "memory_profile" activated
#
PLINKER =       @PLINKER@
CFLAGS =	@CFLAGS@ -Wall
OTHERLIBS =	-lm @LIBS@ @LEXLIB@
YACC =		@YACC@
LEX =		@LEX@
NAWK =		@AWK@
INSTALL =	@INSTALL@
INSTALL_PROGRAM = @INSTALL_PROGRAM@
INSTALL_DATA =	@INSTALL_DATA@
AR =		@AR@

#----------------------------------------------------------------------
# Installation names and directories
#----------------------------------------------------------------------

# Name of the library to create
LIBRARY =       lib$(PRODUCT).a

# Directory in which to install architecture-independent files
# Set by ./configure --prefix=...
prefix =        @prefix@

# Directory in which to install architecture-dependent files
# Set by ./configure --exec-prefix=...
exec_prefix =   @exec_prefix@

# Directory in which to install binaries
bindir =        $(exec_prefix)/bin

# Directory in which to install libraries
libdir =        $(exec_prefix)/lib

# Directory in which to install headers
includedir =    $(prefix)/include


#----------------------------------------------------------------------
# Include the make templates from all the packages
#
# Each of these templates (e.g., array/array.make) should contains lines
# of the form
#
# CSRC += source1.c source2.c
# HEADERS += header1.h header2.h
# LEXSRC += file1.l
# YACCSRC += file2.y
# GENERATEDCSRC += smtLex.c smtRead.c
#----------------------------------------------------------------------

MAKEINCLUDES = $(foreach package, $(PKGS), \
	$(master_srcdir)/src/$(package)/$(package).make)

include $(MAKEINCLUDES)

OBJECTS = $(addprefix $(objectdir)/,$(GENERATEDCSRC:.c=.o) $(CSRC:.c=.o))

#----------------------------------------------------------------------
# Include the dependency files from each package directory.
# A missing dependency file does not produce an error.
#----------------------------------------------------------------------

DEPENDENCIES = $(foreach package, $(PKGS), \
	$(master_srcdir)/src/$(package)/$(package).d)

-include $(DEPENDENCIES)

INCLUDEDIRS = \
		$(foreach package, $(PKGS), -I$(master_srcdir)/src/$(package)) \
		-I$(objectdir)

LIBRARYDIRS = $(LIBDIRS) 

LIBS = $(OTHERLIBS)

VPATH = $(master_srcdir): \
	$(addprefix :$(master_srcdir)/src/,$(PKGS)): \
	$(objectdir): 

#GMPLIBS = -lgmp

#gmplibdir = /usr/lib/

#----------------------------------------------------------------------
# Examples included in the distribution
#----------------------------------------------------------------------

# Each example is declared only once. If some checking through is done
# make check, then it is declared in one of CHECK_CNF_EXAMPLES, 
# CHECK_SMT_EXAMPLES. If the example
# is just being added to the examples directory in VIS, then add it here.

EXAMPLES = $(CHECK_CNF_EXAMPLES) $(CHECK_SMT_EXAMPLES)

# The "interesting" example files are anything in the examples subdirectories
# except the RCS subdirectories
#
# This is a rather messy way to look for filenames in the local_srcdir,
# then remove the local_srcdir prefix

EXAMPLEFILES = $(patsubst $(local_srcdir)/%, %, \
		$(filter-out %RCS, $(foreach example, $(EXAMPLES), \
		  $(wildcard $(local_srcdir)/examples/$(example)/*))))

#----------------------------------------------------------------------
# Definitions for the distribution file
#----------------------------------------------------------------------

DISTRIBUTION = $(PRODUCT)-$(VERSION)

# Directories to include in the distribution file

DISTDIRS = src helpers share share/help obj doc examples \
	$(addprefix examples/,$(EXAMPLES)) $(addprefix src/,$(PKGS))

# Build/install helper files

HELPERS = $(addprefix helpers/, \
	install-sh mkinstalldirs config.guess config.sub dependency.make)

# Files to include in the distribution file

DISTFILES = \
	configure configure.in Makefile.in README $(HELPERS) \
	$(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES) \
	$(EXAMPLEFILES) \
	$(addprefix doc/,$(DOCUMENTATION)) \
	$(addprefix share/,$(SHAREFILES)) \
	$(addprefix share/help/,$(HELPFILES))

#----------------------------------------------------------------------
# Implicit rules
#----------------------------------------------------------------------

ALLCFLAGS = $(CFLAGS) $(AC_FLAGS) -DBDDcu $(VERDATE) \
		-DNAWK=\"$(NAWK)\" -DLIBRARY=\"$(datadir)\" 

# For compiling a source file into the object directory

$(objectdir)/%.o : %.c
	umask 2 ; $(CC) -c $(ALLCFLAGS) $(INCLUDEDIRS) -o $@ $<

# Place object files into an archive

%.a :
	rm -f $@
	umask 2; $(AR) cq $@ $^
	$(RANLIB) $@

######################################################################
# 				RULES				     #
######################################################################

#:
#: Useful targets:
#:

#----------------------------------------------------------------------
# Rule for getting help
#----------------------------------------------------------------------

.PHONY : help

#: help -- Print a list of targets

# This prints all lines in this Makefile that begin with #:

help :
	@sed -n "s/^#://p" Makefile

#----------------------------------------------------------------------
# Always executed once when the Makefile is run
#----------------------------------------------------------------------

# Make sure the directory in which to place the objects exists

ignored := $(shell umask 2; test -d $(objectdir) || mkdir $(objectdir))

#----------------------------------------------------------------------
# Rules to compile and build libraries and executables
#----------------------------------------------------------------------

.PHONY : all library compile-version delete-version

#:
#: all (the default) -- Compile the main executable
# (force the version to be recompiled)

all : compile-version $(PRODUCT)

# Create the main executable

$(PRODUCT) : $(OBJECTS) 
	umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \
		$(OBJECTS) $(LIBRARYDIRS) $(LIBS) -ldl  

#$(PRODUCT) : $(OBJECTS) $(gmplibdir)/libgmp.la
#	umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \
#		$(OBJECTS) $(LIBRARYDIRS) $(LIBS) -ldl $(GMPLIBS) 

# Force the "version" information to be recompiled

compile-version : delete-version $(objectdir)/main.o

# Delete the object file related to the version

delete-version :
	rm -f $(objectdir)/main.o

# Build a library containing all the objects

#: library -- Create a library of all the objects (useful in a central area)

library : $(LIBRARY)

$(LIBRARY) : $(OBJECTS)

#----------------------------------------------------------------------
# Rules for checking the build
#----------------------------------------------------------------------
.PHONY : check check-examples

# This is a lengthy sed command used to filter out the irrelevant CUSP 
# output that appears when the examples are running.
#
# Sed does not permit space between the trailing p ("print matching
# lines") and the semicolon (end of command).  Hashes are escaped --
# otherwise they are Makefile comments.  This was once a long egrep
# expression, but the string was too long for Ultrix's egrep.

SED_CMD = \
	/^UNSATISFIABLE/p; \
	/^SATISFIABLE/p; \
	/^unsat/p; \
	/^sat/p; \
	/;.*;/p;

# List of all examples to check (A subset of EXAMPLES) 

CHECK_CNF_EXAMPLES = arbiter daio 3blocks bw_large.a hanoi4 rot

CHECK_SMT_EXAMPLES =  2ba bignum_idl1 bignum_idl2 bignum_rdl1 bignum_rdl2 \
     	      	BinarySearch_live_blmc000 CELAR6_SUB0 ckt_PROP14_tf_9 \
	diamonds.10.2.i.a.u DTP_k2_n35_c175_s1 FISCHER3-4-ninc fischer3-mutex-5 \
	inf-bakery-mutex-1 int_incompleteness1 jobshop4-2-2-2-4-4-12 plan-5.cvc

CHECK_EXAMPLES = $(CHECK_SMT_EXAMPLES) $(CHECK_CNF_EXAMPLES) 

# Determine the absolute executable path
# 
# Starting from the current directory, change directory to the directory
# part of the product name, then tack on the filename part of EXECUTABLE

EXECUTABLE = $(PRODUCT)

EXECUTABLEPATH := \
	$(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE))

EXECUTABLEPATH := \
	$(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE))

# Determine the rootname of the examples
#

EXAMPLEPATH = $(master_srcdir)/examples

FULLEXAMPLEPATH := $(shell cd $(EXAMPLEPATH) ; pwd)

#:
#: check -- Test the locally-built executable (runs check-examples)
#:          Include check-cnf-simp-examples to check the cnf solver
#: 	    with its preprocessors. For example, 
# 
# check : check-cnf-examples check-cnf-simp-examples check-smt-examples
#
check : check-cnf-examples check-smt-examples

#: check-examples -- Test each of the examples listed in CHECK_EXAMPLES
#:	    You may want to invoke this with
#:            gmake "CHECK_EXAMPLES=abp bakery" check-examples
#:            gmake EXECUTABLE=cusp check-smt-examples

# For each example,
#
# 1) create the directory checkresults/<example>
# 2) enter that directory
# 3) run CUSP for the example  producing "result.raw"
# 5) filter out relevant lines in the result, producing "result.filtered"
#    and compare this with the "check_result" file in the master source
#    directory.  Differences are written to "result.differences"
check-cnf-examples :
	@test -d checkresults || mkdir checkresults
	@echo "Checking examples.  Results will be in checkresults/<example>/result.raw"
	@echo "Running executable $(EXECUTABLEPATH) for CNFs "
	@echo " (change with EXECUTABLE=...)"
	@echo "Taking examples from $(FULLEXAMPLEPATH)"
	@echo " (change with EXAMPLEPATH=...)"
	@cwd=`pwd` ; \
	for example in $(CHECK_CNF_EXAMPLES) ; \
	do \
	  echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \
	  cd $$cwd ; \
	  test -d checkresults/$$example || \
		mkdir checkresults/$$example ; \
	  cd checkresults/$$example ; \
	  $(EXECUTABLEPATH) -cnf $(FULLEXAMPLEPATH)/$$example/$$example.cnf > result.raw 2> result.stderr ; \
	  sed -n '$(SED_CMD)' result.raw > result.filtered ; \
	  if diff result.filtered \
	  	$(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \
	  then \
	    echo "passed" ; \
	    rm result.differences ; \
	  else \
	    echo "failed (more checkresults/$$example/result.differences)" ; \
	  fi ; \
	done
       
check-cnf-simp-examples :
	@test -d checkresults || mkdir checkresults
	@echo "Checking examples.  Results will be in checkresults/<example>/result.raw"
	@echo "Running executable $(EXECUTABLEPATH) for CNFs "
	@echo " (change with EXECUTABLE=...)"
	@echo "Taking examples from $(FULLEXAMPLEPATH)"
	@echo " (change with EXAMPLEPATH=...)"
	@cwd=`pwd` ; \
	for example in $(CHECK_CNF_EXAMPLES) ; \
	do \
	  echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \
	  cd $$cwd ; \
	  test -d checkresults/$$example || \
		mkdir checkresults/$$example ; \
	  cd checkresults/$$example ; \
	  $(EXECUTABLEPATH) -cnf $(FULLEXAMPLEPATH)/$$example/$$example.cnf -velim -distill > result.raw 2> result.stderr ; \
	  sed -n '$(SED_CMD)' result.raw > result.filtered ; \
	  if diff result.filtered \
	  	$(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \
	  then \
	    echo "passed" ; \
	    rm result.differences ; \
	  else \
	    echo "failed (more checkresults/$$example/result.differences)" ; \
	  fi ; \
	done

check-smt-examples :
	@test -d checkresults || mkdir checkresults
	@echo "Checking examples.  Results will be in checkresults/<example>/result.raw"
	@echo "Running executable $(EXECUTABLEPATH) for SMTs "
	@echo " (change with EXECUTABLE=...)"
	@echo "Taking examples from $(FULLEXAMPLEPATH)"
	@echo " (change with EXAMPLEPATH=...)"
	@cwd=`pwd` ; \
	for example in $(CHECK_SMT_EXAMPLES) ; \
	do \
	  echo -n "Checking $(EXECUTABLEPATH) $$example ... " ; \
	  cd $$cwd ; \
	  test -d checkresults/$$example || \
		mkdir checkresults/$$example ; \
	  cd checkresults/$$example ; \
	  $(EXECUTABLEPATH) $(FULLEXAMPLEPATH)/$$example/$$example.smt > result.raw 2> result.stderr ; \
	  sed -n '$(SED_CMD)' result.raw > result.filtered ; \
	  if diff result.filtered \
	  	$(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \
	  then \
	    echo "passed" ; \
	    rm result.differences ; \
	  else \
	    awk '/read CNF file/ { print "Warning : CUSP for SMT is not built!"}' result.stderr; \
	    awk '!/read CNF file/ { print "failed (more checkresults/$$example/result.differences)"}' result.stderr; \
	  fi ; \
	done


#----------------------------------------------------------------------
# Rules for installation
#----------------------------------------------------------------------

.PHONY : install uninstall installdirs

#:
#: install -- Install the product and libraries in bindir, libdir,
#:            datadir, etc.

install : $(PRODUCT) $(LIBRARY) installdirs
	@echo "Installing $(bindir)/$(PRODUCT)" 
	@$(INSTALL_PROGRAM) $(PRODUCT) $(bindir)/$(PRODUCT) 
	@echo "Installing $(libdir)/$(LIBRARY)" 
	@$(INSTALL_DATA) $(LIBRARY) $(libdir)/$(LIBRARY) 
	@for file in $(SHAREFILES) ; do \
		echo "Installing $(datadir)/$$file"; \
		$(INSTALL_DATA) $(master_srcdir)/share/$$file \
			$(datadir)/$$file; \
	done
	@for file in $(HELPFILES) ; do \
		echo "Installing $(datadir)/help/$$file"; \
		$(INSTALL_DATA) $(master_srcdir)/share/help/$$file \
			$(datadir)/help/$$file; \
        done
	@for header in $(HEADERS); do \
		echo "Installing $(includedir)/$$header"; \
		$(INSTALL_DATA) $(master_srcdir)/src/*/$$header \
			$(includedir)/$$header; \
        done

#: uninstall -- Reverse the effects of "install"

uninstall :
	rm -f $(bindir)/$(PRODUCT)	
	rm -f $(libdir)/$(LIBRARY)
	@for file in $(SHAREFILES) ; \
	do \
	  echo "Removing $(datadir)/$$file"; \
	  rm -f $(datadir)/$$file; \
	done
	@for file in $(HELPFILES) ; \
	do \
	  echo "Removing $(datadir)/help/$$file"; \
	  rm -f $(datadir)/help/$$file; \
	done
	@for header in $(HEADERS); \
	do \
	  echo "Removing $(includedir)/$$header"; \
	  rm -f $(includedir)/$$header; \
	done

installdirs :
	$(master_srcdir)/helpers/mkinstalldirs \
		$(bindir) $(libdir) $(includedir) $(datadir) $(datadir)/help \
                $(mandir)

#----------------------------------------------------------------------
# Rules for cleaning
#----------------------------------------------------------------------

.PHONY : clean mostlyclean distclean

#:
#: clean -- Remove every file created by building

clean mostlyclean :
	rm -rf $(objectdir)/* $(PRODUCT) include

#: distclean -- Remove every file created by building or configuring

distclean : clean cleandependencies
	rm -f Makefile config.status config.cache config.log

#----------------------------------------------------------------------
# Rule for performing a lint-like check on the source code
#
# Note: This requires gcc or g++
#----------------------------------------------------------------------

.PHONY : check-code

#:
#: check-code -- Run a lint-like check on the source code.
#:               (useful for development)

CHECK_FLAGS := -Wall -pedantic -Wmissing-declarations
ifeq ($(CC),gcc)
  CHECK_FLAGS := $(CHECK_FLAGS) -Wstrict-prototypes -Wmissing-prototypes
endif

check-code : $(CSRC) 
ifneq ($(findstring <$(CC)>,<gcc> <g++>),)
	@rm -f *.o_checkcode
	@for file in $^; \
	do \
	  echo "------------------------ Checking $$file"; \
	  $(CC) -c $(CFLAGS) $(AC_FLAGS) $(CHECK_FLAGS) \
		$(VERDATE) $(INCLUDEDIRS) \
		-o $(objectdir)/checkcode_output.o $$file; \
	  rm -f $(objectdir)/checkcode_output.o; \
	done
	@rm -f *.o_checkcode
else
	@echo "check-code requires gcc or g++"
	@echo "Reconfigure with gcc or g++"
endif

#----------------------------------------------------------------------
# Rules that produce/delete the dependency file for every package
#----------------------------------------------------------------------

.PHONY : dependencies cleandependencies

#:
#: dependencies -- Create a list of dependency files.
#:                 Useful when modifying header files.

# Invoke the "dependency.make" Makefile on each package subdirectory,
# passing the path, etc. to it.
#
# There's a strange feature in autoconf where lines of the form " VPATH="
# are removed from the Makefile.  Thus, a flag is placed before the 
# VPATH= argument below.

dependencies:
ifneq ($(findstring <$(CC)>,<gcc> <g++>),)
	for pkg in $(PKGS) ; \
	do \
	  $(MAKE) --no-print-directory \
		-f $(master_srcdir)/helpers/dependency.make \
		CC="$(CC)" \
		CFLAGS="$(CFLAGS)" VPATH="$(local_srcdir)/src/$$pkg" \
		AC_FLAGS="$(AC_FLAGS)" \
		INCLUDEDIRS="$(INCLUDEDIRS)" objectdir=$(objectdir) \
		PKGNAME=$(local_srcdir)/src/$$pkg/$$pkg \
		$(local_srcdir)/src/$$pkg/$$pkg.d ; \
	done
else
	@echo "dependency requires gcc or g++"
	@echo "Reconfigure with gcc or g++"
endif

cleandependencies:
	rm -f $(local_srcdir)/src/*/*.d

#----------------------------------------------------------------------
# Rules for making a distribution file
#----------------------------------------------------------------------

.PHONY : dist

#:
#: dist -- Create a tarred, gzipped distribution file

# Warning: "tar" under Digital Unix (on DEC Alphas) writes directories
# that don't work under SunOS tar

dist : $(DISTRIBUTION).tar.gz

$(DISTRIBUTION).tar.gz : $(DISTFILES)
ifeq ($(strip $(FULL_MISSING_PKGS)),)
	rm -rf $(DISTRIBUTION)
	umask 022; mkdir $(DISTRIBUTION)
	for dir in $(DISTDIRS); \
	do \
	  umask 022; mkdir $(DISTRIBUTION)/$$dir; \
	done
	@echo "Copying distribution files"
	@for file in $(patsubst $(local_srcdir)/%, %, $^); \
	do \
	  echo "  $$file"; \
	  cp -p $(local_srcdir)/$$file $(DISTRIBUTION)/$$file; \
	done
	- chmod -R a+r $(DISTRIBUTION)
	- chmod -R u+w $(DISTRIBUTION)
	tar cf - $(DISTRIBUTION) | gzip -9 > $(DISTRIBUTION).tar.gz
	rm -rf $(DISTRIBUTION)
else
	@echo "Missing packages: $(FULL_MISSING_PKGS)"
	@echo "Make sure PKGS lists all the packages"
	@exit 1
endif


#----------------------------------------------------------------------
# Rules for debugging the Makefile
#----------------------------------------------------------------------

.PHONY : debug-make

DEBUG_VARS = 	PKGS \
		VPATH \
		INCLUDEDIRS \
		CSRC \
		OBJECTS \
		HEADERS \
		MAKEINCLUDES \
		CFLAGS \
		AC_FLAGS \
		master_srcdir \
		LIBS 

#:
#: debug-make -- Print a list of Makefile variables

debug-make:
	@$(foreach var, $(DEBUG_VARS), echo $(var)=$($(var)) ; )