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).
- 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:
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:
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
--- /dev/null
+# 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.h>]], [[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
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])])
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
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])
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<uint64_t> or not. Some do, some don't.
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])
--- /dev/null
+#!/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
+++ /dev/null
-/autom4te.cache
-/stamp-h
-/config.h.in
-/config.log
-/config.status
-/config.cache
-/libtool
-/stamp-h1
-.dep
-Makefile.in
-/configure
-/aclocal.m4
-*~
-\#*\#
-*.swp
+++ /dev/null
-The core authors and designers of the LFSC proof checker are:
-
- Andy Reynolds
- Aaron Stump
-
+++ /dev/null
-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.
+++ /dev/null
-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 `<wchar.h>' 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.
-
+++ /dev/null
-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
+++ /dev/null
-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 <mdeters@cs.nyu.edu> Thu, 12 Dec 2013 18:16:08 -0500
+++ /dev/null
-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.
+++ /dev/null
-#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 <libgen.h>
-#endif
-#include <stack>
-#include <string.h>
-#include <time.h>
-#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<string, Expr *> symbols;
-hash_map<string, Expr *> symbol_types;
-#else
-Trie<pair<Expr *, Expr *> > *symbols = new Trie<pair<Expr *, Expr *> >;
-#endif
-
-hash_map<string, bool > imports;
-std::map<SymExpr*, int > mark_map;
-std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > 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
- pair<Expr *,Expr *>prev =
- symbols->insert(id.c_str(),pair<Expr *,Expr *>(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<Expr *, Expr *> prevpr =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *, Expr *> >( 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<Expr *, Expr *> prevpr =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *, Expr *> >( 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<Expr *, Expr *> prevpr =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<HoleExpr *> holes;
- vector<bool> 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<Expr *, Expr *> 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<Expr *, Expr *> prev =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *, Expr *> prev =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *, Expr *> prev =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *> vars;
- vector<Expr *> 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<Expr *, Expr *> 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<Expr *, Expr *>(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<Expr*,Expr*>(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<pair<Expr *, Expr *> >::Cleaner {
-public:
- ~Deref() {}
- void clean(pair<Expr *, Expr *> 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<pair<Expr *, Expr *> >::Cleaner *
-Trie<pair<Expr *, Expr *> >::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<Expr *, Expr *>(statType, statKind));
- statType->inc();
- symbols->insert("mpz", pair<Expr *, Expr *>(statMpz, statType));
- symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType));
-#endif
-}
+++ /dev/null
-#ifndef SC2_CHECK_H
-#define SC2_CHECK_H
-
-#include "expr.h"
-#include "trie.h"
-
-#ifdef _MSC_VER
-#include <hash_map>
-#include <stdio.h>
-#else
-#include <ext/hash_map>
-#endif
-
-#include <stack>
-#include <string>
-#include <map>
-
-// see the help message in main.cpp for explanation
-typedef struct args {
- std::vector<std::string> 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<std::string, Expr *> symmap;
-typedef std::hash_map<std::string, SymExpr *> symmap2;
-#else
-typedef __gnu_cxx::hash_map<std::string, Expr *> symmap;
-typedef __gnu_cxx::hash_map<std::string, SymExpr *> symmap2;
-#endif
-extern symmap2 progs;
-extern std::vector< Expr* > ascHoles;
-
-#ifdef USE_HASH_MAPS
-extern symmap symbols;
-extern symmap symbol_types;
-#else
-extern Trie<std::pair<Expr *, Expr *> > *symbols;
-#endif
-
-extern std::map<SymExpr*, int > mark_map;
-
-extern std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > 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
+++ /dev/null
-///////////////////////////////////////////////////////////////////////////////
-// //
-// 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 <assert.h>
-
-/************************************************************************
- * 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
-
+++ /dev/null
-#include "check.h"
-#include "code.h"
-#include <string>
-
-#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<Expr *, Expr *> 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<SymSExpr *> vars;
-
-#ifdef USE_HASH_MAPS
- vector<Expr *>prevs;
-#else
- vector<pair<Expr *,Expr *> >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<Expr *, Expr *>(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<Expr *, Expr *> prev =
- symbols->insert(id.c_str(), pair<Expr *, Expr *>(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<Expr *> 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<Expr *, Expr *> 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<Expr *> argtps;
- int counter = 1;
- while( e->kids[counter] )
- {
- argtps.push_back( check_code( e->kids[counter] ) );
- counter++;
- }
- int iend = counter-1;
-#else
- vector<Expr *> args;
- Expr *h = (Expr *)e->collect_args(args);
-
- int iend = args.size();
- vector<Expr *> 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<Expr *, Expr *> prev =
- symbols->insert(var->s.c_str(), pair<Expr *, Expr *>(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
- vector<Expr *>prevs;
-#else
- vector<pair<Expr *,Expr *> >prevs;
-#endif
- vector<Expr *> 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<Expr *, Expr *>(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( r1<r2 ){
- r1->dec();
- _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<Expr *> 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<Expr *> vars;
- p->collect_args(vars);
- int jend = args.size();
- vector<Expr *> 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<Expr *> 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<Expr *> 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;
-}
+++ /dev/null
-#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
+++ /dev/null
-../../../config/ax_cxx_compile_stdcxx.m4
\ No newline at end of file
+++ /dev/null
-../../../config/ax_cxx_compile_stdcxx_11.m4
\ No newline at end of file
+++ /dev/null
-# -*- 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
+++ /dev/null
-#include "expr.h"
-#include <stdlib.h>
-#include <sstream>
-#ifdef _MSC_VER
-#include <algorithm>
-#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<Expr *> &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<Expr *> &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<Expr *> 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<Expr *> 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<Expr *> &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<Expr *> 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
+++ /dev/null
-#ifndef sc2__expr_h
-#define sc2__expr_h
-
-#include <stdint.h>
-#include <iostream>
-#include <map>
-#include <string>
-#include <unordered_set>
-#include <vector>
-
-#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<uintptr_t>(x);
- }
-};
-
-struct eqExprPtr {
- bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
-};
-
-typedef std::unordered_set<Expr *, hashExprPtr, eqExprPtr> 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<Expr *> &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<Expr *> &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<Expr *> &_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
-
+++ /dev/null
-#include "libwriter.h"
-#include <sstream>
-#include <algorithm>
-#include <fstream>
-
-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 <string>" << 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;
- }
-}
+++ /dev/null
-#ifndef LIB_WRITER_H
-#define LIB_WRITER_H
-
-#include "expr.h"
-#include <map>
-
-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
+++ /dev/null
-#include "expr.h"
-#include "check.h"
-#include <signal.h>
-#include "sccwriter.h"
-#include "libwriter.h"
-#include <time.h>
-
-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;
-}
+++ /dev/null
-#ifndef sc2__position_h
-#define sc2__position_h
-
-#include <iostream>
-#include <stdio.h>
-
-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
+++ /dev/null
-#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<Expr *> 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
+++ /dev/null
-#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
+++ /dev/null
-#include "scccode.h"
-
-void init_compiled_scc(){
-
-}
-
-Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
- return NULL;
-}
-
-
+++ /dev/null
-#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
-
+++ /dev/null
-#include "sccwriter.h"
-
-#include <fstream>
-#include <sstream>
-
-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; a<ind; a++ )
- {
- os << " ";
- }
-}
-
-void sccwriter::write_function_header( std::ostream& os, int index, int opts )
-{
- //write the function header
- std::string fname;
- get_function_name( progNames[index], fname );
- os << "Expr* " << fname.c_str() << "( ";
- CExpr* progvars = (CExpr*)get_prog( index )->kids[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++;
- }
- }
-}
+++ /dev/null
-#ifndef SCC_WRITER_H
-#define SCC_WRITER_H
-
-#include "expr.h"
-#include <vector>
-#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
+++ /dev/null
-#include "trie.h"
-#include <iostream>
-
-class Simple : public Trie<int>::Cleaner {
-public:
- ~Simple() {}
- void clean(int p) {
- (void)p;
- }
-};
-
-template <>
-Trie<int>::Cleaner *Trie<int>::cleaner = new Simple;
-
-void unit_test_trie() {
- Trie<int> 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";
-}
+++ /dev/null
-#ifndef sc2__trie_h
-#define sc2__trie_h
-
-#include <assert.h>
-#include <stdlib.h>
-#include <string.h>
-#include <vector>
-
-template<class Data>
-class Trie {
-protected:
- char *str;
- Data d;
- bool using_next;
- std::vector<Trie<Data> *> 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<Data>;
- }
- else if (!next[c])
- next[c] = new Trie<Data>;
-
- 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<Data> *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<class Data>
-Trie<Data>::~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
-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
@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
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 \
# 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 */
#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();
}
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);
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
#include <fstream>
#include <string>
-// #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;
void SmtEngine::checkProof() {
-#if IS_PROOFS_BUILD
+#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
Chat() << "generating proof..." << endl;
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) */
}
projects / cvc5.git / commitdiff