From: Aina Niemetz Date: Fri, 25 Aug 2017 22:39:16 +0000 (-0700) Subject: Move LFSC checker out of the CVC repository. (#222) X-Git-Tag: cvc5-1.0.0~5664 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0;p=cvc5.git Move LFSC checker out of the CVC repository. (#222) LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball). --- diff --git a/.travis.yml b/.travis.yml index 65b9dcd25..59cc22e0e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,13 +17,11 @@ env: - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ=" - TEST_GROUPS=2 matrix: - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio' - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=0 - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=1 + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --with-lfsc --with-portfolio' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --with-lfsc --with-portfolio' TEST_GROUP=0 + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --with-lfsc --with-portfolio' TEST_GROUP=1 - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof' - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof' - - TRAVIS_LFSC=yes - - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes addons: apt: sources: @@ -89,30 +87,21 @@ script: contrib/new-theory --alternate test_newtheory test_newalttheory || error "NEWTHEORY-ALTERNATE FAILED"; grep -q '^THEORIES *=.* test_newalttheory' src/Makefile.theories || error "NEWTHEORY-ALTERNATE FAILED"; } - LFSCchecks() { - cd proofs/lfsc_checker && - (./configure || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) && - if [ -n "$TRAVIS_LFSC_DISTCHECK" ]; then - make -j2 distcheck || (echo; echo "${red}LFSC DISTCHECK FAILED${normal}"; echo; exit 1); - else - make -j2 || (echo; echo "${red}LFSC BUILD FAILED${normal}"; echo; exit 1); - fi; - } run() { echo "travis_fold:start:$1" echo "Running $1" $1 || exit 1 echo "travis_fold:end:$1" } + [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run addNewTheoryTest [ -n "$TRAVIS_CVC4" ] && run configureCVC4 [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run makeDistcheck [ -n "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_CVC4_DISTCHECK" ] && run makeCheck && run makeExamples [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_CHECK_PORTFOLIO" ] && run makeCheckPortfolio [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_JAVA_API_TEST" ] && run JavaApiTest - [ -n "$TRAVIS_LFSC" ] && run LFSCchecks [ -n "$TRAVIS_COVERITY" ] && echo "Running coverity. Skipping the normal build." - [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && [ -z "$TRAVIS_COVERITY" ] && error "Unknown Travis-CI configuration" + [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_COVERITY" ] && error "Unknown Travis-CI configuration" echo "travis_fold:end:load_script" - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}" matrix: diff --git a/Makefile.am b/Makefile.am index bface9536..e975455ec 100644 --- a/Makefile.am +++ b/Makefile.am @@ -7,11 +7,12 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS_BASE = src test contrib if CVC4_PROOF - SUBDIRS = proofs/signatures proofs/lfsc_checker $(SUBDIRS_BASE) + SUBDIRS = proofs/signatures $(SUBDIRS_BASE) else SUBDIRS = $(SUBDIRS_BASE) endif -DIST_SUBDIRS = proofs/signatures proofs/lfsc_checker $(SUBDIRS_BASE) examples +DIST_SUBDIRS = $(SUBDIRS) examples + .PHONY: examples examples: all diff --git a/config/lfsc.m4 b/config/lfsc.m4 new file mode 100644 index 000000000..eabc71564 --- /dev/null +++ b/config/lfsc.m4 @@ -0,0 +1,85 @@ +# CVC4_CHECK_FOR_LFSC +# ------------------ +# Look for LFSC and link it in, but only if user requested. +AC_DEFUN([CVC4_CHECK_FOR_LFSC], [ +AC_MSG_CHECKING([whether user requested LFSC support]) + +have_liblfsc=0 +LFSC_LIBS= +LFSC_LDFLAGS= + +have_liblfsc=0 +if test "$with_lfsc" = no; then + AC_MSG_RESULT([no, LFSC disabled by user]) +elif test -n "$with_lfsc"; then + AC_MSG_RESULT([yes, LFSC requested by user]) + AC_ARG_VAR(LFSC_HOME, [path to top level of LFSC source tree]) + AC_ARG_WITH( + [lfsc-dir], + AS_HELP_STRING( + [--with-lfsc-dir=PATH], + [path to top level of lfsc source tree] + ), + [LFSC_HOME="$withval"], + [] + ) + + if test -z "$LFSC_HOME" -a -e "$ac_abs_confdir/lfsc-checker"; then + AC_MSG_CHECKING([for LFSC checker library]) + LFSC_HOME="$ac_abs_confdir/lfsc-checker/install" + AC_MSG_RESULT([found LFSC checker in $LFSC_HOME]) + fi + + if test -z "$LFSC_HOME"; then + AC_MSG_FAILURE([must give --with-lfsc-dir=PATH or define environment variable LFSC_HOME!]) + fi + + if ! test -d "$LFSC_HOME" || ! test -x "$LFSC_HOME/bin/lfscc" ; then + AC_MSG_FAILURE([either $LFSC_HOME is not a LFSC install tree or it's not yet built]) + fi + + CPPFLAGS="$CPPFLAGS -I$LFSC_HOME/include" + + AC_MSG_CHECKING([how to link LFSC]) + CVC4_TRY_LFSC_LIB + + if test -z "$LFSC_LIBS"; then + AC_MSG_FAILURE([cannot link against liblfscc!]) + else + AC_MSG_RESULT([$LFSC_LIBS]) + have_liblfsc=1 + fi + + LFSC_LDFLAGS="-L$LFSC_HOME/lib" + +else + AC_MSG_RESULT([no, user didn't request LFSC]) + with_lfsc=no +fi + +])# CVC4_CHECK_FOR_LFSC + +# CVC4_TRY_LFSC_LIB +# ------------------------------ +# Try AC_CHECK_LIB(lfsc) with the given linking libraries +AC_DEFUN([CVC4_TRY_LFSC_LIB], [ + AC_LANG_PUSH([C++]) + + cvc4_save_LIBS="$LIBS" + cvc4_save_LDFLAGS="$LDFLAGS" + cvc4_save_CPPFLAGS="$CPPFLAGS" + + LDFLAGS="-L$LFSC_HOME/lib" + LIBS="-llfscc -lgmp" + + AC_LINK_IFELSE( + [AC_LANG_PROGRAM([[#include ]], [[lfscc_init()]])], + [LFSC_LIBS="-llfscc -lgmp"], + [LFSC_LIBS=]) + + LDFLAGS="$cvc4_save_LDFLAGS" + CPPFLAGS="$cvc4_save_CPPFLAGS" + LIBS="$cvc4_save_LIBS" + + AC_LANG_POP([C++]) +])# CVC4_TRY_LFSC_LIB diff --git a/configure.ac b/configure.ac index 55bd91c9d..1c0240f36 100644 --- a/configure.ac +++ b/configure.ac @@ -16,7 +16,6 @@ AC_CONFIG_SRCDIR([src/include/cvc4_public.h]) AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) AC_CONFIG_LIBOBJ_DIR([src/lib]) -AC_CONFIG_SUBDIRS([proofs/lfsc_checker]) m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) @@ -117,7 +116,22 @@ AC_ARG_WITH([build], if test -z "${with_build+set}"; then with_build=production fi -if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}" -a -z "${with_cryptominisat+set}"; then +if test -z "${enable_optimized+set}" -a \ + -z "${enable_debug_symbols+set}" -a \ + -z "${enable_assertions+set}" -a \ + -z "${enable_tracing+set}" -a \ + -z "${enable_dumping+set}" -a \ + -z "${enable_muzzle+set}" -a \ + -z "${enable_coverage+set}" -a \ + -z "${enable_profiling+set}" -a \ + -z "${enable_statistics+set}" -a \ + -z "${enable_replay+set}" -a \ + -z "${with_gmp+set}" -a \ + -z "${with_cln+set}" -a \ + -z "${with_glpk+set}" -a \ + -z "${with_abc+set}" -a \ + -z "${with_cryptominisat+set}" -a \ + -z "${with_lfsc+set}"; then custom_build_profile=no else custom_build_profile=yes @@ -226,6 +240,12 @@ if test -n "${with_cryptominisat+set}"; then btargs="$btargs cryptominisat" fi fi +if test -n "${with_lfsc+set}"; then + if test "$with_lfsc" = yes; then + enable_proof=yes + btargs="$btargs lfsc" + fi +fi AC_MSG_RESULT([$with_build]) @@ -828,6 +848,18 @@ AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1]) AC_SUBST([CRYPTOMINISAT_LDFLAGS]) AC_SUBST([CRYPTOMINISAT_LIBS]) +# Build with LFSC +AC_ARG_WITH([lfsc], + [AS_HELP_STRING([--with-lfsc], + [use the LFSC proof checker])], [], [with_lfsc=]) +CVC4_CHECK_FOR_LFSC +if test $have_liblfsc -eq 1; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC" +fi +AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1]) +AC_SUBST([LFSC_LDFLAGS]) +AC_SUBST([LFSC_LIBS]) + # Check to see if this version/architecture of GNU C++ explicitly # instantiates std::hash or not. Some do, some don't. @@ -935,7 +967,8 @@ AC_ARG_WITH([cxxtest-dir], TESTS_ENVIRONMENT= RUN_REGRESSION_ARGS= -if test "$enable_proof" = yes; then +# FIXME currently, unsat core regressions are disabled without LFSC +if test "$with_lfsc" = yes; then RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof" fi AC_SUBST([TESTS_ENVIRONMENT]) diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker new file mode 100755 index 000000000..495082387 --- /dev/null +++ b/contrib/get-lfsc-checker @@ -0,0 +1,51 @@ +#!/bin/bash +# +set -e + +lfscrepo="https://github.com/CVC4/LFSC.git" +dirname="lfsc-checker" + + +cd "$(dirname "$0")/.." + +if ! [ -e src/parser/cvc/Cvc.g ]; then + echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +function gitclone { + if which git &> /dev/null + then + git clone "$1" "$2" + else + echo "Need git to clone LFSC checker. Please install git." >&2 + exit 1 + fi +} + +if [ -e lfsc-checker ]; then + echo 'error: file or directory "lfsc-checker" already exists!' >&2 + exit 1 +fi + +mkdir $dirname +cd $dirname + +LFSC_PATH=`pwd` + +gitclone $lfscrepo . +mkdir install +mkdir build +cd build +cmake -DCMAKE_INSTALL_PREFIX:PATH=$LFSC_PATH/install .. +make install +cd .. + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure --with-lfsc diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore deleted file mode 100644 index 0712efe67..000000000 --- a/proofs/lfsc_checker/.gitignore +++ /dev/null @@ -1,15 +0,0 @@ -/autom4te.cache -/stamp-h -/config.h.in -/config.log -/config.status -/config.cache -/libtool -/stamp-h1 -.dep -Makefile.in -/configure -/aclocal.m4 -*~ -\#*\# -*.swp diff --git a/proofs/lfsc_checker/AUTHORS b/proofs/lfsc_checker/AUTHORS deleted file mode 100644 index 0bd0a37b0..000000000 --- a/proofs/lfsc_checker/AUTHORS +++ /dev/null @@ -1,5 +0,0 @@ -The core authors and designers of the LFSC proof checker are: - - Andy Reynolds - Aaron Stump - diff --git a/proofs/lfsc_checker/COPYING b/proofs/lfsc_checker/COPYING deleted file mode 100644 index b220a3147..000000000 --- a/proofs/lfsc_checker/COPYING +++ /dev/null @@ -1,17 +0,0 @@ -LFSC is copyright (C) 2012, 2013 The University of Iowa. -All rights reserved. - -LFSC is open-source; distribution is under the terms of the modified -BSD license. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS 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 -OWNERS 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. diff --git a/proofs/lfsc_checker/INSTALL b/proofs/lfsc_checker/INSTALL deleted file mode 100644 index a1e89e18a..000000000 --- a/proofs/lfsc_checker/INSTALL +++ /dev/null @@ -1,370 +0,0 @@ -Installation Instructions -************************* - -Copyright (C) 1994-1996, 1999-2002, 2004-2011 Free Software Foundation, -Inc. - - Copying and distribution of this file, with or without modification, -are permitted in any medium without royalty provided the copyright -notice and this notice are preserved. This file is offered as-is, -without warranty of any kind. - -Basic Installation -================== - - Briefly, the shell commands `./configure; make; make install' should -configure, build, and install this package. The following -more-detailed instructions are generic; see the `README' file for -instructions specific to this package. Some packages provide this -`INSTALL' file but do not implement all of the features documented -below. The lack of an optional feature in a given package is not -necessarily a bug. More recommendations for GNU packages can be found -in *note Makefile Conventions: (standards)Makefile Conventions. - - The `configure' shell script attempts to guess correct values for -various system-dependent variables used during compilation. It uses -those values to create a `Makefile' in each directory of the package. -It may also create one or more `.h' files containing system-dependent -definitions. Finally, it creates a shell script `config.status' that -you can run in the future to recreate the current configuration, and a -file `config.log' containing compiler output (useful mainly for -debugging `configure'). - - It can also use an optional file (typically called `config.cache' -and enabled with `--cache-file=config.cache' or simply `-C') that saves -the results of its tests to speed up reconfiguring. Caching is -disabled by default to prevent problems with accidental use of stale -cache files. - - If you need to do unusual things to compile the package, please try -to figure out how `configure' could check whether to do them, and mail -diffs or instructions to the address given in the `README' so they can -be considered for the next release. If you are using the cache, and at -some point `config.cache' contains results you don't want to keep, you -may remove or edit it. - - The file `configure.ac' (or `configure.in') is used to create -`configure' by a program called `autoconf'. You need `configure.ac' if -you want to change it or regenerate `configure' using a newer version -of `autoconf'. - - The simplest way to compile this package is: - - 1. `cd' to the directory containing the package's source code and type - `./configure' to configure the package for your system. - - Running `configure' might take a while. While running, it prints - some messages telling which features it is checking for. - - 2. Type `make' to compile the package. - - 3. Optionally, type `make check' to run any self-tests that come with - the package, generally using the just-built uninstalled binaries. - - 4. Type `make install' to install the programs and any data files and - documentation. When installing into a prefix owned by root, it is - recommended that the package be configured and built as a regular - user, and only the `make install' phase executed with root - privileges. - - 5. Optionally, type `make installcheck' to repeat any self-tests, but - this time using the binaries in their final installed location. - This target does not install anything. Running this target as a - regular user, particularly if the prior `make install' required - root privileges, verifies that the installation completed - correctly. - - 6. You can remove the program binaries and object files from the - source code directory by typing `make clean'. To also remove the - files that `configure' created (so you can compile the package for - a different kind of computer), type `make distclean'. There is - also a `make maintainer-clean' target, but that is intended mainly - for the package's developers. If you use it, you may have to get - all sorts of other programs in order to regenerate files that came - with the distribution. - - 7. Often, you can also type `make uninstall' to remove the installed - files again. In practice, not all packages have tested that - uninstallation works correctly, even though it is required by the - GNU Coding Standards. - - 8. Some packages, particularly those that use Automake, provide `make - distcheck', which can by used by developers to test that all other - targets like `make install' and `make uninstall' work correctly. - This target is generally not run by end users. - -Compilers and Options -===================== - - Some systems require unusual options for compilation or linking that -the `configure' script does not know about. Run `./configure --help' -for details on some of the pertinent environment variables. - - You can give `configure' initial values for configuration parameters -by setting variables in the command line or in the environment. Here -is an example: - - ./configure CC=c99 CFLAGS=-g LIBS=-lposix - - *Note Defining Variables::, for more details. - -Compiling For Multiple Architectures -==================================== - - You can compile the package for more than one kind of computer at the -same time, by placing the object files for each architecture in their -own directory. To do this, you can use GNU `make'. `cd' to the -directory where you want the object files and executables to go and run -the `configure' script. `configure' automatically checks for the -source code in the directory that `configure' is in and in `..'. This -is known as a "VPATH" build. - - With a non-GNU `make', it is safer to compile the package for one -architecture at a time in the source code directory. After you have -installed the package for one architecture, use `make distclean' before -reconfiguring for another architecture. - - On MacOS X 10.5 and later systems, you can create libraries and -executables that work on multiple system types--known as "fat" or -"universal" binaries--by specifying multiple `-arch' options to the -compiler but only a single `-arch' option to the preprocessor. Like -this: - - ./configure CC="gcc -arch i386 -arch x86_64 -arch ppc -arch ppc64" \ - CXX="g++ -arch i386 -arch x86_64 -arch ppc -arch ppc64" \ - CPP="gcc -E" CXXCPP="g++ -E" - - This is not guaranteed to produce working output in all cases, you -may have to build one architecture at a time and combine the results -using the `lipo' tool if you have problems. - -Installation Names -================== - - By default, `make install' installs the package's commands under -`/usr/local/bin', include files under `/usr/local/include', etc. You -can specify an installation prefix other than `/usr/local' by giving -`configure' the option `--prefix=PREFIX', where PREFIX must be an -absolute file name. - - You can specify separate installation prefixes for -architecture-specific files and architecture-independent files. If you -pass the option `--exec-prefix=PREFIX' to `configure', the package uses -PREFIX as the prefix for installing programs and libraries. -Documentation and other data files still use the regular prefix. - - In addition, if you use an unusual directory layout you can give -options like `--bindir=DIR' to specify different values for particular -kinds of files. Run `configure --help' for a list of the directories -you can set and what kinds of files go in them. In general, the -default for these options is expressed in terms of `${prefix}', so that -specifying just `--prefix' will affect all of the other directory -specifications that were not explicitly provided. - - The most portable way to affect installation locations is to pass the -correct locations to `configure'; however, many packages provide one or -both of the following shortcuts of passing variable assignments to the -`make install' command line to change installation locations without -having to reconfigure or recompile. - - The first method involves providing an override variable for each -affected directory. For example, `make install -prefix=/alternate/directory' will choose an alternate location for all -directory configuration variables that were expressed in terms of -`${prefix}'. Any directories that were specified during `configure', -but not in terms of `${prefix}', must each be overridden at install -time for the entire installation to be relocated. The approach of -makefile variable overrides for each directory variable is required by -the GNU Coding Standards, and ideally causes no recompilation. -However, some platforms have known limitations with the semantics of -shared libraries that end up requiring recompilation when using this -method, particularly noticeable in packages that use GNU Libtool. - - The second method involves providing the `DESTDIR' variable. For -example, `make install DESTDIR=/alternate/directory' will prepend -`/alternate/directory' before all installation names. The approach of -`DESTDIR' overrides is not required by the GNU Coding Standards, and -does not work on platforms that have drive letters. On the other hand, -it does better at avoiding recompilation issues, and works well even -when some directory options were not specified in terms of `${prefix}' -at `configure' time. - -Optional Features -================= - - If the package supports it, you can cause programs to be installed -with an extra prefix or suffix on their names by giving `configure' the -option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'. - - Some packages pay attention to `--enable-FEATURE' options to -`configure', where FEATURE indicates an optional part of the package. -They may also pay attention to `--with-PACKAGE' options, where PACKAGE -is something like `gnu-as' or `x' (for the X Window System). The -`README' should mention any `--enable-' and `--with-' options that the -package recognizes. - - For packages that use the X Window System, `configure' can usually -find the X include and library files automatically, but if it doesn't, -you can use the `configure' options `--x-includes=DIR' and -`--x-libraries=DIR' to specify their locations. - - Some packages offer the ability to configure how verbose the -execution of `make' will be. For these packages, running `./configure ---enable-silent-rules' sets the default to minimal output, which can be -overridden with `make V=1'; while running `./configure ---disable-silent-rules' sets the default to verbose, which can be -overridden with `make V=0'. - -Particular systems -================== - - On HP-UX, the default C compiler is not ANSI C compatible. If GNU -CC is not installed, it is recommended to use the following options in -order to use an ANSI C compiler: - - ./configure CC="cc -Ae -D_XOPEN_SOURCE=500" - -and if that doesn't work, install pre-built binaries of GCC for HP-UX. - - HP-UX `make' updates targets which have the same time stamps as -their prerequisites, which makes it generally unusable when shipped -generated files such as `configure' are involved. Use GNU `make' -instead. - - On OSF/1 a.k.a. Tru64, some versions of the default C compiler cannot -parse its `' header file. The option `-nodtk' can be used as -a workaround. If GNU CC is not installed, it is therefore recommended -to try - - ./configure CC="cc" - -and if that doesn't work, try - - ./configure CC="cc -nodtk" - - On Solaris, don't put `/usr/ucb' early in your `PATH'. This -directory contains several dysfunctional programs; working variants of -these programs are available in `/usr/bin'. So, if you need `/usr/ucb' -in your `PATH', put it _after_ `/usr/bin'. - - On Haiku, software installed for all users goes in `/boot/common', -not `/usr/local'. It is recommended to use the following options: - - ./configure --prefix=/boot/common - -Specifying the System Type -========================== - - There may be some features `configure' cannot figure out -automatically, but needs to determine by the type of machine the package -will run on. Usually, assuming the package is built to be run on the -_same_ architectures, `configure' can figure that out, but if it prints -a message saying it cannot guess the machine type, give it the -`--build=TYPE' option. TYPE can either be a short name for the system -type, such as `sun4', or a canonical name which has the form: - - CPU-COMPANY-SYSTEM - -where SYSTEM can have one of these forms: - - OS - KERNEL-OS - - See the file `config.sub' for the possible values of each field. If -`config.sub' isn't included in this package, then this package doesn't -need to know the machine type. - - If you are _building_ compiler tools for cross-compiling, you should -use the option `--target=TYPE' to select the type of system they will -produce code for. - - If you want to _use_ a cross compiler, that generates code for a -platform different from the build platform, you should specify the -"host" platform (i.e., that on which the generated programs will -eventually be run) with `--host=TYPE'. - -Sharing Defaults -================ - - If you want to set default values for `configure' scripts to share, -you can create a site shell script called `config.site' that gives -default values for variables like `CC', `cache_file', and `prefix'. -`configure' looks for `PREFIX/share/config.site' if it exists, then -`PREFIX/etc/config.site' if it exists. Or, you can set the -`CONFIG_SITE' environment variable to the location of the site script. -A warning: not all `configure' scripts look for a site script. - -Defining Variables -================== - - Variables not defined in a site shell script can be set in the -environment passed to `configure'. However, some packages may run -configure again during the build, and the customized values of these -variables may be lost. In order to avoid this problem, you should set -them in the `configure' command line, using `VAR=value'. For example: - - ./configure CC=/usr/local2/bin/gcc - -causes the specified `gcc' to be used as the C compiler (unless it is -overridden in the site shell script). - -Unfortunately, this technique does not work for `CONFIG_SHELL' due to -an Autoconf bug. Until the bug is fixed you can use this workaround: - - CONFIG_SHELL=/bin/bash /bin/bash ./configure CONFIG_SHELL=/bin/bash - -`configure' Invocation -====================== - - `configure' recognizes the following options to control how it -operates. - -`--help' -`-h' - Print a summary of all of the options to `configure', and exit. - -`--help=short' -`--help=recursive' - Print a summary of the options unique to this package's - `configure', and exit. The `short' variant lists options used - only in the top level, while the `recursive' variant lists options - also present in any nested packages. - -`--version' -`-V' - Print the version of Autoconf used to generate the `configure' - script, and exit. - -`--cache-file=FILE' - Enable the cache: use and save the results of the tests in FILE, - traditionally `config.cache'. FILE defaults to `/dev/null' to - disable caching. - -`--config-cache' -`-C' - Alias for `--cache-file=config.cache'. - -`--quiet' -`--silent' -`-q' - Do not print messages saying which checks are being made. To - suppress all normal output, redirect it to `/dev/null' (any error - messages will still be shown). - -`--srcdir=DIR' - Look for the package's source code in directory DIR. Usually - `configure' can determine that directory automatically. - -`--prefix=DIR' - Use DIR as the installation prefix. *note Installation Names:: - for more details, including other options available for fine-tuning - the installation locations. - -`--no-create' -`-n' - Run the configure checks, but stop before creating any output - files. - -`configure' also accepts some other, not widely useful, options. Run -`configure --help' for more details. - diff --git a/proofs/lfsc_checker/Makefile.am b/proofs/lfsc_checker/Makefile.am deleted file mode 100644 index ff483f5fb..000000000 --- a/proofs/lfsc_checker/Makefile.am +++ /dev/null @@ -1,30 +0,0 @@ -AM_CXXFLAGS = -Wall -Wno-deprecated - -bin_PROGRAMS = lfsc-checker - -lfsc_checker_SOURCES = \ - main.cpp -lfsc_checker_LDADD = \ - @builddir@/liblfsc_checker.la - -noinst_LTLIBRARIES = liblfsc_checker.la - -liblfsc_checker_la_SOURCES = \ - check.cpp \ - check.h \ - chunking_memory_management.h \ - code.cpp \ - code.h \ - expr.cpp \ - expr.h \ - libwriter.cpp \ - libwriter.h \ - position.h \ - print_smt2.cpp \ - print_smt2.h \ - scccode.cpp \ - scccode.h \ - sccwriter.cpp \ - sccwriter.h \ - trie.cpp \ - trie.h diff --git a/proofs/lfsc_checker/NEWS b/proofs/lfsc_checker/NEWS deleted file mode 100644 index 1a357ab4c..000000000 --- a/proofs/lfsc_checker/NEWS +++ /dev/null @@ -1,9 +0,0 @@ -This file contains a summary of important user-visible changes to the -LFSC proof checker. - -Changes since pre-1.0 (unversioned) releases -============================================ - -* Incorporated the LFSC checker into the CVC4 project. - --- Morgan Deters Thu, 12 Dec 2013 18:16:08 -0500 diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README deleted file mode 100644 index 5073569bc..000000000 --- a/proofs/lfsc_checker/README +++ /dev/null @@ -1,83 +0,0 @@ -lfsc: a high-performance LFSC proof checker. - -Andy Reynolds and Aaron Stump - ----------------------------------------------------------------------- -Command line parameters for LFSC: - -lfsc [sig_1 .... sig_n] [opts_1...opts_n] - -[sig_1 .... sig_n] are signature files, and options [opts_1...opts_n] -are any of the following: - ---compile-scc : Write out all side conditions contained in signatures - specified on the command line to files scccode.h, scccode.cpp (see - below for example) - ---run-scc : Run proof checking with compiled side condition code (see - below). - ---compile-scc-debug : Write side condition code to scccode.h, - scccode.cpp that contains print statements (for debugging running of - side condition code). - - - - -Typical usage: - -./src/opt/lfsc [sig_1 .... sig_n] [proof] [opts_1...opts_n] - -A proof is typically specified at the end of the list of input files -in file [proof]. This will tell LFSC to type check the proof term in -the file [proof]. The extension (*.plf) is commonly used for both -user signature files and proof files. - - - - -Side condition code compilation: - -LFSC may be used with side condition code compilation. This will take -all side conditions ("program" constructs) in the user signature and -produce equivalent C++ code in the output files scccode.h, -scccode.cpp. - -An example for QF_IDL running with side condition code compilation: - -(1) In the src/ directory, run LFSC with the command line parameters: - -./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \ - ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \ - ../sat-tests/th_idl.plf --compile-scc - -This will produce scccode.h and scccode.cpp in the working directory -where lfsc was run (here, src/). - -(2) Recompile the code base for lfsc. This will produce a copy of the -LFSC executable that is capable of calling side conditions directly as -compiled C++. - -(3) To check a proof.plf* with side condition code compilation, run -LFSC with the command line parameters: - -./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \ - ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \ - ../sat-tests/th_idl.plf --run-scc proof.plf - - - -*Note that this proof must be compatible with the proof checking - signature. The proof generator is responsible for producing a proof - in the proper format that can be checked by the proof signature - specified when running LFSC. - -For example, in the case of CLSAT in the QF_IDL logic, older proofs -(proofs produced before Feb 2009) may be incompatible with the newest -version of the resolution checking signature (sat.plf). The newest -version of CLSAT -- which can be checked out from the Iowa repository -with - -svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat - -should produce proofs compatible with the current version of sat.plf. diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp deleted file mode 100644 index e100efa69..000000000 --- a/proofs/lfsc_checker/check.cpp +++ /dev/null @@ -1,1383 +0,0 @@ -#include "position.h" -#include "check.h" -#include "code.h" -#include "expr.h" -#include "trie.h" -#include "sccwriter.h" -#include "libwriter.h" -#ifndef _MSC_VER -#include -#endif -#include -#include -#include -#include "scccode.h" -#include "print_smt2.h" - -using namespace std; -#ifndef _MSC_VER -using namespace __gnu_cxx; -#endif - -int linenum = 1; -int colnum = 1; -const char *filename = 0; -FILE *curfile = 0; - -//#define USE_HASH_MAPS //AJR: deprecated - -symmap2 progs; -std::vector< Expr* > ascHoles; - -#ifdef USE_HASH_MAPS -hash_map symbols; -hash_map symbol_types; -#else -Trie > *symbols = new Trie >; -#endif - -hash_map imports; -std::map mark_map; -std::vector< std::pair< std::string, std::pair > > local_sym_names; - -Expr *not_defeq1 = 0; -Expr *not_defeq2 = 0; - -bool tail_calls = true; -bool big_check = true; - -void report_error(const string &msg) { - if (filename) { - Position p(filename,linenum,colnum); - p.print(cout); - } - cout << "\n"; - cout << msg; - cout << "\n"; - if (not_defeq1 && not_defeq2) { - cout << "The following terms are not definitionally equal:\n1. "; - not_defeq1->print(cout); - cout << "\n2. "; - not_defeq2->print(cout); - } - cout.flush(); - exit(1); -} - -Expr *call_run_code(Expr *code) { - if (dbg_prog) { - cout << "[Running "; - code->print(cout); - cout << "\n"; - } - Expr *computed_result = run_code(code); - if (dbg_prog) { - cout << "] returning "; - if (computed_result) - computed_result->print(cout); - else - cout << "fail"; - cout << "\n"; - } - return computed_result; -} - -char our_getc_c = 0; - -int IDBUF_LEN = 2048; -char idbuf[2048]; - -Expr *statType = new CExpr(TYPE); -Expr *statKind = new CExpr(KIND); -Expr *statMpz = new CExpr(MPZ); -Expr *statMpq = new CExpr(MPQ); - -int open_parens = 0; - -// only call in check() -void eat_rparen() { - eat_char(')'); - open_parens--; -} - -void eat_excess(int prev) { - while(open_parens > prev) - eat_rparen(); -} - -/* There are four cases for check(): - -1. expected=0, create is false: check() sets computed to be the classifier of - the checked term. - -2. expected=0, create is true: check() returns - the checked expression and sets computed to be its classifier. - -3. expected is non-null, create is false: check returns NULL. - -4. expected is non-null, create is true: check returns the term that - was checked. - -We consume the reference for expected, to enable tail calls in the -application case. - -If is_hole is NULL, then the expression parsed may not be a hole. -Otherwise, it may be, and we will set *is_hole to true if it is -(but leave *is_hole alone if it is not). - -*/ - -bool allow_run = false; -int app_rec_level = 0; - -Expr *check(bool create, Expr *expected, Expr **computed = NULL, - bool *is_hole = 0, bool return_pos = false, bool inAsc = false ) { - start_check: - //std::cout << "check code "; - //if( expected ) - // expected->print( std::cout ); - //std::cout << std::endl; - char d = non_ws(); - switch(d) { - case '(': { - - open_parens++; - - char c = non_ws(); - switch (c) { - case EOF: - report_error("Unexpected end of file."); - break; - case '!': { // the pi case - string id(prefix_id()); -#ifdef DEBUG_SYM_NAMES - Expr *sym = new SymSExpr(id,SYMS_EXPR); -#else - Expr *sym = new SymExpr(id); - //std::cout << "name " << id << " " << sym << std::endl; -#endif - allow_run = true; - int prevo = open_parens; - Expr *domain = check(true, statType); - eat_excess(prevo); - allow_run = false; -#ifdef USE_HASH_MAPS - Expr *prev = symbols[id]; - Expr *prevtp = symbol_types[id]; - symbols[id] = sym; - symbol_types[id] = domain; -#else - pairprev = - symbols->insert(id.c_str(),pair(sym,domain)); -#endif - if (expected) - expected->inc(); - Expr *range = check(create, expected, computed, NULL, return_pos); - eat_excess(prevo); - eat_rparen(); - -#ifdef USE_HASH_MAPS - symbols[id] = prev; - symbol_types[id] = prevtp; -#else - symbols->insert(id.c_str(),prev); -#endif - if (expected) { - int o = expected->followDefs()->getop(); - expected->dec(); - if (o != TYPE && o != KIND) - report_error(string("The expected classifier for a pi abstraction") - +string("is neither \"type\" nor \"kind\".\n") - +string("1. the expected classifier: ") - +expected->toString()); - if (create){ - CExpr* ret = new CExpr(PI, sym, domain, range); - ret->calc_free_in(); - return ret; - } - return 0; - } - else { - if (create){ - CExpr* ret = new CExpr(PI, sym, domain, range); - ret->calc_free_in(); - return ret; - } - int o = (*computed)->followDefs()->getop(); - if (o != TYPE && o != KIND) - report_error(string("The classifier for the range of a pi") - +string("abstraction is neither \"type\" nor ") - +string("\"kind\".\n1. the computed classifier: ") - +range->toString()); - return 0; - } - } - case '%': { // the case for big lambda - if (expected || create || !return_pos || !big_check) - report_error(string("Big lambda abstractions can only be used") - +string("in the return position of a \"bigcheck\"\n") - +string("command.")); - string id(prefix_id()); -#ifdef DEBUG_SYM_NAMES - SymExpr *sym = new SymSExpr(id, SYMS_EXPR); -#else - SymExpr *sym = new SymExpr(id); - //std::cout << "name " << id << " " << sym << std::endl; -#endif - - int prevo = open_parens; - Expr *expected_domain = check(true, statType); - eat_excess(prevo); - -#ifdef USE_HASH_MAPS - Expr *prev = symbols[id]; - Expr *prevtp = symbol_types[id]; - symbols[id] = sym; - symbol_types[id] = expected_domain; -#else - pair prevpr = - symbols->insert(id.c_str(), pair(sym,expected_domain)); - Expr *prev = prevpr.first; - Expr *prevtp = prevpr.second; -#endif - expected_domain->inc(); // because we have stored it in the symbol table - - //will clean up local sym name eventually - local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); - if (prev) - prev->dec(); - if (prevtp) - prevtp->dec(); - create = false; - expected = NULL; - // computed unchanged - is_hole = NULL; - // return_pos unchanged - - // note we will not store the proper return type in computed. - - goto start_check; - } - - case '\\': { // the lambda case - if (!expected) - report_error(string("We are computing a type for a lambda ") - +string("abstraction, but we can only check\n") - +string("such against a type. Try inserting an ") - +string("ascription (using ':').\n")); - Expr *orig_expected = expected; - expected = expected->followDefs(); - if (expected->getop() != PI) - report_error(string("We are type-checking a lambda abstraction, but\n") - +string("the expected type is not a pi abstraction.\n") - +string("1. The expected type: ") + expected->toString()); - string id(prefix_id()); -#ifdef DEBUG_SYM_NAMES - SymExpr *sym = new SymSExpr(id, SYMS_EXPR); -#else - SymExpr *sym = new SymExpr(id); - //std::cout << "name " << id << " " << sym << std::endl; -#endif - - CExpr *pitp = (CExpr *)expected; - Expr *expected_domain = pitp->kids[1]; - Expr *expected_range = pitp->kids[2]; - SymExpr *pivar = (SymExpr *)pitp->kids[0]; - if (expected_range->followDefs()->getop() == TYPE) - report_error(string("The expected classifier for a lambda abstraction") - +string(" a kind, not a type.\n") - +string("1. The expected classifier: ") - +expected->toString()); - - /* we need to map the pivar to the new sym, because in our - higher-order matching we may have (_ x) to unify with t. - The x must be something from an expected type, since only these - can have holes. We want to map expected vars x to computed vars y, - so that we can set the hole to be \ y t, where t contains ys but - not xs. */ - -#ifdef USE_HASH_MAPS - Expr *prev = symbols[id]; - Expr *prevtp = symbol_types[id]; - symbols[id] = sym; - symbol_types[id] = expected_domain; -#else - pair prevpr = - symbols->insert(id.c_str(), pair(sym,expected_domain)); - Expr *prev = prevpr.first; - Expr *prevtp = prevpr.second; -#endif - Expr *prev_pivar_val = pivar->val; - sym->inc(); - pivar->val = sym; - - expected_domain->inc(); // because we have stored it in the symbol table - expected_range->inc(); // because we will pass it to a recursive call - - if (tail_calls && big_check && return_pos && !create) { - //will clean up local sym name eventually - local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); - if (prev_pivar_val) - prev_pivar_val->dec(); - if (prev) - prev->dec(); - if (prevtp) - prevtp->dec(); - orig_expected->dec(); - create = false; - expected = expected_range; - computed = NULL; - is_hole = NULL; - // return_pos unchanged - goto start_check; - } - else { - - int prev = open_parens; - Expr *range = check(create, expected_range, NULL, NULL, return_pos); - eat_excess(prev); - eat_rparen(); - -#ifdef USE_HASH_MAPS - symbols[id] = prev; - symbol_types[id] = prevtp; -#else - symbols->insert(id.c_str(), prevpr); -#endif - expected_domain->dec(); // because removed from the symbol table now - - pivar->val = prev_pivar_val; - - orig_expected->dec(); - - sym->dec(); // the pivar->val reference - if (create) - return new CExpr(LAM, sym, range); - sym->dec(); // the symbol table reference, otherwise in the new LAM - return 0; - } - } - case '^': { // the run case - if (!allow_run || !create || !expected) - report_error(string("A run expression (operator \"^\") appears in") - +string(" a disallowed position.")); - - Expr *code = read_code(); - //string errstr = (string("The first argument in a run expression must be") - // +string(" a call to a program.\n1. the argument: ") - // +code->toString()); - - /* determine expected type of the result term, and make sure - the code term is an allowed one. */ -#if 0 - Expr *progret; - if (code->isArithTerm()) - progret = statMpz; - else { - if (code->getop() != APP) - report_error(errstr); - - CExpr *call = (CExpr *)code; - - // prog is not known to be a SymExpr yet - CExpr *prog = (CExpr *)call->get_head(); - - if (prog->getop() != PROG) - report_error(errstr); - - progret = prog->kids[0]->get_body(); - } -#else - Expr *progret = NULL; - if (code->isArithTerm()) - progret = statMpz; - else { - if (code->getop() == APP) - { - CExpr *call = (CExpr *)code; - - // prog is not known to be a SymExpr yet - CExpr *prog = (CExpr *)call->get_head(); - - if (prog->getop() == PROG) - progret = prog->kids[0]->get_body(); - } - } -#endif - /* determine expected type of the result term, and make sure - the code term is an allowed one. */ - //Expr* progret = check_code( code ); - - /* the next term cannot be a hole where run expressions are introduced. - When they are checked in applications, it can be. */ - int prev = open_parens; - if( progret ) - progret->inc(); - Expr *trm = check(true, progret); - eat_excess(prev); - eat_rparen(); - - if (expected->getop() != TYPE) - report_error(string("The expected type for a run expression is not ") - +string("\"type\".\n") - +string("1. The expected type: ")+expected->toString()); - expected->dec(); - return new CExpr(RUN, code, trm); - } - - case ':': { // the ascription case - statType->inc(); - int prev = open_parens; - Expr *tp = check(true, statType, NULL, NULL, false, true ); - eat_excess(prev); - - if (!expected) - tp->inc(); - - Expr *trm = check(create, tp, NULL, NULL, return_pos); - eat_excess(prev); - eat_rparen(); - if (expected) { - if (!expected->defeq(tp)) - report_error(string("The expected type does not match the ") - +string("ascribed type in an ascription.\n") - +string("1. The expected type: ")+expected->toString() - +string("\n2. The ascribed type: ")+tp->toString()); - - // no need to dec tp, since it was consumed by the call to check - expected->dec(); - if (create) - return trm; - trm->dec(); - return 0; - } - else { - *computed = tp; - if (create) - return trm; - return 0; - } - } - case '@': { // the local definition case - string id(prefix_id()); -#ifdef DEBUG_SYM_NAMES - SymExpr *sym = new SymSExpr(id, SYMS_EXPR); -#else - SymExpr *sym = new SymExpr(id); -#endif - int prev_open = open_parens; - Expr *tp_of_trm = NULL; - Expr *trm = check(true, NULL, &tp_of_trm); - eat_excess(prev_open); - - sym->val = trm; - -#ifdef USE_HASH_MAPS - Expr *prev = symbols[id]; - Expr *prevtp = symbol_types[id]; - symbols[id] = sym; - symbol_types[id] = tp_of_trm; -#else - pair prevpr = - symbols->insert(id.c_str(), pair(sym,tp_of_trm)); - Expr *prev = prevpr.first; - Expr *prevtp = prevpr.second; -#endif - - if (tail_calls && big_check && return_pos && !create) { - if (prev) - prev->dec(); - if (prevtp) - prevtp->dec(); - // all parameters to check() unchanged here - goto start_check; - } - else { - int prev_open = open_parens; - Expr *body = check(create, expected, computed, is_hole, return_pos); - eat_excess(prev_open); - eat_rparen(); - -#ifdef USE_HASH_MAPS - symbols[id] = prev; - symbol_types[id] = prevtp; -#else - symbols->insert(id.c_str(), prevpr); -#endif - tp_of_trm->dec(); // because removed from the symbol table now - - sym->dec(); - return body; - } - } - case '~': { - int prev = open_parens; - Expr *e = check(create, expected, computed, is_hole, return_pos); - eat_excess(prev); - eat_rparen(); - - // this has been only very lightly tested -- ads. - - if (expected) { - if (expected != statMpz && expected != statMpq) - report_error("Negative sign where an numeric expression is expected."); - } - else { - if ((*computed) != statMpz && (*computed) != statMpq) - report_error("Negative sign where an numeric expression is expected."); - } - - if (create) { - if (e->getclass() == INT_EXPR) - { - IntExpr *ee = (IntExpr *)e; - mpz_neg(ee->n, ee->n); - return ee; - } - else if( e->getclass() == RAT_EXPR ) - { - RatExpr *ee = (RatExpr *)e; - mpq_neg(ee->n, ee->n); - return ee; - } - else - { - report_error("Negative sign with expr that is not an int. literal."); - } - } - else - return 0; - } - default: { // the application case - our_ungetc(c); - Expr *head_computed; - int prev = open_parens; - Expr *headtrm = check(create,0,&head_computed); - eat_excess(prev); - - CExpr *headtp = (CExpr *)head_computed->followDefs(); - headtp->inc(); - head_computed->dec(); - if ( headtp->cloned()) { - // we must clone - Expr *orig_headtp = headtp; - headtp = (CExpr *)headtp->clone(); - orig_headtp->dec(); - } - else - headtp->setcloned(); -#ifdef DEBUG_APPS - char tmp[100]; - sprintf(tmp,"(%d) ", app_rec_level++); - cout << tmp << "{ headtp = "; - headtp->debug(); -#endif - char c; - vector holes; - vector free_holes; - while ((c = non_ws()) != ')') { - our_ungetc(c); - if (headtp->getop() != PI) - report_error(string("The type of an applied term is not ") - + string("a pi-type.\n") - + string("\n1. the type of the term: ") - + headtp->toString() - + (headtrm ? (string("\n2. the term: ") - + headtrm->toString()) - : string(""))); - SymExpr *headtp_var = (SymExpr *)headtp->kids[0]; - Expr *headtp_domain = headtp->kids[1]; - Expr *headtp_range = headtp->kids[2]; - if (headtp_domain->getop() == RUN) { - CExpr *run = (CExpr *)headtp_domain; - Expr *code = run->kids[0]; - Expr *expected_result = run->kids[1]; - Expr *computed_result = call_run_code(code); - if (!computed_result) - report_error(string("A side condition failed.\n") - +string("1. the side condition: ") - +code->toString()); - if (!expected_result->defeq(computed_result)) - report_error(string("The expected result of a side condition ") - +string("does not match the computed result.\n") - +string("1. expected result: ") - +expected_result->toString() - +string("\n2. computed result: ") - +computed_result->toString()); - computed_result->dec(); - } - else { - // check an argument - bool var_in_range = headtp->get_free_in();//headtp_range->free_in(headtp_var); - bool arg_is_hole = false; - bool consumed_arg = false; - - bool create_arg = (create || var_in_range); - - headtp_domain->inc(); - - if (tail_calls && !create_arg && headtp_range->getop() != PI) { - // we can make a tail call to check() here. - - if (expected) { - if (!expected->defeq(headtp_range)) - report_error(string("The type expected for an application ") - + string("does not match the computed type.\n") - + string("1. The expected type: ") - + expected->toString() - + string("\n2. The computed type: ") - + headtp_range->toString() - + (headtrm ? (string("\n3. the application: ") - + headtrm->toString()) - : string(""))); - expected->dec(); - } - else { - headtp_range->inc(); - *computed = headtp_range; - } - - headtp->dec(); - - // same as below - for (int i = 0, iend = holes.size(); i < iend; i++) { - if (!holes[i]->val) - /* if the hole is free in the domain, we will be filling - it in when we make our tail call, since the domain - is the expected type for the argument */ - if (!headtp_domain->free_in(holes[i])) - report_error(string("A hole was left unfilled after ") - +string("checking an application.\n")); - holes[i]->dec(); - } - - create = false; - expected = headtp_domain; - computed = NULL; - is_hole = NULL; // the argument cannot be a hole - // return_pos is unchanged - -#ifdef DEBUG_APPS - cout << "Making tail call.\n"; -#endif - - goto start_check; - } - - Expr *arg = check(create_arg, headtp_domain, NULL, &arg_is_hole); - eat_excess(prev); - if (create) { -#ifndef USE_FLAT_APP - headtrm = new CExpr(APP, headtrm, arg); -#else - Expr* orig_headtrm = headtrm; - headtrm = Expr::make_app( headtrm, arg ); - if( orig_headtrm->getclass()==CEXPR ){ - orig_headtrm->dec(); - } -#endif - consumed_arg = true; - } - if (var_in_range) { - Expr *tmp = arg->followDefs(); - tmp->inc(); - headtp_var->val = tmp; - } - if (arg_is_hole) { - if (consumed_arg) - arg->inc(); - else - consumed_arg = true; // not used currently -#ifdef DEBUG_HOLES - cout << "An argument is a hole: "; - arg->debug(); -#endif - holes.push_back((HoleExpr *)arg); - } - } - headtp_range->inc(); - headtp->dec(); - headtp = (CExpr *)headtp_range; - } - open_parens--; - - // check for remaining RUN in the head's type after all the arguments - - if (headtp->getop() == PI && headtp->kids[1]->getop() == RUN) { - CExpr *run = (CExpr *)headtp->kids[1]; - Expr *code = run->kids[0]->followDefs(); - Expr *expected_result = run->kids[1]; - Expr *computed_result = call_run_code(code); - if (!computed_result) - report_error(string("A side condition failed.\n") - +string("1. the side condition: ")+code->toString()); - if (!expected_result->defeq(computed_result)) - report_error(string("The expected result of a side condition ") - +string("does not match the computed result.\n") - +string("1. expected result: ") - +expected_result->toString() - +string("\n2. computed result: ") - +computed_result->toString()); - Expr *tmp = headtp->kids[2]; - tmp->inc(); - headtp->dec(); - headtp = (CExpr *)tmp; - computed_result->dec(); - } - -#ifdef DEBUG_APPS - for (int i = 0, iend = holes.size(); i < iend; i++) { - cout << tmp << "hole "; - holes[i]->debug(); - } - cout << "}"; - app_rec_level--; -#endif - - Expr *ret = 0; - if (expected) { - if (!expected->defeq(headtp)){ - report_error(string("The type expected for an application does not") - + string(" match the computed type.(2) \n") - + string("1. The expected type: ") - + expected->toString() - + string("\n2. The computed type: ") - + headtp->toString() - + (headtrm ? (string("\n3. the application: ") - + headtrm->toString()) - : string(""))); - - } - expected->dec(); - headtp->dec(); - if (create) - ret = headtrm; - } - else { - *computed = headtp; - if (create) - ret = headtrm; - } - - /* do this check here to give the defeq() call above a - chance to fill in some holes */ - for (int i = 0, iend = holes.size(); i < iend; i++) { - if (!holes[i]->val){ - if( inAsc ){ -#ifdef DEBUG_HOLES - std::cout << "Ascription Hole: "; - holes[i]->print( std::cout ); - std::cout << std::endl; -#endif - ascHoles.push_back( holes[i] ); - }else{ - report_error(string("A hole was left unfilled after checking") - +string(" an application (2).\n")); - } - } - holes[i]->dec(); - } - - return ret; - - } // end application case - } - } - case EOF: - report_error("Unexpected end of file."); - break; - - case '_': - if (!is_hole) - report_error("A hole is being used in a disallowed position."); - *is_hole = true; - if (expected) - expected->dec(); - return new HoleExpr(); - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - case '8': - case '9': { - our_ungetc(d); - string v; - char c; - while (isdigit(c = our_getc())) - v.push_back(c); - bool parseMpq = false; - string v2; - if( c=='/' ) - { - parseMpq = true; - v.push_back( c ); - while(isdigit(c = our_getc())) - v.push_back(c); - } - our_ungetc(c); - - - Expr *i = 0; - if (create) { - if( parseMpq ) - { - mpq_t num; - mpq_init(num); - if (mpq_set_str(num,v.c_str(),10) == -1) - report_error("Error reading a numeral."); - i = new RatExpr(num); - } - else - { - mpz_t num; - if (mpz_init_set_str(num,v.c_str(),10) == -1) - report_error("Error reading a numeral."); - i = new IntExpr(num); - } - } - - if (expected) { - if( ( !parseMpq && expected != statMpz ) || ( parseMpq && expected != statMpq ) ) - report_error(string("We parsed a numeric literal, but were ") - +string("expecting a term of a different type.\n") - +string("1. the expected type: ")+expected->toString()); - expected->dec(); - if (create) - return i; - return 0; - } - else { - if( parseMpq ) - { - statMpq->inc(); - *computed = statMpq; - if (create) - return i; - return statMpq; - } - else - { - statMpz->inc(); - *computed = statMpz; - if (create) - return i; - return statMpz; - } - } - } - default: { - our_ungetc(d); - string id(prefix_id()); -#ifdef USE_HASH_MAPS - Expr *ret = symbols[id]; - Expr *rettp = symbol_types[id]; -#else - pair p = symbols->get(id.c_str()); - Expr *ret = p.first; - Expr *rettp = p.second; -#endif - if (!ret) - report_error(string("Undeclared identifier: ")+id); - if (expected) { - if (!expected->defeq(rettp)) - report_error(string("The type expected for a symbol does not") - + string(" match the symbol's type.\n") - + string("1. The symbol: ") - + id - + string("\n2. The expected type: ") - + expected->toString() - + string("\n3. The symbol's type: ") - + rettp->toString()); - expected->dec(); - if (create) { - ret->inc(); - return ret; - } - return 0; - } - else { - if( computed ){ - *computed = rettp; - (*computed)->inc(); - } - if (create) { - ret->inc(); - return ret; - } - return 0; - } - } - } - - report_error("Unexpected operator at the start of a term."); - return 0; -} - -#ifdef USE_HASH_MAPS -void discard_old_symbol(const string &id) { - Expr *tmp = symbols[id]; - if (tmp) - tmp->dec(); - tmp = symbol_types[id]; - if (tmp) - tmp->dec(); -} -#endif - -int check_time; - -void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { - int prev_linenum = linenum; - int prev_colnum = colnum; - const char *prev_filename = filename; - FILE * prev_curfile = curfile; - - // from code.h - dbg_prog = a.show_runs; - run_scc = a.run_scc; - tail_calls = !a.no_tail_calls; - - std::string f; - if (strcmp(_filename,"stdin") == 0) { - curfile = stdin; - f = std::string(_filename); - } - else { - if (prev_curfile) { - f = std::string(prev_filename); -#ifdef _MSC_VER - std::string str( f ); - for( int n=str.length(); n>=0; n-- ){ - if( str[n]=='\\' || str[n]=='/' ){ - str = str.erase( n, str.length()-n ); - break; - } - } - char *tmp = (char*)str.c_str(); -#else - // Note: dirname may modify its argument, so we create a non-const copy. - char *f_copy = strdup(f.c_str()); - std::string str = std::string(dirname(f_copy)); - free(f_copy); -#endif - f = str + std::string("/") + std::string(_filename); - } else { - f = std::string(_filename); - } - curfile = fopen(f.c_str(), "r"); - if (!curfile) - report_error(string("Could not open file \"") + f + - string("\" for reading.\n")); - } - - linenum = 1; - colnum = 1; - filename = f.c_str(); - - char c; - while ((c = non_ws()) && c!=EOF ) { - if( c == '(' ) - { - char d; - switch ((d = non_ws())) { - case 'd': - char b; - if ((b = our_getc()) != 'e') - report_error(string("Unexpected start of command.")); - - switch ((b = our_getc())) { - case 'f': {// expecting "define" - - if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e') - report_error(string("Unexpected start of command.")); - - string id(prefix_id()); - Expr *ttp; - int prevo = open_parens; - Expr *t = check(true, 0, &ttp, NULL, true); - eat_excess(prevo); - - int o = ttp->followDefs()->getop(); - if (o == KIND) - report_error(string("Kind-level definitions are not supported.\n")); - SymSExpr *s = new SymSExpr(id); - s->val = t; -#ifdef USE_HASH_MAPS - discard_old_symbol(id); - symbols[id] = s; - symbol_types[id] = ttp; -#else - pair prev = - symbols->insert(id.c_str(), pair(s,ttp)); - if (prev.first) - prev.first->dec(); - if (prev.second) - prev.second->dec(); -#endif - break; - } - case 'c': {// expecting "declare" - if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' - || our_getc() != 'e') - report_error(string("Unexpected start of command.")); - - string id(prefix_id()); - Expr *ttp; - int prevo = open_parens; - Expr *t = check(true, 0, &ttp, NULL, true); - eat_excess(prevo); - - ttp = ttp->followDefs(); - if (ttp->getop() != TYPE && ttp->getop() != KIND) - report_error(string("The expression declared for \"") - +id+string("\" is neither\na type nor a kind.\n") - +string("1. The expression: ") - +t->toString() - +string("\n2. Its classifier (should be \"type\" ") - +string("or \"kind\"): ")+ttp->toString()); - ttp->dec(); - SymSExpr *s = new SymSExpr(id); -#ifdef USE_HASH_MAPS - discard_old_symbol(id); - symbols[id] = s; - symbol_types[id] = t; -#else - pair prev = - symbols->insert(id.c_str(), pair(s,t)); - if( lw ) - lw->add_symbol( s, t ); - if (prev.first) - prev.first->dec(); - if (prev.second) - prev.second->dec(); -#endif - break; - } - default: - report_error(string("Unexpected start of command.")); - } // switch((b = our_getc())) following "de" - break; - case 'c': { - if (our_getc() != 'h' || our_getc() != 'e' || our_getc() != 'c' || our_getc() != 'k') - report_error(string("Unexpected start of command.")); - if( run_scc ){ - init_compiled_scc(); - } - Expr *computed; - big_check = true; - int prev = open_parens; - (void)check(false, 0, &computed, NULL, true); - - //print out ascription holes - for( int a=0; a<(int)ascHoles.size(); a++ ){ -#ifdef PRINT_SMT2 - print_smt2( ascHoles[a], std::cout ); -#else - ascHoles[a]->print( std::cout ); -#endif - std::cout << std::endl; - } - if( !ascHoles.empty() ) - std::cout << std::endl; - ascHoles.clear(); - - //clean up local symbols - for( int a=0; a<(int)local_sym_names.size(); a++ ){ -#ifdef USE_HASH_MAPS -#else - symbols->insert( local_sym_names[a].first.c_str(), local_sym_names[a].second ); -#endif - } - local_sym_names.clear(); - mark_map.clear(); - - eat_excess(prev); - - computed->dec(); - //cleanup(); - //exit(0); - break; - } - case 'o': { // opaque case - if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q' - || our_getc() != 'u' || our_getc() != 'e') - report_error(string("Unexpected start of command.")); - - string id(prefix_id()); - Expr *ttp; - int prevo = open_parens; - (void)check(false, 0, &ttp, NULL, true); - eat_excess(prevo); - - int o = ttp->followDefs()->getop(); - if (o == KIND) - report_error(string("Kind-level definitions are not supported.\n")); - SymSExpr *s = new SymSExpr(id); -#ifdef USE_HASH_MAPS - discard_old_symbol(id); - symbols[id] = s; - symbol_types[id] = ttp; -#else - pair prev = - symbols->insert(id.c_str(), pair(s,ttp)); - if (prev.first) - prev.first->dec(); - if (prev.second) - prev.second->dec(); -#endif - break; - } - case 'r': { // run case - if (our_getc() != 'u' || our_getc() != 'n') - report_error(string("Unexpected start of command.")); - Expr *code = read_code(); - check_code(code); - cout << "[Running-sc "; - code->print(cout); - Expr *tmp = run_code(code); - cout << "] = \n"; - if (tmp) { - tmp->print(cout); - tmp->dec(); - } - else - cout << "fail"; - cout << "\n"; - code->dec(); - break; - } - case 'p': { // program case - if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' - || our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm') - report_error(string("Unexpected start of command.")); - - string progstr(prefix_id()); - SymSExpr *prog = new SymSExpr(progstr); - if (progs.find(progstr) != progs.end()) - report_error(string("Redeclaring program ")+progstr+string(".")); - progs[progstr] = prog; - eat_char('('); - char d; - vector vars; - vector tps; - Expr *tmp; - while ((d = non_ws()) != ')') { - our_ungetc(d); - eat_char('('); - string varstr = prefix_id(); -#ifdef USE_HASH_MAPS - if (symbols.find(varstr) != symbols.end()) -#else - if (symbols->get(varstr.c_str()).first != NULL) -#endif - report_error(string("A program variable is already declared") - +string(" (as a constant).\n1. The variable: ") - +varstr); - Expr *var = new SymSExpr(varstr); - vars.push_back(var); - statType->inc(); - int prev = open_parens; - Expr *tp = check(true, NULL, &tmp, 0, true); - if( tp->getclass()==SYMS_EXPR ){ -#ifdef USE_HASH_MAPS - Expr *tptp = symbol_types[((SymSExpr*)tp)->s]; -#else - pair p = symbols->get(((SymSExpr*)tp)->s.c_str()); - Expr *tptp = p.second; -#endif - if( !tptp->isType( statType ) ){ - report_error(string("Bad argument for side condition")); - } - }else{ - if (!tp->isDatatype()){ - report_error(string("Type for a program variable is not a ") - +string("datatype.\n1. the type: ")+tp->toString()); - } - } - eat_excess(prev); - - tps.push_back(tp); - eat_char(')'); - -#ifdef USE_HASH_MAPS - symbols[varstr] = var; - symbol_types[varstr] = tp; -#else - symbols->insert(varstr.c_str(), pair(var,tp)); -#endif - } - - if (!vars.size()) - report_error("A program lacks input variables."); - - statType->inc(); - int prev = open_parens; - Expr *progtp = check(true,statType,&tmp,0, true); - eat_excess(prev); - - if (!progtp->isDatatype()) - report_error(string("Return type for a program is not a") - +string(" datatype.\n1. the type: ")+progtp->toString()); - - Expr *progcode = read_code(); - - for (int i = vars.size() - 1, iend = 0; i >= iend; i--) { - vars[i]->inc(); // used below for the program code (progcode) - progtp = new CExpr(PI, vars[i], tps[i], progtp); - progtp->calc_free_in(); - } - - // just put the type here for type checking. Make sure progtp is kid 0. - prog->val = new CExpr(PROG, progtp); - - check_code(progcode); - - progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode); - //if compiling side condition code, give this code to the side condition code writer - if( a.compile_scc ){ - if( scw ){ - scw->add_scc( progstr, (CExpr*)progcode ); - } - } - - // remove the variables from the symbol table. - for (int i = 0, iend = vars.size(); i < iend; i++) { - string &s = ((SymSExpr *)vars[i])->s; - -#ifdef USE_HASH_MAPS - symbols[s] = NULL; - symbol_types[s] = NULL; -#else - symbols->insert(s.c_str(), pair(NULL,NULL)); -#endif - } - - progtp->inc(); - prog->val->dec(); - - prog->val = progcode; - - break; - } - - default: - report_error(string("Unexpected start of command.")); - } // switch((d = non_ws()) - - eat_char(')'); - } // while - else - { - if( c != ')' ) - { - char c2[2]; - c2[1] = 0; - c2[0] = c; - string syn = string("Bad syntax (mismatched parentheses?): "); - syn.append(string(c2)); - report_error(syn); - } - } - } - if (curfile != stdin) - fclose(curfile); - linenum = prev_linenum; - colnum = prev_colnum; - filename = prev_filename; - curfile = prev_curfile; - -} - -class Deref : public Trie >::Cleaner { -public: - ~Deref() {} - void clean(pair p) { - Expr *tmp = p.first; - if (tmp) { -#ifdef DEBUG - cout << "Cleaning up "; - tmp->debug(); -#endif - tmp->dec(); - } - tmp = p.second; - if (tmp) { -#ifdef DEBUG - cout << " : "; - tmp->debug(); -#endif - tmp->dec(); - } -#ifdef DEBUG - cout << "\n"; -#endif - } -}; - -template <> -Trie >::Cleaner * -Trie >::cleaner = new Deref; - -void cleanup() { - symmap::iterator i, iend; -#ifdef USE_HASH_MAPS - Expr *tmp; - for (i = symbols.begin(), iend = symbols.end(); i != iend; i++) { - tmp = i->second; - if (tmp) { -#ifdef DEBUG - cout << "Cleaning up " << i->first << " : "; - tmp->debug(); -#endif - tmp->dec(); - } - } - for (i = symbol_types.begin(), iend = symbol_types.end(); i != iend; i++) { - tmp = i->second; - if (tmp) { -#ifdef DEBUG - cout << "Cleaning up " << i->first << " : "; - tmp->debug(); -#endif - tmp->dec(); - } - } -#else - delete symbols; -#endif - - // clean up programs - - symmap2::iterator j, jend; - for (j = progs.begin(), jend = progs.end(); j != jend; j++) { - SymExpr *p = j->second; - if (p) { - Expr *progcode = p->val; - p->val = NULL; - progcode->dec(); - p->dec(); - } - } -} - -void init() { -#ifdef USE_HASH_MAPS - string tp("type"); - symbols[tp] = statType; - symbol_types[tp] = statKind; - string mpz("mpz"); - symbols[mpz] = statMpz; - symbol_types[mpz] = statType; - statType->inc(); - sym -#else - symbols->insert("type", pair(statType, statKind)); - statType->inc(); - symbols->insert("mpz", pair(statMpz, statType)); - symbols->insert("mpq", pair(statMpq, statType)); -#endif -} diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h deleted file mode 100644 index 756bb4db6..000000000 --- a/proofs/lfsc_checker/check.h +++ /dev/null @@ -1,167 +0,0 @@ -#ifndef SC2_CHECK_H -#define SC2_CHECK_H - -#include "expr.h" -#include "trie.h" - -#ifdef _MSC_VER -#include -#include -#else -#include -#endif - -#include -#include -#include - -// see the help message in main.cpp for explanation -typedef struct args { - std::vector files; - bool show_runs; - bool no_tail_calls; - bool compile_scc; - bool compile_scc_debug; - bool run_scc; - bool use_nested_app; - bool compile_lib; -} args; - -extern int check_time; - -class sccwriter; -class libwriter; - -void init(); - -void check_file(const char *_filename, args a, sccwriter* scw = NULL, libwriter* lw = NULL); - -void cleanup(); - -extern char our_getc_c; - -void report_error(const std::string &); - -extern int linenum; -extern int colnum; -extern const char *filename; -extern FILE *curfile; - -inline void our_ungetc(char c) { - if (our_getc_c != 0) - report_error("Internal error: our_ungetc buffer full"); - our_getc_c = c; - if (c == '\n') { - linenum--; - colnum=-1; - } - else - colnum--; -} - -inline char our_getc() { - char c; - if (our_getc_c > 0) { - c = our_getc_c; - our_getc_c = 0; - } - else{ -#ifndef __linux__ - c = fgetc(curfile); -#else - c = fgetc_unlocked(curfile); -#endif - } - switch(c) { - case '\n': - linenum++; -#ifdef DEBUG_LINES - std::cout << "line " << linenum << "." << std::endl; -#endif - colnum = 1; - break; - case char(EOF): - break; - default: - colnum++; - } - - return c; -} - -// return the next character that is not whitespace -inline char non_ws() { - char c; - while(isspace(c = our_getc())); - if (c == ';') { - // comment to end of line - while((c = our_getc()) != '\n' && c != char(EOF)); - return non_ws(); - } - return c; -} - -inline void eat_char(char expected) { - if (non_ws() != expected) { - char tmp[80]; - sprintf(tmp,"Expecting a \'%c\'",expected); - report_error(tmp); - } -} - -extern int IDBUF_LEN; -extern char idbuf[]; - -inline const char *prefix_id() { - int i = 0; - char c = idbuf[i++] = non_ws(); - while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) { - if (i == IDBUF_LEN) - report_error("Identifier is too long"); - - idbuf[i++] = c = our_getc(); - } - our_ungetc(c); - idbuf[i-1] = 0; - return idbuf; -} - -#ifdef _MSC_VER -typedef std::hash_map symmap; -typedef std::hash_map symmap2; -#else -typedef __gnu_cxx::hash_map symmap; -typedef __gnu_cxx::hash_map symmap2; -#endif -extern symmap2 progs; -extern std::vector< Expr* > ascHoles; - -#ifdef USE_HASH_MAPS -extern symmap symbols; -extern symmap symbol_types; -#else -extern Trie > *symbols; -#endif - -extern std::map mark_map; - -extern std::vector< std::pair< std::string, std::pair > > local_sym_names; - -#ifndef _MSC_VER -namespace __gnu_cxx -{ - template<> struct hash< std::string > - { - size_t operator()( const std::string& x ) const - { - return hash< const char* >()( x.c_str() ); - } - }; -} -#endif - -extern Expr *statMpz; -extern Expr *statMpq; -extern Expr *statType; - -#endif diff --git a/proofs/lfsc_checker/chunking_memory_management.h b/proofs/lfsc_checker/chunking_memory_management.h deleted file mode 100644 index bdf938d32..000000000 --- a/proofs/lfsc_checker/chunking_memory_management.h +++ /dev/null @@ -1,157 +0,0 @@ -/////////////////////////////////////////////////////////////////////////////// -// // -// Copyright (C) 2002 by the Board of Trustees of Leland Stanford // -// Junior University. See LICENSE for details. // -// // -/////////////////////////////////////////////////////////////////////////////// -/* chunking_memory_management.h - Aaron Stump, 6/11/99 - - This file contains macros that allow you easily to add chunking - memory management for classes. - - RCS Version: $Id: chunking_memory_management.h,v 1.1 2004/11/12 16:26:19 stump Exp $ - -*/ -#ifndef _chunking_memory_management_h_ -#define _chunking_memory_management_h_ - -#include - -/************************************************************************ - * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_H() - * Aaron Stump, 6/11/99 - * - * ABSTRACT: This macro should be called exactly once inside the body - * of the declaration of the class THE_CLASS to add chunking memory - * management for the class. That class should not itself declare the - * operators new and delete. The macro - * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC should be called with - * the same value for THE_CLASS in a .cc file for that class. - * - * NOTE that the access specifier will be public after calling this - * macro. - * - * THE_FIELD is a field of the class to use for the next pointer in the - * free list data structure. It can be of any type, but must have enough - * space to hold a pointer. - ************************************************************************/ -#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(THE_CLASS,THE_FIELD) \ -private:\ - static unsigned C_MACROS__CHUNK_SIZE;\ - static unsigned C_MACROS__BLOCK_SIZE;\ - static void *C_MACROS__freelist;\ - static bool C_MACROS__initialized;\ - static char *C_MACROS__next_free_block;\ - static char *C_MACROS__end_of_current_chunk;\ - \ - static void C_MACROS__allocate_new_chunk();\ -\ -public:\ - static void C_MACROS__init_chunks() {\ - if (!C_MACROS__initialized) {\ - C_MACROS__allocate_new_chunk();\ - C_MACROS__initialized = true;\ - }\ - }\ -\ - static void *operator new(size_t size, void *h = NULL);\ - static void operator delete(void *ptr)\ - - -/************************************************************************ - * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_CC() - * Aaron Stump, 6/11/99 - * - * ABSTRACT: This macro should be called exactly once in a .cc file - * for the class THE_CLASS to add chunking memory management for the - * class. This macro should be called with the same value for - * THE_CLASS as was used in calling - * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H in the body of the - * declaration of THE_CLASS. THE_CHUNK_SIZE is the number of blocks - * of memory to get at once using malloc(). A block is the portion - * of memory needed for one instance of THE_CLASS. - * - * - * IMPLEMENTATION: - ************************************************************************ - * FUNCTION: allocate_new_chunk() - * Aaron Stump, 6/8/99 - * - * ABSTRACT: This method allocates a new chunk of memory to use for - * allocating instances of THE_CLASS. - ************************************************************************ - * FUNCTION: new() - * Aaron Stump, 6/8/99 - * - * ABSTRACT: This allocator uses chunks for more efficient allocation. - ************************************************************************ - * FUNCTION: delete() - * Aaron Stump, 6/8/99 - * - * ABSTRACT: This delete() puts the chunk pointed to by ptr on the - * freelist. - ************************************************************************ - * Chunking_Memory_Management_Initializer and its static instance are used - * to call the static init_chunks() method for THE_CLASS. - ************************************************************************/ -#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(THE_CLASS,THE_FIELD,THE_CHUNK_SIZE) \ -unsigned THE_CLASS::C_MACROS__CHUNK_SIZE = THE_CHUNK_SIZE;\ -\ -unsigned THE_CLASS::C_MACROS__BLOCK_SIZE = sizeof(THE_CLASS);\ -\ -void * THE_CLASS::C_MACROS__freelist = NULL;\ -char * THE_CLASS::C_MACROS__next_free_block = NULL;\ -char * THE_CLASS::C_MACROS__end_of_current_chunk = NULL;\ -bool THE_CLASS::C_MACROS__initialized = false;\ -\ -void \ -THE_CLASS::C_MACROS__allocate_new_chunk() {\ -\ - unsigned tmp = C_MACROS__CHUNK_SIZE * C_MACROS__BLOCK_SIZE;\ - char *chunk = (char *)malloc(tmp);\ - \ - assert (chunk != NULL); \ -\ - C_MACROS__next_free_block = chunk;\ - C_MACROS__end_of_current_chunk = chunk + tmp;\ -}\ -\ -void * \ -THE_CLASS::operator new(size_t size, void *h) {\ - (void)size; /* size should always be _BLOCK_SIZE */\ -\ - if (h != NULL)\ - /* we're being told what memory we should use */\ - return h;\ -\ - char *new_block;\ -\ - if (C_MACROS__freelist) {\ - /* we have a block on the freelist that we can use */\ - new_block = (char *)C_MACROS__freelist; \ - C_MACROS__freelist = (void *)((THE_CLASS *)new_block)->THE_FIELD; \ - }\ - else {\ - /* we have to get a new block from a chunk (which we may */\ - /* have to allocate*/\ - \ - if (C_MACROS__next_free_block == C_MACROS__end_of_current_chunk)\ - C_MACROS__allocate_new_chunk();\ - \ - new_block = C_MACROS__next_free_block;\ - C_MACROS__next_free_block += C_MACROS__BLOCK_SIZE;\ - }\ - \ - return new_block;\ -}\ -\ -void \ -THE_CLASS::operator delete(void *ptr) {\ - void **f = (void **)&((THE_CLASS *)ptr)->THE_FIELD; \ - *f = C_MACROS__freelist; \ - C_MACROS__freelist = ptr; \ -} - -#endif - diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp deleted file mode 100644 index 48ebc5578..000000000 --- a/proofs/lfsc_checker/code.cpp +++ /dev/null @@ -1,1404 +0,0 @@ -#include "check.h" -#include "code.h" -#include - -#include "scccode.h" - -using namespace std; - -string *eat_str(const char *str, bool check_end = true) { - string *s = new string(); - char c, d; - while ((c = *str++)) { - d = our_getc(); - if (c != d) { - our_ungetc(d); - return s; - } - s->push_back(d); - } - - if (check_end && - (d = our_getc()) != ' ' && d != '(' && d != '\n' && d != '\t') { - our_ungetc(d); - return s; - } - - delete s; - return 0; -} - -SymSExpr *read_ctor() { - string id(prefix_id()); -#ifdef USE_HASH_TABLES - Expr *s = symbols[id]; - Expr *stp = symbol_types[id]; -#else - pair p = symbols->get(id.c_str()); - Expr *s = p.first; - Expr *stp = p.second; -#endif - - if (!stp) - report_error("Undeclared identifier parsing a pattern."); - - if (s->getclass() != SYMS_EXPR || ((SymExpr *)s)->val) - report_error("The head of a pattern is not a constructor."); - - s->inc(); - - return (SymSExpr *)s; -} - -Expr *read_case() { - eat_char('('); - Expr *pat = NULL; - vector vars; - -#ifdef USE_HASH_MAPS - vectorprevs; -#else - vector >prevs; -#endif - char d = non_ws(); - switch(d) { - case '(': { - // parse application - SymSExpr *s = read_ctor(); - pat = s; - char c; - while ((c = non_ws()) != ')') { - our_ungetc(c); - string varstr(prefix_id()); - SymSExpr *var = new SymSExpr(varstr); - vars.push_back(var); -#ifdef USE_HASH_MAPS - prevs.push_back(symbols[varstr]); - symbols[varstr] = var; -#else - prevs.push_back(symbols->insert(varstr.c_str(), - pair(var,NULL))); -#endif -#ifndef USE_FLAT_APP - pat = new CExpr(APP,pat,var); -#else - Expr* orig_pat = pat; - pat = Expr::make_app(pat,var); - if( orig_pat->getclass()==CEXPR ){ - orig_pat->dec(); - } -#endif - } - break; - } - // default case - case 'd': { - delete eat_str("efault"); - } - break; - case EOF: - report_error("Unexpected end of file parsing a pattern."); - break; - default: - // could be an identifier - our_ungetc(d); - pat = read_ctor(); - break; - } - - Expr *ret = read_code(); - if( pat ) - ret = new CExpr(CASE, pat, ret); - - for (int i = 0, iend = prevs.size(); i < iend; i++) { - string &s = vars[i]->s; -#ifdef USE_HASH_MAPS - symbols[s] = prevs[i]; -#else - symbols->insert(s.c_str(), prevs[i]); -#endif - } - - eat_char(')'); - - return ret; -} - -Expr *read_code() { - string *pref = NULL; - char d = non_ws(); - switch(d) { - case '(': - { - char c = non_ws(); - switch (c) - { - case 'd': - { - our_ungetc('d'); - pref = eat_str("do"); - if (pref) - break; - Expr *ret = read_code(); - while ((c = non_ws()) != ')') { - our_ungetc(c); - ret = new CExpr(DO,ret,read_code()); - } - return ret; - } - case 'f': - { - our_ungetc('f'); - pref = eat_str("fail"); - if (pref) - break; - - Expr *c = read_code(); - eat_char(')'); - - //do we need to check this??? - //if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val) - // report_error(string("\"fail\" must be used with a (undefined) base ") - // +string("type.\n1. the expression used: "+c->toString())); - - return new CExpr(FAIL, c); - } - case 'l': - { - our_ungetc('l'); - pref = eat_str("let"); - if (pref) - break; - - string id(prefix_id()); - SymSExpr *var = new SymSExpr(id); - - Expr *t1 = read_code(); - -#ifdef USE_HASH_MAPS - Expr *prev = symbols[id]; - symbols[id] = var; -#else - pair prev = - symbols->insert(id.c_str(), pair(var,NULL)); -#endif - - Expr *t2 = read_code(); - -#ifdef USE_HASH_MAPS - symbols[id] = prev; -#else - symbols->insert(id.c_str(), prev); -#endif - eat_char(')'); - return new CExpr(LET, var, t1, t2); - } - case 'i': - { - our_ungetc('i'); - pref = eat_str("ifmarked",false); - if (pref) - break; -#ifndef MARKVAR_32 - Expr *e1 = read_code(); - Expr *e2 = read_code(); - Expr *e3 = read_code(); - Expr *ret = new CExpr(IFMARKED, e1, e2, e3); -#else - int index = read_index(); - Expr *e1 = read_code(); - Expr *e2 = read_code(); - Expr *e3 = read_code(); - Expr *ret = NULL; - if( index>=1 && index<=32 ) - { - ret = new CExpr( IFMARKED, new IntExpr( index-1 ), e1, e2, e3 ); - } - else - { - std::cout << "Can't make IFMARKED with index = " << index << std::endl; - } - Expr::markedCount++; - //Expr *ret = new CExpr(IFMARKED, e1, e2, e3); -#endif - eat_char(')'); - return ret; - } - case 'm': - { - char c; - switch ((c = our_getc())) - { - case 'a': - { - char cc; - switch ((cc = our_getc())) { - case 't': - { - our_ungetc('t'); - pref = eat_str("tch"); - if (pref) { - pref->insert(0,"ma"); - break; - } - vector cases; - cases.push_back(read_code()); // the scrutinee - while ((c = non_ws()) != ')' && c != 'd') { - our_ungetc(c); - cases.push_back(read_case()); - } - if (cases.size() == 1) // counting scrutinee - report_error("A match has no cases."); - if (c == 'd') { - // we have a default case - //delete eat_str("efault"); - our_ungetc(c); - cases.push_back(read_case()); - } - return new CExpr(MATCH,cases); - } - case 'r': - { - our_ungetc('r'); - pref = eat_str("rkvar", false); - if (pref) { - pref->insert(0,"ma"); - break; - } - #ifndef MARKVAR_32 - Expr *ret = new CExpr(MARKVAR,read_code()); - #else - int index = read_index(); - CExpr* ret = NULL; - if( index>=1 && index<=32 ) - { - ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); - } - else - { - std::cout << "Can't make MARKVAR with index = " << index << std::endl; - } - Expr::markedCount++; - //Expr *ret = new CExpr(MARKVAR,read_code()); - #endif - - eat_char(')'); - return ret; - } - default: - our_ungetc(c); - pref = new string("ma"); - break; - } - } - case 'p': - { - our_ungetc('p'); - pref = eat_str("p_",false); - if (pref) { - pref->insert(0,"m"); - break; - } - char c = our_getc(); - switch(c) { - case 'a': - { - our_ungetc('a'); - pref = eat_str("add"); - if (pref) { - pref->insert(0,"mp_"); - break; - } - Expr* e1 = read_code(); - Expr* e2 = read_code(); - Expr *ret = new CExpr(ADD, e1, e2); - eat_char(')'); - return ret; - } - case 'n': - { - our_ungetc('n'); - pref = eat_str("neg"); - if (pref) { - pref->insert(0,"mp_"); - break; - } - - Expr *ret = new CExpr(NEG, read_code()); - eat_char(')'); - return ret; - } - case 'i': - { // mpz_if_neg - char c = our_getc(); - if( c=='f' ) - { - c = our_getc(); - switch( c ) - { - case 'n': { - our_ungetc('n'); - pref = eat_str("neg"); - if( pref ) { - pref->insert(0,"mp_if"); - break; - } - Expr* e1 = read_code(); - Expr* e2 = read_code(); - Expr* e3 = read_code(); - Expr* ret = new CExpr(IFNEG, e1, e2, e3 ); - eat_char(')'); - return ret; - } - case 'z': { - our_ungetc('z'); - pref = eat_str("zero"); - if( pref ) { - pref->insert(0,"mp_if"); - break; - } - Expr* e1 = read_code(); - Expr* e2 = read_code(); - Expr* e3 = read_code(); - Expr* ret = new CExpr(IFZERO, e1, e2, e3 ); - eat_char(')'); - return ret; - } - default: - our_ungetc(c); - pref = new string("mp_if"); - break; - } - } - else - { - our_ungetc(c); - pref = new string("mp_i"); - break; - } - } - case 'm': - { - our_ungetc('m'); - pref = eat_str("mul"); - if( pref ){ - pref->insert(0,"mp_"); - break; - } - Expr* e1 = read_code(); - Expr* e2 = read_code(); - Expr* ret = new CExpr(MUL, e1, e2 ); - eat_char(')'); - return ret; - } - case 'd': - { - our_ungetc('d'); - pref = eat_str("div"); - if( pref ){ - pref->insert(0,"mp_"); - break; - } - Expr* e1 = read_code(); - Expr* e2 = read_code(); - Expr* ret = new CExpr(DIV, e1, e2 ); - eat_char(')'); - return ret; - } - default: - our_ungetc(c); - pref = new string("mp_"); - break; - } - } - default: - our_ungetc(c); - pref = new string("m"); - break; - } - break; - } - case '~': { - Expr *e = read_code(); - if( e->getclass()==INT_EXPR ) - { - IntExpr *ee = (IntExpr *)e; - mpz_neg(ee->n, ee->n); - eat_char(')'); - return ee; - } - else if( e->getclass() == RAT_EXPR ) - { - RatExpr *ee = (RatExpr *)e; - mpq_neg(ee->n, ee->n); - eat_char(')'); - return ee; - } - else - { - report_error("Negative sign with expr that is not an int. literal."); - } - } - case 'c': - { - our_ungetc('c'); - pref = eat_str("compare"); - if (pref) - break; - Expr *e1 = read_code(); - Expr *e2 = read_code(); - Expr *e3 = read_code(); - Expr *e4 = read_code(); - eat_char(')'); - return new CExpr(COMPARE, e1, e2, e3, e4); - } - break; - case EOF: - report_error("Unexpected end of file."); - break; - default: - { // the application case - our_ungetc(c); - break; - } - } - // parse application - if (pref) - // we have eaten part of the name of an applied identifier - pref->append(prefix_id()); - else - pref = new string(prefix_id()); - - Expr *ret = progs[*pref]; - if (!ret) -#ifdef USE_HASH_TABLES - ret = symbols[*pref]; -#else - ret = symbols->get(pref->c_str()).first; -#endif - - if (!ret) - report_error(string("Undeclared identifier at head of an application: ") - +*pref); - - ret->inc(); - delete pref; - - while ((c = non_ws()) != ')') { - our_ungetc(c); -#ifndef USE_FLAT_APP - ret = new CExpr(APP,ret,read_code()); -#else - Expr* ke = read_code(); - Expr* orig_ret = ret; - ret = Expr::make_app(ret,ke); - if( orig_ret->getclass()==CEXPR ){ - orig_ret->dec(); - } -#endif - } - return ret; - } // end case '(' - case EOF: - report_error("Unexpected end of file."); - break; - case '_': - report_error("Holes may not be used in code."); - return NULL; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - case '8': - case '9': - { - our_ungetc(d); - string v; - char c; - while (isdigit(c = our_getc())) - v.push_back(c); - bool parseMpq = false; - if( c=='/' ) - { - parseMpq = true; - v.push_back(c); - while(isdigit(c = our_getc())) - v.push_back(c); - } - our_ungetc(c); - if( parseMpq ) - { - mpq_t num; - mpq_init(num); - if (mpq_set_str(num,v.c_str(),10) == -1 ) - report_error("Error reading a mpq numeral."); - - Expr* e = new RatExpr( num ); - return e; - } - else - { - mpz_t num; - if (mpz_init_set_str(num,v.c_str(),10) == -1) - report_error("Error reading a numeral."); - return new IntExpr(num); - } - } - default: - { - our_ungetc(d); - string id(prefix_id()); -#ifdef USE_HASH_MAPS - Expr *ret = symbols[id]; -#else - pair p = symbols->get(id.c_str()); - Expr *ret = p.first; -#endif - if (!ret) - ret = progs[id]; - if (!ret) - report_error(string("Undeclared identifier: ")+id); - ret->inc(); - return ret; - } - } - report_error("Unexpected operator in a piece of code."); - return 0; -} - -// the input is owned by the caller, the output by us (so do not dec it). -Expr *check_code(Expr *_e) { - CExpr *e = (CExpr *)_e; - switch (e->getop()) { - case NOT_CEXPR: - switch (e->getclass()) { - case INT_EXPR: - return statMpz; - case RAT_EXPR: - return statMpq; - case SYM_EXPR: { - report_error("Internal error: an LF variable is encountered in code"); - break; - } - case SYMS_EXPR: { -#ifdef USE_HASH_MAPS - Expr *tp = symbol_types[((SymSExpr *)e)->s]; -#else - Expr *tp = symbols->get(((SymSExpr *)e)->s.c_str()).second; -#endif - if (!tp) - report_error(string("A symbol is missing a type in a piece of code.") - +string("\n1. the symbol: ")+((SymSExpr *)e)->s); - return tp; - } - case HOLE_EXPR: - report_error("Encountered a hole unexpectedly in code."); - default: - report_error("Unrecognized form of expr in code."); - } - case APP: { -#ifdef USE_FLAT_APP - Expr* h = e->kids[0]->followDefs(); - vector argtps; - int counter = 1; - while( e->kids[counter] ) - { - argtps.push_back( check_code( e->kids[counter] ) ); - counter++; - } - int iend = counter-1; -#else - vector args; - Expr *h = (Expr *)e->collect_args(args); - - int iend = args.size(); - vector argtps(iend); - for (int i = 0; i < iend; i++) - argtps[i] = check_code(args[i]); -#endif - - Expr *tp = NULL; - if (h->getop() == PROG){ - tp = ((CExpr *)h)->kids[0]; - }else { -#ifdef USE_HASH_MAPS - tp = symbol_types[((SymSExpr *)h)->s]; -#else - tp = symbols->get(((SymSExpr *)h)->s.c_str()).second; -#endif - } - - if (!tp) - report_error(string("The head of an application is missing a type in ") - +string("code.\n1. the application: ")+e->toString()); - - tp = tp->followDefs(); - - if (tp->getop() != PI) - report_error(string("The head of an application does not have ") - +string("functional type in code.") - +string("\n1. the application: ")+e->toString()); - - CExpr *cur = (CExpr *)tp; - int i = 0; - while (cur->getop() == PI) { - if (i >= iend) - report_error(string("A function is not being fully applied in code.\n") - +string("1. the application: ")+e->toString() - +string("\n2. its (functional) type: ")+cur->toString()); - if( argtps[i]->getop()==APP ) - argtps[i] = ((CExpr*)argtps[i])->kids[0]; - if (argtps[i] != cur->kids[1]) { - char buf[1024]; - sprintf(buf,"%d",i); - report_error(string("Type mismatch for argument ") - + string(buf) - + string(" in application in code.\n") - + string("1. the application: ")+e->toString() - + string("\n2. the head's type: ")+tp->toString() -#ifdef USE_FLAT_APP - + string("\n3. the argument: ")+e->kids[i+1]->toString() -#else - + string("\n3. the argument: ")+args[i]->toString() -#endif - + string("\n4. computed type: ")+argtps[i]->toString() - + string("\n5. expected type: ") - +cur->kids[1]->toString()); - } - - //if (cur->kids[2]->free_in((SymExpr *)cur->kids[0])) - if( cur->get_free_in() ){ - cur->calc_free_in(); - //are you sure? - if( cur->get_free_in() ) - report_error(string("A dependently typed function is being applied in") - +string(" code.\n1. the application: ")+e->toString() - +string("\n2. the head's type: ")+tp->toString()); - //ok, reset the mark - cur->setexmark(); - } - - i++; - cur = (CExpr *)cur->kids[2]; - } - if (i < iend) - report_error(string("A function is being fully applied to too many ") - +string("arguments in code.\n") - +string("1. the application: ")+e->toString() - +string("\n2. the head's type: ")+tp->toString()); - - - return cur; - } - //is this right? - case MPZ: - return statType; - break; - case MPQ: - return statType; - break; - case DO: - check_code(e->kids[0]); - return check_code(e->kids[1]); - - case LET: { - SymSExpr * var = (SymSExpr *)e->kids[0]; - - Expr *tp1 = check_code(e->kids[1]); - -#ifdef USE_HASH_MAPS - Expr *prevtp = symbol_types[var->s]; - symbol_types[var->s] = tp1; -#else - pair prev = - symbols->insert(var->s.c_str(), pair(NULL,tp1)); -#endif - - Expr *tp2 = check_code(e->kids[2]); - -#ifdef USE_HASH_MAPS - symbol_types[var->s] = prevtp; -#else - symbols->insert(var->s.c_str(), prev); -#endif - - return tp2; - } - - case ADD: - case MUL: - case DIV: - { - Expr *tp0 = check_code(e->kids[0]); - Expr *tp1 = check_code(e->kids[1]); - - if (tp0 != statMpz && tp0 != statMpq ) - report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n") - +string("1. the argument: ")+e->kids[0]->toString() - +string("\n1. its type: ")+tp0->toString()); - - if (tp0 != tp1) - report_error(string("Arguments to mp_[arith] have differing types.\n") - +string("1. argument 1: ")+e->kids[0]->toString() - +string("\n1. its type: ")+tp0->toString() - +string("2. argument 2: ")+e->kids[1]->toString() - +string("\n2. its type: ")+tp1->toString()); - - return tp0; - } - - case NEG: { - Expr *tp0 = check_code(e->kids[0]); - if (tp0 != statMpz && tp0 != statMpq ) - report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n") - +string("1. the argument: ")+e->kids[0]->toString() - +string("\n1. its type: ")+tp0->toString()); - - return tp0; - } - - case IFNEG: - case IFZERO: { - Expr *tp0 = check_code(e->kids[0]); - if (tp0 != statMpz && tp0 != statMpq) - report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n") - +string("1. the argument: ")+e->kids[0]->toString() - +string("\n1. its type: ")+tp0->toString()); - - SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]); - SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]); - if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2) - report_error(string("\"mp_if\" used with expressions that do not ") - +string("have equal simple datatypes\nfor their types.\n") - +string("0. 0'th expression: ")+e->kids[0]->toString() - +string("\n1. first expression: ")+e->kids[1]->toString() - +string("\n2. second expression: ")+e->kids[2]->toString() - +string("\n3. first expression's type: ")+tp1->toString() - +string("\n4. second expression's type: ")+tp2->toString()); - return tp1; - } - - case FAIL: { - Expr *tp = check_code(e->kids[0]); - if (tp != statType) - report_error(string("\"fail\" is used with an expression which is ") - +string("not a type.\n1. the expression :") - +e->kids[0]->toString() - +string("\n2. its type: ")+tp->toString()); - return e->kids[0]; - } - case MARKVAR: { - SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); - - Expr* tptp = NULL; - - if (tp->getclass() == SYMS_EXPR && !tp->val){ -#ifdef USE_HASH_MAPS - tptp = symbol_types[tp->s]; -#else - tptp = symbols->get(tp->s.c_str()).second; -#endif - } - - if (!tptp->isType( statType )){ - string errstr = (string("\"markvar\" is used with an expression which ") - +string("cannot be a lambda-bound variable.\n") - +string("1. the expression :") - +e->kids[1]->toString() - +string("\n2. its type: ")+tp->toString()); - report_error(errstr); - } - - return tp; - } - - case IFMARKED: - { - SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); - - Expr* tptp = NULL; - - if (tp->getclass() == SYMS_EXPR && !tp->val){ -#ifdef USE_HASH_MAPS - tptp = symbol_types[tp->s]; -#else - tptp = symbols->get(tp->s.c_str()).second; -#endif - } - - if (!tptp->isType( statType ) ){ - string errstr = (string("\"ifmarked\" is used with an expression which ") - +string("cannot be a lambda-bound variable.\n") - +string("1. the expression :") - +e->kids[1]->toString() - +string("\n2. its type: ")+tp->toString()); - report_error(errstr); - } - - SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[2]); - SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[3]); - if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2) - report_error(string("\"ifmarked\" used with expressions that do not ") - +string("have equal simple datatypes\nfor their types.\n") - +string("0. 0'th expression: ")+e->kids[1]->toString() - +string("\n1. first expression: ")+e->kids[2]->toString() - +string("\n2. second expression: ")+e->kids[3]->toString() - +string("\n3. first expression's type: ")+tp1->toString() - +string("\n4. second expression's type: ")+tp2->toString()); - return tp1; - } - case COMPARE: - { - SymSExpr *tp0 = (SymSExpr *)check_code(e->kids[0]); - if (tp0->getclass() != SYMS_EXPR || tp0->val){ - string errstr0 = (string("\"compare\" is used with a first expression which ") - +string("cannot be a lambda-bound variable.\n") - +string("1. the expression :") - +e->kids[0]->toString() - +string("\n2. its type: ")+tp0->toString()); - report_error(errstr0); - } - - SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]); - - if (tp1->getclass() != SYMS_EXPR || tp1->val){ - string errstr1 = (string("\"compare\" is used with a second expression which ") - +string("cannot be a lambda-bound variable.\n") - +string("1. the expression :") - +e->kids[1]->toString() - +string("\n2. its type: ")+tp1->toString()); - report_error(errstr1); - } - - SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]); - SymSExpr *tp3 = (SymSExpr *)check_code(e->kids[3]); - if (tp2->getclass() != SYMS_EXPR || tp2->val || tp2 != tp3) - report_error(string("\"compare\" used with expressions that do not ") - +string("have equal simple datatypes\nfor their types.\n") - +string("\n1. first expression: ")+e->kids[2]->toString() - +string("\n2. second expression: ")+e->kids[3]->toString() - +string("\n3. first expression's type: ")+tp2->toString() - +string("\n4. second expression's type: ")+tp3->toString()); - return tp2; - } - case MATCH: - { - SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]); - Expr *tptp = NULL; - if (scruttp->getclass() == SYMS_EXPR && !scruttp->val){ -#ifdef USE_HASH_MAPS - tptp = symbol_types[scruttp->s]; -#else - tptp = symbols->get(scruttp->s.c_str()).second; -#endif - } - if (!tptp->isType( statType )){ - string errstr = (string("The scrutinee of a match is not ") - +string("a plain piece of data.\n") - +string("1. the scrutinee: ") - +e->kids[0]->toString() - +string("\n2. its type: ")+scruttp->toString()); - report_error(errstr); - } - - int i = 1; - Expr **cur = &e->kids[i]; - Expr *mtp = NULL; - Expr *c_or_default; - CExpr *c; - while ((c_or_default = *cur++)) { - Expr *tp = NULL; - CExpr *pat = NULL; - if (c_or_default->getop() != CASE) - // this is the default of the MATCH - tp = check_code(c_or_default); - else { - // this is a CASE of the MATCH - c = (CExpr *)c_or_default; - pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR - if (pat->getclass() == SYMS_EXPR) - tp = check_code(c->kids[1]); - else { - // extend type context and then check the body of the case -#ifdef USE_HASH_MAPS - vectorprevs; -#else - vector >prevs; -#endif - vector vars; - SymSExpr *ctor = (SymSExpr *)pat->collect_args(vars); -#ifdef USE_HASH_MAPS - CExpr *ctortp = (CExpr *)symbol_types[ctor->s]; -#else - CExpr *ctortp = (CExpr *)symbols->get(ctor->s.c_str()).second; -#endif - CExpr *curtp = ctortp; - for (int i = 0, iend = vars.size(); i < iend; i++) { - if ( curtp->followDefs()->getop() != PI) - report_error(string("Too many arguments to a constructor in") - +string(" a pattern.\n1. the pattern: ") - +pat->toString() - +string("\n2. the head's type: " - +ctortp->toString())); -#ifdef USE_HASH_MAPS - prevs.push_back(symbol_types[((SymSExpr *)vars[i])->s]); - symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1]; -#else - prevs.push_back - (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), - pair(NULL, - ((CExpr *)(curtp->followDefs()))->kids[1]))); -#endif - curtp = (CExpr *)((CExpr *)(curtp->followDefs()))->kids[2]; - } - - tp = check_code(c->kids[1]); - - for (int i = 0, iend = prevs.size(); i < iend; i++) { -#ifdef USE_HASH_MAPS - symbol_types[((SymSExpr *)vars[i])->s] = prevs[i]; -#else - symbols->insert(((SymSExpr *)vars[i])->s.c_str(), prevs[i]); -#endif - } - } - } - - // check that the type for the body of this case -- or the default value -- - // matches the type for the previous case if we had one. - - if (!mtp) - mtp = tp; - else - if (mtp != tp) - report_error(string("Types for bodies of match cases or the default differ.") - +string("\n1. type for first case's body: ") - +mtp->toString() - +(pat == NULL ? string("\n2. type for the default") - : (string("\n2. type for the body of case for ") - +pat->toString())) - +string(": ")+tp->toString()); - - } - - return mtp; - } - } // end switch - - report_error("Type checking an unrecognized form of code (internal error)."); - return NULL; -} - -bool dbg_prog; -bool run_scc; -int dbg_prog_indent_lvl = 0; - -void dbg_prog_indent(std::ostream &os) { - for (int i = 0; i < dbg_prog_indent_lvl; i++) - os << " "; -} - -Expr *run_code(Expr *_e) { - start_run_code: - CExpr *e = (CExpr *)_e; - if( e ) - { - //std::cout << ". "; - //e->print( std::cout ); - //std::cout << std::endl; - //std::cout << e->getop() << " " << e->getclass() << std::endl; - } - switch (e->getop()) { - case NOT_CEXPR: - switch(e->getclass()) { - case INT_EXPR: - case RAT_EXPR: - e->inc(); - return e; - case HOLE_EXPR: { - Expr *tmp = e->followDefs(); - if (tmp == e) - report_error("Encountered an unfilled hole running code."); - tmp->inc(); - return tmp; - } - case SYMS_EXPR: - case SYM_EXPR: { - Expr *tmp = e->followDefs(); - //std::cout << "follow def = "; - //tmp->print( std::cout ); - //std::cout << std::endl; - if (tmp == e) { - e->inc(); - return e; - } - tmp->inc(); - return tmp; - } - } - case FAIL: - return NULL; - case DO: { - Expr *tmp = run_code(e->kids[0]); - if (!tmp) - return NULL; - tmp->dec(); - _e = e->kids[1]; - goto start_run_code; - } - case LET: { - Expr *r0 = run_code(e->kids[1]); - if (!r0) - return NULL; - SymExpr *var = (SymExpr *)e->kids[0]; - Expr *prev = var->val; - var->val = r0; - Expr *r1 = run_code(e->kids[2]); - var->val = prev; - r0->dec(); - return r1; - } - case ADD: - case MUL: - case DIV: - { - Expr *r1 = run_code(e->kids[0]); - if (!r1) - return NULL; - Expr *r2 = run_code(e->kids[1]); - if (!r2) - return NULL; - if( r1->getclass()==INT_EXPR && r2->getclass()==INT_EXPR ) - { - mpz_t r; - mpz_init(r); - if( e->getop()==ADD ) - mpz_add(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); - else if( e->getop()==MUL ) - mpz_mul(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); - else if( e->getop()==DIV ) - mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); - r1->dec(); - r2->dec(); - return new IntExpr(r); - } - else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR ) - { - mpq_t q; - mpq_init(q); - if( e->getop()==ADD ) - mpq_add(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); - else if( e->getop()==MUL ) - mpq_mul(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); - else if( e->getop()==DIV ) - mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); - r1->dec(); - r2->dec(); - return new RatExpr(q); - } - else - { - //std::cout << "An arithmetic operation failed. " << r1->getclass() << " " << r2->getclass() << std::endl; - r1->dec(); - r2->dec(); - return NULL; - } - } - case NEG: { - Expr *r1 = run_code(e->kids[0]); - if (!r1) - return NULL; - if (r1->getclass() == INT_EXPR) { - mpz_t r; - mpz_init(r); - mpz_neg(r, ((IntExpr *)r1)->n); - r1->dec(); - return new IntExpr(r); - } - else if( r1->getclass() == RAT_EXPR ) { - mpq_t q; - mpq_init(q); - mpq_neg(q, ((RatExpr *)r1)->n); - r1->dec(); - return new RatExpr(q); - } - else - { - std::cout << "An arithmetic negation failed. " << r1->getclass() << std::endl; - //((SymSExpr*)r1)->val->print( std::cout ); - std::cout << ((SymSExpr*)r1)->val << std::endl; - r1->dec(); - return NULL; - } - } - case IFNEG: - case IFZERO:{ - Expr *r1 = run_code(e->kids[0]); - if (!r1) - return NULL; - - bool cond = true; - if( r1->getclass() == INT_EXPR ){ - if( e->getop() == IFNEG ) - cond = mpz_sgn( ((IntExpr *)r1)->n )<0; - else if( e->getop() == IFZERO ) - cond = mpz_sgn( ((IntExpr *)r1)->n )==0; - }else if( r1->getclass() == RAT_EXPR ){ - if( e->getop() == IFNEG ) - cond = mpq_sgn( ((RatExpr *)r1)->n )<0; - else if( e->getop() == IFZERO ) - cond = mpq_sgn( ((RatExpr *)r1)->n )==0; - } - else - { - std::cout << "An arithmetic if-expression failed. " << r1->getclass() << std::endl; - r1->dec(); - return NULL; - } - r1->dec(); - - - if( cond ) - _e = e->kids[1]; - else - _e = e->kids[2]; - goto start_run_code; - } - case IFMARKED: { - Expr *r1 = run_code(e->kids[1]); - if (!r1) - return NULL; - if(r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR ){ - r1->dec(); - return NULL; - } -#ifndef MARKVAR_32 - if (r1->getexmark()) { -#else - if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) ){ -#endif - r1->dec(); - _e = e->kids[2]; - goto start_run_code; - } - // else - r1->dec(); - _e = e->kids[3]; - goto start_run_code; - } - case COMPARE: - { - Expr *r1 = run_code(e->kids[0]); - if (!r1) - return NULL; - if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) { - r1->dec(); - return NULL; - } - Expr *r2 = run_code(e->kids[1]); - if (!r2) - return NULL; - if (r2->getclass() != SYM_EXPR && r2->getclass() != SYMS_EXPR) { - r2->dec(); - return NULL; - } - if( r1dec(); - _e = e->kids[2]; - goto start_run_code; - } - //else - r2->dec(); - _e = e->kids[3]; - goto start_run_code; - } - case MARKVAR: { - Expr *r1 = run_code(e->kids[1]); - if (!r1) - return NULL; - if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) { - r1->dec(); - return NULL; - } -#ifndef MARKVAR_32 - if (r1->getexmark()) - r1->clearexmark(); - else - r1->setexmark(); -#else - if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) ) - ((SymExpr*)r1)->clearmark( ((IntExpr*)e->kids[0])->get_num() ); - else - ((SymExpr*)r1)->setmark( ((IntExpr*)e->kids[0])->get_num() ); -#endif - return r1; - } - case MATCH: { - Expr *scrut = run_code(e->kids[0]); - if (!scrut) - return 0; - vector args; - Expr *hd = scrut->collect_args(args); - Expr **cases = &e->kids[1]; - // CExpr *c; - Expr *c_or_default; - while ((c_or_default = *cases++)) { - - if (c_or_default->getop() != CASE){ - //std::cout << "run the default " << std::endl; - //c_or_default->print( std::cout ); - // this is the default of the MATCH - return run_code(c_or_default); - } - - // this is a CASE of the MATCH - CExpr *c = (CExpr *)c_or_default; - Expr *p = c->kids[0]; - if (hd == p->get_head()) { - vector vars; - p->collect_args(vars); - int jend = args.size(); - vector old_vals(jend); - for (int j = 0; j < jend; j++) { - SymExpr *var = (SymExpr *)vars[j]; - old_vals[j] = var->val; - var->val = args[j]; - args[j]->inc(); - } - scrut->dec(); - Expr *ret = run_code(c->kids[1] /* the body of the case */); - for (int j = 0; j < jend; j++) { - ((SymExpr *)vars[j])->val = old_vals[j]; - args[j]->dec(); - } - return ret; - } - } - break; - } - case APP: { - Expr *tmp = e->whr(); - if (e != tmp) { - _e = tmp; - goto start_run_code; - } - - // e is in weak head normal form - - vector args; - Expr *hd = e->collect_args(args); - for (int i = 0, iend = args.size(); i < iend; i++) - if (!(args[i] = run_code(args[i]))) { - for (int j = 0; j < i; j++) - args[j]->dec(); - return NULL; - } - if (hd->getop() != PROG) { - hd->inc(); - Expr *tmp = Expr::build_app(hd,args); - return tmp; - } - - assert(hd->getclass() == CEXPR); - CExpr *prog = (CExpr *)hd; - assert(prog->kids[1]->getclass() == CEXPR); - Expr **cur = ((CExpr *)prog->kids[1])->kids; - vector old_vals; - SymExpr *var; - int i = 0; - - if( run_scc && e->get_head( false )->getclass()==SYMS_EXPR ) - { - //std::cout << "running " << ((SymSExpr*)e->get_head( false ))->s.c_str() << " with " << (int)args.size() << " arguments" << std::endl; -//#ifndef USE_FLAT_APP -// for( int a=0; a<(int)args.size(); a++ ) -// { -// args[a] = CExpr::convert_to_flat_app( args[a] ); -// } -//#endif - Expr *ret = run_compiled_scc( e->get_head( false ), args ); - for (int i = 0, iend = args.size(); i < iend; i++) { - args[i]->dec(); - } -//#ifndef USE_FLAT_APP -// ret = CExpr::convert_to_tree_app( ret ); -//#endif - //ret->inc(); - return ret; - } - else - { - while((var = (SymExpr *)*cur++)) { - // Check whether not enough arguments were supplied - if (i >= args.size()) { - for (size_t i = 0; i < args.size(); i++) { - args[i]->dec(); - } - return NULL; - } - - old_vals.push_back(var->val); - var->val = args[i++]; - } - - // Check whether too many arguments were supplied - if (i < args.size()) { - for (size_t i = 0; i < args.size(); i++) { - args[i]->dec(); - } - return NULL; - } - - if (dbg_prog) { - dbg_prog_indent(cout); - cout << "["; - e->print(cout); - cout << "\n"; - } - dbg_prog_indent_lvl++; - - Expr *ret = run_code(prog->kids[2]); - - dbg_prog_indent_lvl--; - if (dbg_prog) { - dbg_prog_indent(cout); - cout << "= "; - if (ret) - ret->print(cout); - else - cout << "fail"; - cout << "]\n"; - } - - cur = ((CExpr *)prog->kids[1])->kids; - i = 0; - while((var = (SymExpr *)*cur++)) { - assert(i < args.size()); - args[i]->dec(); - var->val = old_vals[i++]; - } - return ret; - } - } - } // end switch - return NULL; -} - -int read_index() -{ - int index = 1; - string v; - char c; - while (isdigit(c = our_getc())) - v.push_back(c); - our_ungetc(c); - if( v.length()>0 ) - { - index = atoi( v.c_str() ); - } - return index; -} diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h deleted file mode 100644 index 9d00a6378..000000000 --- a/proofs/lfsc_checker/code.h +++ /dev/null @@ -1,15 +0,0 @@ -#ifndef SC2_CODE_H -#define SC2_CODE_H - -#include "expr.h" - -Expr *read_code(); -Expr *check_code(Expr *); // compute the type for the given code -Expr *run_code(Expr *); - -int read_index(); - -extern bool dbg_prog; -extern bool run_scc; - -#endif diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 deleted file mode 120000 index 0543a154f..000000000 --- a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 +++ /dev/null @@ -1 +0,0 @@ -../../../config/ax_cxx_compile_stdcxx.m4 \ No newline at end of file diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 deleted file mode 120000 index 77adcd7a9..000000000 --- a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 +++ /dev/null @@ -1 +0,0 @@ -../../../config/ax_cxx_compile_stdcxx_11.m4 \ No newline at end of file diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac deleted file mode 100644 index 9ef902237..000000000 --- a/proofs/lfsc_checker/configure.ac +++ /dev/null @@ -1,51 +0,0 @@ -# -*- Autoconf -*- -# Process this file with autoconf to produce a configure script. - -AC_PREREQ([2.61]) -AC_INIT([lfsc-checker], [1.0], [cvc-bugs@cs.nyu.edu]) -AC_CONFIG_SRCDIR([libwriter.h]) -AC_CONFIG_AUX_DIR([config]) -AC_CONFIG_MACRO_DIR([config]) -AC_CONFIG_HEADERS([config.h]) -AM_INIT_AUTOMAKE([1.11 foreign no-define tar-pax]) -LT_INIT - -AC_CANONICAL_BUILD -AC_CANONICAL_HOST -AC_CANONICAL_TARGET - -m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) - -# on by default -AM_MAINTAINER_MODE([enable]) - -# turn off static lib building by default -AC_ENABLE_SHARED -AC_DISABLE_STATIC - -# Checks for programs. -AC_PROG_CXX -AC_PROG_CC - -# C++11 support in the compiler is now mandatory. Check for support and add -# switches if necessary. -AX_CXX_COMPILE_STDCXX_11([ext], [mandatory]) - -# Checks for libraries. -# FIXME: Replace `main' with a function in `-lgmp': -AC_CHECK_LIB([gmp], [__gmpz_init]) - -# Checks for header files. -AC_CHECK_HEADERS([stdlib.h string.h]) - -# Checks for typedefs, structures, and compiler characteristics. -AC_HEADER_STDBOOL -AC_C_INLINE -AC_TYPE_SIZE_T - -# Checks for library functions. -AC_FUNC_MALLOC -AC_CHECK_FUNCS([strdup]) - -AC_CONFIG_FILES([Makefile]) -AC_OUTPUT diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp deleted file mode 100644 index 8c8120edb..000000000 --- a/proofs/lfsc_checker/expr.cpp +++ /dev/null @@ -1,986 +0,0 @@ -#include "expr.h" -#include -#include -#ifdef _MSC_VER -#include -#endif -#include "check.h" - -using namespace std; - -int HoleExpr::next_id = 0; -int Expr::markedCount = 0; - -C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768); - -//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768); - -#define USE_HOLE_PATH_COMPRESSION - -void Expr::debug() { - print(cout); - /* - cout << "\nAt " << this << "\n"; - cout << "marked = " << getmark() << "\n"; - */ - cout << "\n"; - cout.flush(); -} - -bool destroy_progs = false; - -#define destroydec(rr) \ - do { \ - Expr *r = rr; \ - int ref = r->data >> 9; \ - ref = ref - 1; \ - if (ref == 0) { \ - _e = r; \ - goto start_destroy; \ - } \ - else \ - r->data = (ref << 9) | (r->data & 511); \ - } while(0) - -//removed from below "ref = ref -1;": r->debugrefcnt(ref,DEC); - -void Expr::destroy(Expr *_e, bool dec_kids) { - start_destroy: - switch (_e->getclass()) { - case INT_EXPR: - delete (IntExpr *)_e; - break; - case SYMS_EXPR: { - SymSExpr *e = (SymSExpr *)_e; - if (e->val && e->val->getop() != PROG) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case SYM_EXPR: { - SymExpr *e = (SymExpr *)_e; - if (e->val && e->val->getop() != PROG) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case HOLE_EXPR: { - HoleExpr *e = (HoleExpr *)_e; - if (e->val) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case CEXPR: { - CExpr *e = (CExpr *)_e; - if (dec_kids) { - Expr **cur = e->kids; - Expr *tmp; - while((tmp = *cur++)) { - if (*cur) - tmp->dec(); - else { - delete e; - destroydec(tmp); - break; - } - } - } - else - delete e; - break; - } - } -} - -Expr *Expr::clone() { - switch (getclass()) { - case INT_EXPR: - case RAT_EXPR: - inc(); - return this; - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *e = (SymExpr *)this; - if (e->val) - if (e->val->getop() != PROG) - return e->val->clone(); - e->inc(); - return e; - } - case HOLE_EXPR: { - HoleExpr *e = (HoleExpr *)this; - if (e->val) - return e->val->clone(); - e->inc(); - return e; - } - case CEXPR: { - CExpr *e = (CExpr *)this; - int op = e->getop(); - switch(op) { - case LAM: { -#ifdef DEBUG_SYM_NAMES - SymSExpr *var = (SymSExpr *)e->kids[0]; - SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); -#else - SymExpr *var = (SymExpr *)e->kids[0]; - SymExpr *newvar = new SymExpr(*var); -#endif - Expr *prev = var->val; - var->val = newvar; - Expr *bod = e->kids[1]->clone(); - var->val = prev; - return new CExpr(LAM,newvar,bod); - } - case PI: { -#ifdef DEBUG_SYM_NAMES - SymSExpr *var = (SymSExpr *)e->kids[0]; - SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); -#else - SymExpr *var = (SymExpr *)e->kids[0]; - SymExpr *newvar = new SymExpr(*var); -#endif - Expr *tp = e->kids[1]->clone(); - Expr *prev = var->val; - var->val = newvar; - Expr *bod = e->kids[2]->clone(); - var->val = prev; - Expr* ret = new CExpr(PI,newvar,tp,bod); - if( data&256 ) - ret->data |=256; - return ret; - } - default: { - Expr **cur = e->kids; - Expr *tmp; - int size = 0; - while((*cur++)) - size++; - Expr **kids = new Expr*[size+1]; - kids[size]=0; - cur = e->kids; - bool diff_kid = false; - int i = 0; - while((tmp = *cur++)) { - Expr *c = tmp->clone(); - diff_kid |= (c != tmp); - kids[i++] = c; - } - if (diff_kid) - return new CExpr(op, true /* dummy */, kids); - for (int i = 0, iend = size; i != iend; i++) - kids[i]->dec(); - delete[] kids; - e->inc(); - return e; - } - } - } - } - std::abort(); // should never be reached -} - - -Expr* Expr::build_app(Expr *hd, const std::vector &args, int start) { -#ifndef USE_FLAT_APP - Expr *ret = hd; - for (int i = start, iend = args.size(); i < iend; i++) - ret = new CExpr(APP,ret,args[i]); - return ret; -#else - if( start>=(int)args.size() ) - return hd; - else - { - Expr **kids = new Expr *[args.size() - start + 2]; - kids[0] = hd; - for (int i = start, iend = args.size(); i < iend; i++) - kids[i - start + 1] = args[i]; - kids[args.size() - start + 1] = NULL; - return new CExpr(APP, true /* dummy */, kids); - } -#endif -} - -Expr* Expr::make_app(Expr* e1, Expr* e2 ) -{ - //std::cout << "make app from "; - //e1->print( std::cout ); - //std::cout << " "; - //e2->print( std::cout ); - //std::cout << std::endl; - CExpr *ret; - if( e1->getclass()==CEXPR ){ - int counter = 0; - while( ((CExpr*)e1)->kids[counter] ){ - counter++; - } - Expr **kids = new Expr *[counter + 2]; - counter = 0; - while( ((CExpr*)e1)->kids[counter] ){ - kids[counter] = ((CExpr *)e1)->kids[counter]; - kids[counter]->inc(); - counter++; - } - kids[counter] = e2; - kids[counter + 1] = NULL; - ret = new CExpr(APP, true /* dummy */, kids); - }else{ - ret = new CExpr( APP, e1, e2 ); - } - //ret->print( std::cout ); - //std::cout << std::endl; - return ret; -} - -int Expr::cargCount = 0; - -Expr *Expr::collect_args(std::vector &args, bool follow_defs) { - //cargCount++; - //if( cargCount%1000==0) - //std::cout << cargCount << std::endl; -#ifndef USE_FLAT_APP - CExpr *e = (CExpr *)this; - args.reserve(16); - while( e->getop() == APP ) { - args.push_back(e->kids[1]); - e = (CExpr *)e->kids[0]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - std::reverse(args.begin(),args.end()); - return e; -#else - CExpr *e = (CExpr *)this; - args.reserve(16); - if( e->getop()==APP ){ - int counter = 1; - while( e->kids[counter] ) { - args.push_back(e->kids[counter]); - counter++; - } - e = (CExpr*)e->kids[0]; - } - if (follow_defs) - return e->followDefs(); - else - return e; -#endif -} - -Expr *Expr::get_head(bool follow_defs) const { - CExpr *e = (CExpr *)this; - while( e->getop() == APP ) { - e = (CExpr *)e->kids[0]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - return e; -} - -Expr *Expr::get_body(int op, bool follow_defs) const { - CExpr *e = (CExpr *)this; - while( e->getop() == op ) { - e = (CExpr *)e->kids[2]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - return e; -} - -// if the return value is different from this, then it is a new reference -Expr *CExpr::whr() { - vector args; - if (get_head()->getop() == LAM) { - CExpr *head = (CExpr *)collect_args(args, true); - Expr *cloned_head; - if (head->cloned()) { - // we must clone - head = (CExpr *)head->clone(); - cloned_head = head; - } - else { - head->setcloned(); - cloned_head = 0; - } - int i = 0; - int iend = args.size(); - - /* we will end up incrementing the ref count for all the args, - since each is either pointed to by a var (following a - beta-reduction), or else just an argument in the new - application we build below. */ - - do { - Expr *tmp = args[i++]->followDefs(); - ((SymExpr *)head->kids[0])->val = tmp; - tmp->inc(); - head = (CExpr *)head->kids[1]; - } while(head->getop() == LAM && i < iend); - for (; i < iend; i++) - args[i]->inc(); - head->inc(); - if (cloned_head) - cloned_head->dec(); - return build_app(head,args,i); - } - else - return this; -} - -Expr* CExpr::convert_to_tree_app( Expr* e ) -{ - if( e->getop()==APP ) - { - std::vector< Expr* > kds; - int counter = 1; - while( ((CExpr*)e)->kids[counter] ) - { - kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) ); - counter++; - } - Expr* app = Expr::build_app( e->get_head(), kds ); - //app->inc(); - return app; - } - else - { - return e; - } -} - -Expr* CExpr::convert_to_flat_app( Expr* e ) -{ - if( e->getop()==APP ) - { - std::vector< Expr* > args; - Expr* hd = ((CExpr*)e)->collect_args( args ); - Expr **kids = new Expr *[args.size() + 2]; - kids[0] = hd; - for (size_t a = 0; a < args.size(); a++) { - kids[a + 1] = convert_to_flat_app(args[a]); - } - kids[args.size() + 1] = 0; - CExpr *nce = new CExpr(APP, true /* dummy */, kids); - nce->inc(); - return nce; - } - else - { - return e; - } -} - -bool Expr::defeq(Expr *e) { - /* we handle a few special cases up front, where this Expr might - equal e, even though they have different opclass (i.e., different - structure). */ - - if (this == e) - return true; - int op1 = getop(); - int op2 = e->getop(); - switch (op1) { - case ASCRIBE: - return ((CExpr *)this)->kids[0]->defeq(e); - case APP: { - Expr *tmp = ((CExpr *)this)->whr(); - if (tmp != this) { - bool b = tmp->defeq(e); - tmp->dec(); - return b; - } - if (get_head()->getclass() == HOLE_EXPR) { - vector args; - Expr *head = collect_args(args, true); - Expr *t = e; - t->inc(); - for (int i = 0, iend = args.size(); i < iend; i++) { - // don't worry about SYMS_EXPR's, since we should not be in code here. - if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark()) - /* we cannot fill the hole in this case. Either this is not - a variable or we are using a variable again. */ - return false; - SymExpr *v = (SymExpr *)args[i]; - - // we may have been mapping from expected var v to a computed var - Expr *tmp = (v->val ? v->val : v); - - tmp->inc(); - t = new CExpr(LAM, tmp, t); - args[i]->setexmark(); - } - for (int i = 0, iend = args.size(); i < iend; i++) - args[i]->clearexmark(); -#ifdef DEBUG_HOLES - cout << "Filling hole "; - head->debug(); - cout << "with "; - t->debug(); -#endif - ((HoleExpr *)head)->val = t; - return true; - } - break; - } - case NOT_CEXPR: - switch (getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)this; - if (h->val) - return h->val->defeq(e); -#ifdef DEBUG_HOLES - cout << "Filling hole "; - h->debug(); - cout << "with "; - e->debug(); -#endif -#ifdef USE_HOLE_PATH_COMPRESSION - Expr *tmp = e->followDefs(); -#else - Expr *tmp = e; -#endif - h->val = tmp; - tmp->inc(); - return true; - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)this; - if (s->val) - return s->val->defeq(e); - break; - } - } - break; - } - - switch (op2) { - case ASCRIBE: - return defeq(((CExpr *)e)->kids[0]); - case APP: { - Expr *tmp = ((CExpr *)e)->whr(); - if (tmp != e) { - bool b = defeq(tmp); - tmp->dec(); - return b; - } - break; - } - case NOT_CEXPR: - switch (e->getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)e; - if (h->val) - return defeq(h->val); - -#ifdef DEBUG_HOLES - cout << "Filling hole "; - h->debug(); - cout << "with "; - debug(); -#endif -#ifdef USE_HOLE_PATH_COMPRESSION - Expr *tmp = followDefs(); -#else - Expr *tmp = this; -#endif - h->val = tmp; - tmp->inc(); - return true; - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)e; - if (s->val) - return defeq(s->val); - break; - } - } - break; - } - - /* at this point, e1 and e2 must have the same opclass if they are - to be equal. */ - - if (op1 != op2) - return false; - - if (op1 == NOT_CEXPR) { - switch(getclass()) { - case INT_EXPR: { - IntExpr *i1 = (IntExpr *)this; - IntExpr *i2 = (IntExpr *)e; - return (mpz_cmp(i1->n,i2->n) == 0); - } - case RAT_EXPR: { - RatExpr *r1 = (RatExpr *)this; - RatExpr *r2 = (RatExpr *)e; - return (mpq_cmp(r1->n,r2->n) == 0); - } - case SYMS_EXPR: - case SYM_EXPR: - return (this == e); - } - } - - /* Now op1 and op2 must both be CExprs, and must have the same op to be - equal. */ - - CExpr *e1 = (CExpr *)this; - CExpr *e2 = (CExpr *)e; - - int last = 1; - switch (op1) { - case PI: - if (!e1->kids[1]->defeq(e2->kids[1])) - return false; - last++; - // fall through to LAM case - case LAM: { - - /* It is critical that we point e1's var. (v1) back to e2's (call - it v2). The reason this is critical is that we assume any - holes are in e1. So we could end up with (_ v1) = t. We wish - to fill _ in this case with (\ v2 t). If v2 pointed to v1, we - could not return (\ v1 t), because the fact that v2 points to - v1 would then be lost. - */ - SymExpr *v1 = (SymExpr *)e1->kids[0]; - Expr *prev_v1_val = v1->val; - v1->val = e2->kids[0]->followDefs(); - bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]); - v1->val = prev_v1_val; - return bodies_equal; - } - case APP: -#ifndef USE_FLAT_APP - return (e1->kids[0]->defeq(e2->kids[0]) && - e1->kids[1]->defeq(e2->kids[1])); -#else - { - int counter = 0; - while( e1->kids[counter] ){ - if( e1->kids[counter]!=e2->kids[counter] ){ - if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) - return false; - //--- optimization : replace child with equivalent pointer if was defeq - // Heuristic: prefer symbolic kids because they may be cheaper to - // deal with (e.g. in free_in()). - if (e2->kids[counter]->isSymbolic() || - (!e1->kids[counter]->isSymbolic() && - e1->kids[counter]->getrefcnt() < - e2->kids[counter]->getrefcnt())) { - e1->kids[counter]->dec(); - e2->kids[counter]->inc(); - e1->kids[counter] = e2->kids[counter]; - }else{ - e2->kids[counter]->dec(); - e1->kids[counter]->inc(); - e2->kids[counter] = e1->kids[counter]; - } - } - //--- - counter++; - } - return e2->kids[counter]==NULL; - } -#endif - case TYPE: - case KIND: - case MPZ: - // already checked that both exprs have the same opclass. - return true; - } // switch(op1) - - std::abort(); // never reached. -} - -int Expr::fiCounter = 0; - -bool Expr::_free_in(Expr *x, expr_ptr_set_t *visited) { - // fiCounter++; - // if( fiCounter%1==0 ) - // std::cout << fiCounter << std::endl; - if (visited->find(this) != visited->end()) { - return false; - } - - switch (getop()) { - case NOT_CEXPR: - switch (getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)this; - if (h->val) return h->val->_free_in(x, visited); - return (h == x); - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)this; - if (s->val && s->val->getclass() == HOLE_EXPR) - /* we do not need to follow the "val" pointer except in this - one case, when x is a hole (which we do not bother to check - here) */ - return s->val->_free_in(x, visited); - return (s == x); - } - case INT_EXPR: - return false; - } - break; - case LAM: - case PI: - if (x == ((CExpr *)this)->kids[0]) - return false; - // fall through - default: { - // must be a CExpr - assert(this->getclass() == CEXPR); - CExpr *e = (CExpr *)this; - Expr *tmp; - Expr **cur = e->kids; - visited->insert(this); - while ((tmp = *cur++)) - if (tmp->_free_in(x, visited)) return true; - return false; - } - } - std::abort(); // should not be reached -} - -void Expr::calc_free_in(){ - data &= ~256; - data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] ); -} - -string Expr::toString() { - ostringstream oss; - print(oss); - return oss.str(); -} - -static void print_kids(ostream &os, Expr **kids) { - Expr *tmp; - while ((tmp = *kids++)) { - os << " "; - tmp->print(os); - } -} - -static void print_vector(ostream &os, const vector &v) { - for(int i = 0, iend = v.size(); i < iend; i++) { - os << " "; - v[i]->print(os); - } -} - -void Expr::print(ostream &os) { - CExpr *e = (CExpr *)this; // for CEXPR cases - - //std::cout << e->getop() << " "; - /* -#ifdef DEBUG_REFCNT - os << "<"; - char tmp[10]; - sprintf(tmp,"%d",getrefcnt()); - os << tmp << "> "; -#endif -*/ - - switch(getop()) { - case NOT_CEXPR: { - switch(getclass()) { - case INT_EXPR: - { - IntExpr *e = (IntExpr *)this; - if (mpz_sgn(e->n) < 0) { - os << "(~ "; - mpz_t tmp; - mpz_init(tmp); - mpz_neg(tmp,e->n); - char *s = mpz_get_str(0,10,tmp); - os << s; - free(s); - mpz_clear(tmp); - os << ")"; - //os << "mpz"; - } - else { - char *s = mpz_get_str(0,10,e->n); - os << s; - free(s); - //os << "mpz"; - } - break; - } - case RAT_EXPR: - { - RatExpr *e = (RatExpr *)this; - char *s = mpq_get_str(0,10,e->n); - os << s; - if (mpq_sgn(e->n) < 0) { - os << "(~ "; - mpq_t tmp; - mpq_init(tmp); - mpq_neg(tmp,e->n); - char *s = mpq_get_str(0,10,tmp); - os << s; - free(s); - mpq_clear(tmp); - os << ")"; - } - else { - char *s = mpq_get_str(0,10,e->n); - os << s; - free(s); - } - break; - } -#ifndef DEBUG_SYM_NAMES - case SYM_EXPR: - { - SymExpr *e = (SymExpr *)this; - if (e->val) { - if (e->val->getop() == PROG) { - os << e; -#ifdef DEBUG_SYMS - os << "[PROG]"; -#endif - }else{ -#ifdef DEBUG_SYMS - os << e; - os << "[SYM "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - } - } - else - os << e; - break; - } -#else - case SYM_EXPR: /* if we are debugging sym names, then - SYM_EXPRs are really SymSExprs. */ -#endif - case SYMS_EXPR: { - SymSExpr *e = (SymSExpr *)this; - if (e->val) { - if (e->val->getop() == PROG) { - os << e->s; -#ifdef DEBUG_SYMS - os << "[PROG]"; -#endif - }else{ -#ifdef DEBUG_SYMS - os << e->s; - os << "[SYM "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - } - } - else - os << e->s; - break; - } - case HOLE_EXPR: - { - HoleExpr *e = (HoleExpr *)this; - if (e->val) { -#ifdef DEBUG_SYMS - os << "_" << "[HOLE "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - }else { - os << "_"; -#ifdef DEBUG_HOLE_NAMES - char tmp[100]; - sprintf(tmp,"%d",e->id); - os << "[ " << tmp << "]"; -#else - os << "[ " << e << "]"; -#endif - } - break; - } - default: - os << "; unrecognized form of expr"; - break; - } - break; - } // case NOT_CEXPR - case APP: { - os << "("; - vector args; - Expr *head = collect_args(args, false /* follow_defs */); - head->print(os); - print_vector(os, args); - os << ")"; - break; - } - case LAM: - os << "(\\"; - print_kids(os, e->kids); - os << ")"; - break; - case PI: - os << "(!"; - print_kids(os, e->kids); - os << ")"; - break; - case TYPE: - os << "type"; - break; - case KIND: - os << "kind"; - break; - case MPZ: - os << "mpz"; - break; - case MPQ: - os << "mpq"; - break; - case ADD: - os << "(mp_add"; - print_kids(os,e->kids); - os << ")"; - break; - case MUL: - os << "(mp_mul"; - print_kids(os,e->kids); - os << ")"; - break; - case DIV: - os << "(mp_div"; - print_kids(os,e->kids); - os << ")"; - break; - case NEG: - os << "(mp_neg"; - print_kids(os,e->kids); - os << ")"; - break; - case IFNEG: - os << "(ifneg"; - print_kids(os,e->kids); - os << ")"; - break; - case IFZERO: - os << "(ifzero"; - print_kids(os,e->kids); - os << ")"; - break; - case RUN: - os << "(run"; - print_kids(os,e->kids); - os << ")"; - break; - case PROG: - os << "(prog"; - print_kids(os,e->kids); - os << ")"; - break; - case PROGVARS: - os << "("; - print_kids(os,e->kids); - os << ")"; - break; - case MATCH: - os << "(match"; - print_kids(os,e->kids); - os << ")"; - break; - case CASE: - os << "("; - print_kids(os,e->kids); - os << ")"; - break; - case LET: - os << "(let"; - print_kids(os,e->kids); - os << ")"; - break; - case DO: - os << "(do"; - print_kids(os,e->kids); - os << ")"; - break; - case IFMARKED: - os << "(ifmarked"; - print_kids(os,e->kids); - os << ")"; - break; - case COMPARE: - os << "(compare"; - print_kids(os,e->kids); - os << ")"; - break; - case MARKVAR: - os << "(markvar"; - print_kids(os,e->kids); - os << ")"; - break; - case FAIL: - os << "(fail "; - print_kids(os, e->kids); - os << ")"; - break; - case ASCRIBE: - os << "(:"; - print_kids(os, e->kids); - os << ")"; - break; - default: - os << "; unrecognized form of expr(2) " << getop() << " " << getclass(); - } // switch(getop()) -} - -bool Expr::isType( Expr* statType ){ - Expr* typ = this; - while( typ!=statType ){ - if( typ->getop()==PI ){ - typ = ((CExpr*)typ)->kids[2]; - }else{ - return false; - } - } - return true; -} - -int SymExpr::symmCount = 0; -#ifdef MARKVAR_32 -int SymExpr::mark() -{ - if( mark_map.find( this )== mark_map.end() ) - { - symmCount++; - mark_map[this] = 0; - } - return mark_map[this]; -} -void SymExpr::smark( int m ) -{ - mark_map[this] = m; -} -#endif diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h deleted file mode 100644 index 0677533da..000000000 --- a/proofs/lfsc_checker/expr.h +++ /dev/null @@ -1,423 +0,0 @@ -#ifndef sc2__expr_h -#define sc2__expr_h - -#include -#include -#include -#include -#include -#include - -#include "chunking_memory_management.h" -#include "gmp.h" - -#define USE_FLAT_APP //AJR: off deprecated -#define MARKVAR_32 -//#define DEBUG_SYM_NAMES -//#define DEBUG_SYMS - -// Expr class -enum { CEXPR = 0, - INT_EXPR, - RAT_EXPR, - HOLE_EXPR, - SYM_EXPR, - SYMS_EXPR }; - -// operators for CExprs -enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR - APP, - PI, - LAM, - TYPE, - KIND, - ASCRIBE, - MPZ, - MPQ, - - PROG, - PROGVARS, - MATCH, - CASE, - PAT, - DO, - ADD, - MUL, - DIV, - NEG, - IFNEG, - IFZERO, - LET, - RUN, - FAIL, - MARKVAR, - IFMARKED, - COMPARE -}; - -class Expr; -class SymExpr; - -struct hashExprPtr { - size_t operator()(const Expr *x) const { - return reinterpret_cast(x); - } -}; - -struct eqExprPtr { - bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; } -}; - -typedef std::unordered_set expr_ptr_set_t; - -class Expr { -protected: - /* bits 0-2: Expr class - bits 3-7: operator - bit 8: a flag for already cloned, free_in calculation - bits 9-31: ref count*/ - int data; - - enum { INC, DEC, CREATE }; - void debugrefcnt(int ref, int what) { - std::cout << "["; - debug(); - switch(what) { - case INC: - std::cout << " inc to "; - break; - case DEC: - std::cout << " dec to "; - break; - case CREATE: - std::cout << " creating]\n"; - return; - } - char tmp[10]; - sprintf(tmp,"%d",ref); - std::cout << tmp << "]\n"; - } - - Expr(int _class, int _op) - : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) - { } - - bool _free_in(Expr *x, expr_ptr_set_t *visited); - - public: - virtual ~Expr() {} - - static int markedCount; - inline Expr* followDefs(); - inline int getclass() const { return data & 7; } - int getexmark() const { return data & 256; } - void setexmark() { data |= 256; } - void clearexmark() { data &= ~256; } - inline int getop() const { return (data >> 3) & 31; } - int cloned() const { return data & 256; } - void setcloned() { data |= 256; } - - inline int getrefcnt() { return data >> 9; } - inline void inc() { - int ref = getrefcnt(); - //static int iCounter = 0; - //iCounter++; - //if( iCounter%10000==0 ){ - // //print( std::cout ); - // std::cout << " " << ref << std::endl; - //} - ref = ref<4194303 ? ref + 1 : ref; -#ifdef DEBUG_REFCNT - debugrefcnt(ref,INC); -#endif - data = (ref << 9) | (data & 511); - } - static void destroy(Expr *, bool); - inline void dec(bool dec_kids = true) { - int ref = getrefcnt(); - ref = ref - 1; -#ifdef DEBUG_REFCNT - debugrefcnt(ref,DEC); -#endif - if (ref == 0) - destroy(this,dec_kids); - else - data = (ref << 9) | (data & 511); - } - - //must pass statType (the expr representing "type") to this function - bool isType( Expr* statType ); - - inline bool isDatatype() const { - return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ; - } - inline bool isArithTerm() const { - return getop() == ADD || getop() == NEG; - } - inline bool isSymbolic() const { - return getclass() == SYM_EXPR || getclass() == SYMS_EXPR; - } - - static Expr *build_app(Expr *hd, const std::vector &args, - int start = 0); - - static Expr *make_app(Expr* e1, Expr* e2 ); - - /* if this is an APP, return the head, and store the args in args. - If follow_defs is true, we proceed through defined heads; - otherwise not. */ - Expr *collect_args(std::vector &args, bool follow_defs = true); - - Expr *get_head(bool follow_defs = true) const; - - Expr *get_body(int op = PI, bool follow_defs = true) const; - - std::string toString(); - - void print(std::ostream &); - void debug(); - - /* check whether or not this expr is alpha equivalent to e. If this - expr contains unfilled holes, fill them as we go. We do not fill - holes in e. We do not take responsibility for the reference to - this nor the reference to e. */ - bool defeq(Expr *e); - - /* return a clone of this expr. All abstractions are really duplicated - in memory. Other expressions may not actually be duplicated in - memory, but their refcounts will be incremented. */ - Expr *clone(); - - // x can be a SymExpr or a HoleExpr. - bool free_in(Expr *x) { - expr_ptr_set_t visited; - return _free_in(x, &visited); - } - bool get_free_in() const { return data & 256; } - void calc_free_in(); - - static int cargCount; - static int fiCounter; -}; - -class CExpr : public Expr { -public: - C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(CExpr,kids); - - Expr **kids; - virtual ~CExpr() { - delete[] kids; - } - CExpr(int _op) : Expr(CEXPR, _op), kids() { - kids = new Expr *[1]; - kids[0] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() { - kids = new Expr *[2]; - kids[0] = e1; - kids[1] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - CExpr(int _op, Expr *e1, Expr *e2) - : Expr(CEXPR, _op), kids() { - kids = new Expr *[3]; - kids[0] = e1; - kids[1] = e2; - kids[2] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - CExpr(int _op, Expr *e1, Expr *e2, Expr *e3) - : Expr(CEXPR, _op), kids() { - kids = new Expr *[4]; - kids[0] = e1; - kids[1] = e2; - kids[2] = e3; - kids[3] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4) - : Expr(CEXPR, _op), kids() { - kids = new Expr *[5]; - kids[0] = e1; - kids[1] = e2; - kids[2] = e3; - kids[3] = e4; - kids[4] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - CExpr(int _op, const std::vector &_kids) - : Expr(CEXPR, _op), kids() { - int i, iend = _kids.size(); - kids = new Expr *[iend + 1]; - for (i = 0; i < iend; i++) - kids[i] = _kids[i]; - kids[i] = 0; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - - // _kids must be null-terminated. - CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) { - (void)dummy; -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - - Expr *whr(); - - static Expr* convert_to_tree_app( Expr* ce ); - static Expr* convert_to_flat_app( Expr* ce ); -}; - -class IntExpr : public Expr { - public: - mpz_t n; - virtual ~IntExpr() { - mpz_clear(n); - } - IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { - mpz_init_set(n,_n); -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() { - mpz_init_set_si( n, _n ); - } - - unsigned long int get_num() { return mpz_get_ui( n ); } -}; - -class RatExpr : public Expr { - public: - mpq_t n; - virtual ~RatExpr() { - mpq_clear(n); - } - RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { - mpq_init( n ); - mpq_set(n,_n); -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - mpq_canonicalize( n ); - } - RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() { - mpq_init( n ); - mpq_set_si( n, _n1, _n2 ); - mpq_canonicalize( n ); - } -}; - -class SymExpr : public Expr { - public: - Expr *val; // may be set by beta-reduction and clone(). - static int symmCount; - - SymExpr(std::string _s, int theclass = SYM_EXPR) - : Expr(theclass, 0), val(0) - { - (void)_s; -#ifdef DEBUG_REFCNT - if (theclass == SYM_EXPR) - debugrefcnt(1,CREATE); -#endif - } - SymExpr(const SymExpr &e, int theclass = SYM_EXPR) - : Expr(theclass, 0), val(0) - { - (void)e; -#ifdef DEBUG_REFCNT - if (theclass == SYM_EXPR) - debugrefcnt(1,CREATE); -#endif - } - - virtual ~SymExpr() {} - -#ifdef MARKVAR_32 -private: - int mark(); - void smark( int m ); -public: - int getmark( int i = 0 ) { return (mark() >> i)&1; } - void setmark( int i = 0 ) { smark( mark() | (1 << i) ); } - void clearmark( int i = 0 ) { smark( mark() & ~(1 << i) ); } -#endif -}; - -class SymSExpr : public SymExpr { - public: - std::string s; - SymSExpr(std::string _s, int theclass = SYMS_EXPR) - : SymExpr(_s, theclass), s(_s) - { -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) - : SymExpr(e, theclass), s(e.s) - { -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - - virtual ~SymSExpr() {} -}; - -class HoleExpr : public Expr { - static int next_id; -public: -#ifdef DEBUG_HOLE_NAMES - int id; -#endif - HoleExpr() - : Expr(HOLE_EXPR, 0), val(0) - { -#ifdef DEBUG_HOLE_NAMES - id = next_id++; -#endif -#ifdef DEBUG_REFCNT - debugrefcnt(1,CREATE); -#endif - } - Expr *val; // may be set during subst(), defeq(), and clone(). -}; - -inline Expr * Expr::followDefs() { - switch(getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)this; - if (h->val) - return h->val->followDefs(); - break; - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *h = (SymExpr *)this; - if (h->val) - return h->val->followDefs(); - break; - } - } - - return this; -} - -#endif - diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp deleted file mode 100644 index 016016c9d..000000000 --- a/proofs/lfsc_checker/libwriter.cpp +++ /dev/null @@ -1,238 +0,0 @@ -#include "libwriter.h" -#include -#include -#include - -void libwriter::get_var_name( const std::string& n, std::string& nn ) { - nn = std::string( n.c_str() ); - for( int i = 0; i <(int)n.length(); i++ ){ - char c = n[i]; - if (c <= 47) - c += 65; - else if (c >= 58 && c <= 64) - c += 97-58; - if ((c >= 91 && c <= 94) || c == 96) - c += 104-91; - else if (c >= 123) - c -= 4; - nn[i] = c; - } -} - -void libwriter::write_file() -{ - //std::cout << "write lib" << std::endl; - std::ostringstream os_enum; - std::ostringstream os_print; - std::ostringstream os_constructor_h; - std::ostringstream os_constructor_c; - - for ( int a=0; a<(int)syms.size(); a++ ) { - //std::cout << "sym #" << (a+1) << ": "; - //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl; - //defs[a]->print( std::cout ); - //std::cout << std::endl; - - if( defs[a]->getclass()==CEXPR ){ - //calculate which arguments are required for input - std::vector< Expr* > args; - std::vector< bool > argsNeed; - std::vector< Expr* > argTypes; - CExpr* c = ((CExpr*)defs[a]); - while( c->getop()==PI ){ - //std::cout << c->kids[0] << std::endl; - if( ((CExpr*)c->kids[1])->getop()!=RUN ){ - args.push_back( c->kids[0] ); - argsNeed.push_back( true ); - argTypes.push_back( c->kids[1] ); - } - for( int b=0; b<(int)args.size(); b++ ){ - if( argsNeed[b] ){ - if( ((CExpr*)c->kids[1])->getop()==RUN ){ - if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){ - argsNeed[b] = false; - } - }else{ - if( c->kids[1]->free_in( args[b] ) ){ - argsNeed[b] = false; - } - } - } - } - c = (CExpr*)(c->kids[2]); - } - - //record if this declares a judgement - if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){ - //std::cout << "This is a judgement" << std::endl; - judgements.push_back( syms[a] ); - //record if this declares a proof rule - }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){ - std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl; - //std::cout << "These are required to input:" << std::endl; - //for( int b=0; b<(int)args.size(); b++ ){ - // if( argsNeed[b] ){ - // std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl; - // } - //} - os_enum << " rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl; - - os_print << " case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \""; - os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl; - - std::ostringstream os_args; - os_args << "("; - bool firstTime = true; - for( int b=0; b<(int)args.size(); b++ ){ - if( argsNeed[b] ){ - if( !firstTime ) - os_args << ","; - std::string str; - get_var_name( ((SymSExpr*)args[b])->s, str ); - os_args << " LFSCProof* " << str.c_str(); - firstTime = false; - } - } - if( !firstTime ){ - os_args << " "; - } - os_args << ")"; - - os_constructor_h << " static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str(); - os_constructor_h << os_args.str().c_str() << ";" << std::endl; - - os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str(); - os_constructor_c << os_args.str().c_str() << "{" << std::endl; - os_constructor_c << " LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl; - for( int b=0; b<(int)args.size(); b++ ){ - os_constructor_c << " kids[" << b << "] = "; - if( argsNeed[b] ){ - std::string str; - get_var_name( ((SymSExpr*)args[b])->s, str ); - os_constructor_c << str.c_str(); - }else{ - os_constructor_c << "hole"; - } - os_constructor_c << ";" << std::endl; - } - os_constructor_c << " kids[" << (int)args.size() << "] = 0;" << std::endl; - os_constructor_c << " return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl; - os_constructor_c << "}" << std::endl << std::endl; - } - } - - //write the header - static std::string filename( "lfsc_proof" ); - std::fstream fsh; - std::string fnameh( filename ); - fnameh.append(".h"); - fsh.open( fnameh.c_str(), std::ios::out ); - - fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl; - fsh << "#define LFSC_PROOF_LIB_H" << std::endl; - fsh << std::endl; - fsh << "#include " << std::endl; - fsh << std::endl; - fsh << "class LFSCProof{" << std::endl; - fsh << "protected:" << std::endl; - fsh << " enum{" << std::endl; - fsh << os_enum.str().c_str(); - fsh << " };" << std::endl; - fsh << " static LFSCProof* hole;" << std::endl; - fsh << " LFSCProof(){}" << std::endl; - fsh << "public:" << std::endl; - fsh << " virtual ~LFSCProof(){}" << std::endl; - fsh << " static void init();" << std::endl; - fsh << std::endl; - fsh << " //functions to build LFSC proofs" << std::endl; - fsh << os_constructor_h.str().c_str(); - fsh << std::endl; - fsh << " virtual void set_child( int i, LFSCProof* e ) {}" << std::endl; - fsh << " virtual void print( std::ostream& os ){}" << std::endl; - fsh << "};" << std::endl; - fsh << std::endl; - fsh << "class LFSCProofC : public LFSCProof{" << std::endl; - fsh << " short id;" << std::endl; - fsh << " LFSCProof **kids;" << std::endl; - fsh << "public:" << std::endl; - fsh << " LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl; - fsh << " void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl; - fsh << " void print( std::ostream& os );" << std::endl; - fsh << "};" << std::endl; - fsh << std::endl; - fsh << "class LFSCProofSym : public LFSCProof{" << std::endl; - fsh << "private:" << std::endl; - fsh << " std::string s;" << std::endl; - fsh << " LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl; - fsh << "public:" << std::endl; - fsh << " static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl; - fsh << " static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl; - fsh << " ~LFSCProofSym(){}" << std::endl; - fsh << " void print( std::ostream& os ) { os << s.c_str(); }" << std::endl; - fsh << "};" << std::endl; - fsh << std::endl; - fsh << "class LFSCProofLam : public LFSCProof{" << std::endl; - fsh << " LFSCProofSym* var;" << std::endl; - fsh << " LFSCProof* body;" << std::endl; - fsh << " LFSCProof* typ;" << std::endl; - fsh << " LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl; - fsh << "public:" << std::endl; - fsh << " static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl; - fsh << " return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl; - fsh << " }" << std::endl; - fsh << " ~LFSCProofLam(){}" << std::endl; - fsh << std::endl; - fsh << " void print( std::ostream& os );" << std::endl; - fsh << "};" << std::endl; - fsh << std::endl; - fsh << "#endif" << std::endl; - - //write the cpp - std::fstream fsc; - std::string fnamec( filename ); - fnamec.append(".cpp"); - fsc.open( fnamec.c_str(), std::ios::out ); - - fsc << "#include \"lfsc_proof.h\"" << std::endl; - fsc << std::endl; - fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl; - fsc << std::endl; - fsc << "void LFSCProof::init(){" << std::endl; - fsc << " hole = LFSCProofSym::make( \"_\" );" << std::endl; - fsc << "}" << std::endl; - fsc << std::endl; - fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl; - fsc << " os << \"(\";" << std::endl; - fsc << " switch( id ){" << std::endl; - fsc << os_print.str().c_str(); - fsc << " }" << std::endl; - fsc << " int counter = 0;" << std::endl; - fsc << " while( kids[counter] ){" << std::endl; - fsc << " os << \" \";" << std::endl; - fsc << " kids[counter]->print( os );" << std::endl; - fsc << " counter++;" << std::endl; - fsc << " }" << std::endl; - fsc << " os << \")\";" << std::endl; - fsc << "}" << std::endl; - fsc << std::endl; - fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl; - fsc << " os << \"(\";" << std::endl; - fsc << " if( typ ){" << std::endl; - fsc << " os << \"% \";" << std::endl; - fsc << " }else{" << std::endl; - fsc << " os << \"\\\\ \";" << std::endl; - fsc << " }" << std::endl; - fsc << " var->print( os );" << std::endl; - fsc << " if( typ ){" << std::endl; - fsc << " os << \" \";" << std::endl; - fsc << " typ->print( os );" << std::endl; - fsc << " }" << std::endl; - fsc << " os << std::endl;" << std::endl; - fsc << " body->print( os );" << std::endl; - fsc << " os << \")\";" << std::endl; - fsc << "}" << std::endl; - fsc << std::endl; - fsc << os_constructor_c.str().c_str(); - fsc << std::endl; - } -} diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h deleted file mode 100644 index 91db5e911..000000000 --- a/proofs/lfsc_checker/libwriter.h +++ /dev/null @@ -1,28 +0,0 @@ -#ifndef LIB_WRITER_H -#define LIB_WRITER_H - -#include "expr.h" -#include - -class libwriter -{ -private: - std::vector< Expr* > syms; - std::vector< Expr* > defs; - - std::vector< Expr* > judgements; - //get the variable name - void get_var_name( const std::string& n, std::string& nn ); -public: - libwriter(){} - virtual ~libwriter(){} - - void add_symbol( Expr* s, Expr* t ) { - syms.push_back( s ); - defs.push_back( t ); - } - - void write_file(); -}; - -#endif diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp deleted file mode 100644 index 1d8ba5809..000000000 --- a/proofs/lfsc_checker/main.cpp +++ /dev/null @@ -1,140 +0,0 @@ -#include "expr.h" -#include "check.h" -#include -#include "sccwriter.h" -#include "libwriter.h" -#include - -using namespace std; - -args a; - -static void parse_args(int argc, char **argv, args &a) -{ - char *arg0 = *argv; - - /* skip 0'th argument */ - argv++; - argc--; - - while (argc) { - - if ((strncmp("-h", *argv, 2) == 0) || - (strncmp("--h", *argv, 3) == 0)) { - cout << "Usage: " << arg0 << " [options] infile1 ...infile_n\n"; - cout << "If no infiles are named on the command line, input is read\n" - << "from stdin. Specifying the infile \"stdin\" will also read\n" - << "from stdin. Options are:\n\n"; - cout << "--show-runs: print debugging information for runs of side condition code\n"; - cout << "--compile-scc: compile side condition code\n"; - cout << "--compile-scc-debug: compile debug versions of side condition code\n"; - cout << "--run-scc: use compiled side condition code\n"; - exit(0); - } - else if(strcmp("--show-runs", *argv) == 0) { - argc--; argv++; - a.show_runs = true; - } - else if(strcmp("--no-tail-calls", *argv) == 0) { - // this is just for debugging. - argc--; argv++; - a.no_tail_calls = true; - } - else if( strcmp("--compile-scc", *argv) == 0 ){ - argc--; argv++; - a.compile_scc = true; - a.compile_scc_debug = false; - } - else if( strcmp("--compile-scc-debug", *argv) == 0 ) - { - argc--; argv++; - a.compile_scc = true; - a.compile_scc_debug = true; - } - else if( strcmp("--compile-lib", *argv) == 0 ) - { - argc--; argv++; - a.compile_lib = true; - } - else if( strcmp("--run-scc", *argv) == 0 ){ - argc--; argv++; - a.run_scc = true; - } - else if( strcmp("--use-nested-app", *argv) == 0 ){ - argc--; argv++; - a.use_nested_app = true; //not implemented yet - }else { - a.files.push_back(*argv); - argc--; argv++; - } - } -} - -void sighandler(int /* signum */) { - cerr << "\nInterrupted. sc is aborting.\n"; - exit(1); -} - -int main(int argc, char **argv) { - - a.show_runs = false; - a.no_tail_calls = false; - a.compile_scc = false; - a.run_scc = false; - a.use_nested_app = false; - - signal(SIGINT, sighandler); - - parse_args(argc, argv, a); - - init(); - - check_time = (int)clock(); - - if (a.files.size()) { - sccwriter* scw = NULL; - libwriter* lw = NULL; - if( a.compile_scc ){ - scw = new sccwriter( a.compile_scc_debug ? opt_write_call_debug : 0 ); - } - if( a.compile_lib ){ - lw = new libwriter; - } - /* process the files named */ - int i = 0, iend = a.files.size(); - for (; i < iend; i++) { - const char *filename = a.files[i].c_str(); - check_file(filename, a, scw, lw); - } - if( scw ){ - scw->write_file(); - delete scw; - } - if( lw ){ -#ifdef DEBUG_SYM_NAMES - lw->write_file(); - delete lw; -#else - std::cout << "ERROR libwriter: Must compile LFSC with DEBUG_SYM_NAMES flag (see Expr.h)" << std::endl; -#endif - } - } - else - check_file("stdin", a); - - //std::cout << "time = " << (int)clock() - t << std::endl; - //while(1){} - -#ifdef DEBUG - cout << "Clearing globals.\n"; - cout.flush(); - - cleanup(); - a.files.clear(); -#endif - - std::cout << "Proof checked successfully!" << std::endl << std::endl; - std::cout << "time = " << (int)clock() - check_time << std::endl; - std::cout << "sym count = " << SymExpr::symmCount << std::endl; - std::cout << "marked count = " << Expr::markedCount << std::endl; -} diff --git a/proofs/lfsc_checker/position.h b/proofs/lfsc_checker/position.h deleted file mode 100644 index a5c51ffc6..000000000 --- a/proofs/lfsc_checker/position.h +++ /dev/null @@ -1,30 +0,0 @@ -#ifndef sc2__position_h -#define sc2__position_h - -#include -#include - -class Position { -public: - const char *filename; - int linenum; - int colnum; - - Position(const char *_f, int l, int c) : filename(_f), linenum(l), colnum(c) - {} - void print(std::ostream &os) { - os << filename; - if (colnum == -1) { - char tmp[1024]; - sprintf(tmp, ", line %d, end of column: ", linenum); - os << tmp; - } - else { - char tmp[1024]; - sprintf(tmp, ", line %d, column %d: ", linenum, colnum); - os << tmp; - } - } -}; - -#endif diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp deleted file mode 100644 index 40d9d1206..000000000 --- a/proofs/lfsc_checker/print_smt2.cpp +++ /dev/null @@ -1,122 +0,0 @@ -#include "print_smt2.h" - -#ifdef PRINT_SMT2 - -void print_smt2( Expr* p, std::ostream& s, short mode ) -{ - switch( p->getclass() ) - { - case CEXPR: - { - switch( p->getop() ) - { - case APP: - { - std::vector args; - Expr *head = p->collect_args(args, false); - short newMode = get_mode( head ); - if( is_smt2_poly_formula( head ) ) - { - s << "("; - head->print( s ); - s << " "; - print_smt2( args[1], s, newMode ); - s << " "; - print_smt2( args[2], s, newMode ); - s << ")"; - } - else if( ( mode==2 || mode==3 ) && mode==newMode ) - { - print_smt2( args[0], s, newMode ); - s << " "; - print_smt2( args[1], s, newMode ); - } - else if( newMode==1 ) - { - if( mode!=1 || newMode!=mode ){ - s << "("; - } - print_smt2( args[2], s, newMode ); - s << " "; - print_smt2( args[3], s, 0 ); - if( mode!=1 || newMode!=mode ){ - s << ")"; - } - } - else - { - s << "("; - switch( newMode ) - { - case 4: s << "=>";break; - default: head->print( s );break; - } - s << " "; - for( int a=0; a<(int)args.size(); a++ ){ - print_smt2( args[a], s, newMode ); - if( a!=(int)args.size()-1 ) - s << " "; - } - s << ")"; - } - } - break; - default: - std::cout << "Unhandled op " << p->getop() << std::endl; - break; - } - } - break; - case HOLE_EXPR: - { - HoleExpr *e = (HoleExpr *)p; - if( e->val ){ - print_smt2( e->val, s, mode ); - }else{ - s << "_"; - } - } - break; - case SYMS_EXPR: - case SYM_EXPR: - if( ((SymExpr*)p)->val ) - print_smt2( ((SymExpr*)p)->val, s, mode ); - else - p->print( s ); - break; - default: - std::cout << "Unhandled class " << p->getclass() << std::endl; - break; - } -} - -bool is_smt2_poly_formula( Expr* e ) -{ - if( e->getclass()==SYMS_EXPR ) - { - SymSExpr* s = (SymSExpr*)e; - static std::string eq("="); - static std::string distinct("distinct"); - return s->s==eq || s->s==distinct; - }else{ - return false; - } -} - -short get_mode( Expr* e ) -{ - if( e->getclass()==SYMS_EXPR ){ - SymSExpr* s = (SymSExpr*)e; - static std::string applys("apply"); - if ( s->s==applys ) return 1; - static std::string ands("and"); - if ( s->s==ands ) return 2; - static std::string ors("or"); - if ( s->s==ors ) return 3; - static std::string impls("impl"); - if ( s->s==impls ) return 4; - } - return 0; -} - -#endif diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h deleted file mode 100644 index 9bee0e81c..000000000 --- a/proofs/lfsc_checker/print_smt2.h +++ /dev/null @@ -1,17 +0,0 @@ -#ifndef PRINT_SMT2_H -#define PRINT_SMT2_H - -#define PRINT_SMT2 - -#include "expr.h" - -#ifdef PRINT_SMT2 -void print_smt2( Expr* p, std::ostream& s, short mode = 0 ); - -bool is_smt2_poly_formula( Expr* p ); -short get_mode( Expr* p ); - -#endif - - -#endif diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp deleted file mode 100644 index 19712579c..000000000 --- a/proofs/lfsc_checker/scccode.cpp +++ /dev/null @@ -1,11 +0,0 @@ -#include "scccode.h" - -void init_compiled_scc(){ - -} - -Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){ - return NULL; -} - - diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h deleted file mode 100644 index 2ab549c10..000000000 --- a/proofs/lfsc_checker/scccode.h +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef SCC_CODE_H -#define SCC_CODE_H - -#include "check.h" - -void init_compiled_scc(); - -Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ); - -#endif - diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp deleted file mode 100644 index d93341ab8..000000000 --- a/proofs/lfsc_checker/sccwriter.cpp +++ /dev/null @@ -1,977 +0,0 @@ -#include "sccwriter.h" - -#include -#include - -int sccwriter::exprCount = 0; -int sccwriter::strCount = 0; -int sccwriter::argsCount = 0; -int sccwriter::rnumCount = 0; - -int sccwriter::get_prog_index( const std::string& str ) -{ - for( int a=0; a<(int)progNames.size(); a++ ){ - if( progNames[a]==str ){ - return a; - } - } - return -1; -} - -int sccwriter::get_prog_index_by_expr( Expr* e ) -{ - for( int a=0; a<(int)progPtrs.size(); a++ ){ - if( progPtrs[a]==e ){ - return a; - } - } - return -1; -} - -bool sccwriter::is_var( const std::string& str ) -{ - for( int a=0; a<(int)vars.size(); a++ ){ - if( vars[a]==str ){ - return true; - } - } - return false; -} - -void sccwriter::add_global_sym( const std::string& str ) -{ - for( int a=0; a<(int)globalSyms.size(); a++ ){ - if( globalSyms[a]==str ){ - return; - } - } - globalSyms.push_back( str ); -} - -void sccwriter::indent( std::ostream& os, int ind ) -{ - for( int a=0; akids[1]; - int counter = 0; - //write each argument - while( progvars->kids[counter] ) - { - if( counter!=0 ) - { - os << ", "; - } - os << "Expr* "; - write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); - //add to vars if options are set to do so - if( opts&opt_write_add_args ) - { - vars.push_back( ((SymSExpr*)progvars->kids[counter])->s ); - } - counter++; - } - os << " )"; - if( opts&opt_write_call_debug ) - { - os << "{" << std::endl; - indent( os, 1 ); - os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl; - counter = 0; - while( progvars->kids[counter] ) - { - if( counter!=0 ) - { - indent( os, 1 ); - os << "std::cout << \", \";" << std::endl; - } - indent( os, 1 ); - write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); - os << "->print( std::cout );" << std::endl; - counter++; - } - indent( os, 1 ); - os << "std::cout << std::endl;" << std::endl; - } -} - -void sccwriter::get_function_name( const std::string& pname, std::string& fname ) -{ - fname = std::string( "f_" ); - fname.append( pname ); -} - -void sccwriter::write_variable( const std::string& n, std::ostream& os ) -{ - std::string nn; - get_var_name( n, nn ); - os << nn.c_str(); -} - -void sccwriter::get_var_name( const std::string& n, std::string& nn ) { - nn = std::string( n.c_str() ); - for( int i = 0; i <(int)n.length(); i++ ){ - char c = n[i]; - if (c <= 47) - c += 65; - else if (c >= 58 && c <= 64) - c += 97-58; - if ((c >= 91 && c <= 94) || c == 96) - c += 104-91; - else if (c >= 123) - c -= 4; - nn[i] = c; - } -} - -void sccwriter::write_file() -{ - static std::string filename( "scccode" ); - - //writer the h file - std::fstream fsh; - std::string fnameh( filename ); - fnameh.append(".h"); - fsh.open( fnameh.c_str(), std::ios::out ); - //write the header in h - fsh << "#ifndef SCC_CODE_H" << std::endl; - fsh << "#define SCC_CODE_H" << std::endl << std::endl; - //include necessary files in h file - fsh << "#include \"check.h\"" << std::endl << std::endl; - //write the init function - fsh << "void init_compiled_scc();" << std::endl << std::endl; - //write the entry function - fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl; - //write the side condition code functions - for( int n=0; n<(int)progs.size(); n++ ) - { - //write the header in the h file - fsh << "inline "; - write_function_header( fsh, n ); - fsh << ";" << std::endl << std::endl; - } - fsh << "#endif" << std::endl << std::endl; - fsh.close(); - - - //writer the cpp code - std::fstream fsc; - std::string fnamec( filename ); - fnamec.append(".cpp"); - fsc.open( fnamec.c_str(), std::ios::out ); - //include the h file in the cpp - fsc << "#include \"scccode.h\"" << std::endl << std::endl; - std::ostringstream fsc_funcs; - //write the side condition code functions - for( currProgram=0; currProgram<(int)progs.size(); currProgram++ ) - { - //reset naming counters - vars.clear(); - exprCount = 0; - strCount = 0; - argsCount = 0; - rnumCount = 0; - - //for debugging - std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl; - - //write the function header - write_function_header( fsc_funcs, currProgram, opt_write_add_args|options ); - if( (options&opt_write_call_debug)==0 ) - { - fsc_funcs << "{" << std::endl; - } - //write the code - //std::vector< std::string > cleanVec; - //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec ); - //debug_write_code( progs[n].second->kids[2], fsc, 1 ); - std::string expr; - write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr ); - indent( fsc_funcs, 1 ); - fsc_funcs << "return " << expr.c_str() << ";" << std::endl; - fsc_funcs << "}" << std::endl << std::endl; - } - //write the predefined symbols necessary - symbols and progs - for( int a=0; a<(int)globalSyms.size(); a++ ) - { - fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl; - } - for( int a=0; a<(int)progs.size(); a++ ) - { - fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl; - } - fsc << std::endl; - //write the init function - initialize symbols and progs - fsc << "void init_compiled_scc(){" << std::endl; - for( int a=0; a<(int)globalSyms.size(); a++ ) - { - indent( fsc, 1 ); - fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl; - } - for( int a=0; a<(int)progs.size(); a++ ) - { - indent( fsc, 1 ); - fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl; - } - fsc << "}" << std::endl << std::endl; - fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl; - //for( int n=0; n<(int)progs.size(); n++ ){ - // indent( fsc, 1 ); - // fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl; - //} - for( int n=0; n<(int)progs.size(); n++ ){ - indent( fsc, 1 ); - if( n!=0 ){ - fsc << "}else "; - } - //for each function, test to see if the string matches the name of the function - fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl; - indent( fsc, 2 ); - std::string fname; - get_function_name( progNames[n], fname ); - //map the function to the proper function - fsc << "return " << fname.c_str() << "( "; - //write the arguments to the function from args - CExpr* progvars = (CExpr*)get_prog( n )->kids[1]; - int counter = 0; - bool firstTime = true; - while( progvars->kids[counter] ) - { - if( !firstTime ) - { - fsc << ", "; - } - fsc << "args[" << counter << "]"; - firstTime = false; - counter++; - } - fsc << " );" << std::endl; - } - indent( fsc, 1 ); - fsc << "}else{" << std::endl; - indent( fsc, 2 ); - //return null in the case the function could not be found - fsc << "return NULL;" << std::endl; - indent( fsc, 1 ); - fsc << "}" << std::endl; - fsc << "}" << std::endl << std::endl; - fsc << fsc_funcs.str().c_str(); - - fsc.close(); -} - -void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts ) -{ - std::string retModString; - std::string incString; - if ( retModStr ) - { - retModString = std::string( retModStr ); - retModString.append( " = " ); - incString = std::string( retModStr ); - incString.append( "->inc();" ); - } - switch( code->getclass() ) - { - case INT_EXPR: - { - indent( os, ind ); - os << retModString.c_str(); - os << "new IntExpr( (signed long int)" << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - case RAT_EXPR: - { - mpz_t num, den; - mpz_init(num); - mpz_init(den); - mpq_get_num( num, ((RatExpr*)code)->n ); - mpq_get_den( den, ((RatExpr*)code)->n ); - indent( os, ind ); - os << retModString.c_str(); - os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - case SYMS_EXPR: - { - //if it is a variable, simply write it to buffer - if( is_var( ((SymSExpr*)code)->s ) ) - { - indent( os, ind ); - os << retModString.c_str(); - write_variable( ((SymSExpr*)code)->s.c_str(), os ); - os << ";" << std::endl; - } - else //else must look at symbol lookup table - { - std::string var; - get_var_name( ((SymSExpr*)code)->s, var ); - indent( os, ind ); - os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl; - add_global_sym( var ); - } - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - default: - switch( code->getop() ) - { - case APP: - { - //collect the arguments - std::vector< Expr* > argVector; - code->collect_args( argVector ); - //write the arguments - std::vector< std::string > args; - for( int a=0; a<(int)argVector.size(); a++ ) - { - std::string expr; - write_expr( argVector[a], os, ind, expr ); - args.push_back( expr ); - } - //write_args( (CExpr*)code, os, ind, 1, args ); - Expr* hd = code->get_head(); - //map to a program in the case that it is a program - if( hd->getop()==PROG && get_prog_index_by_expr( hd )!=-1 ) - { - indent( os, ind ); - os << retModString << "f_" << progNames[ get_prog_index_by_expr( hd ) ].c_str() << "( "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << " );" << std::endl; - for( int a=0; a<(int)args.size(); a++ ) - { - write_dec( args[a], os, ind ); - } - } - else - { -#ifdef USE_FLAT_APP - std::string expr; - write_expr( hd, os, ind, expr ); - indent( os, ind ); - os << retModString << "new CExpr( APP, "; - os << expr.c_str() << ", "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << " );" << std::endl; -#else - std::string expr; - write_expr( hd, os, ind, expr ); - indent( os, ind ); - os << retModString; - for( int a=0; a<(int)args.size(); a++ ) - { - os << "new CExpr( APP, "; - } - os << expr.c_str() << ", "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - os << " )"; - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << ";" << std::endl; -#endif - //indent( os, ind ); - //os << expr.c_str() << "->dec();" << std::endl; - } - } - break; - case MATCH: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr ); - //get the head - std::ostringstream sshd; - sshd << "e" << exprCount; - exprCount++; - indent( os, ind ); - os << "Expr* " << sshd.str().c_str() << " = " << expr.c_str() << "->followDefs()->get_head();" << std::endl; - //write the arguments - std::vector< std::string > args; - write_args( (CExpr*)code, os, ind, 1, args ); - bool encounterDefault = false; - //now make an if statement corresponding to the match - int a = 0; - while( ((CExpr*)code)->kids[a+1] ) - { - indent( os, ind ); - if( a!=0 ){ - os << "}else"; - } - if( ((CExpr*)code)->kids[a+1]->getop()!=CASE ){ - encounterDefault = true; - os << "{" << std::endl; - //write the body of the case - write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - }else{ - if( a!=0 ) - os << " "; - os << "if( " << sshd.str().c_str() << "==" << args[a].c_str() << " ){" << std::endl; - //collect args from the variable in the code - std::ostringstream ssargs; - ssargs << "args" << argsCount; - argsCount++; -#ifndef USE_FLAT_APP - indent( os, ind+1 ); - os << "std::vector< Expr* > " << ssargs.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->collect_args( " << ssargs.str().c_str() << " );" << std::endl; -#endif - //set the variables defined in the pattern equal to the arguments - std::vector< Expr* > caseArgs; - ((CExpr*)((CExpr*)code)->kids[a+1])->kids[0]->collect_args( caseArgs ); - for( int b=0; b<(int)caseArgs.size(); b++ ) - { - indent( os, ind+1 ); - os << "Expr* "; - write_variable( ((SymSExpr*)caseArgs[b])->s.c_str(), os ); -#ifdef USE_FLAT_APP - os << " = ((CExpr*)" << expr.c_str() << "->followDefs())->kids[" << b+1 << "];" << std::endl; -#else - os << " = " << ssargs.str().c_str() << "[" << b << "];" << std::endl; -#endif - vars.push_back( ((SymSExpr*)caseArgs[b])->s ); - } - //write the body of the case - write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr, opt_write_case_body ); - } - a++; - } - if( !encounterDefault ) - { - indent( os, ind ); - os << "}else{" << std::endl; - indent( os, ind + 1 ); - os << "std::cout << \"Could not find match for expression in function f_"; - os << progNames[currProgram].c_str() << " \";" << std::endl; - indent( os, ind + 1 ); - os << sshd.str().c_str() << "->print( std::cout );" << std::endl; - indent( os, ind + 1 ); - os << "std::cout << std::endl;" << std::endl; - indent( os, ind + 1 ); - os << "exit( 1 );" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - } - write_dec( expr, os, ind ); - for( int a=0; a<(int)args.size(); a++ ) - { - write_dec( args[a], os, ind ); - } - } - break; - case CASE: - if( opts&opt_write_case_body ) - { - write_code( ((CExpr*)code)->kids[1], os, ind, retModStr ); - } - else - { - write_code( ((CExpr*)code)->kids[0]->get_head(), os, ind, retModStr ); - } - break; - case DO: - { - //write each of the children in sequence - int counter = 0; - while( ((CExpr*)code)->kids[counter] ) - { - if( ((CExpr*)code)->kids[counter+1]==NULL ) - { - write_code( ((CExpr*)code)->kids[counter], os, ind, retModStr ); - } - else - { - std::string expr; - write_expr( ((CExpr*)code)->kids[counter], os, ind, expr ); - //clean up memory - write_dec( expr, os, ind ); - } - counter++; - } - } - break; - case LET: - { - indent( os, ind ); - os << "Expr* "; - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); - os << " = NULL;" << std::endl; - std::ostringstream ss; - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss ); - write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() ); - //add it to the variables - vars.push_back( ((SymSExpr*)((CExpr*)code)->kids[0])->s ); - write_code( ((CExpr*)code)->kids[2], os, ind, retModStr ); - //clean up memory - indent( os, ind ); - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); - os << "->dec();" << std::endl; - } - break; - case FAIL: - { - indent( os, ind ); - os << retModString.c_str() << "NULL;" << std::endl; - } - break; -#ifndef MARKVAR_32 - case MARKVAR: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); - //set the mark on the expression - indent( os, ind ); - os << "if (" << expr.c_str() << "->followDefs()->getmark())" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->clearmark();" << std::endl; - indent( os, ind ); - os << "else" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->setmark();" << std::endl; - //write the return if necessary - if( retModStr!=NULL ){ - indent( os, ind ); - os << retModString.c_str() << expr.c_str() << ";" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - write_dec( expr, os, ind ); - } - break; - case IFMARKED: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); - //if mark is set, write code for kids[1] - indent( os, ind ); - os << "if (" << expr.c_str() << "->followDefs()->getmark()){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+1, retModStr ); - //else write code for kids[2] - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr, os, ind ); - } - break; -#else - case MARKVAR: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); - //set the mark on the expression - indent( os, ind ); - os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << "))" << std::endl; - indent( os, ind+1 ); - os << "((SymExpr*)" << expr.c_str() << "->followDefs())->clearmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; - indent( os, ind ); - os << "else" << std::endl; - indent( os, ind+1 ); - os << "((SymExpr*)" << expr.c_str() << "->followDefs())->setmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; - //write the return if necessary - if( retModStr!=NULL ){ - indent( os, ind ); - os << retModString.c_str() << expr.c_str() << ";" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - write_dec( expr, os, ind ); - } - break; - case COMPARE: - { - std::string expr1, expr2; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1, opt_write_check_sym_expr ); - write_expr( ((CExpr*)code)->kids[1], os, ind, expr2, opt_write_check_sym_expr ); - indent( os, ind ); - os << "if( ((SymExpr*)" << expr1.c_str() << ")->followDefs() < ((SymExpr*)" << expr2.c_str() << ")->followDefs() ){" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - write_dec( expr2, os, ind ); - } - break; - case IFMARKED: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); - //if mark is set, write code for kids[1] - indent( os, ind ); - os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ")){" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - //else write code for kids[2] - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr, os, ind ); - } - break; -#endif - case ADD: - case MUL: - case DIV: - { - //calculate the value for the first expression - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - //calculate the value for the second expression - std::string expr2; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr2 ); - std::ostringstream ss; - ss << "rnum" << rnumCount; - rnumCount++; - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpz_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpz_"; - if( code->getop()==ADD ) - os << "add"; - else - os << "mul"; - os << "( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n, ((IntExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpq_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpq_"; - if( code->getop()==ADD ) - os << "add"; - else if( code->getop()==MUL ) - os << "mul"; - else - os << "div"; - os << "( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n, ((RatExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - write_dec( expr2, os, ind ); - } - break; - case NEG: - { - //calculate the value for the first expression - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - std::ostringstream ss; - ss << "rnum" << rnumCount; - rnumCount++; - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpz_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpz_neg( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpq_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpq_neg( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - } - break; - case IFNEG: - case IFZERO: - { - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) "; - if( code->getop()==IFNEG ) - os << "<"; - else - os << "=="; - os << " 0 ){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) "; - if( code->getop()==IFNEG ) - os << "<"; - else - os << "=="; - os << " 0 ){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - } - break; - case RUN:/*?*/break; - case PI:/*?*/break; - case LAM:/*?*/break; - case TYPE:/*?*/break; - case KIND:/*?*/break; - case ASCRIBE:/*?*/break; - case MPZ:/*?*/break; - case PROG:/*?*/break; - case PROGVARS:/*?*/break; - case PAT:/*?*/break; - } - break; - } -} - -void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, - std::vector< std::string >& args, int opts ) -{ - bool encounterCase = false; - while( code->kids[childCounter] && - (!encounterCase || code->kids[childCounter]->getop()==CASE ) ) - { - encounterCase = encounterCase || code->kids[childCounter]->getop()==CASE; - if( code->kids[childCounter]->getclass()==SYMS_EXPR ) - { - args.push_back( ((SymSExpr*)code->kids[childCounter])->s ); - } - else - { - //calculate the value for the argument - std::string expr; - write_expr( code->kids[childCounter], os, ind, expr, opts ); - args.push_back( expr ); - } - childCounter++; - } -} - -void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts ) -{ - if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) ) - { - get_var_name( ((SymSExpr*)code)->s, expr ); - indent( os, ind ); - os << expr.c_str() << "->inc();" << std::endl; - } - else - { - std::ostringstream ss; - ss << "e" << exprCount; - exprCount++; - //declare the expression - indent( os, ind ); - if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) ) - { - os << "static "; - } - os << "Expr* " << ss.str().c_str() << " = NULL;" << std::endl; - //write the expression - std::ostringstream ss2; - ss2 << ss.str().c_str(); - write_code( code, os, ind, ss2.str().c_str(), opts ); - - //if is not a sym expression, then decrement the expression and return null - if( opts&opt_write_check_sym_expr ) - { - indent( os, ind ); - os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl; - indent( os, ind+1 ); - os << "exit( 1 );" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - } - - expr = std::string( ss.str().c_str() ); - vars.push_back( expr ); - } - //increment the counter for memory management - //indent( os, ind ); - //os << expr.c_str() << "->inc();" << std::endl; -} - -void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind ) -{ - bool wd = true; - if( wd ) - { - indent( os, ind ); - os << expr.c_str() << "->dec();" << std::endl; - } -} - -void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind ) -{ - indent( os, ind ); - switch( code->getclass() ) - { - case INT_EXPR: - os << "int_expr"; - break; - case HOLE_EXPR: - os << "hole_expr"; - break; - case SYM_EXPR: - os << "sym_expr"; - break; - case SYMS_EXPR: - os << "syms_expr: " << ((SymSExpr*)code)->s.c_str(); - break; - default: - switch( code->getop() ) - { - case APP: - os << "app"; - break; - case PI: - os << "pi"; - break; - case LAM: - os << "lam"; - break; - case TYPE: - os << "type"; - break; - case KIND: - os << "kind"; - break; - case ASCRIBE: - os << "ascribe"; - break; - case MPZ: - os << "mpz"; - break; - case PROG: - os << "prog"; - break; - case PROGVARS: - os << "progvars"; - break; - case MATCH: - os << "match"; - break; - case CASE: - os << "case"; - break; - case PAT: - os << "pat"; - break; - case DO: - os << "do"; - break; - case ADD: - os << "add"; - break; - case NEG: - os << "neg"; - break; - case LET: - os << "let"; - break; - case RUN: - os << "run"; - break; - case FAIL: - os << "fail"; - break; - case MARKVAR: - os << "markvar"; - break; - case IFMARKED: - os << "ifmarked"; - break; - case COMPARE: - os << "compare"; - break; - default: - os << "???"; - break; - } - } - os << std::endl; - if( code->getop()!=0 ) - { - CExpr* ce = (CExpr*)code; - int counter = 0; - while( ce->kids[counter] ){ - debug_write_code( ce->kids[counter], os, ind+1 ); - counter++; - } - } -} diff --git a/proofs/lfsc_checker/sccwriter.h b/proofs/lfsc_checker/sccwriter.h deleted file mode 100644 index bd9732579..000000000 --- a/proofs/lfsc_checker/sccwriter.h +++ /dev/null @@ -1,86 +0,0 @@ -#ifndef SCC_WRITER_H -#define SCC_WRITER_H - -#include "expr.h" -#include -#include "check.h" - -enum -{ - opt_write_case_body = 0x00000001, - opt_write_check_sym_expr = 0x00000002, - opt_write_add_args = 0x000000004, - opt_write_no_inc = 0x00000008, - - opt_write_call_debug = 0x00000010, - opt_write_nested_app = 0x00000020, -}; - -class sccwriter -{ -private: - //options - int options; - //programs to write to file - symmap progs; - //list of indicies in progs - std::vector< Expr* > progPtrs; - std::vector< std::string > progNames; - int currProgram; - //current variables in the scope - std::vector< std::string > vars; - //global variables stored for lookups - std::vector< std::string > globalSyms; - //symbols that must be dec'ed - std::vector< std::string > decSyms; - //get program - CExpr* get_prog( int n ) { return (CExpr*)progs[ progNames[n] ]; } - //get index for string - int get_prog_index_by_expr( Expr* e ); - int get_prog_index( const std::string& str ); - //is variable in current scope - bool is_var( const std::string& str ); - //add global sym - void add_global_sym( const std::string& str ); - //expression count - static int exprCount; - //string count - static int strCount; - //args count - static int argsCount; - //num count - static int rnumCount; - //indent - static void indent( std::ostream& os, int ind ); - //write function header - void write_function_header( std::ostream& os, int index, int opts = 0 ); - void write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts = 0 ); - //write all children starting at child counter to stream, store in Expr* e_...e_; - void write_args( CExpr* code, std::ostream& os, int ind, int childCounter, std::vector< std::string >& args, int opts = 0 ); - //write expression - store result of code into e_ for some Expr* e_; - void write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts = 0 ); - //write variable - void write_variable( const std::string& n, std::ostream& os ); - //get function name - void get_function_name( const std::string& pname, std::string& fname ); - //get the variable name - void get_var_name( const std::string& n, std::string& nn ); - //write dec - void write_dec( const std::string& expr, std::ostream& os, int ind ); -public: - sccwriter( int opts = 0 ) : options( opts ){} - virtual ~sccwriter(){} - - void add_scc( const std::string& pname, Expr* exp ) { - //progs.push_back( std::pair< std::string, CExpr* >( pname, exp ) ); - progs[pname] = exp; - progPtrs.push_back( exp ); - progNames.push_back( pname ); - } - - void write_file(); - //write code - static void debug_write_code( Expr* code, std::ostream& os, int ind ); -}; - -#endif diff --git a/proofs/lfsc_checker/trie.cpp b/proofs/lfsc_checker/trie.cpp deleted file mode 100644 index fedb508b0..000000000 --- a/proofs/lfsc_checker/trie.cpp +++ /dev/null @@ -1,24 +0,0 @@ -#include "trie.h" -#include - -class Simple : public Trie::Cleaner { -public: - ~Simple() {} - void clean(int p) { - (void)p; - } -}; - -template <> -Trie::Cleaner *Trie::cleaner = new Simple; - -void unit_test_trie() { - Trie t; - t.insert("a", 1); - t.insert("b", 2); - t.insert("abc", 3); - t.insert("b", 0); - std::cout << "a: " << t.get("a") << "\n"; - std::cout << "b: " << t.get("b") << "\n"; - std::cout << "abc: " << t.get("abc") << "\n"; -} diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h deleted file mode 100644 index 401fdb453..000000000 --- a/proofs/lfsc_checker/trie.h +++ /dev/null @@ -1,123 +0,0 @@ -#ifndef sc2__trie_h -#define sc2__trie_h - -#include -#include -#include -#include - -template -class Trie { -protected: - char *str; - Data d; - bool using_next; - std::vector *> next; - - // s is assumed to be non-empty (and non-null) - Data insert_next(const char *s, const Data &x) { - assert(s != NULL && s[0] != '\0'); - unsigned c = s[0]; - if (c >= next.size()) { - using_next = true; - next.resize(c+1); - next[c] = new Trie; - } - else if (!next[c]) - next[c] = new Trie; - - return next[c]->insert(&s[1], x); - } - - // s is assumed to be non-empty (and non-null) - Data get_next(const char *s) { - assert(s != NULL && s[0] != '\0'); - unsigned c = s[0]; - if (c >= next.size()) - return Data(); - Trie *n = next[c]; - if (!n) - return Data(); - return n->get(&s[1]); - } - -public: - Trie() : str(), d(), using_next(false), next() { } - - ~Trie(); - - class Cleaner { - public: - virtual ~Cleaner() {} - virtual void clean(Data d) = 0; - }; - - static Cleaner *cleaner; - - Data get(const char *s) { - if (!s[0] && (!str || !str[0])) - return d; - if (str && strcmp(str, s) == 0) return d; - if (using_next) - return get_next(s); - return Data(); - } - - Data insert(const char *s, const Data &x) { - if (s[0] == 0) { - // we need to insert x right here. - if (str) { - if (str[0] == 0) { - // we need to replace d with x - Data old = d; - d = x; - return old; - } - // we need to push str into next. - (void)insert_next(str,d); - free(str); - } - str = strdup(s); - d = x; - return Data(); - } - - if (str) { - // cannot store x here - if (str[0] != 0) { - insert_next(str,d); - free(str); - str = 0; - d = Data(); - } - return insert_next(s,x); - } - - if (using_next) - // also cannot store x here - return insert_next(s,x); - - // we can insert x here as an optimization - str = strdup(s); - d = x; - return Data(); - } - -}; - -template -Trie::~Trie() -{ - cleaner->clean(d); - for (int i = 0, iend = next.size(); i < iend; i++) { - Trie *t = next[i]; - if (t) - delete t; - } - if (str) - free(str); -} - -extern void unit_test_trie(); - -#endif diff --git a/src/Makefile.am b/src/Makefile.am index 151bcaaa6..916733016 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -16,7 +16,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -D __STDC_LIMIT_MACROS \ -D __STDC_FORMAT_MACROS \ - -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker + -I@builddir@ -I@srcdir@/include -I@srcdir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = lib base options util expr smt_util prop/minisat prop/bvminisat . parser compat bindings main @@ -476,7 +476,6 @@ libcvc4_la_LIBADD = \ @builddir@/prop/bvminisat/libbvminisat.la if CVC4_PROOF libcvc4_la_LIBADD += \ - @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la \ @top_builddir@/proofs/signatures/libsignatures.la endif @@ -498,6 +497,12 @@ libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS) libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS) endif +if CVC4_USE_LFSC +libcvc4_la_LIBADD += $(LFSC_LIBS) +libcvc4_la_LDFLAGS += $(LFSC_LDFLAGS) +endif + + BUILT_SOURCES = \ theory/rewriter_tables.h \ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 93133be24..6d9201dde 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -120,6 +120,12 @@ namespace CVC4 { # define IS_CRYPTOMINISAT_BUILD false #endif /* CVC4_USE_CRYPTOMINISAT */ +#if CVC4_USE_LFSC +#define IS_LFSC_BUILD true +#else /* CVC4_USE_LFSC */ +#define IS_LFSC_BUILD false +#endif /* CVC4_USE_LFSC */ + #ifdef HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 5658b17b0..87dc1ecc1 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1281,6 +1281,17 @@ void OptionsHandler::proofEnabledBuild(std::string option, bool value) throw(Opt #endif /* CVC4_PROOF */ } +void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) { +#ifndef CVC4_USE_LFSC + if (value) { + std::stringstream ss; + ss << "option `" << option << "' requires a build of CVC4 with integrated " + "LFSC; this binary was not built with LFSC"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_LFSC */ +} + void OptionsHandler::notifyDumpToFile(std::string option) { d_options->d_dumpToFileListeners.notify(); } diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 16c77b166..923a87d3a 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -143,6 +143,7 @@ public: SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); void setProduceAssertions(std::string option, bool value) throw(); void proofEnabledBuild(std::string option, bool value) throw(OptionException); + void LFSCEnabledBuild(std::string option, bool value); void notifyDumpToFile(std::string option); void notifySetRegularOutputChannel(std::string option); void notifySetDiagnosticOutputChannel(std::string option); diff --git a/src/options/smt_options b/src/options/smt_options index 5f50ed202..00424e103 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -33,7 +33,7 @@ option omitDontCares --omit-dont-cares bool :default false When producing a model, omit variables whose value does not matter option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch turn on proof generation -option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :notify notifyBeforeSearch :read-write +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate LFSCEnabledBuild :notify notifyBeforeSearch :read-write after UNSAT/VALID, machine-check the generated proof option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs output proofs after every UNSAT/VALID response diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index f25dd5a51..f48f6753d 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -28,15 +28,16 @@ #include #include -// #warning "TODO: Why is lfsc's check.h being included like this?" -#include "check.h" - #include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" #include "smt/smt_engine.h" #include "util/statistics_registry.h" +#if (IS_LFSC_BUILD && IS_PROOFS_BUILD) +#include "lfscc.h" +#endif + using namespace CVC4; using namespace std; @@ -61,7 +62,7 @@ public: void SmtEngine::checkProof() { -#if IS_PROOFS_BUILD +#if (IS_LFSC_BUILD && IS_PROOFS_BUILD) Chat() << "generating proof..." << endl; @@ -113,23 +114,15 @@ void SmtEngine::checkProof() { pfStream << proof::plf_signatures << endl; pf->toStream(pfStream); pfStream.close(); - args a; - a.show_runs = false; - a.no_tail_calls = false; - a.compile_scc = false; - a.compile_scc_debug = false; - a.run_scc = false; - a.use_nested_app = false; - a.compile_lib = false; - init(); - check_file(pfFile, a); + lfscc_init(); + lfscc_check_file(pfFile, false, false, false, false, false, false, false); + // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup + // segfaults on regress0/bv/core/bitvec7.smt + //lfscc_cleanup(); free(pfFile); close(fd); -#else /* IS_PROOFS_BUILD */ - +#else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */ Unreachable("This version of CVC4 was built without proof support; cannot check proofs."); - -#endif /* IS_PROOFS_BUILD */ - +#endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */ }