summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2013-12-17 17:52:40 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2013-12-17 17:52:40 -0600
commitc30f459b03572907b06f839535ac4694c0c37b0d (patch)
tree4112cd96e30928f4b57787eabe98a0aaa178540e
parent8d89e06c34a0a22e006a74d48d4cc8843b293f73 (diff)
parentf411ca8ce97f488fd0db0a79abe8b4e61521ae69 (diff)
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r--.travis.yml37
-rw-r--r--COPYING71
-rw-r--r--INSTALL7
-rw-r--r--Makefile.am16
-rw-r--r--Makefile.builds.in4
-rw-r--r--NEWS8
-rw-r--r--README4
-rw-r--r--config/cvc4.m43
-rw-r--r--config/readline.m43
-rw-r--r--configure.ac181
-rw-r--r--proofs/lfsc_checker/.gitignore16
-rw-r--r--proofs/lfsc_checker/AUTHORS5
-rw-r--r--proofs/lfsc_checker/COPYING17
-rw-r--r--proofs/lfsc_checker/INSTALL370
-rw-r--r--proofs/lfsc_checker/Makefile.am30
-rw-r--r--proofs/lfsc_checker/NEWS9
-rw-r--r--proofs/lfsc_checker/README83
-rw-r--r--proofs/lfsc_checker/check.cpp1383
-rw-r--r--proofs/lfsc_checker/check.h167
-rw-r--r--proofs/lfsc_checker/chunking_memory_management.h157
-rw-r--r--proofs/lfsc_checker/code.cpp1377
-rw-r--r--proofs/lfsc_checker/code.h15
-rw-r--r--proofs/lfsc_checker/configure.ac47
-rw-r--r--proofs/lfsc_checker/expr.cpp966
-rw-r--r--proofs/lfsc_checker/expr.h367
-rw-r--r--proofs/lfsc_checker/libwriter.cpp238
-rw-r--r--proofs/lfsc_checker/libwriter.h28
-rw-r--r--proofs/lfsc_checker/main.cpp139
-rw-r--r--proofs/lfsc_checker/position.h30
-rw-r--r--proofs/lfsc_checker/print_smt2.cpp122
-rw-r--r--proofs/lfsc_checker/print_smt2.h17
-rw-r--r--proofs/lfsc_checker/scccode.cpp609
-rw-r--r--proofs/lfsc_checker/scccode.h27
-rw-r--r--proofs/lfsc_checker/sccwriter.cpp977
-rw-r--r--proofs/lfsc_checker/sccwriter.h86
-rw-r--r--proofs/lfsc_checker/trie.cpp24
-rw-r--r--proofs/lfsc_checker/trie.h129
-rw-r--r--src/Makefile.am7
-rw-r--r--src/main/options1
-rw-r--r--src/smt/boolean_terms.cpp54
-rw-r--r--src/smt/boolean_terms.h5
-rw-r--r--src/smt/options2
-rw-r--r--src/smt/smt_engine.cpp101
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/smt/smt_engine_check_proof.cpp36
-rw-r--r--src/util/configuration.h4
-rw-r--r--src/util/configuration_private.h34
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/bug544.smt210
49 files changed, 7829 insertions, 202 deletions
diff --git a/.travis.yml b/.travis.yml
index aabb37762..b8d958ed5 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -3,9 +3,11 @@ compiler:
- gcc
- clang
env:
- - TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c'
- - TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c'
- - TRAVIS_CVC4_DISTCHECK=yes
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c'
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c'
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes
+ - TRAVIS_LFSC=yes
+ - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes
before_install:
# dhart/ppa is for cxxtest package, which doesn't appear officially until quantal
- travis_retry sudo apt-add-repository -y ppa:dhart/ppa
@@ -16,23 +18,34 @@ before_script:
- export PATH=$PATH:$JAVA_HOME/bin
- export JAVA_CPPFLAGS=-I$JAVA_HOME/include
- ./autogen.sh
- - echo $TRAVIS_CVC4_CONFIG
- - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
- - ./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)
script:
- normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
- - if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then
- make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1);
+ - if [ -n "$TRAVIS_CVC4" ]; then
+ echo "CVC4 config - $TRAVIS_CVC4_CONFIG" &&
+ (./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) &&
+ if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then
+ make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1);
+ else
+ (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) &&
+ (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
+ (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1));
+ fi;
+ elif [ -n "$TRAVIS_LFSC" ]; then
+ 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;
else
- (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) &&
- (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
- (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1));
+ echo "${red}Unknown Travis-CI configuration${normal}";
+ exit 1;
fi &&
(echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}")
matrix:
fast_finish: true
notifications:
email:
- recipients: mdeters@cs.nyu.edu
on_success: change
on_failure: always
diff --git a/COPYING b/COPYING
index 40cbdaa6b..4be4fdfa4 100644
--- a/COPYING
+++ b/COPYING
@@ -1,11 +1,15 @@
CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University
and The University of Iowa. All rights reserved.
-CVC4 is open-source; distribution is under the terms of the modified BSD
-license. However, certain builds of CVC4 link against GPLed libraries,
-and therefore the use of these builds is restricted in non-open-source
-projects. See below for a discussion of CLN and GLPK, and how to ensure
-you have a build that doesn't link against GPLed libraries.
+The source code of CVC4 is open and available to students, researchers,
+software companies, and everyone else to study, to modify, and to
+redistribute original or modified versions; distribution is under the
+terms of the modified BSD license. However, CVC4 can be configured (and
+is, by default) to link against some GPLed libraries, and therefore the
+use of these builds may be restricted in non-GPL-compatible projects.
+See below for a discussion of CLN, GLPK, and Readline (the three GPLed
+optional library dependences for CVC4), and how to ensure you have a
+build that doesn't link against GPLed libraries.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
@@ -19,7 +23,7 @@ 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.
--- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Tue, 17 Dec 2013 14:35:55 -0500
CVC4 incorporates MiniSat code, excluded from the above copyright.
See src/sat/minisat. Its copyright:
@@ -232,28 +236,59 @@ Their copyright:
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
-for Numbers, available here:
+CVC4 can be optionally configured to link against CLN, the Class Library for
+Numbers, available here:
http://www.ginac.de/CLN/
Please be advised that as this library is covered under the GPLv3, if you
choose to use the combined work, "CVC4+CLN," by building CVC4 with CLN,
then it is also covered under the GPLv3. If you want to make sure you build
-a version of CVC4 that uses libgmp, the GNU Multiple Precision Arithmetic
-Library, configure CVC4 with "--with-gmp" before building (though that is the
-default). It can then be used in contexts where you want to license CVC4
-under the (modified) BSD license.
+a version of CVC4 that uses no GPLed libraries, configure CVC4 with the
+"--bsd" option before building. CVC4 can then be used in contexts where you
+want to license CVC4 under the (modified) BSD license.
-Certain builds of CVC4 link against a GPLed library, GLPK, the GNU Linear
+CVC4 can be optionally configured to link against GLPK, the GNU Linear
Programming Kit, available here:
http://www.gnu.org/software/glpk/
Please be advised that as this library is covered under the GPLv3, if
you choose to use the combined work, "CVC4+GLPK," by building CVC4 with
-GLPK, then it is also covered under the GPLv3. If you want to make sure
-you build a version of CVC4 that does not use GLPK, configure CVC4 with
-"--without-glpk" before building (though that is the default). It can
-then be used in contexts where you want to license CVC4 under the
-(modified) BSD license.
+GLPK, then it is also covered under the GPLv3. If you want to make sure you
+build a version of CVC4 that uses no GPLed libraries, configure CVC4 with the
+"--bsd" option before building. CVC4 can then be used in contexts where you
+want to license CVC4 under the (modified) BSD license.
+
+CVC4 can be optionally configured to link against GNU Readline for improved
+text-editing support in interactive mode. GNU Readline is available here:
+
+ http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html
+
+Please be advised that as this library is covered under the GPLv3, if
+you choose to use the combined work, "CVC4+Readline," by building CVC4 with
+Readline, then it is also covered under the GPLv3. If you want to make sure
+you build a version of CVC4 that uses no GPLed libraries, configure CVC4 with
+the "--bsd" option before building. CVC4 can then be used in contexts where
+you want to license CVC4 under the (modified) BSD license.
+
+CVC4 sources incorporate those of the LFSC proof checker, which is
+covered by the following license:
+
+ LFSC is copyright (C) 2012, 2013 The University of Iowa. All rights
+ reserved.
+
+ LFSC is open-source; distribution is under the terms of the modified
+ BSD license.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+ AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/INSTALL b/INSTALL
index f0e1f6cc6..d8634f3e8 100644
--- a/INSTALL
+++ b/INSTALL
@@ -126,7 +126,12 @@ GLPK.
The GNU Readline library is optionally used to provide command
editing, tab completion, and history functionality at the CVC prompt
(when running in interactive mode). Check your distribution for a
-package named "libreadline-dev" or "readline-devel" or similar.
+package named "libreadline-dev" or "readline-devel" or similar. This
+library is covered by the GNU General Public License, version 3. Like
+the above-mentioned libraries, if you choose to use CVC4 with readline
+support, you are licensing CVC4 under that same license. (Please visit
+http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more
+details about readline.)
The Boost C++ threading library (often packaged independently of the
Boost base library) is needed to run CVC4 in "portfolio"
diff --git a/Makefile.am b/Makefile.am
index 41586cbe7..40f4c7006 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -5,8 +5,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
AUTOMAKE_OPTIONS = foreign
ACLOCAL_AMFLAGS = -I config
-SUBDIRS = src test contrib
-DIST_SUBDIRS = $(SUBDIRS) examples
+SUBDIRS_BASE = src test contrib
+if CVC4_PROOF
+ SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE)
+else
+ SUBDIRS = $(SUBDIRS_BASE)
+endif
+DIST_SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE) examples
.PHONY: examples
examples: all
@@ -125,7 +130,12 @@ EXTRA_DIST = \
doc/SmtEngine.3cvc_template.in \
doc/options.3cvc_template.in \
doc/libcvc4parser.3.in \
- doc/libcvc4compat.3.in
+ doc/libcvc4compat.3.in \
+ proofs/signatures/example.plf \
+ proofs/signatures/sat.plf \
+ proofs/signatures/smt.plf \
+ proofs/signatures/th_base.plf
+
man_MANS = \
doc/cvc4.1 \
doc/pcvc4.1 \
diff --git a/Makefile.builds.in b/Makefile.builds.in
index 33df24f95..296e5a974 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -192,12 +192,12 @@ endif
# The descent into "src" with target "check" is to build check
# prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...).
-check test units:
+check test units: all
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
systemtests regress: all
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
-units%:
+units%: all
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
+(cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@))
regress%: all
diff --git a/NEWS b/NEWS
index 46f5deee2..dd1de35a4 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,14 @@ Changes since 1.3
=================
* Timed statistics are now properly updated even on process abort.
+* The LFSC proof checker has been incorporated into CVC4 sources.
+* By default, CVC4 builds in "production" mode (optimized, with fewer
+ internal checks on). The common alternative is a "debug" build, which
+ is much slower. CVC4 also builds with GPL dependences by default now
+ (if those libraries are available), as this is the best-performing
+ version of CVC4. However, the new configure option "--bsd" disables
+ these GPL dependences and builds the best-performing BSD-licenced version
+ of CVC4.
Changes since 1.2
=================
diff --git a/README b/README
index c09fe979c..c5b751d0a 100644
--- a/README
+++ b/README
@@ -17,8 +17,8 @@ from any previous version.
CVC4 is intended to be an open and extensible SMT engine. It can be
used as a stand-alone tool or as a library. It has been designed to
increase the performance and reduce the memory overhead of its
-predecessors. It is written entirely in C++ and is released under a
-free software license (see the file COPYING in the source
+predecessors. It is written entirely in C++ and is released under an
+open-source software license (see the file COPYING in the source
distribution).
*** Getting started with CVC4
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index aefce193a..4b8b2e342 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -16,8 +16,9 @@ AC_DEFUN([CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE],
handle_option() {
ac_option="$[]1"
case $ac_option in
+ --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;;
-*|*=*) ;;
- production|production-*|debug|debug-*|default|default-*|competition|competition-*)
+ production|production-*|debug|debug-*|competition|competition-*)
# regexp `\?' not supported on Mac OS X
ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
ac_cvc4_build_profile_set=yes
diff --git a/config/readline.m4 b/config/readline.m4
index 44be9ff41..c298f3db4 100644
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -9,6 +9,9 @@ readline_compentry_func_returns_charp=0
READLINE_LIBS=
if test "$with_readline" = no; then
AC_MSG_RESULT([no, readline disabled by user])
+elif test "$with_readline" = check -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+ AC_MSG_RESULT([no, user requested BSD-compatible dependences only])
+ with_readline=no
else
if test "$with_readline" = check; then
AC_MSG_RESULT([no preference by user, will auto-detect])
diff --git a/configure.ac b/configure.ac
index 89d59cfff..9650030c0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -10,12 +10,13 @@ m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[
dnl Preprocess CL args. Defined in config/cvc4.m4
CVC4_AC_INIT
-AC_PREREQ(2.61)
-AC_INIT([cvc4], _CVC4_RELEASE_STRING)
+AC_PREREQ([2.68])
+AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc-bugs@cs.nyu.edu])
AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
AC_CONFIG_AUX_DIR([config])
AC_CONFIG_MACRO_DIR([config])
AC_CONFIG_LIBOBJ_DIR([src/lib])
+AC_CONFIG_SUBDIRS([proofs/lfsc_checker])
m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
@@ -107,10 +108,10 @@ fi
AC_MSG_CHECKING([for requested build profile])
AC_ARG_WITH([build],
[AS_HELP_STRING([--with-build=profile],
- [for profile in {production,debug,default,competition,personal}])])
+ [for profile in {production,debug,competition,personal}])])
-if test -z "${with_build+set}" -o "$with_build" = default; then
- with_build=default
+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}"; then
custom_build_profile=no
@@ -237,11 +238,8 @@ AC_PROG_INSTALL
CVC4_GCC_VERSION
-# [chris 8/24/2010] The user *must* specify --with-cln to get CLN
-# (and, thus, opt in to the GPL dependency).
-
-cvc4_use_gmp=0
-cvc4_use_cln=0
+cvc4_use_gmp=2
+cvc4_use_cln=2
AC_ARG_WITH(
[cln],
@@ -249,41 +247,49 @@ AC_ARG_WITH(
[--with-cln],
[use CLN instead of GMP]
),
- [if test "$withval" != no; then
- cvc4_use_cln=1
- fi
+ [case "$withval" in
+ y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
+ n|no|N|NO) cvc4_use_cln=0 ;;
+ esac
]
)
-# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
-# the default. Could be useful if other options are added later.
-
AC_ARG_WITH(
[gmp],
AS_HELP_STRING(
[--with-gmp],
- [use GMP instead of CLN (default)]
+ [use GMP instead of CLN]
),
- [if test "$withval" = no; then
- if test $cvc4_use_cln = 0; then
- AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
- fi
- else
- cvc4_use_gmp=1
- fi
+ [case "$withval" in
+ y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
+ n|no|N|NO) cvc4_use_gmp=0 ;;
+ esac
]
)
-if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
- # error
- AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
+if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
+ AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
+fi
+if test $cvc4_use_gmp = 1; then
+ cvc4_use_cln=0
+elif test $cvc4_use_gmp = 0; then
+ cvc4_use_cln=1
+elif test $cvc4_use_cln = 1; then
+ cvc4_use_gmp=0
+elif test $cvc4_use_cln = 0; then
+ cvc4_use_gmp=1
fi
# try GMP, fail if not found; GMP is required for both CLN and for GMP
# versions of CVC4
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
-if test $cvc4_use_cln = 1; then
+if test $cvc4_use_cln = 2 -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+ cvc4_use_cln=0
+ cvc4_use_gmp=1
+fi
+
+if test $cvc4_use_cln != 0; then
# [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
# gracefully. You can only specify it once for a given library name. That
# is, even on separate if/else branches, you can't put
@@ -295,12 +301,12 @@ if test $cvc4_use_cln = 1; then
AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
AC_LANG_POP([C++])
],
- [if test $cvc4_use_cln = 0; then
- # fall back to GMP
- AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
- else
+ [if test $cvc4_use_cln = 1; then
# fail
AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
+ else
+ # fall back to GMP
+ AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
fi
]
)
@@ -331,11 +337,6 @@ if test -z "$ac_confdir"; then
ac_confdir="$srcdir"
fi
build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
-if test "$custom_build_profile" = yes; then
- if test "$with_build" = default; then
- build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
- fi
-fi
AC_MSG_RESULT($build_type)
# Require building in target and build-specific build directory:
@@ -515,6 +516,7 @@ AC_MSG_RESULT([$enable_proof])
if test "$enable_proof" = yes; then
CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
fi
+AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
AC_MSG_CHECKING([whether to optimize libcvc4])
@@ -897,7 +899,7 @@ if test -z "$LFSC"; then
elif test "$enable_proof" = yes; then
support_proof_tests='yes, proof regression tests enabled'
else
- support_proof_tests='no, proof generation disabled for this build'
+ support_proof_tests='no, proof-generation disabled for this build'
fi
AC_SUBST([LFSC])
AC_SUBST([LFSCARGS])
@@ -1288,29 +1290,12 @@ fi
AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
-
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
-
-AC_OUTPUT
-
# Final information to the user
+gpl=no
licensewarn=
if test "$custom_build_profile" = yes; then
- if test "$with_build" = default; then
- with_build=custom
- else
- with_build="$with_build (customized)"
- fi
+ with_build="$with_build (customized)"
fi
support_unit_tests='cxxtest not found; unit tests not supported'
@@ -1327,46 +1312,50 @@ else
fi
if test $have_libglpk -eq 1; then
- licensewarn="${licensewarn}Please note that CVC4 will be built against the GNU Linear Programming
-Kit (GLPK). This library is covered under the GPL, so use of this build
-of CVC4 will be more restrictive than CVC4's license would normally
-suggest. For full details of GLPK and its license, please visit
- http://www.gnu.org/software/glpk/
-To build CVC4 without GLPK, configure --without-glpk (which is the default).
+ gpl=yes
+ gpllibs="${gpllibs} glpk"
+fi
-"
+if test $have_libreadline -eq 1; then
+ gpl=yes
+ gpllibs="${gpllibs} readline"
fi
if test $cvc4_cln_or_gmp = cln; then
mplibrary='cln (GPL)'
- licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
-Numbers (CLN). This library is covered under the GPL, so use of this
-build of CVC4 will be more restrictive than CVC4's license would
-normally suggest. For full details of CLN and its license, please visit
- http://www.ginac.de/CLN/
-To build CVC4 with GMP instead (which is covered under the more permissive
-LGPL), configure --without-cln.
-
-"
+ gpl=yes
+ gpllibs="${gpllibs} cln"
if test $with_portfolio = yes; then
- licensewarn="${licensewarn}
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-
-Note that CLN is UNSAFE FOR USE in parallel contexts!
-This build of CVC4 cannot be used safely as a portfolio solver.
-since the result of building with CLN will include numerous race
-conditions on the refcounts internal to CLN.
-
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+ AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
+Please specify only one of --with-portfolio and --with-cln.])
+ fi
+else
+ mplibrary='gmp'
+fi
-"
+if test "$gpl" = yes; then
+ if test -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+ AC_ERROR([Bad configuration detected: user requested BSD-licensed code only, but also requested GPLed libraries:$gpllibs])
fi
+
+ licensewarn="${licensewarn}"'****************************************************************************
+Please note that CVC4 will be built against the following GPLed libraries:
+ '"$gpllibs"'
+As these libraries are covered under the GPLv3, so is this build of CVC4.
+CVC4 is also available to you under the terms of the (modified) BSD license.
+If you prefer to license CVC4 under those terms, please configure with the
+option "--bsd".
+****************************************************************************
+
+'
+ license="GPLv3 (due to optional libraries; see below)"
else
- mplibrary='gmp (LGPL)'
+ license="modified BSD"
fi
+if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
+AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
+
CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
if test "$CVC4_BUILD_LIBCOMPAT" = no; then
@@ -1384,6 +1373,20 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then
fi
fi
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
+
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
+
+AC_OUTPUT
+
cat <<EOF
CVC4 $VERSION
@@ -1392,7 +1395,7 @@ Build profile: $with_build
Build ID : $build_type
Optimized : $optimized
Debug symbols: $enable_debug_symbols
-Proof : $enable_proof
+Proofs : $enable_proof
Statistics : $enable_statistics
Replay : $enable_replay
Assertions : $enable_assertions
@@ -1404,7 +1407,6 @@ Unit tests : $support_unit_tests
Proof tests : $support_proof_tests
gcov support : $enable_coverage
gprof support: $enable_profiling
-Readline : $with_readline
Static libs : $enable_static
Shared libs : $enable_shared
@@ -1418,6 +1420,7 @@ Portfolio : $with_portfolio
MP library : $mplibrary
GLPK : $with_glpk
+Readline : $with_readline
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
@@ -1432,6 +1435,8 @@ libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
Install into : $prefix
+CVC4 license : $license
+
${licensewarn}Now just type make, followed by make check or make install, as you like.
EOF
diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
new file mode 100644
index 000000000..1f799d15a
--- /dev/null
+++ b/proofs/lfsc_checker/.gitignore
@@ -0,0 +1,16 @@
+/autom4te.cache
+/stamp-h
+/config.h.in
+/config.log
+/config.status
+/config.cache
+/libtool
+/stamp-h1
+.dep
+Makefile.in
+/configure
+/aclocal.m4
+*~
+\#*\#
+/config/
+*.swp
diff --git a/proofs/lfsc_checker/AUTHORS b/proofs/lfsc_checker/AUTHORS
new file mode 100644
index 000000000..0bd0a37b0
--- /dev/null
+++ b/proofs/lfsc_checker/AUTHORS
@@ -0,0 +1,5 @@
+The core authors and designers of the LFSC proof checker are:
+
+ Andy Reynolds
+ Aaron Stump
+
diff --git a/proofs/lfsc_checker/COPYING b/proofs/lfsc_checker/COPYING
new file mode 100644
index 000000000..b220a3147
--- /dev/null
+++ b/proofs/lfsc_checker/COPYING
@@ -0,0 +1,17 @@
+LFSC is copyright (C) 2012, 2013 The University of Iowa.
+All rights reserved.
+
+LFSC is open-source; distribution is under the terms of the modified
+BSD license.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/proofs/lfsc_checker/INSTALL b/proofs/lfsc_checker/INSTALL
new file mode 100644
index 000000000..a1e89e18a
--- /dev/null
+++ b/proofs/lfsc_checker/INSTALL
@@ -0,0 +1,370 @@
+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.
+
diff --git a/proofs/lfsc_checker/Makefile.am b/proofs/lfsc_checker/Makefile.am
new file mode 100644
index 000000000..ff483f5fb
--- /dev/null
+++ b/proofs/lfsc_checker/Makefile.am
@@ -0,0 +1,30 @@
+AM_CXXFLAGS = -Wall -Wno-deprecated
+
+bin_PROGRAMS = lfsc-checker
+
+lfsc_checker_SOURCES = \
+ main.cpp
+lfsc_checker_LDADD = \
+ @builddir@/liblfsc_checker.la
+
+noinst_LTLIBRARIES = liblfsc_checker.la
+
+liblfsc_checker_la_SOURCES = \
+ check.cpp \
+ check.h \
+ chunking_memory_management.h \
+ code.cpp \
+ code.h \
+ expr.cpp \
+ expr.h \
+ libwriter.cpp \
+ libwriter.h \
+ position.h \
+ print_smt2.cpp \
+ print_smt2.h \
+ scccode.cpp \
+ scccode.h \
+ sccwriter.cpp \
+ sccwriter.h \
+ trie.cpp \
+ trie.h
diff --git a/proofs/lfsc_checker/NEWS b/proofs/lfsc_checker/NEWS
new file mode 100644
index 000000000..1a357ab4c
--- /dev/null
+++ b/proofs/lfsc_checker/NEWS
@@ -0,0 +1,9 @@
+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
diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README
new file mode 100644
index 000000000..5073569bc
--- /dev/null
+++ b/proofs/lfsc_checker/README
@@ -0,0 +1,83 @@
+lfsc: a high-performance LFSC proof checker.
+
+Andy Reynolds and Aaron Stump
+
+----------------------------------------------------------------------
+Command line parameters for LFSC:
+
+lfsc [sig_1 .... sig_n] [opts_1...opts_n]
+
+[sig_1 .... sig_n] are signature files, and options [opts_1...opts_n]
+are any of the following:
+
+--compile-scc : Write out all side conditions contained in signatures
+ specified on the command line to files scccode.h, scccode.cpp (see
+ below for example)
+
+--run-scc : Run proof checking with compiled side condition code (see
+ below).
+
+--compile-scc-debug : Write side condition code to scccode.h,
+ scccode.cpp that contains print statements (for debugging running of
+ side condition code).
+
+
+
+
+Typical usage:
+
+./src/opt/lfsc [sig_1 .... sig_n] [proof] [opts_1...opts_n]
+
+A proof is typically specified at the end of the list of input files
+in file [proof]. This will tell LFSC to type check the proof term in
+the file [proof]. The extension (*.plf) is commonly used for both
+user signature files and proof files.
+
+
+
+
+Side condition code compilation:
+
+LFSC may be used with side condition code compilation. This will take
+all side conditions ("program" constructs) in the user signature and
+produce equivalent C++ code in the output files scccode.h,
+scccode.cpp.
+
+An example for QF_IDL running with side condition code compilation:
+
+(1) In the src/ directory, run LFSC with the command line parameters:
+
+./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
+ ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
+ ../sat-tests/th_idl.plf --compile-scc
+
+This will produce scccode.h and scccode.cpp in the working directory
+where lfsc was run (here, src/).
+
+(2) Recompile the code base for lfsc. This will produce a copy of the
+LFSC executable that is capable of calling side conditions directly as
+compiled C++.
+
+(3) To check a proof.plf* with side condition code compilation, run
+LFSC with the command line parameters:
+
+./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
+ ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
+ ../sat-tests/th_idl.plf --run-scc proof.plf
+
+
+
+*Note that this proof must be compatible with the proof checking
+ signature. The proof generator is responsible for producing a proof
+ in the proper format that can be checked by the proof signature
+ specified when running LFSC.
+
+For example, in the case of CLSAT in the QF_IDL logic, older proofs
+(proofs produced before Feb 2009) may be incompatible with the newest
+version of the resolution checking signature (sat.plf). The newest
+version of CLSAT -- which can be checked out from the Iowa repository
+with
+
+svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat
+
+should produce proofs compatible with the current version of sat.plf.
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
new file mode 100644
index 000000000..8ef114115
--- /dev/null
+++ b/proofs/lfsc_checker/check.cpp
@@ -0,0 +1,1383 @@
+#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
+
+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, 0);
+Expr *statKind = new CExpr(KIND, 0);
+Expr *statMpz = new CExpr(MPZ,0);
+Expr *statMpq = new CExpr(MPQ,0);
+
+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;
+ 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
+ headtrm = Expr::make_app( headtrm, arg );
+#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;
+
+
+ char *f;
+ if (strcmp(_filename,"stdin") == 0) {
+ curfile = stdin;
+ f = strdup(_filename);
+ }
+ else {
+ if (prev_curfile) {
+ f = strdup(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
+ char *tmp = dirname(f);
+#endif
+ delete f;
+ f = new char[strlen(tmp) + 10 + strlen(_filename)];
+ strcpy(f,tmp);
+ strcat(f,"/");
+ strcat(f,_filename);
+ }
+ else
+ f = strdup(_filename);
+ curfile = fopen(f,"r");
+ if (!curfile)
+ report_error(string("Could not open file \"")
+ + string(f)
+ + string("\" for reading.\n"));
+ }
+
+ linenum = 1;
+ colnum = 1;
+ filename = f;
+
+ 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);
+ }
+ }
+ }
+ free(f);
+ 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
+}
diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h
new file mode 100644
index 000000000..a70599b0f
--- /dev/null
+++ b/proofs/lfsc_checker/check.h
@@ -0,0 +1,167 @@
+#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 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 != 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 != 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
diff --git a/proofs/lfsc_checker/chunking_memory_management.h b/proofs/lfsc_checker/chunking_memory_management.h
new file mode 100644
index 000000000..bdf938d32
--- /dev/null
+++ b/proofs/lfsc_checker/chunking_memory_management.h
@@ -0,0 +1,157 @@
+///////////////////////////////////////////////////////////////////////////////
+// //
+// 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
+
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
new file mode 100644
index 000000000..225700580
--- /dev/null
+++ b/proofs/lfsc_checker/code.cpp
@@ -0,0 +1,1377 @@
+#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
+ pat = Expr::make_app(pat,var);
+#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();
+ ret = Expr::make_app(ret,ke);
+#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;
+ 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;
+ }
+
+ CExpr *prog = (CExpr *)hd;
+ 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++)) {
+ old_vals.push_back(var->val);
+ var->val = args[i++];
+ }
+
+ 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++)) {
+ 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;
+} \ No newline at end of file
diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h
new file mode 100644
index 000000000..9d00a6378
--- /dev/null
+++ b/proofs/lfsc_checker/code.h
@@ -0,0 +1,15 @@
+#ifndef SC2_CODE_H
+#define SC2_CODE_H
+
+#include "expr.h"
+
+Expr *read_code();
+Expr *check_code(Expr *); // compute the type for the given code
+Expr *run_code(Expr *);
+
+int read_index();
+
+extern bool dbg_prog;
+extern bool run_scc;
+
+#endif
diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
new file mode 100644
index 000000000..245b0ea65
--- /dev/null
+++ b/proofs/lfsc_checker/configure.ac
@@ -0,0 +1,47 @@
+# -*- Autoconf -*-
+# Process this file with autoconf to produce a configure script.
+
+AC_PREREQ([2.68])
+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
+
+# Checks for libraries.
+# FIXME: Replace `main' with a function in `-lgmp':
+AC_CHECK_LIB([gmp], [__gmpz_init])
+
+# Checks for header files.
+AC_CHECK_HEADERS([stdlib.h string.h])
+
+# Checks for typedefs, structures, and compiler characteristics.
+AC_HEADER_STDBOOL
+AC_C_INLINE
+AC_TYPE_SIZE_T
+
+# Checks for library functions.
+AC_FUNC_MALLOC
+AC_CHECK_FUNCS([strdup])
+
+AC_CONFIG_FILES([Makefile])
+AC_OUTPUT
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
new file mode 100644
index 000000000..7ffc6469a
--- /dev/null
+++ b/proofs/lfsc_checker/expr.cpp
@@ -0,0 +1,966 @@
+#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; \
+ r->debugrefcnt(ref,DEC); \
+ if (ref == 0) { \
+ _e = r; \
+ goto start_destroy; \
+ } \
+ else \
+ r->data = (ref << 9) | (r->data & 511); \
+ } while(0)
+
+
+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;
+ }
+ }
+ }
+ }
+ return 0; // 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
+ {
+ CExpr *ret = new CExpr( APP );
+ ret->kids = new Expr* [args.size()-start+2];
+ ret->kids[0] = hd;
+ for (int i = start, iend = args.size(); i < iend; i++)
+ ret->kids[i-start+1] = args[i];
+ ret->kids[args.size()-start+1] = NULL;
+ return ret;
+ }
+#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++;
+ }
+ ret = new CExpr( APP );
+ ret->kids = new Expr* [counter+2];
+ counter = 0;
+ while( ((CExpr*)e1)->kids[counter] ){
+ ret->kids[counter] = ((CExpr*)e1)->kids[counter];
+ counter++;
+ }
+ ret->kids[counter] = e2;
+ ret->kids[counter+1] = NULL;
+ }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) {
+ 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) {
+ 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 );
+ CExpr* nce = new CExpr( APP );
+ nce->kids = new Expr *[(int)args.size()+2];
+ nce->kids[0] = hd;
+ for( int a=0; a<(int)args.size(); a++ )
+ {
+ nce->kids[a+1] = convert_to_flat_app( args[a] );
+ }
+ nce->kids[(int)args.size()+1] = 0;
+ 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( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) )
+ return false;
+ 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)
+
+ return false; // never reached.
+}
+
+int Expr::fiCounter = 0;
+
+bool Expr::free_in(Expr *x) {
+ //fiCounter++;
+ //if( fiCounter%1==0 )
+ // std::cout << fiCounter << std::endl;
+ switch(getop()) {
+ case NOT_CEXPR:
+ switch (getclass()) {
+ case HOLE_EXPR: {
+ HoleExpr *h = (HoleExpr *)this;
+ if (h->val)
+ return h->val->free_in(x);
+ 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);
+ 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
+ CExpr *e = (CExpr *)this;
+ Expr *tmp;
+ Expr **cur = e->kids;
+ while ((tmp = *cur++))
+ if (tmp->free_in(x))
+ return true;
+ return false;
+ }
+ }
+ return false; // 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 \ No newline at end of file
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
new file mode 100644
index 000000000..32a62ab33
--- /dev/null
+++ b/proofs/lfsc_checker/expr.h
@@ -0,0 +1,367 @@
+#ifndef sc2__expr_h
+#define sc2__expr_h
+
+#include "gmp.h"
+#include <string>
+#include <vector>
+#include <iostream>
+#include <map>
+#include "chunking_memory_management.h"
+
+#define USE_FLAT_APP
+#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 SymExpr;
+
+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;
+
+ void destroy(bool dec_kids);
+
+ enum { INC, DEC, CREATE };
+ void debugrefcnt(int ref, int what) {
+#ifdef DEBUG_REFCNT
+ 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";
+#else
+ (void)ref;
+ (void)what;
+#endif
+ }
+
+ Expr(int _class, int _op)
+ : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class)
+ { }
+
+public:
+ 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;
+ debugrefcnt(ref,INC);
+ data = (ref << 9) | (data & 511);
+ }
+ static void destroy(Expr *, bool);
+ inline void dec(bool dec_kids = true) {
+ int ref = getrefcnt();
+ ref = ref - 1;
+ debugrefcnt(ref,DEC);
+ 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() {
+ return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
+ }
+ inline bool isArithTerm() {
+ return getop() == ADD || getop() == NEG;
+ }
+
+ 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);
+
+ Expr *get_body(int op = PI, bool follow_defs = true);
+
+ 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);
+ bool get_free_in() { 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;
+ ~CExpr() {
+ delete[] kids;
+ }
+ CExpr(int _op) : Expr(CEXPR, _op), kids() {
+ kids = new Expr *[1];
+ kids[0] = 0;
+ debugrefcnt(1,CREATE);
+ }
+ CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
+ kids = new Expr *[2];
+ kids[0] = e1;
+ kids[1] = 0;
+ debugrefcnt(1,CREATE);
+ }
+ CExpr(int _op, Expr *e1, Expr *e2)
+ : Expr(CEXPR, _op), kids() {
+ kids = new Expr *[3];
+ kids[0] = e1;
+ kids[1] = e2;
+ kids[2] = 0;
+ debugrefcnt(1,CREATE);
+ }
+ 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;
+ debugrefcnt(1,CREATE);
+ }
+ 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;
+ debugrefcnt(1,CREATE);
+ }
+ 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;
+ debugrefcnt(1,CREATE);
+ }
+
+ // _kids must be null-terminated.
+ CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
+ (void)dummy;
+ debugrefcnt(1,CREATE);
+ }
+
+ 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;
+ ~IntExpr() {
+ mpz_clear(n);
+ }
+ IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
+ mpz_init_set(n,_n);
+ debugrefcnt(1,CREATE);
+ }
+ 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;
+ ~RatExpr() {
+ mpq_clear(n);
+ }
+ RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
+ mpq_init( n );
+ mpq_set(n,_n);
+ debugrefcnt(1,CREATE);
+ 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;
+ if (theclass == SYM_EXPR)
+ debugrefcnt(1,CREATE);
+ }
+ SymExpr(const SymExpr &e, int theclass = SYM_EXPR)
+ : Expr(theclass, 0), val(0)
+ {
+ (void)e;
+ if (theclass == SYM_EXPR)
+ debugrefcnt(1,CREATE);
+ }
+#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)
+ {
+ debugrefcnt(1,CREATE);
+ }
+ SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR)
+ : SymExpr(e, theclass), s(e.s)
+ {
+ debugrefcnt(1,CREATE);
+ }
+};
+
+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
+ debugrefcnt(1,CREATE);
+ }
+ Expr *val; // may be set during subst(), defeq(), and clone().
+};
+
+inline Expr * Expr::followDefs() {
+ switch(getclass()) {
+ case HOLE_EXPR: {
+ HoleExpr *h = (HoleExpr *)this;
+ if (h->val)
+ return h->val->followDefs();
+ break;
+ }
+ case SYMS_EXPR:
+ case SYM_EXPR: {
+ SymExpr *h = (SymExpr *)this;
+ if (h->val)
+ return h->val->followDefs();
+ break;
+ }
+ }
+
+ return this;
+}
+
+#endif
+
diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp
new file mode 100644
index 000000000..49e9bbaad
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.cpp
@@ -0,0 +1,238 @@
+#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;
+ }
+}
diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h
new file mode 100644
index 000000000..093cf541b
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.h
@@ -0,0 +1,28 @@
+#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
diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp
new file mode 100644
index 000000000..80f36e69f
--- /dev/null
+++ b/proofs/lfsc_checker/main.cpp
@@ -0,0 +1,139 @@
+#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 << "time = " << (int)clock() - check_time << std::endl;
+ std::cout << "sym count = " << SymExpr::symmCount << std::endl;
+ std::cout << "marked count = " << Expr::markedCount << std::endl;
+}
diff --git a/proofs/lfsc_checker/position.h b/proofs/lfsc_checker/position.h
new file mode 100644
index 000000000..a5c51ffc6
--- /dev/null
+++ b/proofs/lfsc_checker/position.h
@@ -0,0 +1,30 @@
+#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
diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
new file mode 100644
index 000000000..bf068c248
--- /dev/null
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -0,0 +1,122 @@
+#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!=args.size()-1 )
+ s << " ";
+ }
+ s << ")";
+ }
+ }
+ break;
+ default:
+ std::cout << "Unhandled op " << p->getop() << std::endl;
+ break;
+ }
+ }
+ break;
+ case HOLE_EXPR:
+ {
+ HoleExpr *e = (HoleExpr *)p;
+ if( e->val ){
+ print_smt2( e->val, s, mode );
+ }else{
+ s << "_";
+ }
+ }
+ break;
+ case SYMS_EXPR:
+ case SYM_EXPR:
+ if( ((SymExpr*)p)->val )
+ print_smt2( ((SymExpr*)p)->val, s, mode );
+ else
+ p->print( s );
+ break;
+ default:
+ std::cout << "Unhandled class " << p->getclass() << std::endl;
+ break;
+ }
+}
+
+bool is_smt2_poly_formula( Expr* e )
+{
+ if( e->getclass()==SYMS_EXPR )
+ {
+ SymSExpr* s = (SymSExpr*)e;
+ static std::string eq("=");
+ static std::string distinct("distinct");
+ return s->s==eq || s->s==distinct;
+ }else{
+ return false;
+ }
+}
+
+short get_mode( Expr* e )
+{
+ if( e->getclass()==SYMS_EXPR ){
+ SymSExpr* s = (SymSExpr*)e;
+ static std::string applys("apply");
+ if ( s->s==applys ) return 1;
+ static std::string ands("and");
+ if ( s->s==ands ) return 2;
+ static std::string ors("or");
+ if ( s->s==ors ) return 3;
+ static std::string impls("impl");
+ if ( s->s==impls ) return 4;
+ }
+ return 0;
+}
+
+#endif
diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h
new file mode 100644
index 000000000..c70b1dfa4
--- /dev/null
+++ b/proofs/lfsc_checker/print_smt2.h
@@ -0,0 +1,17 @@
+#ifndef PRINT_SMT2_H
+#define PRINT_SMT2_H
+
+#define PRINT_SMT2
+
+#include "expr.h"
+
+#ifdef PRINT_SMT2
+void print_smt2( Expr* p, std::ostream& s, short mode = 0 );
+
+bool is_smt2_poly_formula( Expr* p );
+short get_mode( Expr* p );
+
+#endif
+
+
+#endif
diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
new file mode 100644
index 000000000..cff762a08
--- /dev/null
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -0,0 +1,609 @@
+#include "scccode.h"
+
+Expr* e_pos;
+Expr* e_neg;
+Expr* e_tt;
+Expr* e_ff;
+Expr* e_cln;
+Expr* e_clc;
+Expr* e_concat;
+Expr* e_clr;
+Expr* e_litvar;
+Expr* e_litpol;
+Expr* e_notb;
+Expr* e_iffb;
+Expr* e_clear_mark;
+Expr* e_append;
+Expr* e_simplify_clause_h;
+Expr* e_simplify_clause;
+
+void init_compiled_scc(){
+ e_pos = symbols->get("pos").first;
+ e_neg = symbols->get("neg").first;
+ e_tt = symbols->get("tt").first;
+ e_ff = symbols->get("ff").first;
+ e_cln = symbols->get("cln").first;
+ e_clc = symbols->get("clc").first;
+ e_concat = symbols->get("concat").first;
+ e_clr = symbols->get("clr").first;
+ e_litvar = progs["litvar"];
+ e_litpol = progs["litpol"];
+ e_notb = progs["notb"];
+ e_iffb = progs["iffb"];
+ e_clear_mark = progs["clear_mark"];
+ e_append = progs["append"];
+ e_simplify_clause_h = progs["simplify_clause_h"];
+ e_simplify_clause = progs["simplify_clause"];
+}
+
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
+ if( p==e_litvar ){
+ return f_litvar( args[0] );
+ }else if( p==e_litpol ){
+ return f_litpol( args[0] );
+ }else if( p==e_notb ){
+ return f_notb( args[0] );
+ }else if( p==e_iffb ){
+ return f_iffb( args[0], args[1] );
+ }else if( p==e_clear_mark ){
+ return f_clear_mark( args[0] );
+ }else if( p==e_append ){
+ return f_append( args[0], args[1] );
+ }else if( p==e_simplify_clause_h ){
+ return f_simplify_clause_h( args[0], args[1] );
+ }else if( p==e_simplify_clause ){
+ return f_simplify_clause( args[0] );
+ }else{
+ return NULL;
+ }
+}
+
+Expr* f_litvar( Expr* l ){
+ Expr* e0;
+ l->inc();
+ Expr* e1 = l->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_pos;
+ e2->inc();
+ Expr* e3;
+ e3 = e_neg;
+ e3->inc();
+ if( e1==e2 ){
+ Expr* x = ((CExpr*)l->followDefs())->kids[1];
+ e0 = x;
+ e0->inc();
+ }else if( e1==e3 ){
+ Expr* x = ((CExpr*)l->followDefs())->kids[1];
+ e0 = x;
+ e0->inc();
+ }else{
+ std::cout << "Could not find match for expression in function f_litvar ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ l->dec();
+ e2->dec();
+ e3->dec();
+ return e0;
+}
+
+Expr* f_litpol( Expr* l ){
+ Expr* e0;
+ l->inc();
+ Expr* e1 = l->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_pos;
+ e2->inc();
+ Expr* e3;
+ e3 = e_neg;
+ e3->inc();
+ if( e1==e2 ){
+ Expr* x = ((CExpr*)l->followDefs())->kids[1];
+ e0 = e_tt;
+ e0->inc();
+ }else if( e1==e3 ){
+ Expr* x = ((CExpr*)l->followDefs())->kids[1];
+ e0 = e_ff;
+ e0->inc();
+ }else{
+ std::cout << "Could not find match for expression in function f_litpol ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ l->dec();
+ e2->dec();
+ e3->dec();
+ return e0;
+}
+
+Expr* f_notb( Expr* b ){
+ Expr* e0;
+ b->inc();
+ Expr* e1 = b->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_ff;
+ e2->inc();
+ Expr* e3;
+ e3 = e_tt;
+ e3->inc();
+ if( e1==e2 ){
+ e0 = e_tt;
+ e0->inc();
+ }else if( e1==e3 ){
+ e0 = e_ff;
+ e0->inc();
+ }else{
+ std::cout << "Could not find match for expression in function f_notb ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ b->dec();
+ e2->dec();
+ e3->dec();
+ return e0;
+}
+
+Expr* f_iffb( Expr* b1, Expr* b2 ){
+ Expr* e0;
+ b1->inc();
+ Expr* e1 = b1->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_tt;
+ e2->inc();
+ Expr* e3;
+ e3 = e_ff;
+ e3->inc();
+ if( e1==e2 ){
+ e0 = b2;
+ e0->inc();
+ }else if( e1==e3 ){
+ b2->inc();
+ e0 = f_notb( b2 );
+ b2->dec();
+ }else{
+ std::cout << "Could not find match for expression in function f_iffb ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ b1->dec();
+ e2->dec();
+ e3->dec();
+ return e0;
+}
+
+Expr* f_clear_mark( Expr* v ){
+ Expr* e0;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0)){
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0))
+ ((SymExpr*)v->followDefs())->clearmark(0);
+ else
+ ((SymExpr*)v->followDefs())->setmark(0);
+ e0 = v;
+ e0->inc();
+ v->dec();
+ }else{
+ e0 = v;
+ e0->inc();
+ }
+ v->dec();
+ return e0;
+}
+
+Expr* f_append( Expr* c1, Expr* c2 ){
+ Expr* e0;
+ c1->inc();
+ Expr* e1 = c1->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_cln;
+ e2->inc();
+ Expr* e3;
+ e3 = e_clc;
+ e3->inc();
+ if( e1==e2 ){
+ e0 = c2;
+ e0->inc();
+ }else if( e1==e3 ){
+ Expr* l = ((CExpr*)c1->followDefs())->kids[1];
+ Expr* c1h = ((CExpr*)c1->followDefs())->kids[2];
+ l->inc();
+ Expr* e4;
+ c1h->inc();
+ c2->inc();
+ e4 = f_append( c1h, c2 );
+ c1h->dec();
+ c2->dec();
+ static Expr* e5;
+ e5 = e_clc;
+ e5->inc();
+ e0 = new CExpr( APP, e5, l, e4 );
+ }else{
+ std::cout << "Could not find match for expression in function f_append ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ c1->dec();
+ e2->dec();
+ e3->dec();
+ return e0;
+}
+
+Expr* f_simplify_clause_h( Expr* pol, Expr* c ){
+ Expr* e0;
+ c->inc();
+ Expr* e1 = c->followDefs()->get_head();
+ Expr* e2;
+ e2 = e_cln;
+ e2->inc();
+ Expr* e3;
+ e3 = e_clc;
+ e3->inc();
+ Expr* e4;
+ e4 = e_concat;
+ e4->inc();
+ Expr* e5;
+ e5 = e_clr;
+ e5->inc();
+ if( e1==e2 ){
+ e0 = e_cln;
+ e0->inc();
+ }else if( e1==e3 ){
+ Expr* l = ((CExpr*)c->followDefs())->kids[1];
+ Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
+ Expr* v;
+ l->inc();
+ v = f_litvar( l );
+ l->dec();
+ Expr* e6;
+ Expr* e7;
+ l->inc();
+ e7 = f_litpol( l );
+ l->dec();
+ pol->inc();
+ e6 = f_iffb( e7, pol );
+ e7->dec();
+ pol->dec();
+ Expr* e8 = e6->followDefs()->get_head();
+ Expr* e9;
+ e9 = e_tt;
+ e9->inc();
+ Expr* e10;
+ e10 = e_ff;
+ e10->inc();
+ if( e8==e9 ){
+ Expr* m;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0)){
+ m = e_tt;
+ m->inc();
+ }else{
+ Expr* e11;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0))
+ ((SymExpr*)v->followDefs())->clearmark(0);
+ else
+ ((SymExpr*)v->followDefs())->setmark(0);
+ e11 = v;
+ e11->inc();
+ v->dec();
+ e11->dec();
+ m = e_ff;
+ m->inc();
+ }
+ v->dec();
+ Expr* ch;
+ pol->inc();
+ c1->inc();
+ ch = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ m->inc();
+ Expr* e12 = m->followDefs()->get_head();
+ Expr* e13;
+ e13 = e_tt;
+ e13->inc();
+ Expr* e14;
+ e14 = e_ff;
+ e14->inc();
+ if( e12==e13 ){
+ Expr* e15;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1)){
+ e15 = v;
+ e15->inc();
+ }else{
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1))
+ ((SymExpr*)v->followDefs())->clearmark(1);
+ else
+ ((SymExpr*)v->followDefs())->setmark(1);
+ e15 = v;
+ e15->inc();
+ v->dec();
+ }
+ v->dec();
+ e15->dec();
+ e0 = ch;
+ e0->inc();
+ }else if( e12==e14 ){
+ Expr* e16;
+ Expr* e17;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1)){
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1))
+ ((SymExpr*)v->followDefs())->clearmark(1);
+ else
+ ((SymExpr*)v->followDefs())->setmark(1);
+ e17 = v;
+ e17->inc();
+ v->dec();
+ }else{
+ e17 = v;
+ e17->inc();
+ }
+ v->dec();
+ e17->dec();
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0))
+ ((SymExpr*)v->followDefs())->clearmark(0);
+ else
+ ((SymExpr*)v->followDefs())->setmark(0);
+ e16 = v;
+ e16->inc();
+ v->dec();
+ e16->dec();
+ l->inc();
+ ch->inc();
+ static Expr* e18;
+ e18 = e_clc;
+ e18->inc();
+ e0 = new CExpr( APP, e18, l, ch );
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e12->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ m->dec();
+ e13->dec();
+ e14->dec();
+ ch->dec();
+ m->dec();
+ }else if( e8==e10 ){
+ l->inc();
+ Expr* e19;
+ pol->inc();
+ c1->inc();
+ e19 = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ static Expr* e20;
+ e20 = e_clc;
+ e20->inc();
+ e0 = new CExpr( APP, e20, l, e19 );
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e8->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ e6->dec();
+ e9->dec();
+ e10->dec();
+ v->dec();
+ }else if( e1==e4 ){
+ Expr* c1 = ((CExpr*)c->followDefs())->kids[1];
+ Expr* c2 = ((CExpr*)c->followDefs())->kids[2];
+ pol->inc();
+ Expr* e21 = pol->followDefs()->get_head();
+ Expr* e22;
+ e22 = e_ff;
+ e22->inc();
+ Expr* e23;
+ e23 = e_tt;
+ e23->inc();
+ if( e21==e22 ){
+ Expr* e24;
+ pol->inc();
+ c1->inc();
+ e24 = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ Expr* e25;
+ pol->inc();
+ c2->inc();
+ e25 = f_simplify_clause_h( pol, c2 );
+ pol->dec();
+ c2->dec();
+ static Expr* e26;
+ e26 = e_concat;
+ e26->inc();
+ e0 = new CExpr( APP, e26, e24, e25 );
+ }else if( e21==e23 ){
+ Expr* e27;
+ pol->inc();
+ c1->inc();
+ e27 = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ Expr* e28;
+ pol->inc();
+ c2->inc();
+ e28 = f_simplify_clause_h( pol, c2 );
+ pol->dec();
+ c2->dec();
+ e0 = f_append( e27, e28 );
+ e27->dec();
+ e28->dec();
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e21->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ pol->dec();
+ e22->dec();
+ e23->dec();
+ }else if( e1==e5 ){
+ Expr* l = ((CExpr*)c->followDefs())->kids[1];
+ Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
+ Expr* e29;
+ Expr* e30;
+ l->inc();
+ e30 = f_litpol( l );
+ l->dec();
+ pol->inc();
+ e29 = f_iffb( e30, pol );
+ e30->dec();
+ pol->dec();
+ Expr* e31 = e29->followDefs()->get_head();
+ Expr* e32;
+ e32 = e_ff;
+ e32->inc();
+ Expr* e33;
+ e33 = e_tt;
+ e33->inc();
+ if( e31==e32 ){
+ l->inc();
+ Expr* e34;
+ pol->inc();
+ c1->inc();
+ e34 = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ static Expr* e35;
+ e35 = e_clr;
+ e35->inc();
+ e0 = new CExpr( APP, e35, l, e34 );
+ }else if( e31==e33 ){
+ Expr* v;
+ l->inc();
+ v = f_litvar( l );
+ l->dec();
+ Expr* m;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0)){
+ m = e_tt;
+ m->inc();
+ }else{
+ Expr* e36;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0))
+ ((SymExpr*)v->followDefs())->clearmark(0);
+ else
+ ((SymExpr*)v->followDefs())->setmark(0);
+ e36 = v;
+ e36->inc();
+ v->dec();
+ e36->dec();
+ m = e_ff;
+ m->inc();
+ }
+ v->dec();
+ Expr* ch;
+ pol->inc();
+ c1->inc();
+ ch = f_simplify_clause_h( pol, c1 );
+ pol->dec();
+ c1->dec();
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1)){
+ m->inc();
+ Expr* e37 = m->followDefs()->get_head();
+ Expr* e38;
+ e38 = e_tt;
+ e38->inc();
+ Expr* e39;
+ e39 = e_ff;
+ e39->inc();
+ if( e37==e38 ){
+ e0 = ch;
+ e0->inc();
+ }else if( e37==e39 ){
+ Expr* e40;
+ Expr* e41;
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(1))
+ ((SymExpr*)v->followDefs())->clearmark(1);
+ else
+ ((SymExpr*)v->followDefs())->setmark(1);
+ e41 = v;
+ e41->inc();
+ v->dec();
+ e41->dec();
+ v->inc();
+ if ( ((SymExpr*)v->followDefs())->getmark(0))
+ ((SymExpr*)v->followDefs())->clearmark(0);
+ else
+ ((SymExpr*)v->followDefs())->setmark(0);
+ e40 = v;
+ e40->inc();
+ v->dec();
+ e40->dec();
+ e0 = ch;
+ e0->inc();
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e37->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ m->dec();
+ e38->dec();
+ e39->dec();
+ }else{
+ e0 = NULL;
+ }
+ v->dec();
+ ch->dec();
+ m->dec();
+ v->dec();
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e31->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ e29->dec();
+ e32->dec();
+ e33->dec();
+ }else{
+ std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+ e1->print( std::cout );
+ std::cout << std::endl;
+ exit( 1 );
+ }
+ c->dec();
+ e2->dec();
+ e3->dec();
+ e4->dec();
+ e5->dec();
+ return e0;
+}
+
+Expr* f_simplify_clause( Expr* c ){
+ Expr* e0;
+ static Expr* e1;
+ e1 = e_tt;
+ e1->inc();
+ Expr* e2;
+ static Expr* e3;
+ e3 = e_ff;
+ e3->inc();
+ c->inc();
+ e2 = f_simplify_clause_h( e3, c );
+ e3->dec();
+ c->dec();
+ e0 = f_simplify_clause_h( e1, e2 );
+ e1->dec();
+ e2->dec();
+ return e0;
+}
+
diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h
new file mode 100644
index 000000000..6f5efc8b5
--- /dev/null
+++ b/proofs/lfsc_checker/scccode.h
@@ -0,0 +1,27 @@
+#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 );
+
+inline Expr* f_litvar( Expr* l );
+
+inline Expr* f_litpol( Expr* l );
+
+inline Expr* f_notb( Expr* b );
+
+inline Expr* f_iffb( Expr* b1, Expr* b2 );
+
+inline Expr* f_clear_mark( Expr* v );
+
+inline Expr* f_append( Expr* c1, Expr* c2 );
+
+inline Expr* f_simplify_clause_h( Expr* pol, Expr* c );
+
+inline Expr* f_simplify_clause( Expr* c );
+
+#endif
+
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp
new file mode 100644
index 000000000..d11a96b19
--- /dev/null
+++ b/proofs/lfsc_checker/sccwriter.cpp
@@ -0,0 +1,977 @@
+#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( " << 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 << ";" << 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() << ";" << std::endl;
+ //write the expression
+ std::ostringstream ss2;
+ ss2 << ss.str().c_str();
+ write_code( code, os, ind, ss2.str().c_str(), opts );
+
+ //if is not a sym expression, then decrement the expression and return null
+ if( opts&opt_write_check_sym_expr )
+ {
+ indent( os, ind );
+ os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl;
+ indent( os, ind+1 );
+ os << "exit( 1 );" << std::endl;
+ indent( os, ind );
+ os << "}" << std::endl;
+ }
+
+ expr = std::string( ss.str().c_str() );
+ vars.push_back( expr );
+ }
+ //increment the counter for memory management
+ //indent( os, ind );
+ //os << expr.c_str() << "->inc();" << std::endl;
+}
+
+void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind )
+{
+ bool wd = true;
+ if( wd )
+ {
+ indent( os, ind );
+ os << expr.c_str() << "->dec();" << std::endl;
+ }
+}
+
+void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )
+{
+ indent( os, ind );
+ switch( code->getclass() )
+ {
+ case INT_EXPR:
+ os << "int_expr";
+ break;
+ case HOLE_EXPR:
+ os << "hole_expr";
+ break;
+ case SYM_EXPR:
+ os << "sym_expr";
+ break;
+ case SYMS_EXPR:
+ os << "syms_expr: " << ((SymSExpr*)code)->s.c_str();
+ break;
+ default:
+ switch( code->getop() )
+ {
+ case APP:
+ os << "app";
+ break;
+ case PI:
+ os << "pi";
+ break;
+ case LAM:
+ os << "lam";
+ break;
+ case TYPE:
+ os << "type";
+ break;
+ case KIND:
+ os << "kind";
+ break;
+ case ASCRIBE:
+ os << "ascribe";
+ break;
+ case MPZ:
+ os << "mpz";
+ break;
+ case PROG:
+ os << "prog";
+ break;
+ case PROGVARS:
+ os << "progvars";
+ break;
+ case MATCH:
+ os << "match";
+ break;
+ case CASE:
+ os << "case";
+ break;
+ case PAT:
+ os << "pat";
+ break;
+ case DO:
+ os << "do";
+ break;
+ case ADD:
+ os << "add";
+ break;
+ case NEG:
+ os << "neg";
+ break;
+ case LET:
+ os << "let";
+ break;
+ case RUN:
+ os << "run";
+ break;
+ case FAIL:
+ os << "fail";
+ break;
+ case MARKVAR:
+ os << "markvar";
+ break;
+ case IFMARKED:
+ os << "ifmarked";
+ break;
+ case COMPARE:
+ os << "compare";
+ break;
+ default:
+ os << "???";
+ break;
+ }
+ }
+ os << std::endl;
+ if( code->getop()!=0 )
+ {
+ CExpr* ce = (CExpr*)code;
+ int counter = 0;
+ while( ce->kids[counter] ){
+ debug_write_code( ce->kids[counter], os, ind+1 );
+ counter++;
+ }
+ }
+}
diff --git a/proofs/lfsc_checker/sccwriter.h b/proofs/lfsc_checker/sccwriter.h
new file mode 100644
index 000000000..f8922934f
--- /dev/null
+++ b/proofs/lfsc_checker/sccwriter.h
@@ -0,0 +1,86 @@
+#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
diff --git a/proofs/lfsc_checker/trie.cpp b/proofs/lfsc_checker/trie.cpp
new file mode 100644
index 000000000..fedb508b0
--- /dev/null
+++ b/proofs/lfsc_checker/trie.cpp
@@ -0,0 +1,24 @@
+#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";
+}
diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h
new file mode 100644
index 000000000..094a9060a
--- /dev/null
+++ b/proofs/lfsc_checker/trie.h
@@ -0,0 +1,129 @@
+#ifndef sc2__trie_h
+#define sc2__trie_h
+
+#include <vector>
+#include <string.h>
+#include <stdlib.h>
+
+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) {
+ 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) {
+ 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;
+
+ bool eqstr(const char *s1, const char *s2) {
+ while (*s1 && *s2) {
+ if (*s1++ != *s2++)
+ return false;
+ }
+ return (*s1 == *s2);
+ }
+
+ Data get(const char *s) {
+ if (!s[0] && (!str || !str[0]))
+ return d;
+ if (str && eqstr(str,s))
+ 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
diff --git a/src/Makefile.am b/src/Makefile.am
index 3637cb089..18382a8ab 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -16,7 +16,7 @@ AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
-D __STDC_LIMIT_MACROS \
-D __STDC_FORMAT_MACROS \
- -I@builddir@ -I@srcdir@/include -I@srcdir@
+ -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
@@ -104,6 +104,7 @@ libcvc4_la_SOURCES = \
prop/sat_solver_registry.cpp \
prop/options_handlers.h \
smt/smt_engine.cpp \
+ smt/smt_engine_check_proof.cpp \
smt/smt_engine.h \
smt/model_postprocessor.cpp \
smt/model_postprocessor.h \
@@ -393,6 +394,10 @@ libcvc4_la_LIBADD = \
@builddir@/expr/libexpr.la \
@builddir@/prop/minisat/libminisat.la \
@builddir@/prop/bvminisat/libbvminisat.la
+if CVC4_PROOF
+libcvc4_la_LIBADD += \
+ @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la
+endif
if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
libcvc4_la_LIBADD += \
diff --git a/src/main/options b/src/main/options
index ba36e43ab..faac6b8f1 100644
--- a/src/main/options
+++ b/src/main/options
@@ -7,6 +7,7 @@ module DRIVER "main/options.h" Driver
common-option version -V --version/ bool
identify this CVC4 binary
+alias --license = --version
common-option help -h --help/ bool
full command line reference
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 30aa79aca..c1596dddc 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -43,8 +43,10 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
d_tt(),
d_ffDt(),
d_ttDt(),
+ d_varCache(),
d_termCache(),
- d_typeCache() {
+ d_typeCache(),
+ d_datatypeCache() {
// set up our "false" and "true" conversions based on command-line option
if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
@@ -250,10 +252,10 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
- d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
- d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+ d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+ d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+ d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
}
}
out = &newD;
@@ -400,12 +402,18 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
if(!childrenPushed) {
Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
- BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
- if(i != d_termCache.end()) {
+ BooleanTermVarCache::iterator i = d_varCache.find(top);
+ if(i != d_varCache.end()) {
result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
worklist.pop();
goto next_worklist;
}
+ BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
+ if(j != d_termCache.end()) {
+ result.top() << ((*j).second.isNull() ? Node(top) : (*j).second);
+ worklist.pop();
+ goto next_worklist;
+ }
if(quantBoolVars.find(top) != quantBoolVars.end()) {
// this Bool variable is quantified over and we're changing it to a BitVector var
@@ -511,7 +519,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
@@ -536,7 +544,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
nm->mkConst(false), n_ff);
Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
@@ -548,7 +556,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
top.setAttribute(BooleanTermAttr(), n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
@@ -568,12 +576,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
nm->mkNode(kind::EQUAL, n_tt, d_tt));
Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
@@ -588,12 +596,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
@@ -601,7 +609,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
Debug("boolean-terms") << "found a var of datatype type" << endl;
TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
if(t != newT) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
+ Assert(d_varCache.find(top) == d_varCache.end(),
"Node `%s' already in cache ?!", top.toString().c_str());
Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
newT, "a datatype variable introduced by Boolean-term conversion",
@@ -610,12 +618,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
top.setAttribute(BooleanTermAttr(), n);
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
} else {
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
@@ -630,13 +638,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+ Assert(d_varCache.find(top) != d_varCache.end(),
"constructor `%s' not in cache", top.toString().c_str());
- result.top() << d_termCache[make_pair(top, parentTheory)];
+ result.top() << d_varCache[top];
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
@@ -648,13 +656,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+ Assert(d_varCache.find(top) != d_varCache.end(),
"tester or selector `%s' not in cache", top.toString().c_str());
- result.top() << d_termCache[make_pair(top, parentTheory)];
+ result.top() << d_varCache[top];
worklist.pop();
goto next_worklist;
} else {
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
@@ -670,7 +678,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
NodeManager::SKOLEM_EXACT_NAME);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
top.setAttribute(BooleanTermAttr(), n);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index 904d47b5f..89611f5ea 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -35,6 +35,9 @@ namespace attr {
typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
class BooleanTermConverter {
+ /** The type of the Boolean term conversion variable cache */
+ typedef std::hash_map<Node, Node, NodeHashFunction> BooleanTermVarCache;
+
/** The type of the Boolean term conversion cache */
typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
PairHashFunction< Node, bool,
@@ -58,6 +61,8 @@ class BooleanTermConverter {
/** The conversion for "true" when in datatypes contexts. */
Node d_ttDt;
+ /** The cache used during Boolean term variable conversion */
+ BooleanTermVarCache d_varCache;
/** The cache used during Boolean term conversion */
BooleanTermCache d_termCache;
/** The cache used during Boolean term type conversion */
diff --git a/src/smt/options b/src/smt/options
index 05a138f60..69b5102de 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -22,6 +22,8 @@ option expandDefinitions expand-definitions bool :default false
always expand symbol definitions in output
common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
support the get-value and get-model commands
+option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ after UNSAT/VALID, machine-check the generated proof
option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
option dumpModels --dump-models bool :default false
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 88cefbdc2..1f83bb547 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -313,7 +313,6 @@ class SmtEnginePrivate : public NodeManagerListener {
hash_map<unsigned, Node> d_BVDivByZero;
hash_map<unsigned, Node> d_BVRemByZero;
-
/**
* Function symbol used to implement uninterpreted
* int-division-by-zero semantics. Needed to deal with partial
@@ -560,6 +559,11 @@ public:
throw(TypeCheckingException, LogicException);
/**
+ * Rewrite Boolean terms in a Node.
+ */
+ Node rewriteBooleanTerms(TNode n);
+
+ /**
* Simplify node "in" by expanding definitions and applying any
* substitutions learned from preprocessing.
*/
@@ -2899,6 +2903,39 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
return false;
}
+Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+ if(d_booleanTermConverter == NULL) {
+ // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
+ // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
+ // definition, and not dump it properly.
+ d_booleanTermConverter = new BooleanTermConverter(d_smt);
+ }
+ Node retval = d_booleanTermConverter->rewriteBooleanTerms(n);
+ if(retval != n) {
+ switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
+ case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+ case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+ if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(THEORY_BV);
+ d_smt.d_logic.lock();
+ }
+ break;
+ case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+ if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(THEORY_DATATYPES);
+ d_smt.d_logic.lock();
+ }
+ break;
+ default:
+ Unhandled(mode);
+ }
+ }
+ return retval;
+}
+
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
@@ -2956,37 +2993,8 @@ void SmtEnginePrivate::processAssertions() {
dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
{
Chat() << "rewriting Boolean terms..." << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
- if(d_booleanTermConverter == NULL) {
- // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
- // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
- // definition, and not dump it properly.
- d_booleanTermConverter = new BooleanTermConverter(d_smt);
- }
for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]);
- if(n != d_assertionsToPreprocess[i]) {
- switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
- case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
- case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_BV);
- d_smt.d_logic.lock();
- }
- break;
- case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_DATATYPES);
- d_smt.d_logic.lock();
- }
- break;
- default:
- Unhandled(mode);
- }
- }
- d_assertionsToPreprocess[i] = n;
+ d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
}
}
dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
@@ -3350,6 +3358,12 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
checkModel(/* hard failure iff */ ! r.isUnknown());
}
}
+ // Check that UNSAT results generate a proof correctly.
+ if(options::checkProofs()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+ checkProof();
+ }
+ }
return r;
}/* SmtEngine::checkSat() */
@@ -3420,6 +3434,12 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
checkModel(/* hard failure iff */ ! r.isUnknown());
}
}
+ // Check that UNSAT results generate a proof correctly.
+ if(options::checkProofs()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+ checkProof();
+ }
+ }
return r;
}/* SmtEngine::query() */
@@ -3529,9 +3549,14 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
// do not need to apply preprocessing substitutions (should be recorded
// in model already)
+ Node n = Node::fromExpr(e);
+ Trace("smt") << "--- getting value of " << n << endl;
+ TypeNode expectedType = n.getType();
+
// Expand, then normalize
hash_map<Node, Node, NodeHashFunction> cache;
- Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+ n = d_private->expandDefinitions(n, cache);
+ n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
@@ -3541,13 +3566,13 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
resultNode = m->getValue(n);
}
Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
- resultNode = postprocess(resultNode, n.getType());
+ resultNode = postprocess(resultNode, expectedType);
Trace("smt") << "--- model-post returned " << resultNode << endl;
Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
- Trace("smt") << "--- model-post expected " << n.getType() << endl;
+ Trace("smt") << "--- model-post expected " << expectedType << endl;
// type-check the result we got
- Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
+ Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType));
// ensure it's a constant
Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
@@ -3625,9 +3650,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
++i) {
Assert((*i).getType() == boolType);
+ Trace("smt") << "--- getting value of " << *i << endl;
+
// Expand, then normalize
hash_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(*i, cache);
+ n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
@@ -3639,6 +3667,9 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
// type-check the result we got
Assert(resultNode.isNull() || resultNode.getType() == boolType);
+ // ensure it's a constant
+ Assert(resultNode.isConst());
+
vector<SExpr> v;
if((*i).getKind() == kind::APPLY) {
Assert((*i).getNumChildren() == 0);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9655297b3..0781ac1c0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,6 +249,11 @@ class CVC4_PUBLIC SmtEngine {
smt::SmtEnginePrivate* d_private;
/**
+ * Check that a generated Proof (via getProof()) checks.
+ */
+ void checkProof();
+
+ /**
* Check that a generated Model (via getModel()) actually satisfies
* all user assertions.
*/
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
new file mode 100644
index 000000000..e4de1029b
--- /dev/null
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -0,0 +1,36 @@
+/********************* */
+/*! \file smt_engine_check_proof.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/smt_engine.h"
+#include "check.h"
+
+using namespace CVC4;
+using namespace std;
+
+void SmtEngine::checkProof() {
+
+#ifdef CVC4_PROOF
+
+ //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+
+#else /* CVC4_PROOF */
+
+ Unreachable("This version of CVC4 was built without proof support; cannot check proofs.");
+
+#endif /* CVC4_PROOF */
+
+}
diff --git a/src/util/configuration.h b/src/util/configuration.h
index be49e3dcf..696b67715 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -83,12 +83,16 @@ public:
static std::string about();
+ static bool licenseIsGpl();
+
static bool isBuiltWithGmp();
static bool isBuiltWithCln();
static bool isBuiltWithGlpk();
+ static bool isBuiltWithReadline();
+
static bool isBuiltWithCudd();
static bool isBuiltWithTlsSupport();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e33c5fa36..5d078b5ef 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -107,6 +107,18 @@ namespace CVC4 {
# define IS_GLPK_BUILD false
#endif /* CVC4_USE_GLPK */
+#ifdef HAVE_LIBREADLINE
+# define IS_READLINE_BUILD true
+#else /* HAVE_LIBREADLINE */
+# define IS_READLINE_BUILD false
+#endif /* HAVE_LIBREADLINE */
+
+#if CVC4_GPL_DEPS
+# define IS_GPL_BUILD true
+#else /* CVC4_GPL_DEPS */
+# define IS_GPL_BUILD false
+#endif /* CVC4_GPL_DEPS */
+
#ifdef TLS
# define USING_TLS true
#else /* TLS */
@@ -126,24 +138,16 @@ compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
New York University and The University of Iowa\n\n" + \
- ( IS_CLN_BUILD ? "\
-This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without CLN if you want to license CVC4 under the (modified) BSD license.\n\n\
-" : ( IS_GLPK_BUILD ? "\
-This CVC4 library uses GLPK in its arithmetic solver.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, GLPK, the GNU Linear Programming Kit, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+GLPK, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without GLPK if you want to license CVC4 under the (modified) BSD license.\n\n\
+ ( IS_GPL_BUILD ? "\
+This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\
+General Public License (GPL) version 3. Versions of CVC4 are available\n\
+that are covered by the (modified) BSD license. If you want to license\n\
+CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\
+before building from sources.\n\
" : \
"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
CVC4 is open-source and is covered by the BSD license (modified).\n\n\
-" ) ) + "\
+" ) + "\
THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\
See the file COPYING (distributed with the source code, and with all binaries)\n\
for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" )
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1daa0d1e8..5c591d39c 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -152,7 +152,8 @@ BUG_TESTS = \
bug521.minimized.smt2 \
bug522.smt2 \
bug528a.smt2 \
- bug541.smt2
+ bug541.smt2 \
+ bug544.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/bug544.smt2 b/test/regress/regress0/bug544.smt2
new file mode 100644
index 000000000..ec2ef0075
--- /dev/null
+++ b/test/regress/regress0/bug544.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+; EXPECT: (((not (select a x)) false))
+(set-option :produce-models true)
+(set-logic QF_AUFLIA)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun a () (Array U Bool))
+(assert (select a x))
+(check-sat)
+(get-value ((not (select a x))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback