Skip to content
Commits on Source (12)
Expand all Show whitespace changes
Inline Side-by-side
ChangeLog
View file @ d1e30f73
2016-06-27 Steven Eker <eker@install.csl.sri.com>
* tests/Misc/smtTest (MAUDE_LIB): skip test if we don't define USE_CVC4
* configure.ac: use no argument form of AM_INIT_AUTOMAKE
===================================Maude110b===========================================
2016-05-05 Steven Eker <eker@install.csl.sri.com>
* configure.ac: changed bug report address from maude-bugs@maude.cs.uiuc.edu
to maude-bugs@lists.cs.illinois.edu
===================================Maude110===========================================
2016-02-26 Steven Eker <eker@install.csl.sri.com>
* tests/Misc/meseguerFiniteVariant.maude: created
* tests/Misc/meseguerFiniteVariant: created
===================================Maude109===========================================
2014-11-19 Steven Eker <eker@ape.csl.sri.com>
* tests/Misc/assocUnification.maude: added examples to test new capabilities
===================================Maude106===========================================
2014-10-29 Steven Eker <eker@ape.csl.sri.com>
* tests/Misc/smtTest.maude: updated with new syntax and examples
===================================Maude105===========================================
2014-08-14 Steven Eker <eker@ape.csl.sri.com>
* tests/Misc/smtTest.maude: use new syntax
===================================Maude104===========================================
2014-04-22 Steven Eker <eker@ape.csl.sri.com>
* configure.ac: added configuration for CVC4 and POSIX Realtime
Extensions library (needed by CVC4)
===================================Maude103===========================================
2014-04-04 Steven Eker <eker@ape.csl.sri.com>
* tests/Misc/assocUnification (MAUDE_LIB): created
* tests/Misc/assocUnification.maude: created
* tests/Misc/unification.maude: change assoc to assoc id: in TEST2
since assoc is now partially supported
===================================Maude102===========================================
2014-02-06 Steven Eker <eker@ape.csl.sri.com>
* configure.ac: removed rope_UGLY_HACK option
......
INSTALL
View file @ d1e30f73
......@@ -18,11 +18,12 @@ GNU gmp http://www.swox.com/gmp/
GNU libsigsegv http://libsigsegv.sourceforge.net/
Tecla http://www.astro.caltech.edu/~mcs/tecla/
BuDDY http://sourceforge.net/projects/buddy
CVC4 (optional) http://cvc4.cs.nyu.edu/web/
Configuring the 3rd party packages
==================================
Because of C++ ABI incompatibilities, GNU gmp and BuDDy must be
Because of C++ ABI incompatibilities, GNU gmp, BuDDy and CVC4 must be
compiled with the same compiler you will use for Maude.
GNU gmp must be configured with --enable-cxx to generate the C++
......@@ -51,6 +52,10 @@ build Maude with the commands:
./configure
make
If you don't have CVC4 you can pass --with-cvc4=no to configure. This
disables the experimental rewriting modulo SMT feature, and produces
a much smaller binary (CVC4 is much larger than Maude).
A very basic test suite can be run using the command:
make check
......@@ -65,6 +70,7 @@ GMP_LIBS (defaults to -lgmpxx -lgmp)
LIBSIGSEGV_LIB (defaults to -lsigsegv)
TECLA_LIBS (defaults to -ltecla -lcurses)
BUDDY_LIB (defaults to -lbuddy)
CVC4_LIB (defaults to -lcvc4)
A more realistic configure to make, check and install a static binary
using a separate build tree might look something like:
......@@ -90,34 +96,21 @@ $(bindir).
Note for Mac users
==================
Currently (February 7th, 2014):
The official Apple version of gcc is an llvm front end from 2007 and is
not capable of compiling Maude (Apple is pushing developers to clang).
The offical Apple version of flex (2.5.35) contains a serious bug not
present in the GNU version and which can cause Maude to hang.
The are two viable routes to building Maude on Macs:
(1) Install the tools and libraries from Mac Ports (http://www.macports.org/).
(2) Build the tools and libraries from source.
Going the Mac Ports route, the release binary was configured thus:
As of Mavericks, Apple no longer supports gcc so Maude must be compiled with clang.
The easiest way is to install the Mac Ports version of each of
the needed tools and libraries. With Mac Ports installed in /opt/local
I use the configuration line:
../configure \
CC=/opt/local/bin/gcc-mp-4.8 \
CXX=/opt/local/bin/g++-mp-4.8 \
CC=cc \
CXX=c++ \
FLEX=/opt/local/bin/flex \
BISON=/opt/local/bin/bison \
CFLAGS="-Wall -O2 -static-libstdc++ -static-libgcc -fno-crossjumping -fno-stack-protector -fstrict-aliasing -mmacosx-version-min=10.5 -finline-limit=10000" \
CXXFLAGS="-Wall -O2 -static-libstdc++ -static-libgcc -fno-crossjumping -fno-stack-protector -fstrict-aliasing -mmacosx-version-min=10.5 -finline-limit=10000" \
CFLAGS="-Wall -O2 -I/opt/local/include -fno-stack-protector -fstrict-aliasing" \
CXXFLAGS="-Wall -O2 -I/opt/local/include -fno-stack-protector -fstrict-aliasing" \
BUDDY_LIB="/opt/local/lib/libbdd.a" \
TECLA_LIBS="/opt/local/lib/libtecla.a /usr/lib/libncurses.dylib" \
LIBSIGSEGV_LIB="/opt/local/lib/libsigsegv.a" \
GMP_LIBS="/opt/local/lib/libgmp.a /opt/local/lib/libgmpxx.a"
This results in an almost static binary that should run on any x86-64 Mac
running Leopard or later without the installation of extra libraries. Note
that the Apple ncurses library is linked since the Mac Ports version depends
on the Mac Ports terminfo data base, which most users will not have installed.
GMP_LIBS="/opt/local/lib/libgmp.a /opt/local/lib/libgmpxx.a" \
CVC4_LIB="/opt/local/lib/libcvc4.a"
Makefile.in
View file @ d1e30f73
# Makefile.in generated by automake 1.11.3 from Makefile.am.
# Makefile.in generated by automake 1.14.1 from Makefile.am.
# @configure_input@
# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
# 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011 Free Software
# Foundation, Inc.
# Copyright (C) 1994-2013 Free Software Foundation, Inc.
# This Makefile.in is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
# with or without modifications, as long as this notice is preserved.
......@@ -15,6 +14,51 @@
@SET_MAKE@
VPATH = @srcdir@
am__is_gnu_make = test -n '$(MAKEFILE_LIST)' && test -n '$(MAKELEVEL)'
am__make_running_with_option = \
case $${target_option-} in \
?) ;; \
*) echo "am__make_running_with_option: internal error: invalid" \
"target option '$${target_option-}' specified" >&2; \
exit 1;; \
esac; \
has_opt=no; \
sane_makeflags=$$MAKEFLAGS; \
if $(am__is_gnu_make); then \
sane_makeflags=$$MFLAGS; \
else \
case $$MAKEFLAGS in \
*\\[\ \ ]*) \
bs=\\; \
sane_makeflags=`printf '%s\n' "$$MAKEFLAGS" \
| sed "s/$$bs$$bs[$$bs $$bs ]*//g"`;; \
esac; \
fi; \
skip_next=no; \
strip_trailopt () \
{ \
flg=`printf '%s\n' "$$flg" | sed "s/$$1.*$$//"`; \
}; \
for flg in $$sane_makeflags; do \
test $$skip_next = yes && { skip_next=no; continue; }; \
case $$flg in \
*=*|--*) continue;; \
-*I) strip_trailopt 'I'; skip_next=yes;; \
-*I?*) strip_trailopt 'I';; \
-*O) strip_trailopt 'O'; skip_next=yes;; \
-*O?*) strip_trailopt 'O';; \
-*l) strip_trailopt 'l'; skip_next=yes;; \
-*l?*) strip_trailopt 'l';; \
-[dEDm]) skip_next=yes;; \
-[JT]) skip_next=yes;; \
esac; \
case $$flg in \
*$$target_option*) has_opt=yes; break;; \
esac; \
done; \
test $$has_opt = yes
am__make_dryrun = (target_option=n; $(am__make_running_with_option))
am__make_keepgoing = (target_option=k; $(am__make_running_with_option))
pkgdatadir = $(datadir)/@PACKAGE@
pkgincludedir = $(includedir)/@PACKAGE@
pkglibdir = $(libdir)/@PACKAGE@
......@@ -34,11 +78,11 @@ POST_UNINSTALL = :
build_triplet = @build@
host_triplet = @host@
subdir = .
DIST_COMMON = README $(am__configure_deps) $(srcdir)/Makefile.am \
$(srcdir)/Makefile.in $(srcdir)/config.h.in \
$(top_srcdir)/configure AUTHORS COPYING ChangeLog INSTALL NEWS \
compile config.guess config.sub depcomp install-sh missing \
mkinstalldirs
DIST_COMMON = INSTALL NEWS README AUTHORS ChangeLog \
$(srcdir)/Makefile.in $(srcdir)/Makefile.am \
$(top_srcdir)/configure $(am__configure_deps) \
$(srcdir)/config.h.in mkinstalldirs COPYING compile \
config.guess config.sub depcomp install-sh missing
ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
am__aclocal_m4_deps = $(top_srcdir)/configure.ac
am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
......@@ -49,22 +93,62 @@ mkinstalldirs = $(SHELL) $(top_srcdir)/mkinstalldirs
CONFIG_HEADER = config.h
CONFIG_CLEAN_FILES =
CONFIG_CLEAN_VPATH_FILES =
AM_V_P = $(am__v_P_@AM_V@)
am__v_P_ = $(am__v_P_@AM_DEFAULT_V@)
am__v_P_0 = false
am__v_P_1 = :
AM_V_GEN = $(am__v_GEN_@AM_V@)
am__v_GEN_ = $(am__v_GEN_@AM_DEFAULT_V@)
am__v_GEN_0 = @echo " GEN " $@;
am__v_GEN_1 =
AM_V_at = $(am__v_at_@AM_V@)
am__v_at_ = $(am__v_at_@AM_DEFAULT_V@)
am__v_at_0 = @
am__v_at_1 =
SOURCES =
DIST_SOURCES =
RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
html-recursive info-recursive install-data-recursive \
install-dvi-recursive install-exec-recursive \
install-html-recursive install-info-recursive \
install-pdf-recursive install-ps-recursive install-recursive \
installcheck-recursive installdirs-recursive pdf-recursive \
ps-recursive uninstall-recursive
RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \
ctags-recursive dvi-recursive html-recursive info-recursive \
install-data-recursive install-dvi-recursive \
install-exec-recursive install-html-recursive \
install-info-recursive install-pdf-recursive \
install-ps-recursive install-recursive installcheck-recursive \
installdirs-recursive pdf-recursive ps-recursive \
tags-recursive uninstall-recursive
am__can_run_installinfo = \
case $$AM_UPDATE_INFO_DIR in \
n|no|NO) false;; \
*) (install-info --version) >/dev/null 2>&1;; \
esac
RECURSIVE_CLEAN_TARGETS = mostlyclean-recursive clean-recursive \
distclean-recursive maintainer-clean-recursive
AM_RECURSIVE_TARGETS = $(RECURSIVE_TARGETS:-recursive=) \
$(RECURSIVE_CLEAN_TARGETS:-recursive=) tags TAGS ctags CTAGS \
distdir dist dist-all distcheck
am__recursive_targets = \
$(RECURSIVE_TARGETS) \
$(RECURSIVE_CLEAN_TARGETS) \
$(am__extra_recursive_targets)
AM_RECURSIVE_TARGETS = $(am__recursive_targets:-recursive=) TAGS CTAGS \
cscope distdir dist dist-all distcheck
am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) \
$(LISP)config.h.in
# Read a list of newline-separated strings from the standard input,
# and print each of them once, without duplicates. Input order is
# *not* preserved.
am__uniquify_input = $(AWK) '\
BEGIN { nonempty = 0; } \
{ items[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in items) print i; }; } \
'
# Make sure the list of sources is unique. This is necessary because,
# e.g., the same source file might be shared among _SOURCES variables
# for different programs/libraries.
am__define_uniq_tagged_files = \
list='$(am__tagged_files)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | $(am__uniquify_input)`
ETAGS = etags
CTAGS = ctags
CSCOPE = cscope
DIST_SUBDIRS = $(SUBDIRS)
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
distdir = $(PACKAGE)-$(VERSION)
......@@ -75,6 +159,7 @@ am__remove_distdir = \
&& rm -rf "$(distdir)" \
|| { sleep 5 && rm -rf "$(distdir)"; }; \
else :; fi
am__post_remove_distdir = $(am__remove_distdir)
am__relativize = \
dir0=`pwd`; \
sed_first='s,^\([^/]*\)/.*$$,\1,'; \
......@@ -102,12 +187,14 @@ am__relativize = \
reldir="$$dir2"
DIST_ARCHIVES = $(distdir).tar.gz
GZIP_ENV = --best
DIST_TARGETS = dist-gzip
distuninstallcheck_listfiles = find . -type f -print
am__distuninstallcheck_listfiles = $(distuninstallcheck_listfiles) \
| sed 's|^\./|$(prefix)/|' | grep -v '$(infodir)/dir$$'
distcleancheck_listfiles = find . -type f -print
ACLOCAL = @ACLOCAL@
AMTAR = @AMTAR@
AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
......@@ -118,6 +205,7 @@ CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
CPPFLAGS = @CPPFLAGS@
CVC4_LIB = @CVC4_LIB@
CXX = @CXX@
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
......@@ -253,8 +341,8 @@ $(ACLOCAL_M4): $(am__aclocal_m4_deps)
$(am__aclocal_m4_deps):
config.h: stamp-h1
@if test ! -f $@; then rm -f stamp-h1; else :; fi
@if test ! -f $@; then $(MAKE) $(AM_MAKEFLAGS) stamp-h1; else :; fi
@test -f $@ || rm -f stamp-h1
@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) stamp-h1
stamp-h1: $(srcdir)/config.h.in $(top_builddir)/config.status
@rm -f stamp-h1
......@@ -268,22 +356,25 @@ distclean-hdr:
-rm -f config.h stamp-h1
# This directory's subdirectories are mostly independent; you can cd
# into them and run `make' without going through this Makefile.
# To change the values of `make' variables: instead of editing Makefiles,
# (1) if the variable is set in `config.status', edit `config.status'
# (which will cause the Makefiles to be regenerated when you run `make');
# (2) otherwise, pass the desired values on the `make' command line.
$(RECURSIVE_TARGETS):
@fail= failcom='exit 1'; \
for f in x $$MAKEFLAGS; do \
case $$f in \
*=* | --[!k]*);; \
*k*) failcom='fail=yes';; \
esac; \
done; \
# into them and run 'make' without going through this Makefile.
# To change the values of 'make' variables: instead of editing Makefiles,
# (1) if the variable is set in 'config.status', edit 'config.status'
# (which will cause the Makefiles to be regenerated when you run 'make');
# (2) otherwise, pass the desired values on the 'make' command line.
$(am__recursive_targets):
@fail=; \
if $(am__make_keepgoing); then \
failcom='fail=yes'; \
else \
failcom='exit 1'; \
fi; \
dot_seen=no; \
target=`echo $@ | sed s/-recursive//`; \
list='$(SUBDIRS)'; for subdir in $$list; do \
case "$@" in \
distclean-* | maintainer-clean-*) list='$(DIST_SUBDIRS)' ;; \
*) list='$(SUBDIRS)' ;; \
esac; \
for subdir in $$list; do \
echo "Making $$target in $$subdir"; \
if test "$$subdir" = "."; then \
dot_seen=yes; \
......@@ -298,57 +389,12 @@ $(RECURSIVE_TARGETS):
$(MAKE) $(AM_MAKEFLAGS) "$$target-am" || exit 1; \
fi; test -z "$$fail"
$(RECURSIVE_CLEAN_TARGETS):
@fail= failcom='exit 1'; \
for f in x $$MAKEFLAGS; do \
case $$f in \
*=* | --[!k]*);; \
*k*) failcom='fail=yes';; \
esac; \
done; \
dot_seen=no; \
case "$@" in \
distclean-* | maintainer-clean-*) list='$(DIST_SUBDIRS)' ;; \
*) list='$(SUBDIRS)' ;; \
esac; \
rev=''; for subdir in $$list; do \
if test "$$subdir" = "."; then :; else \
rev="$$subdir $$rev"; \
fi; \
done; \
rev="$$rev ."; \
target=`echo $@ | sed s/-recursive//`; \
for subdir in $$rev; do \
echo "Making $$target in $$subdir"; \
if test "$$subdir" = "."; then \
local_target="$$target-am"; \
else \
local_target="$$target"; \
fi; \
($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \
|| eval $$failcom; \
done && test -z "$$fail"
tags-recursive:
list='$(SUBDIRS)'; for subdir in $$list; do \
test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) tags); \
done
ctags-recursive:
list='$(SUBDIRS)'; for subdir in $$list; do \
test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) ctags); \
done
ID: $(am__tagged_files)
$(am__define_uniq_tagged_files); mkid -fID $$unique
tags: tags-recursive
TAGS: tags
ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
mkid -fID $$unique
tags: TAGS
TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
tags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
set x; \
here=`pwd`; \
if ($(ETAGS) --etags-include --version) >/dev/null 2>&1; then \
......@@ -364,12 +410,7 @@ TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \
set "$$@" "$$include_option=$$here/$$subdir/TAGS"; \
fi; \
done; \
list='$(SOURCES) $(HEADERS) config.h.in $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
$(am__define_uniq_tagged_files); \
shift; \
if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
test -n "$$unique" || unique=$$empty_fix; \
......@@ -381,15 +422,11 @@ TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \
$$unique; \
fi; \
fi
ctags: CTAGS
CTAGS: ctags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
list='$(SOURCES) $(HEADERS) config.h.in $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
ctags: ctags-recursive
CTAGS: ctags
ctags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
$(am__define_uniq_tagged_files); \
test -z "$(CTAGS_ARGS)$$unique" \
|| $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
$$unique
......@@ -398,9 +435,31 @@ GTAGS:
here=`$(am__cd) $(top_builddir) && pwd` \
&& $(am__cd) $(top_srcdir) \
&& gtags -i $(GTAGS_ARGS) "$$here"
cscope: cscope.files
test ! -s cscope.files \
|| $(CSCOPE) -b -q $(AM_CSCOPEFLAGS) $(CSCOPEFLAGS) -i cscope.files $(CSCOPE_ARGS)
clean-cscope:
-rm -f cscope.files
cscope.files: clean-cscope cscopelist
cscopelist: cscopelist-recursive
cscopelist-am: $(am__tagged_files)
list='$(am__tagged_files)'; \
case "$(srcdir)" in \
[\\/]* | ?:[\\/]*) sdir="$(srcdir)" ;; \
*) sdir=$(subdir)/$(srcdir) ;; \
esac; \
for i in $$list; do \
if test -f "$$i"; then \
echo "$(subdir)/$$i"; \
else \
echo "$$sdir/$$i"; \
fi; \
done >> $(top_builddir)/cscope.files
distclean-tags:
-rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
-rm -f cscope.out cscope.in.out cscope.po.out cscope.files
distdir: $(DISTFILES)
$(am__remove_distdir)
......@@ -436,13 +495,10 @@ distdir: $(DISTFILES)
done
@list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
if test "$$subdir" = .; then :; else \
test -d "$(distdir)/$$subdir" \
$(am__make_dryrun) \
|| test -d "$(distdir)/$$subdir" \
|| $(MKDIR_P) "$(distdir)/$$subdir" \
|| exit 1; \
fi; \
done
@list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
if test "$$subdir" = .; then :; else \
dir1=$$subdir; dir2="$(distdir)/$$subdir"; \
$(am__relativize); \
new_distdir=$$reldir; \
......@@ -471,40 +527,42 @@ distdir: $(DISTFILES)
|| chmod -R a+r "$(distdir)"
dist-gzip: distdir
tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-bzip2: distdir
tardir=$(distdir) && $(am__tar) | BZIP2=$${BZIP2--9} bzip2 -c >$(distdir).tar.bz2
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-lzip: distdir
tardir=$(distdir) && $(am__tar) | lzip -c $${LZIP_OPT--9} >$(distdir).tar.lz
$(am__remove_distdir)
dist-lzma: distdir
tardir=$(distdir) && $(am__tar) | lzma -9 -c >$(distdir).tar.lzma
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-xz: distdir
tardir=$(distdir) && $(am__tar) | XZ_OPT=$${XZ_OPT--e} xz -c >$(distdir).tar.xz
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-tarZ: distdir
@echo WARNING: "Support for shar distribution archives is" \
"deprecated." >&2
@echo WARNING: "It will be removed altogether in Automake 2.0" >&2
tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-shar: distdir
@echo WARNING: "Support for distribution archives compressed with" \
"legacy program 'compress' is deprecated." >&2
@echo WARNING: "It will be removed altogether in Automake 2.0" >&2
shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz
$(am__remove_distdir)
$(am__post_remove_distdir)
dist-zip: distdir
-rm -f $(distdir).zip
zip -rq $(distdir).zip $(distdir)
$(am__remove_distdir)
$(am__post_remove_distdir)
dist dist-all: distdir
tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz
$(am__remove_distdir)
dist dist-all:
$(MAKE) $(AM_MAKEFLAGS) $(DIST_TARGETS) am__post_remove_distdir='@:'
$(am__post_remove_distdir)
# This target untars the dist file and tries a VPATH configuration. Then
# it guarantees that the distribution is self-contained by making another
......@@ -515,8 +573,6 @@ distcheck: dist
GZIP=$(GZIP_ENV) gzip -dc $(distdir).tar.gz | $(am__untar) ;;\
*.tar.bz2*) \
bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\
*.tar.lzma*) \
lzma -dc $(distdir).tar.lzma | $(am__untar) ;;\
*.tar.lz*) \
lzip -dc $(distdir).tar.lz | $(am__untar) ;;\
*.tar.xz*) \
......@@ -528,18 +584,19 @@ distcheck: dist
*.zip*) \
unzip $(distdir).zip ;;\
esac
chmod -R a-w $(distdir); chmod a+w $(distdir)
mkdir $(distdir)/_build
mkdir $(distdir)/_inst
chmod -R a-w $(distdir)
chmod u+w $(distdir)
mkdir $(distdir)/_build $(distdir)/_inst
chmod a-w $(distdir)
test -d $(distdir)/_build || exit 0; \
dc_install_base=`$(am__cd) $(distdir)/_inst && pwd | sed -e 's,^[^:\\/]:[\\/],/,'` \
&& dc_destdir="$${TMPDIR-/tmp}/am-dc-$$$$/" \
&& am__cwd=`pwd` \
&& $(am__cd) $(distdir)/_build \
&& ../configure --srcdir=.. --prefix="$$dc_install_base" \
&& ../configure \
$(AM_DISTCHECK_CONFIGURE_FLAGS) \
$(DISTCHECK_CONFIGURE_FLAGS) \
--srcdir=.. --prefix="$$dc_install_base" \
&& $(MAKE) $(AM_MAKEFLAGS) \
&& $(MAKE) $(AM_MAKEFLAGS) dvi \
&& $(MAKE) $(AM_MAKEFLAGS) check \
......@@ -562,7 +619,7 @@ distcheck: dist
&& $(MAKE) $(AM_MAKEFLAGS) distcleancheck \
&& cd "$$am__cwd" \
|| exit 1
$(am__remove_distdir)
$(am__post_remove_distdir)
@(echo "$(distdir) archives ready for distribution: "; \
list='$(DIST_ARCHIVES)'; for i in $$list; do echo $$i; done) | \
sed -e 1h -e 1s/./=/g -e 1p -e 1x -e '$$p' -e '$$x'
......@@ -696,13 +753,12 @@ ps-am:
uninstall-am:
.MAKE: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) all \
ctags-recursive install-am install-strip tags-recursive
.MAKE: $(am__recursive_targets) all install-am install-strip
.PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \
all all-am am--refresh check check-am clean clean-generic \
ctags ctags-recursive dist dist-all dist-bzip2 dist-gzip \
dist-lzip dist-lzma dist-shar dist-tarZ dist-xz dist-zip \
.PHONY: $(am__recursive_targets) CTAGS GTAGS TAGS all all-am \
am--refresh check check-am clean clean-cscope clean-generic \
cscope cscopelist-am ctags ctags-am dist dist-all dist-bzip2 \
dist-gzip dist-lzip dist-shar dist-tarZ dist-xz dist-zip \
distcheck distclean distclean-generic distclean-hdr \
distclean-tags distcleancheck distdir distuninstallcheck dvi \
dvi-am html html-am info info-am install install-am \
......@@ -712,8 +768,8 @@ uninstall-am:
install-pdf-am install-ps install-ps-am install-strip \
installcheck installcheck-am installdirs installdirs-am \
maintainer-clean maintainer-clean-generic mostlyclean \
mostlyclean-generic pdf pdf-am ps ps-am tags tags-recursive \
uninstall uninstall-am
mostlyclean-generic pdf pdf-am ps ps-am tags tags-am uninstall \
uninstall-am
# Tell versions [3.59,3.63) of GNU make to not export all variables.
......
NEWS
View file @ d1e30f73
Overview of Changes in alpha110b
================================
* fixed typos and copyright date
* minor configuation fixes
Overview of Changes in alpha110a
================================
* fixed bug in ACU unification that was introduced in alpha108
Overview of Changes in alpha110
===============================
* reorganization of unification sort computations
* added -print-to-stderr flag
* added cycle detection and depth bounds to PIG-PUG
* fixed some uninitialized memory reads in SMT code
Overview of Changes in alpha109
===============================
* new metalevel interface for variant narrowing
* large number of finite variant examples from Jose Meseuger added
to the test suite
Overview of Changes in alpha108a
================================
* fixed bug in variant narrowing where ground terms caused substitution size
mismatch and memory corruption during subsumption check
* replacement rope library avoids build problems on Mac
Overview of Changes in alpha108
===============================
* new associative unification algorithm based on PIG-PUG
* unification infrastructure support for incomplete algorithms
* fixed bug in metaGetIrredundantVariant()
* fixed bug in variant narrowing where collapse terms were being narrowed
with variant equations from the wrong kind
Overview of Changes in alpha107
===============================
* fixed bug where asking for the same variant or variant unify twice in
succession from the metalevel resulted in memory corruption
Overview of Changes in alpha106
===============================
* improvements to linear associative unification integration
* fixed bug in SequenceAssignment code (low level associative unification code)
Overview of Changes in alpha105
===============================
* experimental support for multi-step search modulo SMT
Overview of Changes in alpha104
===============================
* fixed duplicate advisories about missing sorts
* fixed missing echoing bug for commands with 2 optional arguments
* fixed caching bug for descent functions
* experimental support for 1-step rewriting modulo SMT
Overview of Changes in alpha103
===============================
* 0/1 is now a valid Rat constant
* advisory printed when downTerm() fails because of kind clash
* experimental support for calling CVC4
* fixed bug where metaPrettyPrint() was failing to generate needed
disambiguation for built-in data types
Overview of Changes in alpha102
===============================
* experimental support for linear associative unification
Overview of Changes in Maude 2.7 (alpha101)
===========================================
* fixed bug with debug text being output during rewriting
......@@ -16,7 +85,7 @@ Overview of Changes in alpha100a
* code cleaning to remove unused code and avoid many compiler warnings
Overview of Changes in Maude alpha100 (source trees 97, 98, 99 abandoned)
==========================================================================
=========================================================================
* added crude Maude VM based interpreter (sreduce)
Overview of Changes in Maude alpha96c
......
aclocal.m4
View file @ d1e30f73
This diff is collapsed.
config.h.in
View file @ d1e30f73
......@@ -30,6 +30,9 @@
/* Define to 1 if you have the `nsl' library (-lnsl). */
#undef HAVE_LIBNSL
/* Define to 1 if you have the `rt' library (-lrt). */
#undef HAVE_LIBRT
/* Define to 1 if you have the `socket' library (-lsocket). */
#undef HAVE_LIBSOCKET
......@@ -135,6 +138,9 @@
/* Define to 1 if you can safely include both <sys/time.h> and <time.h>. */
#undef TIME_WITH_SYS_TIME
/* use CVC4 SMT solver library */
#undef USE_CVC4
/* use libsigsegv to handle segmentation faults */
#undef USE_LIBSIGSEGV
......
configure
View file @ d1e30f73
This diff is collapsed.
configure.ac
View file @ d1e30f73
......@@ -3,7 +3,7 @@
#
# Initialize autoconf stuff.
#
AC_INIT(Maude, 2.7, [maude-bugs@maude.cs.uiuc.edu])
AC_INIT(Maude, 2.7.1, [maude-bugs@lists.cs.illinois.edu])
#
# Allow directory names that look like macros.
#
......@@ -16,7 +16,7 @@ AC_CANONICAL_HOST
#
# Initialize automake stuff.
#
AM_INIT_AUTOMAKE(Maude, 2.7)
AM_INIT_AUTOMAKE
#
# Cause defines to be put in a header file rather than passed as
# compiler flags.
......@@ -73,6 +73,31 @@ if (test -z "$BUDDY_LIB") then
fi
AC_SUBST(BUDDY_LIB)
#
# Check to see if we should use CVC4 for SMT solving.
#
AC_ARG_WITH(cvc4,
AC_HELP_STRING([--with-cvc4],
[use CVC4 SMT solver library [default=yes]]),
[WITH_CVC4=$withval],
[WITH_CVC4=yes])
if (test $WITH_CVC4 = yes) then
#
# Check if user set a particular CVC4 library to use and if
# not set default.
#
AC_DEFINE([USE_CVC4], [], [use CVC4 SMT solver library])
if (test -z "$CVC4_LIB") then
CVC4_LIB="-lcvc4"
fi
AC_SUBST(CVC4_LIB)
#
# CVC4 needs the clock_gettime() function from the POSIX Realtime Extensions library.
#
AC_CHECK_LIB(rt, clock_gettime)
else
CVC4_LIB=""
fi
#
# Check to see if we should use Tecla for command line editing.
#
AC_ARG_WITH(tecla,
......@@ -357,6 +382,7 @@ AC_CONFIG_FILES([Makefile
src/MSCP10/Makefile
src/StrategyLanguage/Makefile
src/Mixfix/Makefile
src/SMT/Makefile
src/Main/Makefile
tests/Makefile
tests/BuiltIn/Makefile
......
debian/changelog
View file @ d1e30f73
maude (2.7.1-1) UNRELEASED; urgency=medium
* New upstream version
* Fix watch file
* debhelper 11
* Point Vcs fields to salsa.debian.org
* Standards-Version: 4.1.4
* Build-Depends: libcvc4-dev
* Avoid parallel build
-- Andreas Tille <tille@debian.org> Mon, 09 Jul 2018 15:22:41 +0200
maude (2.7-2) unstable; urgency=medium
[ Andreas Tille ]
......
debian/control
View file @ d1e30f73
......@@ -4,18 +4,18 @@ Uploaders: Scott Christley <schristley@mac.com>,
Andreas Tille <tille@debian.org>
Section: science
Priority: optional
Build-Depends: debhelper (>= 9),
autotools-dev,
Build-Depends: debhelper (>= 11~),
libtecla-dev,
libbdd-dev,
libgmp3-dev,
libsigsegv-dev,
bison,
flex (>= 2.5.36),
libncurses5-dev
Standards-Version: 3.9.7
Vcs-Browser: https://anonscm.debian.org/cgit/debian-med/maude.git
Vcs-Git: https://anonscm.debian.org/git/debian-med/maude.git
libncurses5-dev,
libcvc4-dev
Standards-Version: 4.1.4
Vcs-Browser: https://salsa.debian.org/med-team/maude
Vcs-Git: https://salsa.debian.org/med-team/maude.git
Homepage: http://maude.cs.uiuc.edu
Package: maude
......
debian/patches/bison-parse-param.patch
View file @ d1e30f73
......@@ -17,23 +17,3 @@ Description: this is quick and dirty patch to use %parse-param instead
%{
#include <string>
#include <stack>
@@ -91,7 +93,7 @@ SyntaxContainer* oldSyntaxContainer = 0;
Int64 number;
Int64 number2;
-static void yyerror(char *s);
+static void yyerror(void *, char *s);
void cleanUpModuleExpression();
void cleanUpParser();
--- a/src/Mixfix/bottom.yy
+++ b/src/Mixfix/bottom.yy
@@ -23,7 +23,7 @@
%%
static void
-yyerror(char *s)
+yyerror(void *, char *s)
{
if (!(UserLevelRewritingContext::interrupted()))
IssueWarning(LineNumber(lineNumber) << ": " << s);
debian/patches/search-datadir.patch
View file @ d1e30f73
Have maude search in datadir for its files.
--- a/src/Main/main.cc
+++ b/src/Main/main.cc
@@ -269,6 +269,11 @@ findPrelude(string& directory, string& f
@@ -278,6 +278,11 @@ findPrelude(string& directory, string& f
{
if (directoryManager.searchPath(MAUDE_LIB, directory, fileName, R_OK))
return true;
......
debian/patches/strip-build-date.patch
View file @ d1e30f73
......@@ -2,8 +2,8 @@ Description: Strip build date
Strip build date from banner, for reproducibility reasons.
Author: Alexis Bienvenüe <pado@passoire.fr>
--- maude-2.7.orig/src/Mixfix/banner.cc
+++ maude-2.7/src/Mixfix/banner.cc
--- a/src/Mixfix/banner.cc
+++ b/src/Mixfix/banner.cc
@@ -53,8 +53,7 @@ printBanner(std::ostream& s)
Tty(Tty::GREEN) << 'e' <<
Tty(Tty::RESET) << " ---\n";
......@@ -11,6 +11,6 @@ Author: Alexis Bienvenüe <pado@passoire.fr>
- s << "\t " << PACKAGE_STRING << " built: " <<
- __DATE__ << ' ' << __TIME__ << '\n';
+ s << "\t " << PACKAGE_STRING << '\n';
s << "\t Copyright 1997-2014 SRI International\n";
s << "\t Copyright 1997-2016 SRI International\n";
s << "\t\t " << ctime(&secs);
}
debian/rules
View file @ d1e30f73
......@@ -3,7 +3,7 @@
export DH_VERBOSE=1
%:
dh $@ --with autotools_dev
dh $@
override_dh_auto_configure:
dh_auto_configure -- --datadir="/usr/share/maude"
......@@ -12,3 +12,6 @@ override_dh_auto_clean:
dh_auto_clean
rm -f src/Mixfix/surface.output
find tests -name "*.out" -type f -delete
override_dh_auto_build:
dh_auto_build --no-parallel
debian/watch
View file @ d1e30f73
version=4
http://maude.cs.illinois.edu/w/index.php?title=Maude_download_and_installation */Maude-(\d[.\d]+)\.tar\.gz
# Seems we can not replace the '?' by "%3F" successfully :-(
#http://maude.cs.illinois.edu/w/index.php%3Ftitle=Maude_download_and_installation */Maude-(\d[.\d]+)\.tar\.gz
http://maude.cs.illinois.edu/w/index.php?title=Maude_download_and_installation .*/Maude-(\d[.\d]+)\.tar\.gz
src/3rdParty/Makefile.in
View file @ d1e30f73
# Makefile.in generated by automake 1.11.3 from Makefile.am.
# Makefile.in generated by automake 1.14.1 from Makefile.am.
# @configure_input@
# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
# 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011 Free Software
# Foundation, Inc.
# Copyright (C) 1994-2013 Free Software Foundation, Inc.
# This Makefile.in is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
# with or without modifications, as long as this notice is preserved.
......@@ -16,6 +15,51 @@
@SET_MAKE@
VPATH = @srcdir@
am__is_gnu_make = test -n '$(MAKEFILE_LIST)' && test -n '$(MAKELEVEL)'
am__make_running_with_option = \
case $${target_option-} in \
?) ;; \
*) echo "am__make_running_with_option: internal error: invalid" \
"target option '$${target_option-}' specified" >&2; \
exit 1;; \
esac; \
has_opt=no; \
sane_makeflags=$$MAKEFLAGS; \
if $(am__is_gnu_make); then \
sane_makeflags=$$MFLAGS; \
else \
case $$MAKEFLAGS in \
*\\[\ \ ]*) \
bs=\\; \
sane_makeflags=`printf '%s\n' "$$MAKEFLAGS" \
| sed "s/$$bs$$bs[$$bs $$bs ]*//g"`;; \
esac; \
fi; \
skip_next=no; \
strip_trailopt () \
{ \
flg=`printf '%s\n' "$$flg" | sed "s/$$1.*$$//"`; \
}; \
for flg in $$sane_makeflags; do \
test $$skip_next = yes && { skip_next=no; continue; }; \
case $$flg in \
*=*|--*) continue;; \
-*I) strip_trailopt 'I'; skip_next=yes;; \
-*I?*) strip_trailopt 'I';; \
-*O) strip_trailopt 'O'; skip_next=yes;; \
-*O?*) strip_trailopt 'O';; \
-*l) strip_trailopt 'l'; skip_next=yes;; \
-*l?*) strip_trailopt 'l';; \
-[dEDm]) skip_next=yes;; \
-[JT]) skip_next=yes;; \
esac; \
case $$flg in \
*$$target_option*) has_opt=yes; break;; \
esac; \
done; \
test $$has_opt = yes
am__make_dryrun = (target_option=n; $(am__make_running_with_option))
am__make_keepgoing = (target_option=k; $(am__make_running_with_option))
pkgdatadir = $(datadir)/@PACKAGE@
pkgincludedir = $(includedir)/@PACKAGE@
pkglibdir = $(libdir)/@PACKAGE@
......@@ -35,8 +79,8 @@ POST_UNINSTALL = :
build_triplet = @build@
host_triplet = @host@
subdir = src/3rdParty
DIST_COMMON = $(noinst_HEADERS) $(srcdir)/Makefile.am \
$(srcdir)/Makefile.in
DIST_COMMON = $(srcdir)/Makefile.in $(srcdir)/Makefile.am \
$(top_srcdir)/mkinstalldirs $(noinst_HEADERS)
ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
am__aclocal_m4_deps = $(top_srcdir)/configure.ac
am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
......@@ -45,14 +89,49 @@ mkinstalldirs = $(SHELL) $(top_srcdir)/mkinstalldirs
CONFIG_HEADER = $(top_builddir)/config.h
CONFIG_CLEAN_FILES =
CONFIG_CLEAN_VPATH_FILES =
AM_V_P = $(am__v_P_@AM_V@)
am__v_P_ = $(am__v_P_@AM_DEFAULT_V@)
am__v_P_0 = false
am__v_P_1 = :
AM_V_GEN = $(am__v_GEN_@AM_V@)
am__v_GEN_ = $(am__v_GEN_@AM_DEFAULT_V@)
am__v_GEN_0 = @echo " GEN " $@;
am__v_GEN_1 =
AM_V_at = $(am__v_at_@AM_V@)
am__v_at_ = $(am__v_at_@AM_DEFAULT_V@)
am__v_at_0 = @
am__v_at_1 =
SOURCES =
DIST_SOURCES =
am__can_run_installinfo = \
case $$AM_UPDATE_INFO_DIR in \
n|no|NO) false;; \
*) (install-info --version) >/dev/null 2>&1;; \
esac
HEADERS = $(noinst_HEADERS)
am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) $(LISP)
# Read a list of newline-separated strings from the standard input,
# and print each of them once, without duplicates. Input order is
# *not* preserved.
am__uniquify_input = $(AWK) '\
BEGIN { nonempty = 0; } \
{ items[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in items) print i; }; } \
'
# Make sure the list of sources is unique. This is necessary because,
# e.g., the same source file might be shared among _SOURCES variables
# for different programs/libraries.
am__define_uniq_tagged_files = \
list='$(am__tagged_files)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | $(am__uniquify_input)`
ETAGS = etags
CTAGS = ctags
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
ACLOCAL = @ACLOCAL@
AMTAR = @AMTAR@
AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
......@@ -63,6 +142,7 @@ CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
CPPFLAGS = @CPPFLAGS@
CVC4_LIB = @CVC4_LIB@
CXX = @CXX@
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
......@@ -194,26 +274,15 @@ $(ACLOCAL_M4): $(am__aclocal_m4_deps)
cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
$(am__aclocal_m4_deps):
ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
mkid -fID $$unique
tags: TAGS
TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
ID: $(am__tagged_files)
$(am__define_uniq_tagged_files); mkid -fID $$unique
tags: tags-am
TAGS: tags
tags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
set x; \
here=`pwd`; \
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
$(am__define_uniq_tagged_files); \
shift; \
if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
test -n "$$unique" || unique=$$empty_fix; \
......@@ -225,15 +294,11 @@ TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$$unique; \
fi; \
fi
ctags: CTAGS
CTAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
ctags: ctags-am
CTAGS: ctags
ctags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
$(am__define_uniq_tagged_files); \
test -z "$(CTAGS_ARGS)$$unique" \
|| $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
$$unique
......@@ -242,6 +307,21 @@ GTAGS:
here=`$(am__cd) $(top_builddir) && pwd` \
&& $(am__cd) $(top_srcdir) \
&& gtags -i $(GTAGS_ARGS) "$$here"
cscopelist: cscopelist-am
cscopelist-am: $(am__tagged_files)
list='$(am__tagged_files)'; \
case "$(srcdir)" in \
[\\/]* | ?:[\\/]*) sdir="$(srcdir)" ;; \
*) sdir=$(subdir)/$(srcdir) ;; \
esac; \
for i in $$list; do \
if test -f "$$i"; then \
echo "$(subdir)/$$i"; \
else \
echo "$$sdir/$$i"; \
fi; \
done >> $(top_builddir)/cscope.files
distclean-tags:
-rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
......@@ -378,16 +458,17 @@ uninstall-am:
.MAKE: install-am install-strip
.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \
ctags distclean distclean-generic distclean-tags distdir dvi \
dvi-am html html-am info info-am install install-am \
install-data install-data-am install-dvi install-dvi-am \
install-exec install-exec-am install-html install-html-am \
install-info install-info-am install-man install-pdf \
install-pdf-am install-ps install-ps-am install-strip \
installcheck installcheck-am installdirs maintainer-clean \
maintainer-clean-generic mostlyclean mostlyclean-generic pdf \
pdf-am ps ps-am tags uninstall uninstall-am
.PHONY: CTAGS GTAGS TAGS all all-am check check-am clean clean-generic \
cscopelist-am ctags ctags-am distclean distclean-generic \
distclean-tags distdir dvi dvi-am html html-am info info-am \
install install-am install-data install-data-am install-dvi \
install-dvi-am install-exec install-exec-am install-html \
install-html-am install-info install-info-am install-man \
install-pdf install-pdf-am install-ps install-ps-am \
install-strip installcheck installcheck-am installdirs \
maintainer-clean maintainer-clean-generic mostlyclean \
mostlyclean-generic pdf pdf-am ps ps-am tags tags-am uninstall \
uninstall-am
# Tell versions [3.59,3.63) of GNU make to not export all variables.
......
src/ACU_Persistent/Makefile.in
View file @ d1e30f73
# Makefile.in generated by automake 1.11.3 from Makefile.am.
# Makefile.in generated by automake 1.14.1 from Makefile.am.
# @configure_input@
# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
# 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011 Free Software
# Foundation, Inc.
# Copyright (C) 1994-2013 Free Software Foundation, Inc.
# This Makefile.in is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
# with or without modifications, as long as this notice is preserved.
......@@ -17,6 +16,51 @@
VPATH = @srcdir@
am__is_gnu_make = test -n '$(MAKEFILE_LIST)' && test -n '$(MAKELEVEL)'
am__make_running_with_option = \
case $${target_option-} in \
?) ;; \
*) echo "am__make_running_with_option: internal error: invalid" \
"target option '$${target_option-}' specified" >&2; \
exit 1;; \
esac; \
has_opt=no; \
sane_makeflags=$$MAKEFLAGS; \
if $(am__is_gnu_make); then \
sane_makeflags=$$MFLAGS; \
else \
case $$MAKEFLAGS in \
*\\[\ \ ]*) \
bs=\\; \
sane_makeflags=`printf '%s\n' "$$MAKEFLAGS" \
| sed "s/$$bs$$bs[$$bs $$bs ]*//g"`;; \
esac; \
fi; \
skip_next=no; \
strip_trailopt () \
{ \
flg=`printf '%s\n' "$$flg" | sed "s/$$1.*$$//"`; \
}; \
for flg in $$sane_makeflags; do \
test $$skip_next = yes && { skip_next=no; continue; }; \
case $$flg in \
*=*|--*) continue;; \
-*I) strip_trailopt 'I'; skip_next=yes;; \
-*I?*) strip_trailopt 'I';; \
-*O) strip_trailopt 'O'; skip_next=yes;; \
-*O?*) strip_trailopt 'O';; \
-*l) strip_trailopt 'l'; skip_next=yes;; \
-*l?*) strip_trailopt 'l';; \
-[dEDm]) skip_next=yes;; \
-[JT]) skip_next=yes;; \
esac; \
case $$flg in \
*$$target_option*) has_opt=yes; break;; \
esac; \
done; \
test $$has_opt = yes
am__make_dryrun = (target_option=n; $(am__make_running_with_option))
am__make_keepgoing = (target_option=k; $(am__make_running_with_option))
pkgdatadir = $(datadir)/@PACKAGE@
pkgincludedir = $(includedir)/@PACKAGE@
pkglibdir = $(libdir)/@PACKAGE@
......@@ -36,8 +80,9 @@ POST_UNINSTALL = :
build_triplet = @build@
host_triplet = @host@
subdir = src/ACU_Persistent
DIST_COMMON = $(noinst_HEADERS) $(srcdir)/Makefile.am \
$(srcdir)/Makefile.in ChangeLog
DIST_COMMON = $(srcdir)/Makefile.in $(srcdir)/Makefile.am \
$(top_srcdir)/mkinstalldirs $(top_srcdir)/depcomp \
$(noinst_HEADERS) ChangeLog
ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
am__aclocal_m4_deps = $(top_srcdir)/configure.ac
am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
......@@ -49,29 +94,80 @@ CONFIG_CLEAN_VPATH_FILES =
LIBRARIES = $(noinst_LIBRARIES)
AR = ar
ARFLAGS = cru
AM_V_AR = $(am__v_AR_@AM_V@)
am__v_AR_ = $(am__v_AR_@AM_DEFAULT_V@)
am__v_AR_0 = @echo " AR " $@;
am__v_AR_1 =
libACU_Persistent_a_AR = $(AR) $(ARFLAGS)
libACU_Persistent_a_LIBADD =
am_libACU_Persistent_a_OBJECTS = \
libACU_Persistent_a-ACU_RedBlackNode.$(OBJEXT) \
libACU_Persistent_a-ACU_Tree.$(OBJEXT)
libACU_Persistent_a_OBJECTS = $(am_libACU_Persistent_a_OBJECTS)
AM_V_P = $(am__v_P_@AM_V@)
am__v_P_ = $(am__v_P_@AM_DEFAULT_V@)
am__v_P_0 = false
am__v_P_1 = :
AM_V_GEN = $(am__v_GEN_@AM_V@)
am__v_GEN_ = $(am__v_GEN_@AM_DEFAULT_V@)
am__v_GEN_0 = @echo " GEN " $@;
am__v_GEN_1 =
AM_V_at = $(am__v_at_@AM_V@)
am__v_at_ = $(am__v_at_@AM_DEFAULT_V@)
am__v_at_0 = @
am__v_at_1 =
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/depcomp
am__depfiles_maybe = depfiles
am__mv = mv -f
AM_V_lt = $(am__v_lt_@AM_V@)
am__v_lt_ = $(am__v_lt_@AM_DEFAULT_V@)
am__v_lt_0 = --silent
am__v_lt_1 =
CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
AM_V_CXX = $(am__v_CXX_@AM_V@)
am__v_CXX_ = $(am__v_CXX_@AM_DEFAULT_V@)
am__v_CXX_0 = @echo " CXX " $@;
am__v_CXX_1 =
CXXLD = $(CXX)
CXXLINK = $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) $(LDFLAGS) \
-o $@
AM_V_CXXLD = $(am__v_CXXLD_@AM_V@)
am__v_CXXLD_ = $(am__v_CXXLD_@AM_DEFAULT_V@)
am__v_CXXLD_0 = @echo " CXXLD " $@;
am__v_CXXLD_1 =
SOURCES = $(libACU_Persistent_a_SOURCES)
DIST_SOURCES = $(libACU_Persistent_a_SOURCES)
am__can_run_installinfo = \
case $$AM_UPDATE_INFO_DIR in \
n|no|NO) false;; \
*) (install-info --version) >/dev/null 2>&1;; \
esac
HEADERS = $(noinst_HEADERS)
am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) $(LISP)
# Read a list of newline-separated strings from the standard input,
# and print each of them once, without duplicates. Input order is
# *not* preserved.
am__uniquify_input = $(AWK) '\
BEGIN { nonempty = 0; } \
{ items[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in items) print i; }; } \
'
# Make sure the list of sources is unique. This is necessary because,
# e.g., the same source file might be shared among _SOURCES variables
# for different programs/libraries.
am__define_uniq_tagged_files = \
list='$(am__tagged_files)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | $(am__uniquify_input)`
ETAGS = etags
CTAGS = ctags
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
ACLOCAL = @ACLOCAL@
AMTAR = @AMTAR@
AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
......@@ -82,6 +178,7 @@ CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
CPPFLAGS = @CPPFLAGS@
CVC4_LIB = @CVC4_LIB@
CXX = @CXX@
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
......@@ -242,10 +339,11 @@ $(am__aclocal_m4_deps):
clean-noinstLIBRARIES:
-test -z "$(noinst_LIBRARIES)" || rm -f $(noinst_LIBRARIES)
libACU_Persistent.a: $(libACU_Persistent_a_OBJECTS) $(libACU_Persistent_a_DEPENDENCIES) $(EXTRA_libACU_Persistent_a_DEPENDENCIES)
-rm -f libACU_Persistent.a
$(libACU_Persistent_a_AR) libACU_Persistent.a $(libACU_Persistent_a_OBJECTS) $(libACU_Persistent_a_LIBADD)
$(RANLIB) libACU_Persistent.a
$(AM_V_at)-rm -f libACU_Persistent.a
$(AM_V_AR)$(libACU_Persistent_a_AR) libACU_Persistent.a $(libACU_Persistent_a_OBJECTS) $(libACU_Persistent_a_LIBADD)
$(AM_V_at)$(RANLIB) libACU_Persistent.a
mostlyclean-compile:
-rm -f *.$(OBJEXT)
......@@ -257,67 +355,56 @@ distclean-compile:
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/libACU_Persistent_a-ACU_Tree.Po@am__quote@
.cc.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $<
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXXCOMPILE) -c -o $@ $<
.cc.obj:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'`
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'`
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
libACU_Persistent_a-ACU_RedBlackNode.o: ACU_RedBlackNode.cc
@am__fastdepCXX_TRUE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_RedBlackNode.o -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo -c -o libACU_Persistent_a-ACU_RedBlackNode.o `test -f 'ACU_RedBlackNode.cc' || echo '$(srcdir)/'`ACU_RedBlackNode.cc
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='ACU_RedBlackNode.cc' object='libACU_Persistent_a-ACU_RedBlackNode.o' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_RedBlackNode.o -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo -c -o libACU_Persistent_a-ACU_RedBlackNode.o `test -f 'ACU_RedBlackNode.cc' || echo '$(srcdir)/'`ACU_RedBlackNode.cc
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='ACU_RedBlackNode.cc' object='libACU_Persistent_a-ACU_RedBlackNode.o' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_RedBlackNode.o `test -f 'ACU_RedBlackNode.cc' || echo '$(srcdir)/'`ACU_RedBlackNode.cc
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_RedBlackNode.o `test -f 'ACU_RedBlackNode.cc' || echo '$(srcdir)/'`ACU_RedBlackNode.cc
libACU_Persistent_a-ACU_RedBlackNode.obj: ACU_RedBlackNode.cc
@am__fastdepCXX_TRUE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_RedBlackNode.obj -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo -c -o libACU_Persistent_a-ACU_RedBlackNode.obj `if test -f 'ACU_RedBlackNode.cc'; then $(CYGPATH_W) 'ACU_RedBlackNode.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_RedBlackNode.cc'; fi`
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='ACU_RedBlackNode.cc' object='libACU_Persistent_a-ACU_RedBlackNode.obj' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_RedBlackNode.obj -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo -c -o libACU_Persistent_a-ACU_RedBlackNode.obj `if test -f 'ACU_RedBlackNode.cc'; then $(CYGPATH_W) 'ACU_RedBlackNode.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_RedBlackNode.cc'; fi`
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_RedBlackNode.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='ACU_RedBlackNode.cc' object='libACU_Persistent_a-ACU_RedBlackNode.obj' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_RedBlackNode.obj `if test -f 'ACU_RedBlackNode.cc'; then $(CYGPATH_W) 'ACU_RedBlackNode.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_RedBlackNode.cc'; fi`
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_RedBlackNode.obj `if test -f 'ACU_RedBlackNode.cc'; then $(CYGPATH_W) 'ACU_RedBlackNode.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_RedBlackNode.cc'; fi`
libACU_Persistent_a-ACU_Tree.o: ACU_Tree.cc
@am__fastdepCXX_TRUE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_Tree.o -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo -c -o libACU_Persistent_a-ACU_Tree.o `test -f 'ACU_Tree.cc' || echo '$(srcdir)/'`ACU_Tree.cc
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='ACU_Tree.cc' object='libACU_Persistent_a-ACU_Tree.o' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_Tree.o -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo -c -o libACU_Persistent_a-ACU_Tree.o `test -f 'ACU_Tree.cc' || echo '$(srcdir)/'`ACU_Tree.cc
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='ACU_Tree.cc' object='libACU_Persistent_a-ACU_Tree.o' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_Tree.o `test -f 'ACU_Tree.cc' || echo '$(srcdir)/'`ACU_Tree.cc
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_Tree.o `test -f 'ACU_Tree.cc' || echo '$(srcdir)/'`ACU_Tree.cc
libACU_Persistent_a-ACU_Tree.obj: ACU_Tree.cc
@am__fastdepCXX_TRUE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_Tree.obj -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo -c -o libACU_Persistent_a-ACU_Tree.obj `if test -f 'ACU_Tree.cc'; then $(CYGPATH_W) 'ACU_Tree.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_Tree.cc'; fi`
@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='ACU_Tree.cc' object='libACU_Persistent_a-ACU_Tree.obj' libtool=no @AMDEPBACKSLASH@
@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT libACU_Persistent_a-ACU_Tree.obj -MD -MP -MF $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo -c -o libACU_Persistent_a-ACU_Tree.obj `if test -f 'ACU_Tree.cc'; then $(CYGPATH_W) 'ACU_Tree.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_Tree.cc'; fi`
@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Tpo $(DEPDIR)/libACU_Persistent_a-ACU_Tree.Po
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ $(AM_V_CXX)source='ACU_Tree.cc' object='libACU_Persistent_a-ACU_Tree.obj' libtool=no @AMDEPBACKSLASH@
@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
@am__fastdepCXX_FALSE@ $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_Tree.obj `if test -f 'ACU_Tree.cc'; then $(CYGPATH_W) 'ACU_Tree.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_Tree.cc'; fi`
@am__fastdepCXX_FALSE@ $(AM_V_CXX@am__nodep@)$(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(libACU_Persistent_a_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o libACU_Persistent_a-ACU_Tree.obj `if test -f 'ACU_Tree.cc'; then $(CYGPATH_W) 'ACU_Tree.cc'; else $(CYGPATH_W) '$(srcdir)/ACU_Tree.cc'; fi`
ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
mkid -fID $$unique
tags: TAGS
TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
ID: $(am__tagged_files)
$(am__define_uniq_tagged_files); mkid -fID $$unique
tags: tags-am
TAGS: tags
tags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
set x; \
here=`pwd`; \
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
$(am__define_uniq_tagged_files); \
shift; \
if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
test -n "$$unique" || unique=$$empty_fix; \
......@@ -329,15 +416,11 @@ TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$$unique; \
fi; \
fi
ctags: CTAGS
CTAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
$(TAGS_FILES) $(LISP)
list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
unique=`for i in $$list; do \
if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
done | \
$(AWK) '{ files[$$0] = 1; nonempty = 1; } \
END { if (nonempty) { for (i in files) print i; }; }'`; \
ctags: ctags-am
CTAGS: ctags
ctags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files)
$(am__define_uniq_tagged_files); \
test -z "$(CTAGS_ARGS)$$unique" \
|| $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
$$unique
......@@ -346,6 +429,21 @@ GTAGS:
here=`$(am__cd) $(top_builddir) && pwd` \
&& $(am__cd) $(top_srcdir) \
&& gtags -i $(GTAGS_ARGS) "$$here"
cscopelist: cscopelist-am
cscopelist-am: $(am__tagged_files)
list='$(am__tagged_files)'; \
case "$(srcdir)" in \
[\\/]* | ?:[\\/]*) sdir="$(srcdir)" ;; \
*) sdir=$(subdir)/$(srcdir) ;; \
esac; \
for i in $$list; do \
if test -f "$$i"; then \
echo "$(subdir)/$$i"; \
else \
echo "$$sdir/$$i"; \
fi; \
done >> $(top_builddir)/cscope.files
distclean-tags:
-rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
......@@ -485,17 +583,17 @@ uninstall-am:
.MAKE: install-am install-strip
.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \
clean-noinstLIBRARIES ctags distclean distclean-compile \
distclean-generic distclean-tags distdir dvi dvi-am html \
html-am info info-am install install-am install-data \
install-data-am install-dvi install-dvi-am install-exec \
install-exec-am install-html install-html-am install-info \
install-info-am install-man install-pdf install-pdf-am \
install-ps install-ps-am install-strip installcheck \
installcheck-am installdirs maintainer-clean \
.PHONY: CTAGS GTAGS TAGS all all-am check check-am clean clean-generic \
clean-noinstLIBRARIES cscopelist-am ctags ctags-am distclean \
distclean-compile distclean-generic distclean-tags distdir dvi \
dvi-am html html-am info info-am install install-am \
install-data install-data-am install-dvi install-dvi-am \
install-exec install-exec-am install-html install-html-am \
install-info install-info-am install-man install-pdf \
install-pdf-am install-ps install-ps-am install-strip \
installcheck installcheck-am installdirs maintainer-clean \
maintainer-clean-generic mostlyclean mostlyclean-compile \
mostlyclean-generic pdf pdf-am ps ps-am tags uninstall \
mostlyclean-generic pdf pdf-am ps ps-am tags tags-am uninstall \
uninstall-am
......
src/ACU_Theory/ACU_DagNode.cc 100644 → 100755
View file @ d1e30f73
......@@ -501,6 +501,7 @@ ACU_DagNode::computeBaseSortForGroundSubterms()
if (ground)
{
s->computeBaseSort(this);
setGround();
return GROUND;
}
return NONGROUND;
......
src/ACU_Theory/ACU_Symbol.cc 100644 → 100755
View file @ d1e30f73
......@@ -461,6 +461,89 @@ ACU_Symbol::computeGeneralizedSort(const SortBdds& sortBdds,
bdd_freepair(argMap);
}
// experimental code
void
ACU_Symbol::computeGeneralizedSort2(const SortBdds& sortBdds,
const Vector<int>& realToBdd,
DagNode* subject,
Vector<Bdd>& outputBdds)
{
Assert(safeCast(ACU_BaseDagNode*, subject)->isTree() == false,
"Tree case not implemented: " << subject <<
" " << static_cast<void*>(dynamic_cast<ACU_DagNode*>(subject)) <<
" " << static_cast<void*>(dynamic_cast<ACU_TreeDagNode*>(subject)));
ArgVec<ACU_Pair>& args = safeCast(ACU_DagNode*, subject)->argArray;
int lastArg = args.length() - 1;
Vector<Bdd> inputBdds;
Vector<Bdd> middleBdds;
for (int i = 0;; ++i)
{
//
// Generalized sort ith argument.
//
args[i].dagNode->computeGeneralizedSort2(sortBdds, realToBdd, inputBdds);
int multiplicity = args[i].multiplicity;
if (i == 0)
{
--multiplicity;
if (multiplicity == 0)
continue; // must be a next argument
//
// Special case - first argument has multiplicity > 1 so we
// need to clone its sort BDDs.
//
int nrBdds = inputBdds.size();
//
// Need to be careful since we are reading and writing the same Vector
// and a reference can be come stale if the Vector reallocates.
// So we force the reallocation, if needed, up front.
//
inputBdds.resize(2 * nrBdds);
for (int j = 0; j < nrBdds; ++j)
inputBdds[nrBdds + j] = inputBdds[j];
}
for (--multiplicity; multiplicity != 0; --multiplicity)
{
middleBdds.clear();
sortBdds.operatorCompose(this, inputBdds, middleBdds);
//
// Copy middleBdds over first half of inputBdds.
//
Vector<Bdd>::iterator input = inputBdds.begin();
FOR_EACH_CONST(j, Vector<Bdd>, middleBdds)
{
*input = *j;
++input;
}
}
if (i == lastArg)
{
//
// Final application of our sort function with result
// directly appended to outputBdds.
//
sortBdds.operatorCompose(this, inputBdds, outputBdds);
break;
}
else
{
//
// Middle case - write result to middleBdds.
//
middleBdds.clear();
sortBdds.operatorCompose(this, inputBdds, middleBdds);
//
// middleBdds become first part of inputBdds.
//
inputBdds.swap(middleBdds);
}
}
}
bool
ACU_Symbol::canResolveTheoryClash()
{
......@@ -480,10 +563,9 @@ ACU_Symbol::makeUnificationSubproblem()
int
ACU_Symbol::unificationPriority() const
{
return 10;
return 10 + 10 * (getIdentity() != 0);
}
//
// Hash cons code.
//
......