From 2821b7a47e779c7d4f189ffdffaebe4bdb5b9036 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Wed, 29 Feb 2012 20:33:43 +0000 Subject: [PATCH] This should fix the debian build fails: * removed bvpicosat directory as it is currently not used Cleared some of the flurry of warnings my previous merge caused in src/prop/ --- src/prop/bvminisat/core/SolverTypes.h | 9 + src/prop/bvpicosat/LICENSE | 20 - src/prop/bvpicosat/Makefile.am | 24 - src/prop/bvpicosat/Makefile.in | 633 -- src/prop/bvpicosat/NEWS | 93 - src/prop/bvpicosat/README | 5 - src/prop/bvpicosat/VERSION | 1 - src/prop/bvpicosat/app.c | 923 --- src/prop/bvpicosat/config.h | 3 - src/prop/bvpicosat/configure | 151 - src/prop/bvpicosat/main.c | 90 - src/prop/bvpicosat/makefile | 43 - src/prop/bvpicosat/makefile.in | 43 - src/prop/bvpicosat/mkconfig | 35 - src/prop/bvpicosat/picomus.c | 340 -- src/prop/bvpicosat/picosat.c | 7731 ------------------------- src/prop/bvpicosat/picosat.h | 484 -- src/prop/bvpicosat/version.c | 14 - src/prop/cnf_stream.cpp | 2 +- src/prop/minisat/core/SolverTypes.h | 21 +- src/prop/minisat/mtl/Vec.h | 2 +- src/prop/minisat/simp/SimpSolver.h | 2 +- src/prop/minisat/utils/Options.h | 2 +- src/prop/sat_module.cpp | 126 +- src/prop/sat_module.h | 144 +- src/theory/bv/bitblast_strategies.cpp | 13 +- src/theory/bv/bv_sat.cpp | 5 + src/theory/bv/bv_sat.h | 6 +- 28 files changed, 184 insertions(+), 10781 deletions(-) delete mode 100644 src/prop/bvpicosat/LICENSE delete mode 100644 src/prop/bvpicosat/Makefile.am delete mode 100644 src/prop/bvpicosat/Makefile.in delete mode 100644 src/prop/bvpicosat/NEWS delete mode 100644 src/prop/bvpicosat/README delete mode 100644 src/prop/bvpicosat/VERSION delete mode 100644 src/prop/bvpicosat/app.c delete mode 100644 src/prop/bvpicosat/config.h delete mode 100755 src/prop/bvpicosat/configure delete mode 100644 src/prop/bvpicosat/main.c delete mode 100644 src/prop/bvpicosat/makefile delete mode 100644 src/prop/bvpicosat/makefile.in delete mode 100755 src/prop/bvpicosat/mkconfig delete mode 100644 src/prop/bvpicosat/picomus.c delete mode 100644 src/prop/bvpicosat/picosat.c delete mode 100644 src/prop/bvpicosat/picosat.h delete mode 100644 src/prop/bvpicosat/version.c diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index 3709715b9..0439a46c4 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -80,9 +80,18 @@ const Lit lit_Error = { -1 }; // } // does enough constant propagation to produce sensible code, and this appears to be somewhat // fragile unfortunately. + +#ifndef l_True #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants. +#endif + +#ifndef l_False #define l_False (lbool((uint8_t)1)) +#endif + +#ifndef l_Undef #define l_Undef (lbool((uint8_t)2)) +#endif class lbool { uint8_t value; diff --git a/src/prop/bvpicosat/LICENSE b/src/prop/bvpicosat/LICENSE deleted file mode 100644 index b2483af20..000000000 --- a/src/prop/bvpicosat/LICENSE +++ /dev/null @@ -1,20 +0,0 @@ -Copyright (c) 2006 - 2010, Armin Biere, Johannes Kepler University. - -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to -deal in the Software without restriction, including without limitation the -rights to use, copy, modify, merge, publish, distribute, sublicense, and/or -sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in -all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING -FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS -IN THE SOFTWARE. - diff --git a/src/prop/bvpicosat/Makefile.am b/src/prop/bvpicosat/Makefile.am deleted file mode 100644 index c31a3824c..000000000 --- a/src/prop/bvpicosat/Makefile.am +++ /dev/null @@ -1,24 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@srcdir@/ -I@srcdir@/../.. -I@srcdir@/../../.. -I@builddir@/../../.. -I@srcdir@/../../../include -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libpicosat.la -libpicosat_la_SOURCES = \ - app.c \ - picosat.h \ - picosat.c \ - picomus.c \ - version.c - -EXTRA_DIST = \ - main.c \ - README \ - LICENSE \ - NEWS \ - VERSION \ - configure \ - mkconfig \ - makefile.in diff --git a/src/prop/bvpicosat/Makefile.in b/src/prop/bvpicosat/Makefile.in deleted file mode 100644 index a1c392bac..000000000 --- a/src/prop/bvpicosat/Makefile.in +++ /dev/null @@ -1,633 +0,0 @@ -# Makefile.in generated by automake 1.11.1 from Makefile.am. -# @configure_input@ - -# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, -# 2003, 2004, 2005, 2006, 2007, 2008, 2009 Free Software Foundation, -# Inc. -# This Makefile.in is free software; the Free Software Foundation -# gives unlimited permission to copy and/or distribute it, -# with or without modifications, as long as this notice is preserved. - -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY, to the extent permitted by law; without -# even the implied warranty of MERCHANTABILITY or FITNESS FOR A -# PARTICULAR PURPOSE. - -@SET_MAKE@ - -VPATH = @srcdir@ -pkgdatadir = $(datadir)/@PACKAGE@ -pkgincludedir = $(includedir)/@PACKAGE@ -pkglibdir = $(libdir)/@PACKAGE@ -pkglibexecdir = $(libexecdir)/@PACKAGE@ -am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd -install_sh_DATA = $(install_sh) -c -m 644 -install_sh_PROGRAM = $(install_sh) -c -install_sh_SCRIPT = $(install_sh) -c -INSTALL_HEADER = $(INSTALL_DATA) -transform = $(program_transform_name) -NORMAL_INSTALL = : -PRE_INSTALL = : -POST_INSTALL = : -NORMAL_UNINSTALL = : -PRE_UNINSTALL = : -POST_UNINSTALL = : -build_triplet = @build@ -host_triplet = @host@ -target_triplet = @target@ -subdir = src/prop/bvpicosat -DIST_COMMON = README $(srcdir)/Makefile.am $(srcdir)/Makefile.in NEWS -ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ - $(top_srcdir)/config/ax_prog_doxygen.m4 \ - $(top_srcdir)/config/ax_tls.m4 \ - $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ - $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ - $(top_srcdir)/config/gcc_version.m4 \ - $(top_srcdir)/config/libtool.m4 \ - $(top_srcdir)/config/ltoptions.m4 \ - $(top_srcdir)/config/ltsugar.m4 \ - $(top_srcdir)/config/ltversion.m4 \ - $(top_srcdir)/config/lt~obsolete.m4 \ - $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ - $(top_srcdir)/configure.ac -am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ - $(ACLOCAL_M4) -mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h -CONFIG_CLEAN_FILES = -CONFIG_CLEAN_VPATH_FILES = -LTLIBRARIES = $(noinst_LTLIBRARIES) -libpicosat_la_LIBADD = -am_libpicosat_la_OBJECTS = app.lo picosat.lo picomus.lo version.lo -libpicosat_la_OBJECTS = $(am_libpicosat_la_OBJECTS) -AM_V_lt = $(am__v_lt_$(V)) -am__v_lt_ = $(am__v_lt_$(AM_DEFAULT_VERBOSITY)) -am__v_lt_0 = --silent -DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) -depcomp = $(SHELL) $(top_srcdir)/config/depcomp -am__depfiles_maybe = depfiles -am__mv = mv -f -COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ - $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) -LTCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \ - $(LIBTOOLFLAGS) --mode=compile $(CC) $(DEFS) \ - $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \ - $(AM_CFLAGS) $(CFLAGS) -AM_V_CC = $(am__v_CC_$(V)) -am__v_CC_ = $(am__v_CC_$(AM_DEFAULT_VERBOSITY)) -am__v_CC_0 = @echo " CC " $@; -AM_V_at = $(am__v_at_$(V)) -am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) -am__v_at_0 = @ -CCLD = $(CC) -LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \ - $(LIBTOOLFLAGS) --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \ - $(AM_LDFLAGS) $(LDFLAGS) -o $@ -AM_V_CCLD = $(am__v_CCLD_$(V)) -am__v_CCLD_ = $(am__v_CCLD_$(AM_DEFAULT_VERBOSITY)) -am__v_CCLD_0 = @echo " CCLD " $@; -AM_V_GEN = $(am__v_GEN_$(V)) -am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) -am__v_GEN_0 = @echo " GEN " $@; -SOURCES = $(libpicosat_la_SOURCES) -DIST_SOURCES = $(libpicosat_la_SOURCES) -ETAGS = etags -CTAGS = ctags -DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) -ACLOCAL = @ACLOCAL@ -AMTAR = @AMTAR@ -AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ -ANTLR = @ANTLR@ -ANTLR_HOME = @ANTLR_HOME@ -ANTLR_INCLUDES = @ANTLR_INCLUDES@ -ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ -AR = @AR@ -AS = @AS@ -AUTOCONF = @AUTOCONF@ -AUTOHEADER = @AUTOHEADER@ -AUTOMAKE = @AUTOMAKE@ -AWK = @AWK@ -BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ -BOOST_LDPATH = @BOOST_LDPATH@ -BOOST_ROOT = @BOOST_ROOT@ -BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ -BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ -BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ -BUILDING_SHARED = @BUILDING_SHARED@ -BUILDING_STATIC = @BUILDING_STATIC@ -CAMLP4O = @CAMLP4O@ -CC = @CC@ -CCDEPMODE = @CCDEPMODE@ -CFLAGS = @CFLAGS@ -CLN_CFLAGS = @CLN_CFLAGS@ -CLN_LIBS = @CLN_LIBS@ -CPP = @CPP@ -CPPFLAGS = @CPPFLAGS@ -CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ -CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ -CUDD_LDFLAGS = @CUDD_LDFLAGS@ -CUDD_LIBS = @CUDD_LIBS@ -CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ -CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ -CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ -CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ -CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ -CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ -CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ -CVC4_TLS = @CVC4_TLS@ -CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ -CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ -CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ -CXX = @CXX@ -CXXCPP = @CXXCPP@ -CXXDEPMODE = @CXXDEPMODE@ -CXXFLAGS = @CXXFLAGS@ -CXXTEST = @CXXTEST@ -CXXTESTGEN = @CXXTESTGEN@ -CYGPATH_W = @CYGPATH_W@ -DEFS = @DEFS@ -DEPDIR = @DEPDIR@ -DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ -DLLTOOL = @DLLTOOL@ -DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ -DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ -DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ -DSYMUTIL = @DSYMUTIL@ -DUMPBIN = @DUMPBIN@ -DX_CONFIG = @DX_CONFIG@ -DX_DOCDIR = @DX_DOCDIR@ -DX_DOT = @DX_DOT@ -DX_DOXYGEN = @DX_DOXYGEN@ -DX_DVIPS = @DX_DVIPS@ -DX_EGREP = @DX_EGREP@ -DX_ENV = @DX_ENV@ -DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ -DX_FLAG_chi = @DX_FLAG_chi@ -DX_FLAG_chm = @DX_FLAG_chm@ -DX_FLAG_doc = @DX_FLAG_doc@ -DX_FLAG_dot = @DX_FLAG_dot@ -DX_FLAG_html = @DX_FLAG_html@ -DX_FLAG_man = @DX_FLAG_man@ -DX_FLAG_pdf = @DX_FLAG_pdf@ -DX_FLAG_ps = @DX_FLAG_ps@ -DX_FLAG_rtf = @DX_FLAG_rtf@ -DX_FLAG_xml = @DX_FLAG_xml@ -DX_HHC = @DX_HHC@ -DX_LATEX = @DX_LATEX@ -DX_MAKEINDEX = @DX_MAKEINDEX@ -DX_PDFLATEX = @DX_PDFLATEX@ -DX_PERL = @DX_PERL@ -DX_PROJECT = @DX_PROJECT@ -ECHO_C = @ECHO_C@ -ECHO_N = @ECHO_N@ -ECHO_T = @ECHO_T@ -EGREP = @EGREP@ -EXEEXT = @EXEEXT@ -FGREP = @FGREP@ -FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ -GREP = @GREP@ -INSTALL = @INSTALL@ -INSTALL_DATA = @INSTALL_DATA@ -INSTALL_PROGRAM = @INSTALL_PROGRAM@ -INSTALL_SCRIPT = @INSTALL_SCRIPT@ -INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ -JAR = @JAR@ -JAVA = @JAVA@ -JAVAC = @JAVAC@ -JAVAH = @JAVAH@ -JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ -LD = @LD@ -LDFLAGS = @LDFLAGS@ -LFSC = @LFSC@ -LFSCARGS = @LFSCARGS@ -LIBOBJS = @LIBOBJS@ -LIBS = @LIBS@ -LIBTOOL = @LIBTOOL@ -LIPO = @LIPO@ -LN_S = @LN_S@ -LTLIBOBJS = @LTLIBOBJS@ -MAINT = @MAINT@ -MAKEINFO = @MAKEINFO@ -MANIFEST_TOOL = @MANIFEST_TOOL@ -MAN_DATE = @MAN_DATE@ -MKDIR_P = @MKDIR_P@ -NM = @NM@ -NMEDIT = @NMEDIT@ -OBJDUMP = @OBJDUMP@ -OBJEXT = @OBJEXT@ -OCAMLC = @OCAMLC@ -OCAMLFIND = @OCAMLFIND@ -OCAMLMKTOP = @OCAMLMKTOP@ -OTOOL = @OTOOL@ -OTOOL64 = @OTOOL64@ -PACKAGE = @PACKAGE@ -PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@ -PACKAGE_NAME = @PACKAGE_NAME@ -PACKAGE_STRING = @PACKAGE_STRING@ -PACKAGE_TARNAME = @PACKAGE_TARNAME@ -PACKAGE_URL = @PACKAGE_URL@ -PACKAGE_VERSION = @PACKAGE_VERSION@ -PATH_SEPARATOR = @PATH_SEPARATOR@ -PERL = @PERL@ -PERL_CPPFLAGS = @PERL_CPPFLAGS@ -PHP_CPPFLAGS = @PHP_CPPFLAGS@ -PKG_CONFIG = @PKG_CONFIG@ -PYTHON = @PYTHON@ -PYTHON_CONFIG = @PYTHON_CONFIG@ -PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ -PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ -PYTHON_INCLUDE = @PYTHON_INCLUDE@ -PYTHON_PLATFORM = @PYTHON_PLATFORM@ -PYTHON_PREFIX = @PYTHON_PREFIX@ -PYTHON_VERSION = @PYTHON_VERSION@ -RANLIB = @RANLIB@ -READLINE_LIBS = @READLINE_LIBS@ -RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ -SED = @SED@ -SET_MAKE = @SET_MAKE@ -SHELL = @SHELL@ -STATIC_BINARY = @STATIC_BINARY@ -STRIP = @STRIP@ -SWIG = @SWIG@ -TCL_CPPFLAGS = @TCL_CPPFLAGS@ -TEST_CPPFLAGS = @TEST_CPPFLAGS@ -TEST_CXXFLAGS = @TEST_CXXFLAGS@ -TEST_LDFLAGS = @TEST_LDFLAGS@ -VERSION = @VERSION@ -WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ -abs_builddir = @abs_builddir@ -abs_srcdir = @abs_srcdir@ -abs_top_builddir = @abs_top_builddir@ -abs_top_srcdir = @abs_top_srcdir@ -ac_ct_AR = @ac_ct_AR@ -ac_ct_CC = @ac_ct_CC@ -ac_ct_CXX = @ac_ct_CXX@ -ac_ct_DUMPBIN = @ac_ct_DUMPBIN@ -am__include = @am__include@ -am__leading_dot = @am__leading_dot@ -am__quote = @am__quote@ -am__tar = @am__tar@ -am__untar = @am__untar@ -bindir = @bindir@ -build = @build@ -build_alias = @build_alias@ -build_cpu = @build_cpu@ -build_os = @build_os@ -build_vendor = @build_vendor@ -builddir = @builddir@ -datadir = @datadir@ -datarootdir = @datarootdir@ -docdir = @docdir@ -dvidir = @dvidir@ -exec_prefix = @exec_prefix@ -host = @host@ -host_alias = @host_alias@ -host_cpu = @host_cpu@ -host_os = @host_os@ -host_vendor = @host_vendor@ -htmldir = @htmldir@ -includedir = @includedir@ -infodir = @infodir@ -install_sh = @install_sh@ -libdir = @libdir@ -libexecdir = @libexecdir@ -localedir = @localedir@ -localstatedir = @localstatedir@ -mandir = @mandir@ -mk_include = @mk_include@ -mkdir_p = @mkdir_p@ -oldincludedir = @oldincludedir@ -pdfdir = @pdfdir@ -pkgpyexecdir = @pkgpyexecdir@ -pkgpythondir = @pkgpythondir@ -prefix = @prefix@ -program_transform_name = @program_transform_name@ -psdir = @psdir@ -pyexecdir = @pyexecdir@ -pythondir = @pythondir@ -sbindir = @sbindir@ -sharedstatedir = @sharedstatedir@ -srcdir = @srcdir@ -sysconfdir = @sysconfdir@ -target = @target@ -target_alias = @target_alias@ -target_cpu = @target_cpu@ -target_os = @target_os@ -target_vendor = @target_vendor@ -top_build_prefix = @top_build_prefix@ -top_builddir = @top_builddir@ -top_srcdir = @top_srcdir@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@srcdir@/ -I@srcdir@/../.. -I@srcdir@/../../.. -I@builddir@/../../.. -I@srcdir@/../../../include - -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -noinst_LTLIBRARIES = libpicosat.la -libpicosat_la_SOURCES = \ - app.c \ - picosat.h \ - picosat.c \ - picomus.c \ - version.c - -EXTRA_DIST = \ - main.c \ - README \ - LICENSE \ - NEWS \ - VERSION \ - configure \ - mkconfig \ - makefile.in - -all: all-am - -.SUFFIXES: -.SUFFIXES: .c .lo .o .obj -$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) - @for dep in $?; do \ - case '$(am__configure_deps)' in \ - *$$dep*) \ - ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \ - && { if test -f $@; then exit 0; else break; fi; }; \ - exit 1;; \ - esac; \ - done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu src/prop/bvpicosat/Makefile'; \ - $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu src/prop/bvpicosat/Makefile -.PRECIOUS: Makefile -Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status - @case '$?' in \ - *config.status*) \ - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \ - *) \ - echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \ - cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \ - esac; - -$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh - -$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(am__aclocal_m4_deps): - -clean-noinstLTLIBRARIES: - -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES) - @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \ - dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \ - test "$$dir" != "$$p" || dir=.; \ - echo "rm -f \"$${dir}/so_locations\""; \ - rm -f "$${dir}/so_locations"; \ - done -libpicosat.la: $(libpicosat_la_OBJECTS) $(libpicosat_la_DEPENDENCIES) - $(AM_V_CCLD)$(LINK) $(libpicosat_la_OBJECTS) $(libpicosat_la_LIBADD) $(LIBS) - -mostlyclean-compile: - -rm -f *.$(OBJEXT) - -distclean-compile: - -rm -f *.tab.c - -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/app.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/picomus.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/picosat.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/version.Plo@am__quote@ - -.c.o: -@am__fastdepCC_TRUE@ $(AM_V_CC)$(COMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< -@am__fastdepCC_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po -@am__fastdepCC_FALSE@ $(AM_V_CC) @AM_BACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ DEPDIR=$(DEPDIR) $(CCDEPMODE) $(depcomp) @AMDEPBACKSLASH@ -@am__fastdepCC_FALSE@ $(COMPILE) -c $< - -.c.obj: -@am__fastdepCC_TRUE@ $(AM_V_CC)$(COMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'` -@am__fastdepCC_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po -@am__fastdepCC_FALSE@ $(AM_V_CC) @AM_BACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ DEPDIR=$(DEPDIR) $(CCDEPMODE) $(depcomp) @AMDEPBACKSLASH@ -@am__fastdepCC_FALSE@ $(COMPILE) -c `$(CYGPATH_W) '$<'` - -.c.lo: -@am__fastdepCC_TRUE@ $(AM_V_CC)$(LTCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< -@am__fastdepCC_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo -@am__fastdepCC_FALSE@ $(AM_V_CC) @AM_BACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ -@AMDEP_TRUE@@am__fastdepCC_FALSE@ DEPDIR=$(DEPDIR) $(CCDEPMODE) $(depcomp) @AMDEPBACKSLASH@ -@am__fastdepCC_FALSE@ $(LTCOMPILE) -c -o $@ $< - -mostlyclean-libtool: - -rm -f *.lo - -clean-libtool: - -rm -rf .libs _libs - -ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES) - list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ - unique=`for i in $$list; do \ - if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ - done | \ - $(AWK) '{ files[$$0] = 1; nonempty = 1; } \ - END { if (nonempty) { for (i in files) print i; }; }'`; \ - mkid -fID $$unique -tags: TAGS - -TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ - $(TAGS_FILES) $(LISP) - set x; \ - here=`pwd`; \ - list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ - unique=`for i in $$list; do \ - if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ - done | \ - $(AWK) '{ files[$$0] = 1; nonempty = 1; } \ - END { if (nonempty) { for (i in files) print i; }; }'`; \ - shift; \ - if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \ - test -n "$$unique" || unique=$$empty_fix; \ - if test $$# -gt 0; then \ - $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ - "$$@" $$unique; \ - else \ - $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ - $$unique; \ - fi; \ - fi -ctags: CTAGS -CTAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ - $(TAGS_FILES) $(LISP) - list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ - unique=`for i in $$list; do \ - if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ - done | \ - $(AWK) '{ files[$$0] = 1; nonempty = 1; } \ - END { if (nonempty) { for (i in files) print i; }; }'`; \ - test -z "$(CTAGS_ARGS)$$unique" \ - || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \ - $$unique - -GTAGS: - here=`$(am__cd) $(top_builddir) && pwd` \ - && $(am__cd) $(top_srcdir) \ - && gtags -i $(GTAGS_ARGS) "$$here" - -distclean-tags: - -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags - -distdir: $(DISTFILES) - @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ - topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ - list='$(DISTFILES)'; \ - dist_files=`for file in $$list; do echo $$file; done | \ - sed -e "s|^$$srcdirstrip/||;t" \ - -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \ - case $$dist_files in \ - */*) $(MKDIR_P) `echo "$$dist_files" | \ - sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \ - sort -u` ;; \ - esac; \ - for file in $$dist_files; do \ - if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ - if test -d $$d/$$file; then \ - dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \ - if test -d "$(distdir)/$$file"; then \ - find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ - fi; \ - if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ - cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \ - find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ - fi; \ - cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \ - else \ - test -f "$(distdir)/$$file" \ - || cp -p $$d/$$file "$(distdir)/$$file" \ - || exit 1; \ - fi; \ - done -check-am: all-am -check: check-am -all-am: Makefile $(LTLIBRARIES) -installdirs: -install: install-am -install-exec: install-exec-am -install-data: install-data-am -uninstall: uninstall-am - -install-am: all-am - @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am - -installcheck: installcheck-am -install-strip: - $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ - install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ - `test -z '$(STRIP)' || \ - echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install -mostlyclean-generic: - -clean-generic: - -distclean-generic: - -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES) - -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES) - -maintainer-clean-generic: - @echo "This command is intended for maintainers to use" - @echo "it deletes files that may require special tools to rebuild." -clean: clean-am - -clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \ - mostlyclean-am - -distclean: distclean-am - -rm -rf ./$(DEPDIR) - -rm -f Makefile -distclean-am: clean-am distclean-compile distclean-generic \ - distclean-tags - -dvi: dvi-am - -dvi-am: - -html: html-am - -html-am: - -info: info-am - -info-am: - -install-data-am: - -install-dvi: install-dvi-am - -install-dvi-am: - -install-exec-am: - -install-html: install-html-am - -install-html-am: - -install-info: install-info-am - -install-info-am: - -install-man: - -install-pdf: install-pdf-am - -install-pdf-am: - -install-ps: install-ps-am - -install-ps-am: - -installcheck-am: - -maintainer-clean: maintainer-clean-am - -rm -rf ./$(DEPDIR) - -rm -f Makefile -maintainer-clean-am: distclean-am maintainer-clean-generic - -mostlyclean: mostlyclean-am - -mostlyclean-am: mostlyclean-compile mostlyclean-generic \ - mostlyclean-libtool - -pdf: pdf-am - -pdf-am: - -ps: ps-am - -ps-am: - -uninstall-am: - -.MAKE: install-am install-strip - -.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \ - clean-libtool clean-noinstLTLIBRARIES ctags distclean \ - distclean-compile distclean-generic distclean-libtool \ - distclean-tags distdir dvi dvi-am html html-am info info-am \ - install install-am install-data install-data-am install-dvi \ - install-dvi-am install-exec install-exec-am install-html \ - install-html-am install-info install-info-am install-man \ - install-pdf install-pdf-am install-ps install-ps-am \ - install-strip installcheck installcheck-am installdirs \ - maintainer-clean maintainer-clean-generic mostlyclean \ - mostlyclean-compile mostlyclean-generic mostlyclean-libtool \ - pdf pdf-am ps ps-am tags uninstall uninstall-am - - -# Tell versions [3.59,3.63) of GNU make to not export all variables. -# Otherwise a system limit (for SysV at least) may be exceeded. -.NOEXPORT: diff --git a/src/prop/bvpicosat/NEWS b/src/prop/bvpicosat/NEWS deleted file mode 100644 index ea3e1ce26..000000000 --- a/src/prop/bvpicosat/NEWS +++ /dev/null @@ -1,93 +0,0 @@ -news for release 936 since 935 ------------------------------- - -* simple minimal unsatisfiable core (MUS) extractor 'picomus' - (example for using 'picosat_mus_assumptions' and 'picosat_coreclause') - -* added 'picosat_mus_assumptions' - -* added 'picosat_{set_}propagations' - -* new 'int' return value for 'picosat_enable_trace_generation' to - check for trace code being compiled - -news for release 935 since 926 ------------------------------- - -* added 'picosat_failed_assumptions' (plural) - -* new '-A ' command line option - -* fixed failed assumption issues - -* added 'picosat_remove_learned' - -* added 'picosat_reset_{phases,scores}' - -* added 'picosat_set_less_important_lit' - -* added 'picosat_res' - -news for release 926 since 846 ------------------------------- - -* random initial phase (API of 'picosat_set_default_phase' changed) - -* fixed accumulative failed assumption (multiple times) - -* fixed missing original clause in core generation with assumptions - -* fixed debugging code for memory allocation - -* shared library in addition to static library - -* removed potential UNKNOWN result without decision limit - -* added picosat_set_more_important_lit - -* added picosat_coreclause - -* propagation of binary clauses until completion - -* fixed API usage 'assume;sat;sat' - -* literals move to front (LMTF) during traversal of visited clauses - -* switched from inner/outer to Luby style restart scheduling - -* less agressive reduce schedule - -* replaced watched literals with head and tail pointers - -* add 'picosat_failed_assumption', which allows to avoid tracing and core - generation, if one is only interested in assumptions in the core - -* fixed a BUG in the generic iterator code of clauses - (should rarely happen unless you use a very sophisticated malloc lib) - -news for release 846 since 632 ------------------------------- - -* cleaned up assumption handling (actually removed buggy optimization) - -* incremental core generation - -* experimental 'all different constraint' handling as in our FMCAD'08 paper - -* new API calls: - - - picosat_add_ado_lit (add all different object literal) - - picosat_deref_top_level (deref top level assignment) - - picosat_changed (check whether extension was possible) - - picosat_measure_all_calls (per default do not measure adding time) - - picosat_set_prefix (set prefix for messages) - -* 64 bit port (and compilation options) - -* optional NVSIDS visualization code - -* resource controlled failed literal implementation - -* disconnect long clauses satisfied at lower decision level - -* controlling restarts diff --git a/src/prop/bvpicosat/README b/src/prop/bvpicosat/README deleted file mode 100644 index 89d6ea5f6..000000000 --- a/src/prop/bvpicosat/README +++ /dev/null @@ -1,5 +0,0 @@ -These are the sources of the PicoSAT solver. -The preprocessor is not included. -To compile run './configure && make'. -The API is document in 'picosat.h'. -See also 'NEWS' and 'LICENSE'. diff --git a/src/prop/bvpicosat/VERSION b/src/prop/bvpicosat/VERSION deleted file mode 100644 index 10c7f0b94..000000000 --- a/src/prop/bvpicosat/VERSION +++ /dev/null @@ -1 +0,0 @@ -936 diff --git a/src/prop/bvpicosat/app.c b/src/prop/bvpicosat/app.c deleted file mode 100644 index 667a2ac8c..000000000 --- a/src/prop/bvpicosat/app.c +++ /dev/null @@ -1,923 +0,0 @@ -#include "picosat.h" - -#include -#include -#include -#include - -#define GUNZIP "gunzip -c %s" -#define GZIP "gzip -c -f > %s" - -FILE * popen (const char *, const char*); -int pclose (FILE *); - -static int lineno; -static FILE *input; -static int inputid; -static FILE *output; -static int verbose; -static int sargc; -static char ** sargv; -static char buffer[100]; -static char *bhead = buffer; -static const char *eob = buffer + 80; -static FILE * incremental_rup_file; - -extern void picosat_enter (void); -extern void picosat_leave (void); - -static char page[4096]; -static char * top; -static char * end; - -static int -next (void) -{ - size_t bytes; - int res; - - if (top == end) - { - if (end < page + sizeof page) - return EOF; - - bytes = fread (page, 1, sizeof page, input); - if (bytes == 0) - return EOF; - - top = page; - end = page + bytes; - } - - res = *top++; - - if (res == '\n') - lineno++; - - return res; -} - -static const char * -parse (int force) -{ - int ch, sign, lit, vars, clauses; - - lineno = 1; - inputid = fileno (input); - -SKIP_COMMENTS: - ch = next (); - if (ch == 'c') - { - while ((ch = next ()) != EOF && ch != '\n') - ; - goto SKIP_COMMENTS; - } - - if (isspace (ch)) - goto SKIP_COMMENTS; - - if (ch != 'p') -INVALID_HEADER: - return "missing or invalid 'p cnf ' header"; - - if (!isspace (next ())) - goto INVALID_HEADER; - - while (isspace (ch = next ())) - ; - - if (ch != 'c' || next () != 'n' || next () != 'f' || !isspace (next ())) - goto INVALID_HEADER; - - while (isspace (ch = next ())) - ; - - if (!isdigit (ch)) - goto INVALID_HEADER; - - vars = ch - '0'; - while (isdigit (ch = next ())) - vars = 10 * vars + (ch - '0'); - - if (!isspace (ch)) - goto INVALID_HEADER; - - while (isspace (ch = next ())) - ; - - if (!isdigit (ch)) - goto INVALID_HEADER; - - clauses = ch - '0'; - while (isdigit (ch = next ())) - clauses = 10 * clauses + (ch - '0'); - - if (!isspace (ch) && ch != '\n' ) - goto INVALID_HEADER; - - if (verbose) - { - fprintf (output, "c parsed header 'p cnf %d %d'\n", vars, clauses); - fflush (output); - } - - picosat_adjust (vars); - - if (incremental_rup_file) - picosat_set_incremental_rup_file (incremental_rup_file, vars, clauses); - - lit = 0; -READ_LITERAL: - ch = next (); - - if (ch == 'c') - { - while ((ch = next ()) != EOF && ch != '\n') - ; - goto READ_LITERAL; - } - - if (ch == EOF) - { - if (lit) - return "trailing 0 missing"; - - if (clauses && !force) - return "clause missing"; - - return 0; - } - - if (isspace (ch)) - goto READ_LITERAL; - - sign = 1; - if (ch == '-') - { - sign = -1; - ch = next (); - } - - if (!isdigit (ch)) - return "expected number"; - - lit = ch - '0'; - while (isdigit (ch = next ())) - lit = 10 * lit + (ch - '0'); - - if (!clauses && !force) - return "too many clauses"; - - if (lit) - { - if (lit > vars && !force) - return "maximal variable index exceeded"; - - lit *= sign; - } - else - clauses--; - - picosat_add (lit); - - goto READ_LITERAL; -} - -static void -bflush (void) -{ - *bhead = 0; - fputs (buffer, output); - fputc ('\n', output); - bhead = buffer; -} - -static void -printi (int i) -{ - char *next; - int l; - -REENTER: - if (bhead == buffer) - *bhead++ = 'v'; - - l = sprintf (bhead, " %d", i); - next = bhead + l; - - if (next >= eob) - { - bflush (); - goto REENTER; - } - else - bhead = next; -} - -static void -printa (void) -{ - int max_idx = picosat_variables (), i, lit; - - assert (bhead == buffer); - - for (i = 1; i <= max_idx; i++) - { - lit = (picosat_deref (i) > 0) ? i : -i; - printi (lit); - } - - printi (0); - if (bhead > buffer) - bflush (); -} - -static int -has_suffix (const char *str, const char *suffix) -{ - const char *tmp = strstr (str, suffix); - if (!tmp) - return 0; - - return str + strlen (str) - strlen (suffix) == tmp; -} - -static void -write_core_variables (FILE * file) -{ - int i, max_idx = picosat_variables (), count = 0; - for (i = 1; i <= max_idx; i++) - if (picosat_corelit (i)) - { - fprintf (file, "%d\n", i); - count++; - } - - if (verbose) - fprintf (output, "c found and wrote %d core variables\n", count); -} - -static int -next_assumption (int start) -{ - char * arg, c; - int res; - res = start + 1; - while (res < sargc) - { - arg = sargv[res++]; - if (!strcmp (arg, "-a")) - { - assert (res < sargc); - break; - } - - if (arg[0] == '-') { - c = arg[1]; - if (c == 'l' || c == 'i' || c == 's' || c == 'o' || c == 't' || - c == 'T' || c == 'r' || c == 'R' || c == 'c' || c == 'V' || - c == 'U' || c == 'A') res++; - } - } - if (res >= sargc) res = 0; - return res; -} - -static void -write_failed_assumptions (FILE * file) -{ - int i, lit, count = 0; -#ifndef NDEBUG - int max_idx = picosat_variables (); -#endif - i = 0; - while ((i = next_assumption (i))) { - lit = atoi (sargv[i]); - if (!picosat_failed_assumption (lit)) continue; - fprintf (file, "%d\n", lit); - count++; - } - if (verbose) - fprintf (output, "c found and wrote %d failed assumptions\n", count); -#ifndef NDEBUG - for (i = 1; i <= max_idx; i++) - if (picosat_failed_assumption (i)) - count--; -#endif - assert (!count); -} - -static void -write_to_file (const char *name, const char *type, void (*writer) (FILE *)) -{ - int pclose_file, zipped = has_suffix (name, ".gz"); - FILE *file; - char *cmd; - - if (zipped) - { - cmd = malloc (strlen (GZIP) + strlen (name)); - sprintf (cmd, GZIP, name); - file = popen (cmd, "w"); - free (cmd); - pclose_file = 1; - } - else - { - file = fopen (name, "w"); - pclose_file = 0; - } - - if (file) - { - if (verbose) - fprintf (output, - "c\nc writing %s%s to '%s'\n", - zipped ? "gzipped " : "", type, name); - - writer (file); - - if (pclose_file) - pclose (file); - else - fclose (file); - } - else - fprintf (output, "*** picosat: can not write to '%s'\n", name); -} - -#define USAGE \ -"usage: picosat [