diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
commit | 2821b7a47e779c7d4f189ffdffaebe4bdb5b9036 (patch) | |
tree | 16101f79b9c8927645fa896306c1e5cb83721332 /src | |
parent | 9062483193f4ec9b38aaa57b228cae1fb551566a (diff) |
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/
Diffstat (limited to 'src')
28 files changed, 184 insertions, 10781 deletions
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 <failedlits>' 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 <assert.h> -#include <string.h> -#include <ctype.h> -#include <stdio.h> - -#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 <variables> <clauses>' 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 [ <option> ... ] [ <input> ]\n" \ -"\n" \ -"where <option> is one of the following\n" \ -"\n" \ -" -h print this command line option summary and exit\n" \ -" --version print version and exit\n" \ -" --config print build configuration and exit\n" \ -"\n" \ -" -v enable verbose output\n" \ -" -f ignore invalid header\n" \ -" -n do not print satisfying assignment\n" \ -" -p print formula in DIMACS format and exit\n" \ -" -a <lit> start with an assumption\n" \ -" -l <limit> set decision limit (no limit per default)\n" \ -" -P <limit> set propagation limit (no limit per default)\n" \ -" -i [0-3] [0-3]=[FALSE,TRUE,JWH,RAND] initial phase (default 2=JWH)\n" \ -" -s <seed> set random number generator seed (default 0)\n" \ -" -o <output> set output file (<stdout> per default)\n" \ -" -t <trace> generate compact proof trace file\n" \ -" -T <trace> generate extended proof trace file\n" \ -" -r <trace> generate reverse unit propagation proof file\n" \ -" -R <trace> generate reverse unit propagation proof file incrementally\n" \ -" -c <core> generate clausal core file in DIMACS format\n" \ -" -V <core> generate file listing core variables\n" \ -" -U <core> generate file listing used variables\n" \ -" -A <core> generate file listing failed assumptions\n" \ -"\n" \ -"and <input> is an optional input file in DIMACS format.\n" - -int -picosat_main (int argc, char **argv) -{ - int res, done, err, print_satisfying_assignment, force, print_formula; - const char *compact_trace_name, *extended_trace_name, * rup_trace_name; - const char * clausal_core_name, * variable_core_name; - int assumption, assumptions, defaultphase; - const char *input_name, *output_name; - const char * failed_assumptions_name; - int close_input, pclose_input; - long long propagation_limit; - int i, decision_limit; - double start_time; - unsigned seed; - FILE *file; - int trace; - - start_time = picosat_time_stamp (); - - sargc = argc; - sargv = argv; - - clausal_core_name = 0; - variable_core_name = 0; - failed_assumptions_name = 0; - output_name = 0; - compact_trace_name = 0; - extended_trace_name = 0; - rup_trace_name = 0; - incremental_rup_file = 0; - close_input = 0; - pclose_input = 0; - input_name = "<stdin>"; - input = stdin; - output = stdout; - verbose = 0; - done = err = 0; - decision_limit = -1; - propagation_limit = -1; - defaultphase = 2; - assumptions = 0; - force = 0; - trace = 0; - seed = 0; - - top = end = page + sizeof page; - - print_satisfying_assignment = 1; - print_formula = 0; - - for (i = 1; !done && !err && i < argc; i++) - { - if (!strcmp (argv[i], "-h")) - { - fputs (USAGE, output); - done = 1; - } - else if (!strcmp (argv[i], "--version")) - { - fprintf (output, "%s\n", picosat_version ()); - done = 1; - } - else if (!strcmp (argv[i], "--config")) - { - fprintf (output, "%s\n", picosat_config ()); - done = 1; - } - else if (!strcmp (argv[i], "-v")) - { - verbose++; - } - else if (!strcmp (argv[i], "-f")) - { - force = 1; - } - else if (!strcmp (argv[i], "-n")) - { - print_satisfying_assignment = 0; - } - else if (!strcmp (argv[i], "-p")) - { - print_formula = 1; - } - else if (!strcmp (argv[i], "-l")) - { - if (++i == argc) - { - fprintf (output, "*** picosat: argument to '-l' missing\n"); - err = 1; - } - else - decision_limit = atoi (argv[i]); - } - else if (!strcmp (argv[i], "-P")) - { - if (++i == argc) - { - fprintf (output, "*** picosat: argument to '-P' missing\n"); - err = 1; - } - else - propagation_limit = atoll (argv[i]); - } - else if (!strcmp (argv[i], "-i")) - { - if (++i == argc) - { - fprintf (output, "*** picosat: argument to '-i' missing\n"); - err = 1; - } - else if (!argv[i][1] && ('0' <= argv[i][0] && argv[i][0] <= '3')) - { - defaultphase = argv[i][0] - '0'; - } - else - { - fprintf (output, "*** picosat: invalid argument to '-i'\n"); - err = 1; - } - } - else if (!strcmp (argv[i], "-a")) - { - if (++i == argc) - { - fprintf (output, "*** picosat: argument to '-a' missing\n"); - err = 1; - } - else if (!atoi (argv[i])) - { - fprintf (output, "*** picosat: argument to '-a' zero\n"); - err = 1; - } - else - { - /* Handle assumptions further down - */ - assumptions++; - } - } - else if (!strcmp (argv[i], "-s")) - { - if (++i == argc) - { - fprintf (output, "*** picosat: argument to '-s' missing\n"); - err = 1; - } - else - seed = atoi (argv[i]); - } - else if (!strcmp (argv[i], "-o")) - { - if (output_name) - { - fprintf (output, - "*** picosat: " - "multiple output files '%s' and '%s'\n", - output_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-o' missing\n"); - err = 1; - } - else if (!(file = fopen (argv[i], "w"))) - { - fprintf (output, - "*** picosat: " - "can not write output file '%s'\n", argv[i]); - err = 1; - } - else - { - output_name = argv[i]; - output = file; - } - } - else if (!strcmp (argv[i], "-t")) - { - if (compact_trace_name) - { - fprintf (output, - "*** picosat: " - "multiple compact trace files '%s' and '%s'\n", - compact_trace_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-t' missing\n"); - err = 1; - } - else - { - compact_trace_name = argv[i]; - trace = 1; - } - } - else if (!strcmp (argv[i], "-T")) - { - if (extended_trace_name) - { - fprintf (output, - "*** picosat: " - "multiple extended trace files '%s' and '%s'\n", - extended_trace_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-T' missing\n"); - err = 1; - } - else - { - extended_trace_name = argv[i]; - trace = 1; - } - } - else if (!strcmp (argv[i], "-r")) - { - if (rup_trace_name) - { - fprintf (output, - "*** picosat: " - "multiple RUP trace files '%s' and '%s'\n", - rup_trace_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-r' missing\n"); - err = 1; - } - else - { - rup_trace_name = argv[i]; - trace = 1; - } - } - else if (!strcmp (argv[i], "-R")) - { - if (rup_trace_name) - { - fprintf (output, - "*** picosat: " - "multiple RUP trace files '%s' and '%s'\n", - rup_trace_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-R' missing\n"); - err = 1; - } - else if (!(file = fopen (argv[i], "w"))) - { - fprintf (output, - "*** picosat: can not write to '%s'\n", argv[i]); - err = 1; - } - else - { - rup_trace_name = argv[i]; - incremental_rup_file = file; - } - } - else if (!strcmp (argv[i], "-c")) - { - if (clausal_core_name) - { - fprintf (output, - "*** picosat: " - "multiple clausal core files '%s' and '%s'\n", - clausal_core_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-c' missing\n"); - err = 1; - } - else - { - clausal_core_name = argv[i]; - trace = 1; - } - } - else if (!strcmp (argv[i], "-V")) - { - if (variable_core_name) - { - fprintf (output, - "*** picosat: " - "multiple variable core files '%s' and '%s'\n", - variable_core_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-V' missing\n"); - err = 1; - } - else - { - variable_core_name = argv[i]; - trace = 1; - } - } - else if (!strcmp (argv[i], "-A")) - { - if (failed_assumptions_name) - { - fprintf (output, - "*** picosat: " - "multiple failed assumptions files '%s' and '%s'\n", - failed_assumptions_name, argv[i]); - err = 1; - } - else if (++i == argc) - { - fprintf (output, "*** picosat: argument ot '-A' missing\n"); - err = 1; - } - else - failed_assumptions_name = argv[i]; - } - else if (argv[i][0] == '-') - { - fprintf (output, - "*** picosat: " - "unknown command line option '%s' (try '-h')\n", argv[i]); - err = 1; - } - else if (close_input || pclose_input) - { - fprintf (output, - "*** picosat: " - "multiple input files '%s' and '%s'\n", - input_name, argv[i]); - err = 1; - } - else if (has_suffix (argv[i], ".gz")) - { - char *cmd = malloc (strlen (GUNZIP) + strlen (argv[i])); - sprintf (cmd, GUNZIP, argv[i]); - if ((file = popen (cmd, "r"))) - { - input_name = argv[i]; - pclose_input = 1; - input = file; - } - else - { - fprintf (output, - "*** picosat: " - "can not read compressed input file '%s'\n", argv[i]); - err = 1; - } - free (cmd); - } - else if (!(file = fopen (argv[i], "r"))) /* TODO .gz ? */ - { - fprintf (output, - "*** picosat: can not read input file '%s'\n", argv[i]); - err = 1; - } - else - { - input_name = argv[i]; - close_input = 1; - input = file; - } - } - - res = PICOSAT_UNKNOWN; - - if (!done && !err) - { - const char *err_msg; - - if (verbose) - { - fprintf (output, - "c PicoSAT SAT Solver Version %s\n", - picosat_version ()); - - fprintf (output, "c %s\n", picosat_copyright ()); - fprintf (output, "c %s\n", picosat_config ()); - } - - picosat_init (); - picosat_enter (); - - if (output_name) - picosat_set_output (output); - - picosat_set_verbosity (verbose); - - if (verbose) fputs ("c\n", output); - - if (trace) - { - if (verbose) - fprintf (output, "c tracing proof\n"); - picosat_enable_trace_generation (); - } - - if (defaultphase) - { - if (verbose) - fprintf (output, "c using %d as default phase\n", defaultphase); - - picosat_set_global_default_phase (defaultphase); - } - - if (propagation_limit >= 0) - { - if (verbose) - fprintf (output, "c propagation limit of %lld propagations\n", - propagation_limit); - picosat_set_propagation_limit ( - (unsigned long long) propagation_limit); - } - - if (verbose) - fprintf (output, "c\nc parsing %s\n", input_name); - - if ((err_msg = parse (force))) - { - fprintf (output, "%s:%d: %s\n", input_name, lineno, err_msg); - err = 1; - } - else - { - if (assumptions) - { - i = 0; - while ((i = next_assumption (i))) - { - assert (i < argc); - assumption = atoi (argv[i]); - assert (assumption); - - picosat_assume (assumption); - - if (verbose) - fprintf (output, "c assumption %d\n", assumption); - } - } - - if (print_formula) - { - picosat_print (output); - } - else - { - if (verbose) - fprintf (output, - "c initialized %u variables\n" - "c found %u non trivial clauses\n", - picosat_variables (), - picosat_added_original_clauses ()); - - picosat_set_seed (seed); - if (verbose) - fprintf (output, - "c\nc random number generator seed %u\n", - seed); - - res = picosat_sat (decision_limit); - - if (res == PICOSAT_UNSATISFIABLE) - { - fputs ("s UNSATISFIABLE\n", output); - - if (compact_trace_name) - write_to_file (compact_trace_name, - "compact trace", - picosat_write_compact_trace); - - if (extended_trace_name) - write_to_file (extended_trace_name, - "extended trace", - picosat_write_extended_trace); - - if (!incremental_rup_file && rup_trace_name) - write_to_file (rup_trace_name, - "rup trace", - picosat_write_rup_trace); - - if (clausal_core_name) - write_to_file (clausal_core_name, - "clausal core", - picosat_write_clausal_core); - - if (variable_core_name) - write_to_file (variable_core_name, - "variable core", write_core_variables); - - if (failed_assumptions_name) - write_to_file (failed_assumptions_name, - "failed assumptions", - write_failed_assumptions); - } - else if (res == PICOSAT_SATISFIABLE) - { - fputs ("s SATISFIABLE\n", output); - - if (print_satisfying_assignment) - printa (); - } - else - fputs ("s UNKNOWN\n", output); - } - } - - if (!err && verbose) - { - fputs ("c\n", output); - picosat_stats (); - fprintf (output, - "c %.1f seconds total run time\n", - picosat_time_stamp () - start_time); - } - - picosat_leave (); - picosat_reset (); - } - - if (incremental_rup_file) - fclose (incremental_rup_file); - - if (close_input) - fclose (input); - - if (pclose_input) - pclose (input); - - if (output_name) - fclose (output); - - return res; -} diff --git a/src/prop/bvpicosat/config.h b/src/prop/bvpicosat/config.h deleted file mode 100644 index aa6888822..000000000 --- a/src/prop/bvpicosat/config.h +++ /dev/null @@ -1,3 +0,0 @@ -#define PICOSAT_CC "gcc" -#define PICOSAT_CFLAGS "-DSTATS -DTRACE -Wall -Wextra -DNDEBUG -O2" -#define PICOSAT_VERSION "936" diff --git a/src/prop/bvpicosat/configure b/src/prop/bvpicosat/configure deleted file mode 100755 index 23cf0efb4..000000000 --- a/src/prop/bvpicosat/configure +++ /dev/null @@ -1,151 +0,0 @@ -#!/bin/sh - -satcompetition=no - -log=no -debug=no -optimize=no -stats=undefined -trace=undefined -static=yes -shared=no -thirtytwobit=no -static=no - -while [ $# -gt 0 ] -do - case $1 in - -l|--log) debug=yes; log=yes;; - -g|--debug) debug=yes; optimize=no;; - -s|--stats) stats=yes;; - -t|--trace) trace=yes;; - --no-stats) stats=no;; - --no-trace) trace=no;; - -32|--32|-m32) thirtytwobit=yes;; - -static|--static) static=yes;; - -O) debug=no; optimize=yes;; - *) cat <<EOF -usage: ./configure [<option> ...] - -where <option> is one of the following: - - -g|--debug includ debugging code and symbols - -l|--log add low level logging code - -s|--stats include and enable more expensive stats counters - -t|--trace compile with trace generation support (more memory) - --no-stats disable expensive stats - --no-trace enable trace generation (less memory) - -32|--32|-m32 compile for 32 bit machine even on 64 bit host - -static|--static only produce static library - -shared|--shared produce shared library as well - -O optimize a lot and disable trace generation -EOF -exit 1 -;; - esac -shift -done - -echo "version ... `cat VERSION`" - -if [ $satcompetition = yes ] -then - debug=no - optimize=yes - stats=no - trace=no - thirtytwobit=yes - static=yes - shared=no -fi - -echo "debug ... $debug" -echo "optimize ... $optimize" -echo "log ... $log" - -if [ $stats = undefined ] -then - if [ $optimize = yes ] - then - stats=no - else - stats=yes - fi -fi -echo "stats ... $stats" - -if [ $trace = undefined ] -then - if [ $optimize = yes ] - then - trace=no - else - trace=yes - fi -fi -echo "trace ... $trace" - -echo "static ... $static" - -echo "shared ... $shared" - -[ "X$CC" = X ] && CC=gcc - -if [ X"$CFLAGS" = X ] -then - case X"$CC" in - *wine*|*mingw*) CFLAGS="-DNGETRUSAGE -DNALLSIGNALS";; - *);; - esac - [ $log = yes ] && CFLAGS="$CFLAGS -DLOGGING" - [ $stats = yes ] && CFLAGS="$CFLAGS -DSTATS" - [ $trace = yes ] && CFLAGS="$CFLAGS -DTRACE" - [ $static = yes ] && CFLAGS="$CFLAGS -static" - case X"$CC" in - X*gcc*) - CFLAGS="$CFLAGS -Wall -Wextra" - [ $thirtytwobit = yes ] && CFLAGS="$CFLAGS -m32" - if [ $debug = yes ] - then - CFLAGS="$CFLAGS -g3 -ggdb" - else - CFLAGS="$CFLAGS -DNDEBUG" - if [ $optimize = yes ] - then - CFLAGS="$CFLAGS -O3 -fomit-frame-pointer -finline-limit=1000000" - else - CFLAGS="$CFLAGS -O2" - fi - fi - ;; - *) - if [ $debug = yes ] - then - CFLAGS="$CFLAGS -g" - else - CFLAGS="$CFLAGS -O" - fi - ;; - esac -fi - -TARGETS="picosat picomus libpicosat.a" -if [ $shared = yes ] -then - TARGETS="$TARGETS libpicosat.so" - CFLAGS="$CFLAGS -fPIC" -fi -echo "targets ... $TARGETS" - -echo "cc ... $CC" - -echo "cflags ... $CFLAGS" - -echo -n "makefile ..." -rm -f makefile -sed \ - -e "s,@CC@,$CC," \ - -e "s,@CFLAGS@,$CFLAGS," \ - -e "s,@TARGETS@,$TARGETS," \ -makefile.in > makefile -echo " done" diff --git a/src/prop/bvpicosat/main.c b/src/prop/bvpicosat/main.c deleted file mode 100644 index cb82580fa..000000000 --- a/src/prop/bvpicosat/main.c +++ /dev/null @@ -1,90 +0,0 @@ -#include <signal.h> -#include <stdlib.h> -#include <string.h> - -#include "picosat.h" - -int picosat_main (int, char **); - -static int catched; - -static void (*sig_int_handler); -static void (*sig_segv_handler); -static void (*sig_abrt_handler); -static void (*sig_term_handler); -#ifndef NALLSIGNALS -static void (*sig_kill_handler); -static void (*sig_xcpu_handler); -static void (*sig_xfsz_handler); -#endif - -static void -resetsighandlers (void) -{ - (void) signal (SIGINT, sig_int_handler); - (void) signal (SIGSEGV, sig_segv_handler); - (void) signal (SIGABRT, sig_abrt_handler); - (void) signal (SIGTERM, sig_term_handler); -#ifndef NALLSIGNALS - (void) signal (SIGKILL, sig_kill_handler); - (void) signal (SIGXCPU, sig_xcpu_handler); - (void) signal (SIGXFSZ, sig_xfsz_handler); -#endif -} - -static void -message (int sig) -{ - picosat_message (1, ""); - picosat_message (1, "*** CAUGHT SIGNAL %d ***", sig); - picosat_message (1, ""); -} - -static void -catch (int sig) -{ - if (!catched) - { - message (sig); - catched = 1; - picosat_stats (); - message (sig); - } - - resetsighandlers (); - raise (sig); -} - -static void -setsighandlers (void) -{ - sig_int_handler = signal (SIGINT, catch); - sig_segv_handler = signal (SIGSEGV, catch); - sig_abrt_handler = signal (SIGABRT, catch); - sig_term_handler = signal (SIGTERM, catch); -#ifndef NALLSIGNALS - sig_kill_handler = signal (SIGKILL, catch); - sig_xcpu_handler = signal (SIGXCPU, catch); - sig_xfsz_handler = signal (SIGXFSZ, catch); -#endif -} - -int -main (int argc, char **argv) -{ - int res, verbose; - - for (verbose = argc - 1; verbose; verbose--) - if (!strcmp (argv[verbose], "-v")) - break; - - if (verbose) - setsighandlers (); - - res = picosat_main (argc, argv); - - if (verbose) - resetsighandlers (); - - return res; -} diff --git a/src/prop/bvpicosat/makefile b/src/prop/bvpicosat/makefile deleted file mode 100644 index f6fd2f099..000000000 --- a/src/prop/bvpicosat/makefile +++ /dev/null @@ -1,43 +0,0 @@ -CC=gcc -CFLAGS= -DSTATS -DTRACE -Wall -Wextra -DNDEBUG -O2 - -all: picosat picomus libpicosat.a - -clean: - rm -f picosat *.exe *.s *.o *.a *.so - rm -f makefile config.h - rm -f gmon.out *~ - -picosat: libpicosat.a app.o main.o - $(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat - -picomus: libpicosat.a picomus.o - $(CC) $(CFLAGS) -o $@ picomus.o -L. -lpicosat - -app.o: app.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -picomus.o: picomus.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -main.o: main.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -picosat.o: picosat.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -version.o: version.c config.h makefile - $(CC) $(CFLAGS) -c $< - -config.h: makefile VERSION mkconfig # and actually picosat.c - rm -f $@; ./mkconfig > $@ - -libpicosat.a: picosat.o version.o - ar rc $@ picosat.o version.o - ranlib $@ - -SONAME=-Xlinker -soname -Xlinker libpicosat.so -libpicosat.so: picosat.o version.o - $(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME) - -.PHONY: all clean diff --git a/src/prop/bvpicosat/makefile.in b/src/prop/bvpicosat/makefile.in deleted file mode 100644 index 8c8f22299..000000000 --- a/src/prop/bvpicosat/makefile.in +++ /dev/null @@ -1,43 +0,0 @@ -CC=@CC@ -CFLAGS=@CFLAGS@ - -all: @TARGETS@ - -clean: - rm -f picosat *.exe *.s *.o *.a *.so - rm -f makefile config.h - rm -f gmon.out *~ - -picosat: libpicosat.a app.o main.o - $(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat - -picomus: libpicosat.a picomus.o - $(CC) $(CFLAGS) -o $@ picomus.o -L. -lpicosat - -app.o: app.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -picomus.o: picomus.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -main.o: main.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -picosat.o: picosat.c picosat.h makefile - $(CC) $(CFLAGS) -c $< - -version.o: version.c config.h makefile - $(CC) $(CFLAGS) -c $< - -config.h: makefile VERSION mkconfig # and actually picosat.c - rm -f $@; ./mkconfig > $@ - -libpicosat.a: picosat.o version.o - ar rc $@ picosat.o version.o - ranlib $@ - -SONAME=-Xlinker -soname -Xlinker libpicosat.so -libpicosat.so: picosat.o version.o - $(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME) - -.PHONY: all clean diff --git a/src/prop/bvpicosat/mkconfig b/src/prop/bvpicosat/mkconfig deleted file mode 100755 index d0c8fa835..000000000 --- a/src/prop/bvpicosat/mkconfig +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/sh - -die () { - echo "*** mkconfig: $*" 1>&2 - exit 1 -} - -[ -f makefile ] || die "can not find 'makefile'" - -sed \ - -e '/^C[A-Z]*=/!d' \ - -e 's,^,#define PICOSAT_,' \ - -e 's,= *, ",' \ - -e 's,$,",' \ - makefile - -id="" -if [ -d .git -a -f .git/HEAD ] -then - head="`awk 'NF == 1' .git/HEAD`" - if [ x"$head" = x ] - then - head="`awk '{print $2}' .git/HEAD`" - if [ ! x"$head" = x -a -f ".git/$head" ] - then - id=" `cat .git/$head`" - fi - else - id=" $head" - fi -fi - -echo "#define PICOSAT_VERSION \"`cat VERSION`$id\"" - -exit 0 diff --git a/src/prop/bvpicosat/picomus.c b/src/prop/bvpicosat/picomus.c deleted file mode 100644 index bf98dc644..000000000 --- a/src/prop/bvpicosat/picomus.c +++ /dev/null @@ -1,340 +0,0 @@ -/**************************************************************************** -Copyright (c) 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. -****************************************************************************/ - -#include "picosat.h" - -#include <stdio.h> -#include <assert.h> -#include <string.h> -#include <stdarg.h> -#include <ctype.h> - -#define MAXNONREDROUNDS 3 -#define MINCOREROUNDS 5 -#define MAXCOREROUNDS 100 - -typedef struct Cls { int lit, red, * lits; } Cls; - -static int verbose; -static int fclose_input, pclose_input, close_output; -static FILE * input_file, * output_file; -static const char * input_name, * output_name; -static int lineno = 1; -static int nvars, nclauses; -static Cls * clauses; -static int * lits, nlits, szlits; -static double start; -static int reductions; - -static int next (void) { - int res = fgetc (input_file); - if (res == '\n') lineno++; - return res; -} - -static void msg (const char * fmt, ...) { - va_list ap; - if (!verbose) return; - fputs ("c [picomus] ", stderr); - va_start (ap, fmt); - vfprintf (stderr, fmt, ap); - va_end (ap); - fputc ('\n', stderr); - fflush (stderr); -} - -static const char * parse (void) { - int ch, n, lit, sign, i; - Cls * c; -HEADER: - ch = next (); - if (ch == 'c') { - while ((ch = next ()) != '\n') - if (ch == EOF) return "EOF after 'c'"; - goto HEADER; - } - if (ch == '\r') goto HEADER; - if (ch != 'p') return "expected 'c' or 'p'"; - if (fscanf (input_file, " cnf %d %d", &nvars, &nclauses) != 2) - return "invalid header"; - msg ("p cnf %d %d", nvars, nclauses); - clauses = calloc (nclauses, sizeof *clauses); - lit = n = 0; -LIT: - ch = next (); - if (ch == ' ' || ch == '\n' || ch == '\t' || ch == '\r') goto LIT; - if (ch == 'c') { - while ((ch = next ()) != '\n') - if (ch == EOF) return "EOF after 'c'"; - goto LIT; - } - if (ch == EOF) { - if (lit) return "zero missing"; - if (n < nclauses) return "clauses missing"; - return 0; - } - if (n == nclauses) return "too many clauses"; - if (ch == '-') { - sign = -1; - ch = next (); - if (!isdigit (ch)) return "expected digit after '-'"; - } else sign = 1; - if (!isdigit (ch)) return "expected digit"; - lit = ch - '0'; - while (isdigit (ch = next ())) - lit = 10 * lit + (ch - '0'); - if (lit > nvars) return "maximum variable index exceeded"; - if (lit) { - lit *= sign; - if (nlits == szlits) { - szlits = szlits ? 2 * szlits : 1; - lits = realloc (lits, szlits * sizeof *lits); - } - lits[nlits++] = lit; - } else { - c = clauses + n++; - c->lits = malloc ((nlits + 1) * sizeof *c->lits); - for (i = 0; i < nlits; i++) - c->lits[i] = lits[i]; - c->lits[i] = 0; - nlits = 0; - } - goto LIT; -} - -static void die (const char * fmt, ...) { - va_list ap; - fputs ("*** picomus: ", stderr); - va_start (ap, fmt); - vfprintf (stderr, fmt, ap); - va_end (ap); - fputc ('\n', stderr); - fflush (stderr); - exit (1); -} - -static double percent (double a, double b) { return b?100.0*a/b:0.0; } - -static void callback (void * dummy, const int * mus) { - int remaining; - const int * p; - (void) dummy; - if (!verbose) return; - remaining = 0; - for (p = mus; *p; p++) remaining++; - assert (remaining <= nclauses); - reductions++; - msg ("reduction %d to %d out of %d (%.0f%%) after %.1f sec", - reductions, - remaining, nclauses, percent (remaining, nclauses), - picosat_time_stamp () - start); -} - -int main (int argc, char ** argv) { - int i, * p, n, oldn, red, nonred, tmp, res, round, printed, len; - const char * err; - const int * q; - char * cmd; - Cls * c; - start = picosat_time_stamp (); - for (i = 1; i < argc; i++) { - if (!strcmp (argv[i], "-h")) { - printf ( - "picomus [-v][-h][<input>[<output>]]\n" - "\n" - "This tool is a SAT solver that uses the PicoSAT library to\n" - "generate a 'minimal unsatisfiable core' also known as 'minimal\n" - "unsatisfiable set' (MUS) of a CNF in DIMACS format.\n" - "\n" - "Both file argumetns can be \"-\" and then denote <stdin> resp.\n" - "<stdout>. If no input file is given <stdin> is used. If no\n" - "output file is specified the MUS is only computed, but not\n" - "printed.\n" - "\n" - "Otherwise the output conforms to the standard SAT solver\n" - "format used at SAT competitions.\n" - "\n" -#ifndef TRACE - "WARNING: PicosSAT is compiled without trace support.\n" - "\n" - "This typically slows down this MUS extractor, since\n" - "it only relies on clause selector variables and\n" - "can not make use of core extraction. To enable\n" - "trace generation use './configure --trace' or\n" - "'./configure -O --trace' when building PicoSAT.\n" -#else - "Since trace generation code is included, this binary\n" - "uses both core extraction and clause selector variables.\n" -#endif - ); - exit (0); - } else if (!strcmp (argv[i], "-v")) verbose++; - else if (output_name) die ("too many arguments"); - else if (!input_name) input_name = argv[i]; - else output_name = argv[i]; - } - if (input_name && strcmp (input_name, "-")) { - len = strlen (input_name); - if (len >= 3 && !strcmp (input_name + len - 3, ".gz")) { - cmd = malloc (len + 20); - sprintf (cmd, "gunzip -c %s 2>/dev/null", input_name); - input_file = popen (cmd, "r"); - pclose_input = 1; - free (cmd); - } else input_file = fopen (input_name, "r"), fclose_input = 1; - if (!input_file) die ("can not read '%s'", input_name); - } else input_file = stdin, input_name = "-"; - if ((err = parse ())) { - fprintf (stderr, "%s:%d: %s\n", input_name, lineno, err); - fflush (stderr); - exit (1); - } - if (fclose_input) fclose (input_file); - if (pclose_input) pclose (input_file); - picosat_init (); - picosat_set_prefix ("c [picosat] "); - picosat_set_output (stderr); - if (verbose > 1) picosat_set_verbosity (verbose - 1); - printed = 0; - if (picosat_enable_trace_generation ()) { - n = nclauses; - nonred = 0; - for (round = 1; round <= MAXCOREROUNDS; round++) { - if (verbose > 1) - msg ("starting core extraction round %d", round); - picosat_set_seed (round); - for (i = 0; i < nclauses; i++) { - c = clauses + i; - if (c->red) { - picosat_add (1); - picosat_add (-1); - } else { - for (p = c->lits; *p; p++) - picosat_add (*p); - } - tmp = picosat_add (0); - assert (tmp == i); - } - res = picosat_sat (-1); - if (res == 10) { assert (round == 1); goto SAT; } - assert (res == 20); - if (!printed) { - assert (round == 1); - printed = 1; - printf ("s UNSATISFIABLE\n"); - fflush (stdout); - } - for (i = 0; i < nclauses; i++) { - c = clauses + i; - if (c->red) { assert (!picosat_coreclause (i)); continue; } - if (picosat_coreclause (i)) continue; - c->red = 1; - } - oldn = n; - n = 0; - for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++; - msg ("extracted core %d of size %d out of %d (%.0f%%) after %.1f sec", - round, n, nclauses, percent (n, nclauses), - picosat_time_stamp () - start); - assert (oldn >= n); - picosat_reset (); - picosat_init (); - picosat_set_prefix ("c [picosat] "); - picosat_set_output (stderr); - if (round >= MINCOREROUNDS) { - red = oldn - n; - if (red < 10 && (100*red + 99)/oldn < 2) { - nonred++; - if (nonred > MAXNONREDROUNDS) break; - } - } - if (round < MAXCOREROUNDS) picosat_enable_trace_generation (); - } - } - for (i = 0; i < nclauses; i++) { - c = clauses + i; - if (c->red) { - picosat_add (1); - picosat_add (-1); - tmp = picosat_add (0); - assert (tmp == i); - continue; - } - c->lit = nvars + i + 1; - picosat_add (-c->lit); - for (p = c->lits; *p; p++) - (void) picosat_add (*p); - tmp = picosat_add (0); - assert (tmp == i); - } - for (i = 0; i < nclauses; i++) { - c = clauses + i; - if (c->red) continue; - picosat_assume (c->lit); - } - res = picosat_sat (-1); - if (res == 20) { - if (!printed) printf ("s UNSATISFIABLE\n"), fflush (stdout); - for (i = 0; i < nclauses; i++) clauses[i].red = 1; - q = picosat_mus_assumptions (0, callback, 1); - while ((i = *q++)) { - i -= nvars + 1; - assert (0 <= i && i < nclauses); - clauses[i].red = 0; - } - } else { -SAT: - assert (res == 10); - printf ("s SATISFIABLE\n"); fflush (stdout); - for (i = 1; i <= nvars; i++) - printf ("v %d\n", ((picosat_deref (i) < 0) ? -1 : 1) * i); - printf ("v 0\n"); - } - if (verbose) picosat_stats (); - picosat_reset (); - n = 0; - for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++; - red = nclauses - n; - msg ("found %d redundant clauses %.0f%%", red, percent (red, nclauses)); - if (output_name && strcmp (output_name, "-")) { - output_file = fopen (output_name, "w"); - if (!output_file) die ("can not write '%s'", output_name); - close_output = 1; - } else if (output_name && !strcmp (output_name, "-")) output_file = stdout; - if (output_file) { - fprintf (output_file, "p cnf %d %d\n", nvars, n); - for (i = 0; i < nclauses; i++) - if (!clauses[i].red) { - for (p = clauses[i].lits; *p; p++) fprintf (output_file, "%d ", *p); - fprintf (output_file, "0\n"); - } - if (close_output) fclose (output_file); - } - msg ("%s %d irredundant clauses %.0f%%", - output_file ? "printed" : "computed", n, percent (n, nclauses)); - for (i = 0; i < nclauses; i++) free (clauses[i].lits); - free (clauses); - free (lits); - msg ("%d reductions in %.1f seconds", - reductions, picosat_time_stamp () - start); - return res; -} diff --git a/src/prop/bvpicosat/picosat.c b/src/prop/bvpicosat/picosat.c deleted file mode 100644 index 490d235cc..000000000 --- a/src/prop/bvpicosat/picosat.c +++ /dev/null @@ -1,7731 +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. -****************************************************************************/ - -#include <stdlib.h> -#include <stdio.h> -#include <string.h> -#include <assert.h> -#include <limits.h> -#include <ctype.h> -#include <stdarg.h> - -#include "picosat.h" - -/* By default code for 'all different constraints' is disabled, since 'NADC' - * is defined. -#define NADC - */ - -/* By default we enable failed literals, since 'NFL' is undefined. - * - */ -#define NFL - -/* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined. - * -#define NDSC - */ - -/* Do not use luby restart schedule instead of inner/outer. - * -#define NLUBY - */ - -// #define VISCORES /* keep this disabled */ - -#ifdef VISCORES -// #define WRITEGIF -#endif - -#ifdef VISCORES -#ifndef WRITEGIF -#include <unistd.h> /* for 'usleep' */ -#endif -#endif - -#define MINRESTART 100 /* minimum restart interval */ -#define MAXRESTART 1000000 /* maximum restart interval */ -#define RDECIDE 1000 /* interval of random decisions */ -#define FRESTART 110 /* restart increase factor in percent */ -#define FREDUCE 110 /* reduce increase factor in percent */ -#define FFLIPPED 10000 /* flipped reduce factor */ -#define FFLIPPEDPREC 10000000/* flipped reduce factor precision */ - -#ifndef TRACE -#define NO_BINARY_CLAUSES /* store binary clauses more compactly */ -#endif - -/* For debugging purposes you may want to define 'LOGGING', which actually - * can be enforced by using the '--log' option for the configure script. - */ -#ifdef LOGGING -#define LOG(code) do { code; } while (0) -#else -#define LOG(code) do { } while (0) -#endif -#define NOLOG(code) do { } while (0) /* log exception */ -#define ONLYLOG(code) do { code; } while (0) /* force logging */ - -#define FALSE ((Val)-1) -#define UNDEF ((Val)0) -#define TRUE ((Val)1) - -#define COMPACT_TRACECHECK_TRACE_FMT 0 -#define EXTENDED_TRACECHECK_TRACE_FMT 1 -#define RUP_TRACE_FMT 2 - -#define NEWN(p,n) do { (p) = new (sizeof (*(p)) * (n)); } while (0) -#define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0) -#define CLR(p) CLRN(p,1) -#define DELETEN(p,n) \ - do { delete (p, sizeof (*(p)) * (n)); (p) = 0; } while (0) - -#define RESIZEN(p,old_num,new_num) \ - do { \ - size_t old_size = sizeof (*(p)) * (old_num); \ - size_t new_size = sizeof (*(p)) * (new_num); \ - (p) = resize ((p), old_size, new_size) ; \ - } while (0) - -#define ENLARGE(start,head,end) \ - do { \ - unsigned old_num = (unsigned)((end) - (start)); \ - size_t new_num = old_num ? (2 * old_num) : 1; \ - unsigned count = (head) - (start); \ - assert ((start) <= (start)); \ - RESIZEN((start),old_num,new_num); \ - (head) = (start) + count; \ - (end) = (start) + new_num; \ - } while (0) - -#define NOTLIT(l) (lits + (1 ^ ((l) - lits))) - -#define LIT2IDX(l) ((unsigned)((l) - lits) / 2) -#define LIT2IMPLS(l) (impls + (unsigned)((l) - lits)) -#define LIT2INT(l) (LIT2SGN(l) * LIT2IDX(l)) -#define LIT2SGN(l) (((unsigned)((l) - lits) & 1) ? -1 : 1) -#define LIT2VAR(l) (vars + LIT2IDX(l)) -#define LIT2HTPS(l) (htps + (unsigned)((l) - lits)) -#define LIT2JWH(l) (jwh + ((l) - lits)) - -#ifndef NDSC -#define LIT2DHTPS(l) (dhtps + (unsigned)((l) - lits)) -#endif - -#ifdef NO_BINARY_CLAUSES -typedef unsigned long Wrd; -#define ISLITREASON(cls) (1&(Wrd)cls) -#define LIT2REASON(lit) \ - (assert (lit->val==TRUE), ((Cls*)(1 + (2*(lit - lits))))) -#define REASON2LIT(cls) ((Lit*)(lits + ((Wrd)cls)/2)) -#endif - -#define ENDOFCLS(c) ((void*)((c)->lits + (c)->size)) - -#define SOC ((oclauses == ohead) ? lclauses : oclauses) -#define EOC lhead -#define NXC(p) (((p) + 1 == ohead) ? lclauses : (p) + 1) - -#define OIDX2IDX(idx) (2 * ((idx) + 1)) -#define LIDX2IDX(idx) (2 * (idx) + 1) - -#define ISLIDX(idx) ((idx)&1) - -#define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1) -#define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2) - -#define EXPORTIDX(idx) \ - ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ohead - oclauses)) : IDX2OIDX(idx)) + 1) - -#define IDX2CLS(i) \ - (assert(i), (ISLIDX(i) ? lclauses : oclauses)[(i)/2 - !ISLIDX(i)]) - -#define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? zhains[(i)/2] : 0)) - -#define CLS2TRD(c) (((Trd*)(c)) - 1) -#define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx) - -#define CLS2ACT(c) \ - ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c))) - -#define VAR2LIT(v) (lits + 2 * ((v) - vars)) -#define VAR2RNK(v) (rnks + ((v) - vars)) - -#define RNK2LIT(r) (lits + 2 * ((r) - rnks)) -#define RNK2VAR(r) (vars + ((r) - rnks)) - -#define BLK_FILL_BYTES 8 -#define SIZE_OF_BLK (sizeof (Blk) - BLK_FILL_BYTES) - -#define PTR2BLK(void_ptr) \ - ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - SIZE_OF_BLK) : 0) - -#define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0) -#define PERCENT(a,b) (100.0 * AVERAGE(a,b)) - -#define ABORT(msg) \ - do { \ - fputs ("*** picosat: " msg "\n", stderr); \ - abort (); \ - } while (0) - -#define ABORTIF(cond,msg) \ - do { \ - if (!(cond)) break; \ - ABORT (msg); \ - } while (0) - -#define ZEROFLT (0x00000000u) -#define INFFLT (0xffffffffu) - -#define FLTCARRY (1u << 25) -#define FLTMSB (1u << 24) -#define FLTMAXMANTISSA (FLTMSB - 1) - -#define FLTMANTISSA(d) ((d) & FLTMAXMANTISSA) -#define FLTEXPONENT(d) ((int)((d) >> 24) - 128) - -#define FLTMINEXPONENT (-128) -#define FLTMAXEXPONENT (127) - -#define cmpswapflt(a,b) \ - do { \ - Flt tmp; \ - if (((a) < (b))) \ - { \ - tmp = (a); \ - (a) = (b); \ - (b) = tmp; \ - } \ - } while (0) - -#define unpackflt(u,m,e) \ - do { \ - (m) = FLTMANTISSA(u); \ - (e) = FLTEXPONENT(u); \ - (m) |= FLTMSB; \ - } while (0) - -#define INSERTION_SORT_LIMIT 10 - -#define internal_sorting_swap(T,p,q) \ -do { \ - T tmp = *(q); \ - *(q) = *(p); \ - *(p) = tmp; \ -} while (0) - -#define internal_sorting_cmpswap(T,cmp,p,q) \ -do { \ - if ((cmp) (*(p), *(q)) > 0) \ - internal_sorting_swap (T, p, q); \ -} while(0) - -#define internal_quicksort_partition(T,cmp,a,l,r) \ -do { \ - T pivot; \ - int j; \ - i = (l) - 1; /* result in 'i' */ \ - j = (r); \ - pivot = (a)[j]; \ - for (;;) \ - { \ - while ((cmp) ((a)[++i], pivot) < 0) \ - ; \ - while ((cmp) (pivot, (a)[--j]) < 0) \ - if (j == (l)) \ - break; \ - if (i >= j) \ - break; \ - internal_sorting_swap (T, (a) + i, (a) + j); \ - } \ - internal_sorting_swap (T, (a) + i, (a) + (r)); \ -} while(0) - -#define internal_quicksort(T,cmp,a,n) \ -do { \ - int l = 0, r = (n) - 1, m, ll, rr, i; \ - assert (ihead == indices); \ - if (r - l <= INSERTION_SORT_LIMIT) \ - break; \ - for (;;) \ - { \ - m = (l + r) / 2; \ - internal_sorting_swap (T, (a) + m, (a) + r - 1); \ - internal_sorting_cmpswap (T, cmp, (a) + l, (a) + r - 1); \ - internal_sorting_cmpswap (T, cmp, (a) + l, (a) + r); \ - internal_sorting_cmpswap (T, cmp, (a) + r - 1, (a) + r); \ - internal_quicksort_partition (T, cmp, (a), l + 1, r - 1); \ - if (i - l < r - i) \ - { \ - ll = i + 1; \ - rr = r; \ - r = i - 1; \ - } \ - else \ - { \ - ll = l; \ - rr = i - 1; \ - l = i + 1; \ - } \ - if (r - l > INSERTION_SORT_LIMIT) \ - { \ - assert (rr - ll > INSERTION_SORT_LIMIT); \ - if (ihead == eoi) \ - ENLARGE (indices, ihead, eoi); \ - *ihead++ = ll; \ - if (ihead == eoi) \ - ENLARGE (indices, ihead, eoi); \ - *ihead++ = rr; \ - } \ - else if (rr - ll > INSERTION_SORT_LIMIT) \ - { \ - l = ll; \ - r = rr; \ - } \ - else if (ihead > indices) \ - { \ - r = *--ihead; \ - l = *--ihead; \ - } \ - else \ - break; \ - } \ -} while (0) - -#define internal_insertion_sort(T,cmp,a,n) \ -do { \ - T pivot; \ - int l = 0, r = (n) - 1, i, j; \ - for (i = r; i > l; i--) \ - internal_sorting_cmpswap (T, cmp, (a) + i - 1, (a) + i); \ - for (i = l + 2; i <= r; i++) \ - { \ - j = i; \ - pivot = (a)[i]; \ - while ((cmp) (pivot, (a)[j - 1]) < 0) \ - { \ - (a)[j] = (a)[j - 1]; \ - j--; \ - } \ - (a)[j] = pivot; \ - } \ -} while (0) - -#ifdef NDEBUG -#define check_sorted(cmp,a,n) do { } while(0) -#else -#define check_sorted(cmp,a,n) \ -do { \ - int i; \ - for (i = 0; i < (n) - 1; i++) \ - assert ((cmp) ((a)[i], (a)[i + 1]) <= 0); \ -} while(0) -#endif - -#define sort(T,cmp,a,n) \ -do { \ - T * aa = (a); \ - int nn = (n); \ - internal_quicksort (T, cmp, aa, nn); \ - internal_insertion_sort (T, cmp, aa, nn); \ - assert (ihead == indices); \ - check_sorted (cmp, aa, nn); \ -} while (0) - -#define WRDSZ (sizeof (long) * 8) - -typedef unsigned Flt; /* 32 bit deterministic soft float */ -typedef Flt Act; /* clause and variable activity */ -typedef struct Blk Blk; /* allocated memory block */ -typedef struct Cls Cls; /* clause */ -typedef struct Lit Lit; /* literal */ -typedef struct Rnk Rnk; /* variable to score mapping */ -typedef signed char Val; /* TRUE, UNDEF, FALSE */ -typedef struct Var Var; /* variable */ -#ifdef TRACE -typedef struct Trd Trd; /* trace data for clauses */ -typedef struct Zhn Zhn; /* compressed chain (=zain) data */ -typedef unsigned char Znt; /* compressed antecedent data */ -#endif - -#ifdef NO_BINARY_CLAUSES -typedef struct Ltk Ltk; - -struct Ltk -{ - Lit ** start; - unsigned count : WRDSZ == 32 ? 27 : 32; - unsigned ldsize : WRDSZ == 32 ? 5 : 32; -}; -#endif - -struct Lit -{ - Val val; -}; - -struct Var -{ - unsigned mark : 1; - unsigned resolved : 1; - unsigned phase : 1; - unsigned assigned : 1; - unsigned used : 1; - unsigned failed : 1; -#ifdef TRACE - unsigned core : 1; -#endif - unsigned level : WRDSZ == 32 ? 24 : 32; - Cls *reason; -#ifndef NADC - Lit ** inado; - Lit ** ado; - Lit *** adotabpos; -#endif -}; - -struct Rnk -{ - Act score; - unsigned pos : 30; /* 0 iff not on heap */ - unsigned moreimportant : 1; - unsigned lessimportant : 1; -}; - -struct Cls -{ - unsigned size; - unsigned learned:1; - unsigned collect:1; - unsigned locked:1; - unsigned fixed:1; - unsigned used:1; -#ifndef NDEBUG - unsigned connected:1; -#endif -#ifdef TRACE - unsigned core:1; - unsigned collected:1; -#endif - Cls *next[2]; - Lit *lits[2]; -}; - -#ifdef TRACE -struct Zhn -{ - unsigned ref:31; - unsigned core:1; - Znt * liz; - Znt znt[0]; -}; - -struct Trd -{ - unsigned idx; - Cls cls[0]; -}; -#endif - -struct Blk -{ -#ifndef NDEBUG - union - { - size_t size; /* this is what we really use */ - void *as_two_ptrs[2]; /* 2 * sizeof (void*) alignment of data */ - } - header; -#endif - char data[BLK_FILL_BYTES]; -}; - -static enum State -{ - RESET = 0, - READY = 1, - SAT = 2, - UNSAT = 3, - UNKNOWN = 4, -} -state = RESET; - -static int last_sat_call_result; - -static FILE *out; -static char * prefix; -static int verbosity; -static unsigned level; -static unsigned max_var; -static unsigned size_vars; - -static Lit * __attribute__((aligned(64))) lits; -static Var *vars; -static Rnk *rnks; -static Flt *jwh; -static Cls **htps; -#ifndef NDSC -static Cls **dhtps; -#endif -#ifdef NO_BINARY_CLAUSES -static Ltk *impls; -static Cls impl, cimpl; -static int implvalid, cimplvalid; -#else -static Cls **impls; -#endif -static Lit **trail, **thead, **eot, **ttail, ** ttail2; -#ifndef NADC -static Lit **ttailado; -#endif -static unsigned adecidelevel; -static Lit **als, **alshead, **alstail, **eoals; -static int *fals, *falshead, *eofals; -static int *mass, szmass; -static Lit *failed_assumption; -static int extracted_all_failed_assumptions; -static Rnk **heap, **hhead, **eoh; -static Cls **oclauses, **ohead, **eoo; /* original clauses */ -static Cls **lclauses, **lhead, ** eol; /* learned clauses */ -#ifdef TRACE -static int trace; -static Zhn **zhains, **zhead, **eoz; -static int ocore = -1; -#endif -static FILE * rup; -static int rupstarted; -static int rupvariables; -static int rupclauses; -static Cls *mtcls; -static Cls *conflict; -static Lit **added, **ahead, **eoa; -static Var **marked, **mhead, **eom; -static Var **dfs, **dhead, **eod; -static Cls **resolved, **rhead, **eor; -static unsigned char *buffer, *bhead, *eob; -static Act vinc, lscore, ilvinc, ifvinc; -#ifdef VISCORES -static Act fvinc, nvinc; -#endif -static Act cinc, lcinc, ilcinc, fcinc; -static unsigned srng; -static size_t current_bytes; -static size_t max_bytes; -static size_t recycled; -static double seconds; -static double entered; -static unsigned nentered; -static int measurealltimeinlib; -static char *rline[2]; -static int szrline, rcount; -static double levelsum; -static unsigned iterations; -static int reports; -static int lastrheader = -2; -static unsigned calls; -static unsigned decisions; -static unsigned restarts; -static unsigned simps; -static unsigned fsimplify; -static unsigned isimplify; -static unsigned reductions; -static unsigned lreduce; -static unsigned lreduceadjustcnt; -static unsigned lreduceadjustinc; -static unsigned lastreduceconflicts; -static unsigned llocked; /* locked large learned clauses */ -static unsigned lrestart; -#ifdef NLUBY -static unsigned drestart; -static unsigned ddrestart; -#else -static unsigned lubycnt; -static unsigned lubymaxdelta; -static int waslubymaxdelta; -#endif -static unsigned long long lsimplify; -static unsigned long long propagations; -static unsigned long long lpropagations; -static unsigned fixed; /* top level assignments */ -#ifndef NFL -static unsigned failedlits; -static unsigned ifailedlits; -static unsigned efailedlits; -static unsigned flcalls; -#ifdef STATS -static unsigned flrounds; -static unsigned long long flprops; -static unsigned long long floopsed, fltried, flskipped; -#endif -static unsigned long long fllimit; -static int simplifying; -static Lit ** saved; -static unsigned saved_size; -#endif -static unsigned conflicts; -static unsigned noclauses; /* current number large original clauses */ -static unsigned nlclauses; /* current number large learned clauses */ -static unsigned olits; /* current literals in large original clauses */ -static unsigned llits; /* current literals in large learned clauses */ -static unsigned oadded; /* added original clauses */ -static unsigned ladded; /* added learned clauses */ -static unsigned loadded; /* added original large clauses */ -static unsigned lladded; /* added learned large clauses */ -static unsigned addedclauses; /* oadded + ladded */ -static unsigned vused; /* used variables */ -static unsigned llitsadded; /* added learned literals */ -#ifdef STATS -static unsigned loused; /* used large original clauses */ -static unsigned llused; /* used large learned clauses */ -static unsigned long long visits; -static unsigned long long bvisits; -static unsigned long long tvisits; -static unsigned long long lvisits; -static unsigned long long othertrue; -static unsigned long long othertrue2; -static unsigned long long othertruel; -static unsigned long long othertrue2u; -static unsigned long long othertruelu; -static unsigned long long ltraversals; -static unsigned long long traversals; -#ifdef TRACE -static unsigned long long antecedents; -#endif -static unsigned uips; -static unsigned znts; -static unsigned assumptions; -static unsigned rdecisions; -static unsigned sdecisions; -static size_t srecycled; -static size_t rrecycled; -static unsigned long long derefs; -#endif -static unsigned minimizedllits; -static unsigned nonminimizedllits; -#ifndef NADC -static Lit *** ados, *** hados, *** eados; -static Lit *** adotab; -static unsigned nadotab; -static unsigned szadotab; -static Cls * adoconflict; -static unsigned adoconflicts; -static unsigned adoconflictlimit = UINT_MAX; -static int addingtoado; -static int adodisabled; -#endif -static unsigned long long flips; -#ifdef STATS -static unsigned long long forced; -static unsigned long long assignments; -static unsigned inclreduces; -static unsigned staticphasedecisions; -static unsigned skippedrestarts; -#endif -static int * indices, * ihead, *eoi; -static unsigned sdflips; -static int defaultphase; - -static unsigned long long saved_flips; -static unsigned saved_max_var; -static unsigned min_flipped = UINT_MAX; - -static void * emgr; -static void * (*enew)(void*,size_t); -static void * (*eresize)(void*,void*,size_t,size_t); -static void (*edelete)(void*,void*,size_t); - -#ifdef VISCORES -static FILE * fviscores; -#endif - -static Flt -packflt (unsigned m, int e) -{ - Flt res; - assert (m < FLTMSB); - assert (FLTMINEXPONENT <= e); - assert (e <= FLTMAXEXPONENT); - res = m | ((e + 128) << 24); - return res; -} - -static Flt -base2flt (unsigned m, int e) -{ - if (!m) - return ZEROFLT; - - if (m < FLTMSB) - { - do - { - if (e <= FLTMINEXPONENT) - return ZEROFLT; - - e--; - m <<= 1; - - } - while (m < FLTMSB); - } - else - { - while (m >= FLTCARRY) - { - if (e >= FLTMAXEXPONENT) - return INFFLT; - - e++; - m >>= 1; - } - } - - m &= ~FLTMSB; - return packflt (m, e); -} - -static Flt -addflt (Flt a, Flt b) -{ - unsigned ma, mb, delta; - int ea, eb; - - cmpswapflt (a, b); - if (!b) - return a; - - unpackflt (a, ma, ea); - unpackflt (b, mb, eb); - - assert (ea >= eb); - delta = ea - eb; - mb >>= delta; - if (!mb) - return a; - - ma += mb; - if (ma & FLTCARRY) - { - if (ea == FLTMAXEXPONENT) - return INFFLT; - - ea++; - ma >>= 1; - } - - assert (ma < FLTCARRY); - ma &= FLTMAXMANTISSA; - - return packflt (ma, ea); -} - -static Flt -mulflt (Flt a, Flt b) -{ - unsigned ma, mb; - unsigned long long accu; - int ea, eb; - - cmpswapflt (a, b); - if (!b) - return ZEROFLT; - - unpackflt (a, ma, ea); - unpackflt (b, mb, eb); - - ea += eb; - ea += 24; - if (ea > FLTMAXEXPONENT) - return INFFLT; - - if (ea < FLTMINEXPONENT) - return ZEROFLT; - - accu = ma; - accu *= mb; - accu >>= 24; - - if (accu >= FLTCARRY) - { - if (ea == FLTMAXEXPONENT) - return INFFLT; - - ea++; - accu >>= 1; - - if (accu >= FLTCARRY) - return INFFLT; - } - - assert (accu < FLTCARRY); - assert (accu & FLTMSB); - - ma = accu; - ma &= ~FLTMSB; - - return packflt (ma, ea); -} - -static int -ISDIGIT (char c) -{ - return '0' <= c && c <= '9'; -} - -static Flt -ascii2flt (const char *str) -{ - Flt ten = base2flt (10, 0); - Flt onetenth = base2flt (26843546, -28); - Flt res = ZEROFLT, tmp, base; - const char *p = str; - char ch; - - ch = *p++; - - if (ch != '.') - { - if (!ISDIGIT (ch)) - return INFFLT; /* better abort ? */ - - res = base2flt (ch - '0', 0); - - while ((ch = *p++)) - { - if (ch == '.') - break; - - if (!ISDIGIT (ch)) - return INFFLT; /* better abort? */ - - res = mulflt (res, ten); - tmp = base2flt (ch - '0', 0); - res = addflt (res, tmp); - } - } - - if (ch == '.') - { - ch = *p++; - if (!ISDIGIT (ch)) - return INFFLT; /* better abort ? */ - - base = onetenth; - tmp = mulflt (base2flt (ch - '0', 0), base); - res = addflt (res, tmp); - - while ((ch = *p++)) - { - if (!ISDIGIT (ch)) - return INFFLT; /* better abort? */ - - base = mulflt (base, onetenth); - tmp = mulflt (base2flt (ch - '0', 0), base); - res = addflt (res, tmp); - } - } - - return res; -} - -#if defined(VISCORES) - -static double -flt2double (Flt f) -{ - double res; - unsigned m; - int e, i; - - unpackflt (f, m, e); - res = m; - - if (e < 0) - { - for (i = e; i < 0; i++) - res *= 0.5; - } - else - { - for (i = 0; i < e; i++) - res *= 2.0; - } - - return res; -} - -#endif - -static int -log2flt (Flt a) -{ - return FLTEXPONENT (a) + 24; -} - -static int -cmpflt (Flt a, Flt b) -{ - if (a < b) - return -1; - - if (a > b) - return 1; - - return 0; -} - -static void * -new (size_t size) -{ - size_t bytes; - Blk *b; - - if (!size) - return 0; - - bytes = size + SIZE_OF_BLK; - - if (enew) - b = enew (emgr, bytes); - else - b = malloc (bytes); - - ABORTIF (!b, "out of memory in 'new'"); -#ifndef NDEBUG - b->header.size = size; -#endif - current_bytes += size; - if (current_bytes > max_bytes) - max_bytes = current_bytes; - return b->data; -} - -static void -delete (void *void_ptr, size_t size) -{ - size_t bytes; - Blk *b; - - if (!void_ptr) - { - assert (!size); - return; - } - - assert (size); - b = PTR2BLK (void_ptr); - - assert (size <= current_bytes); - current_bytes -= size; - - assert (b->header.size == size); - - bytes = size + SIZE_OF_BLK; - if (edelete) - edelete (emgr, b, bytes); - else - free (b); -} - -static void * -resize (void *void_ptr, size_t old_size, size_t new_size) -{ - size_t old_bytes, new_bytes; - Blk *b; - - b = PTR2BLK (void_ptr); - - assert (old_size <= current_bytes); - current_bytes -= old_size; - - if ((old_bytes = old_size)) - { - assert (old_size && b->header.size == old_size); - old_bytes += SIZE_OF_BLK; - } - else - assert (!b); - - if ((new_bytes = new_size)) - new_bytes += SIZE_OF_BLK; - - if (eresize) - b = eresize (emgr, b, old_bytes, new_bytes); - else - b = realloc (b, new_bytes); - - if (!new_size) - { - assert (!b); - return 0; - } - - ABORTIF (!b, "out of memory in 'resize'"); -#ifndef NDEBUG - b->header.size = new_size; -#endif - - current_bytes += new_size; - if (current_bytes > max_bytes) - max_bytes = current_bytes; - - return b->data; -} - -static unsigned -int2unsigned (int l) -{ - return (l < 0) ? 1 + 2 * -l : 2 * l; -} - -static Lit * -int2lit (int l) -{ - return lits + int2unsigned (l); -} - -static Lit ** -end_of_lits (Cls * cls) -{ - return cls->lits + cls->size; -} - -static int -lit2idx (Lit * lit) -{ - return (lit - lits) / 2; -} - -static int -lit2sign (Lit * lit) -{ - return ((lit - lits) & 1) ? -1 : 1; -} - - -static int -lit2int (Lit * l) -{ - return lit2idx (l) * lit2sign (l); -} - -#if !defined(NDEBUG) || defined(LOGGING) - -static void -dumplits (Lit ** lits, Lit ** eol) -{ - int first; - Lit ** p; - - if (lits == eol) - { - /* empty clause */ - } - else if (lits + 1 == eol) - { - fprintf (out, "%d ", lit2int (lits[0])); - } - else - { - assert (lits + 2 <= eol); - first = (abs (lit2int (lits[0])) > abs (lit2int (lits[1]))); - fprintf (out, "%d ", lit2int (lits[first])); - fprintf (out, "%d ", lit2int (lits[!first])); - for (p = lits + 2; p < eol; p++) - fprintf (out, "%d ", lit2int (*p)); - } - - fputc ('0', out); -} - -static void -dumpcls (Cls * cls) -{ - Lit **eol; - - if (cls) - { - eol = end_of_lits (cls); - dumplits (cls->lits, eol); -#ifdef TRACE - if (trace) - fprintf (out, " clause(%u)", CLS2IDX (cls)); -#endif - } - else - fputs ("DECISION", out); -} - -static void -dumpclsnl (Cls * cls) -{ - dumpcls (cls); - fputc ('\n', out); -} - -void -dumpcnf (void) -{ - Cls **p, *cls; - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - - dumpclsnl (*p); - } -} - -#endif - -static void -delete_prefix (void) -{ - if (!prefix) - return; - - delete (prefix, strlen (prefix) + 1); - prefix = 0; -} - -static void -new_prefix (const char * str) -{ - delete_prefix (); - assert (str); - prefix = new (strlen (str) + 1); - strcpy (prefix, str); -} - -static void -init (void) -{ - static int count; - - ABORTIF (state != RESET, "API usage: multiple initializations"); - - count = 3 - !enew - !eresize - !edelete; - ABORTIF (count && !enew, "API usage: missing 'picosat_set_new'"); - ABORTIF (count && !eresize, "API usage: missing 'picosat_set_resize'"); - ABORTIF (count && !edelete, "API usage: missing 'picosat_set_delete'"); - - assert (!max_var); /* check for proper reset */ - assert (!size_vars); /* check for proper reset */ - - size_vars = 1; - - NEWN (lits, 2 * size_vars); - NEWN (jwh, 2 * size_vars); - NEWN (htps, 2 * size_vars); -#ifndef NDSC - NEWN (dhtps, 2 * size_vars); -#endif - NEWN (impls, 2 * size_vars); - NEWN (vars, size_vars); - NEWN (rnks, size_vars); - - ENLARGE (heap, hhead, eoh); /* because '0' pos denotes not on heap */ - hhead = heap + 1; - - vinc = base2flt (1, 0); /* initial variable activity */ - ifvinc = ascii2flt ("1.05"); /* variable score rescore factor */ -#ifdef VISCORES - fvinc = ascii2flt ("0.9523809"); /* 1/f = 1/1.1 */ - nvinc = ascii2flt ("0.0476191"); /* 1 - 1/f = 1 - 1/1.1 */ -#endif - lscore = base2flt (1, 90); /* variable activity rescore limit */ - ilvinc = base2flt (1, -90); /* inverse of 'lscore' */ - - cinc = base2flt (1, 0); /* initial clause activity */ - fcinc = ascii2flt ("1.001"); /* clause activity rescore factor */ - lcinc = base2flt (1, 90); /* clause activity rescore limit */ - ilcinc = base2flt (1, -90); /* inverse of 'ilcinc' */ - - lreduceadjustcnt = lreduceadjustinc = 100; - lpropagations = ~0ull; - - out = stdout; - new_prefix ("c "); - verbosity = 0; - -#ifdef NO_BINARY_CLAUSES - memset (&impl, 0, sizeof (impl)); - impl.size = 2; - - memset (&cimpl, 0, sizeof (impl)); - cimpl.size = 2; -#endif - -#ifdef VISCORES - fviscores = popen ( - "/usr/bin/gnuplot -background black" - " -xrm 'gnuplot*textColor:white'" - " -xrm 'gnuplot*borderColor:white'" - " -xrm 'gnuplot*axisColor:white'" - , "w"); - fprintf (fviscores, "unset key\n"); - // fprintf (fviscores, "set log y\n"); - fflush (fviscores); - system ("rm -rf /tmp/picosat-viscores"); - system ("mkdir /tmp/picosat-viscores"); - system ("mkdir /tmp/picosat-viscores/data"); -#ifdef WRITEGIF - system ("mkdir /tmp/picosat-viscores/gif"); - fprintf (fviscores, - "set terminal gif giant animate opt size 1024,768 x000000 xffffff" - "\n"); - - fprintf (fviscores, - "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n"); -#endif -#endif - defaultphase = 2; - state = READY; - last_sat_call_result = 0; -} - -static size_t -bytes_clause (unsigned size, unsigned learned) -{ - size_t res; - - res = sizeof (Cls); - res += size * sizeof (Lit *); - res -= 2 * sizeof (Lit *); - - if (learned && size > 2) - res += sizeof (Act); /* add activity */ - -#ifdef TRACE - if (trace) - res += sizeof (Trd); /* add trace data */ -#endif - - return res; -} - -static Cls * -new_clause (unsigned size, unsigned learned) -{ - size_t bytes; - void * tmp; -#ifdef TRACE - Trd *trd; -#endif - Cls *res; - - bytes = bytes_clause (size, learned); - tmp = new (bytes); - -#ifdef TRACE - if (trace) - { - trd = tmp; - - if (learned) - trd->idx = LIDX2IDX (lhead - lclauses); - else - trd->idx = OIDX2IDX (ohead - oclauses); - - res = trd->cls; - } - else -#endif - res = tmp; - - res->size = size; - res->learned = learned; - - res->collect = 0; -#ifndef NDEBUG - res->connected = 0; -#endif - res->locked = 0; - res->fixed = 0; - res->used = 0; -#ifdef TRACE - res->core = 0; -#ifndef NDEBUG - res->collected = 0; -#endif -#endif - - if (learned && size > 2) - *CLS2ACT (res) = cinc; - - return res; -} - -static void -delete_clause (Cls * cls) -{ - size_t bytes; -#ifdef TRACE - Trd *trd; -#endif - - bytes = bytes_clause (cls->size, cls->learned); - -#ifdef TRACE - if (trace) - { - trd = CLS2TRD (cls); - delete (trd, bytes); - } - else -#endif - delete (cls, bytes); -} - -static void -delete_clauses (void) -{ - Cls **p; - for (p = SOC; p != EOC; p = NXC (p)) - if (*p) - delete_clause (*p); - - DELETEN (oclauses, eoo - oclauses); - DELETEN (lclauses, eol - lclauses); - - ohead = eoo = lhead = eol = 0; -} - -#ifdef TRACE - -static void -delete_zhain (Zhn * zhain) -{ - const Znt *p, *znt; - - assert (zhain); - - znt = zhain->znt; - for (p = znt; *p; p++) - ; - - delete (zhain, sizeof (Zhn) + (p - znt) + 1); -} - -static void -delete_zhains (void) -{ - Zhn **p, *z; - for (p = zhains; p < zhead; p++) - if ((z = *p)) - delete_zhain (z); - - DELETEN (zhains, eoz - zhains); - eoz = zhead = 0; -} - -#endif - -#ifdef NO_BINARY_CLAUSES -static void -lrelease (Ltk * stk) -{ - if (stk->start) - DELETEN (stk->start, (1 << (stk->ldsize))); - memset (stk, 0, sizeof (*stk)); -} -#endif - -#ifndef NADC - -static unsigned -llength (Lit ** a) -{ - Lit ** p; - for (p = a; *p; p++) - ; - return p - a; -} - -static void -resetadoconflict (void) -{ - assert (adoconflict); - delete_clause (adoconflict); - adoconflict = 0; -} - -static void -reset_ados (void) -{ - Lit *** p; - - for (p = ados; p < hados; p++) - DELETEN (*p, llength (*p) + 1); - - DELETEN (ados, eados - ados); - hados = eados = 0; - - DELETEN (adotab, szadotab); - szadotab = nadotab = 0; - - if (adoconflict) - resetadoconflict (); - - adoconflicts = 0; - adoconflictlimit = UINT_MAX; - adodisabled = 0; -} - -#endif - -static void -reset (void) -{ - ABORTIF (state == RESET, "API usage: reset without initialization"); - - delete_clauses (); -#ifdef TRACE - delete_zhains (); -#endif -#ifdef NO_BINARY_CLAUSES - implvalid = 0; - cimplvalid = 0; - { - unsigned i; - for (i = 2; i <= 2 * max_var + 1; i++) - lrelease (impls + i); - } -#endif -#ifndef NADC - reset_ados (); -#endif -#ifndef NFL - DELETEN (saved, saved_size); - saved_size = 0; -#endif - DELETEN (htps, 2 * size_vars); -#ifndef NDSC - DELETEN (dhtps, 2 * size_vars); -#endif - DELETEN (impls, 2 * size_vars); - DELETEN (lits, 2 * size_vars); - DELETEN (jwh, 2 * size_vars); - DELETEN (vars, size_vars); - DELETEN (rnks, size_vars); - - DELETEN (trail, eot - trail); - trail = ttail = ttail2 = thead = eot = 0; -#ifndef NADC - ttailado = 0; -#endif - - DELETEN (heap, eoh - heap); - heap = hhead = eoh = 0; - - DELETEN (als, eoals - als); - als = eoals = alshead = alstail = 0; - extracted_all_failed_assumptions = 0; - failed_assumption = 0; - adecidelevel = 0; - DELETEN (fals, eofals - fals); - fals = eofals = falshead = 0; - DELETEN (mass, szmass); - szmass = 0; - mass = 0; - - size_vars = 0; - max_var = 0; - - mtcls = 0; -#ifdef TRACE - ocore = -1; -#endif - conflict = 0; - - DELETEN (added, eoa - added); - eoa = ahead = 0; - - DELETEN (marked, eom - marked); - eom = mhead = 0; - - DELETEN (dfs, eod - dfs); - eod = dhead = 0; - - DELETEN (resolved, eor - resolved); - eor = rhead = 0; - - DELETEN (buffer, eob - buffer); - eob = bhead = 0; - - DELETEN (indices, eoi - indices); - eoi = ihead = 0; - - delete_prefix (); - - delete (rline[0], szrline); - delete (rline[1], szrline); - rline[0] = rline[1] = 0; - szrline = rcount = 0; - assert (getenv ("LEAK") || !current_bytes); /* found leak if failing */ - max_bytes = 0; - recycled = 0; - current_bytes = 0; - - lrestart = 0; - lreduce = 0; - lastreduceconflicts = 0; - llocked = 0; - lsimplify = 0; - fsimplify = 0; - - seconds = 0; - entered = 0; - nentered = 0; - measurealltimeinlib = 0; - - levelsum = 0.0; - calls = 0; - decisions = 0; - restarts = 0; - simps = 0; - iterations = 0; - reports = 0; - lastrheader = -2; - fixed = 0; -#ifndef NFL - failedlits = 0; - simplifying = 0; - fllimit = 0; -#ifdef STATS - efailedlits = ifailedlits = 0; - fltried = flskipped = floopsed = 0; - flcalls = flrounds = 0; - flprops = 0; -#endif -#endif - propagations = 0; - conflicts = 0; - noclauses = 0; - oadded = 0; - lladded = 0; - loadded = 0; - olits = 0; - nlclauses = 0; - ladded = 0; - addedclauses = 0; - llits = 0; - out = 0; -#ifdef TRACE - trace = 0; -#endif - rup = 0; - rupstarted = 0; - rupclauses = 0; - rupvariables = 0; - level = 0; - - reductions = 0; - - vused = 0; - llitsadded = 0; -#ifdef STATS - loused = 0; - llused = 0; - visits = 0; - bvisits = 0; - tvisits = 0; - lvisits = 0; - othertrue = 0; - othertrue2 = 0; - othertruel = 0; - othertrue2u = 0; - othertruelu = 0; - ltraversals = 0; - traversals = 0; -#ifndef NO_BINARY_CLAUSES - antecedents = 0; -#endif - znts = 0; - uips = 0; - assumptions = 0; - rdecisions = 0; - sdecisions = 0; - srecycled = 0; - rrecycled = 0; -#endif - minimizedllits = 0; - nonminimizedllits = 0; - state = RESET; - srng = 0; - - saved_flips = 0; - saved_max_var = 0; - min_flipped = UINT_MAX; - - flips = 0; -#ifdef STATS - forced = 0; - assignments = 0; -#endif - - sdflips = 0; - defaultphase = 2; - -#ifdef STATS - staticphasedecisions = 0; - inclreduces = 0; - skippedrestarts = 0; -#endif - - emgr = 0; - enew = 0; - eresize = 0; - edelete = 0; -#ifdef VISCORES - pclose (fviscores); - fviscores = 0; -#endif -} - -inline static void -tpush (Lit * lit) -{ - assert (lits < lit && lit <= lits + 2* max_var + 1); - if (thead == eot) - { - unsigned ttail2count = ttail2 - trail; - unsigned ttailcount = ttail - trail; -#ifndef NADC - unsigned ttailadocount = ttailado - trail; -#endif - ENLARGE (trail, thead, eot); - ttail = trail + ttailcount; - ttail2 = trail + ttail2count; -#ifndef NADC - ttailado = trail + ttailadocount; -#endif - } - - *thead++ = lit; -} - -static void -assign_reason (Var * v, Cls * reason) -{ -#ifdef NO_BINARY_CLAUSES - assert (reason != &impl); -#endif - v->reason = reason; -} - -static void -assign_phase (Lit * lit) -{ - unsigned new_phase, idx; - Var * v = LIT2VAR (lit); - -#ifndef NFL - /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if - * we force assignments on the top level. The other assignments will be - * undone and thus we can keep the old saved value of the phase. - */ - if (!level || !simplifying) -#endif - { - new_phase = (LIT2SGN (lit) > 0); - - if (v->assigned) - { - sdflips -= sdflips/FFLIPPED; - - if (new_phase != v->phase) - { - assert (FFLIPPEDPREC >= FFLIPPED); - sdflips += FFLIPPEDPREC / FFLIPPED; - flips++; - - idx = lit2idx (lit); - if (idx < min_flipped) - min_flipped = idx; - - NOLOG (fprintf (out, "%sflipped %d\n", prefix, lit2int (lit))); - } - } - - v->phase = new_phase; - v->assigned = 1; - } - - lit->val = TRUE; - NOTLIT (lit)->val = FALSE; -} - -inline static void -assign (Lit * lit, Cls * reason) -{ - Var * v = LIT2VAR (lit); - assert (lit->val == UNDEF); -#ifdef STATS - assignments++; -#endif - v->level = level; - assign_phase (lit); - assign_reason (v, reason); - tpush (lit); -} - -inline static int -cmp_added (Lit * k, Lit * l) -{ - Val a = k->val, b = l->val; - Var *u, *v; - int res; - - if (a == UNDEF && b != UNDEF) - return -1; - - if (a != UNDEF && b == UNDEF) - return 1; - - u = LIT2VAR (k); - v = LIT2VAR (l); - - if (a != UNDEF) - { - assert (b != UNDEF); - res = v->level - u->level; - if (res) - return res; /* larger level first */ - } - - res = cmpflt (VAR2RNK (v)->score, VAR2RNK (u)->score); - if (res) - return res; /* larger activity first */ - - return u - v; /* smaller index first */ -} - -static void -sorttwolits (Lit ** v) -{ - Lit * a = v[0], * b = v[1]; - - assert (a != b); - - if (a < b) - return; - - v[0] = b; - v[1] = a; -} - -inline static void -sortlits (Lit ** v, unsigned size) -{ - if (size == 2) - sorttwolits (v); /* same order with and with out 'NO_BINARY_CLAUSES' */ - else - sort (Lit *, cmp_added, v, size); -} - -#ifdef NO_BINARY_CLAUSES -static Cls * -setimpl (Lit * a, Lit * b) -{ - assert (!implvalid); - assert (impl.size == 2); - - impl.lits[0] = a; - impl.lits[1] = b; - - sorttwolits (impl.lits); - implvalid = 1; - - return &impl; -} - -static void -resetimpl (void) -{ - assert (implvalid); - implvalid = 0; -} - -static Cls * -setcimpl (Lit * a, Lit * b) -{ - assert (!cimplvalid); - assert (cimpl.size == 2); - - cimpl.lits[0] = a; - cimpl.lits[1] = b; - - sorttwolits (cimpl.lits); - cimplvalid = 1; - - return &cimpl; -} - -static void -resetcimpl (void) -{ - assert (cimplvalid); - cimplvalid = 0; -} - -#endif - -static int -cmp_ptr (void *l, void *k) -{ - return ((char*)l) - (char*)k; /* arbitrarily already reverse */ -} - -static int -cmp_rnk (Rnk * r, Rnk * s) -{ - if (!r->moreimportant && s->moreimportant) - return -1; - - if (r->moreimportant && !s->moreimportant) - return 1; - - if (!r->lessimportant && s->lessimportant) - return 1; - - if (r->lessimportant && !s->lessimportant) - return -1; - - if (r->score < s->score) - return -1; - - if (r->score > s->score) - return 1; - - return -cmp_ptr (r, s); -} - -static void -hup (Rnk * v) -{ - int upos, vpos; - Rnk *u; - -#ifndef NFL - assert (!simplifying); -#endif - - vpos = v->pos; - - assert (0 < vpos); - assert (vpos < hhead - heap); - assert (heap[vpos] == v); - - while (vpos > 1) - { - upos = vpos / 2; - - u = heap[upos]; - - if (cmp_rnk (u, v) > 0) - break; - - heap[vpos] = u; - u->pos = vpos; - - vpos = upos; - } - - heap[vpos] = v; - v->pos = vpos; -} - -static Cls *add_simplified_clause (int learned); - -inline static void -add_antecedent (Cls * c) -{ - assert (c); - -#ifdef NO_BINARY_CLAUSES - if (ISLITREASON (c)) - return; - - if (c == &impl) - return; -#else -#ifdef STATS - antecedents++; -#endif -#endif - if (rhead == eor) - ENLARGE (resolved, rhead, eor); - - assert (rhead < eor); - *rhead++ = c; -} - -#ifdef TRACE - -#ifdef NO_BINARY_CLAUSES -#error "can not combine TRACE and NO_BINARY_CLAUSES" -#endif - -#endif /* TRACE */ - -static void -add_lit (Lit * lit) -{ - assert (lit); - - if (ahead == eoa) - ENLARGE (added, ahead, eoa); - - *ahead++ = lit; -} - -static void -push_var_as_marked (Var * v) -{ - if (mhead == eom) - ENLARGE (marked, mhead, eom); - - *mhead++ = v; -} - -static void -mark_var (Var * v) -{ - assert (!v->mark); - v->mark = 1; - push_var_as_marked (v); -} - -/* Whenever we have a top level derived unit we really should derive a unit - * clause otherwise the resolutions in 'add_simplified_clause' become - * incorrect. - */ -static Cls * -resolve_top_level_unit (Lit * lit, Cls * reason) -{ - unsigned count_resolved; - Lit **p, **eol, *other; - Var *u, *v; - - assert (rhead == resolved); - assert (ahead == added); - - add_lit (lit); - add_antecedent (reason); - count_resolved = 1; - v = LIT2VAR (lit); - - eol = end_of_lits (reason); - for (p = reason->lits; p < eol; p++) - { - other = *p; - u = LIT2VAR (other); - if (u == v) - continue; - - add_antecedent (u->reason); - count_resolved++; - } - - /* Some of the literals could be assumptions. If at least one - * variable is not an assumption, we should resolve. - */ - if (count_resolved >= 2) - { -#ifdef NO_BINARY_CLAUSES - if (reason == &impl) - resetimpl (); -#endif - reason = add_simplified_clause (1); -#ifdef NO_BINARY_CLAUSES - if (reason->size == 2) - { - assert (reason == &impl); - other = reason->lits[0]; - if (lit == other) - other = reason->lits[1]; - assert (other->val == FALSE); - reason = LIT2REASON (NOTLIT (other)); - resetimpl (); - } -#endif - assign_reason (v, reason); - } - else - { - ahead = added; - rhead = resolved; - } - - return reason; -} - -static void -fixvar (Var * v) -{ - Rnk * r; - - assert (VAR2LIT (v) != UNDEF); - assert (!v->level); - - fixed++; - - r = VAR2RNK (v); - r->score = INFFLT; - -#ifndef NFL - if (simplifying) - return; -#endif - - if (!r->pos) - return; - - hup (r); -} - -static void -use_var (Var * v) -{ - if (v->used) - return; - - v->used = 1; - vused++; -} - -static void -assign_forced (Lit * lit, Cls * reason) -{ - Var *v; - - assert (reason); - assert (lit->val == UNDEF); - -#ifdef STATS - forced++; -#endif - assign (lit, reason); - -#ifdef NO_BINARY_CLAUSES - assert (reason != &impl); - if (ISLITREASON (reason)) - reason = setimpl (lit, NOTLIT (REASON2LIT (reason))); -#endif - LOG (fprintf (out, - "%sassign %d at level %d by ", - prefix, lit2int (lit), level); - dumpclsnl (reason)); - - v = LIT2VAR (lit); - if (!level) - use_var (v); - - if (reason && !level && reason->size > 1) - reason = resolve_top_level_unit (lit, reason); - -#ifdef NO_BINARY_CLAUSES - if (ISLITREASON (reason) || reason == &impl) - { - /* DO NOTHING */ - } - else -#endif - if (reason) - { - assert (!reason->locked); - reason->locked = 1; - if (reason->learned && reason->size > 2) - llocked++; - } - -#ifdef NO_BINARY_CLAUSES - if (reason == &impl) - resetimpl (); -#endif - - if (!level) - fixvar (v); -} - -#ifdef NO_BINARY_CLAUSES - -static void -lpush (Lit * lit, Cls * cls) -{ - int pos = (cls->lits[0] == lit); - Ltk * s = LIT2IMPLS (lit); - unsigned oldsize, newsize; - - assert (cls->size == 2); - - if (!s->start) - { - assert (!s->count); - assert (!s->ldsize); - NEWN (s->start, 1); - } - else - { - oldsize = (1 << (s->ldsize)); - assert (s->count <= oldsize); - if (s->count == oldsize) - { - newsize = 2 * oldsize; - RESIZEN (s->start, oldsize, newsize); - s->ldsize++; - } - } - - s->start[s->count++] = cls->lits[pos]; -} - -#endif - -static void -connect_head_tail (Lit * lit, Cls * cls) -{ - Cls ** s; - assert (cls->size >= 1); - if (cls->size == 2) - { -#ifdef NO_BINARY_CLAUSES - lpush (lit, cls); - return; -#else - s = LIT2IMPLS (lit); -#endif - } - else - s = LIT2HTPS (lit); - - if (cls->lits[0] != lit) - { - assert (cls->size >= 2); - assert (cls->lits[1] == lit); - cls->next[1] = *s; - } - else - cls->next[0] = *s; - - *s = cls; -} - -#ifdef TRACE -static void -zpush (Zhn * zhain) -{ - assert (trace); - - if (zhead == eoz) - ENLARGE (zhains, zhead, eoz); - - *zhead++ = zhain; -} - -static int -cmp_resolved (Cls * c, Cls * d) -{ - assert (trace); - - return CLS2IDX (c) - CLS2IDX (d); -} - -static void -bpushc (unsigned char ch) -{ - if (bhead == eob) - ENLARGE (buffer, bhead, eob); - - *bhead++ = ch; -} - -static void -bpushu (unsigned u) -{ - while (u & ~0x7f) - { - bpushc (u | 0x80); - u >>= 7; - } - - bpushc (u); -} - -static void -bpushd (unsigned prev, unsigned this) -{ - unsigned delta; - assert (prev < this); - delta = this - prev; - bpushu (delta); -} - -static void -add_zhain (void) -{ - unsigned prev, this, count, rcount; - Cls **p, *c; - Zhn *res; - - assert (trace); - assert (bhead == buffer); - assert (rhead > resolved); - - rcount = rhead - resolved; - sort (Cls *, cmp_resolved, resolved, rcount); - - prev = 0; - for (p = resolved; p < rhead; p++) - { - c = *p; - this = CLS2TRD (c)->idx; - bpushd (prev, this); - prev = this; - } - bpushc (0); - - count = bhead - buffer; - - res = new (sizeof (Zhn) + count); - res->core = 0; - res->ref = 0; - memcpy (res->znt, buffer, count); - - bhead = buffer; -#ifdef STATS - znts += count - 1; -#endif - zpush (res); -} - -#endif - -static void -add_resolved (int learned) -{ -#if defined(STATS) || defined(TRACE) - Cls **p, *c; - - for (p = resolved; p < rhead; p++) - { - c = *p; - if (c->used) - continue; - - c->used = 1; - - if (c->size <= 2) - continue; - -#ifdef STATS - if (c->learned) - llused++; - else - loused++; -#endif - } -#endif - -#ifdef TRACE - if (learned && trace) - add_zhain (); -#else - (void) learned; -#endif - rhead = resolved; -} - -static void -incjwh (Cls * cls) -{ - Lit **p, *lit, ** eol; - Flt * f, inc, sum; - unsigned size = 0; - Var * v; - Val val; - - eol = end_of_lits (cls); - - for (p = cls->lits; p < eol; p++) - { - lit = *p; - val = lit->val; - - if (val && level > 0) - { - v = LIT2VAR (lit); - if (v->level > 0) - val = UNDEF; - } - - if (val == TRUE) - return; - - if (val != FALSE) - size++; - } - - inc = base2flt (1, -size); - - for (p = cls->lits; p < eol; p++) - { - lit = *p; - f = LIT2JWH (lit); - sum = addflt (*f, inc); - *f = sum; - } -} - -static void -write_rup_header (FILE * file) -{ - char line[80]; - int i; - - sprintf (line, "%%RUPD32 %u %u", rupvariables, rupclauses); - - fputs (line, file); - for (i = 255 - strlen (line); i >= 0; i--) - fputc (' ', file); - - fputc ('\n', file); - fflush (file); -} - -static void -write_int (int d, FILE * file) -{ - static char write_int_buffer[16]; - unsigned tmp; - char * res; - int sign; - - assert (sizeof d <= 4); - - res = write_int_buffer + sizeof write_int_buffer; - *--res = 0; - - sign = (d < 0); - - if (sign) - tmp = (unsigned) -d; - else - tmp = d; - - do { - assert (res > write_int_buffer); - *--res = '0' + (tmp % 10); - tmp /= 10; - } while (tmp); - - if (sign) - { - assert (res > write_int_buffer); - *--res = '-'; - } - - fputs (res, file); -} - -static Cls * -add_simplified_clause (int learned) -{ - unsigned num_true, num_undef, num_false, idx, size, count_resolved; - Lit **p, **q, *lit, ** end; - Cls *res, * reason; - Val val; - Var *v; - -REENTER: - - size = ahead - added; - - add_resolved (learned); - - if (learned) - { - ladded++; - llitsadded += size; - if (size > 2) - { - lladded++; - nlclauses++; - llits += size; - } - } - else - { - oadded++; - if (size > 2) - { - loadded++; - noclauses++; - olits += size; - } - } - - addedclauses++; - assert (addedclauses == ladded + oadded); - -#ifdef NO_BINARY_CLAUSES - if (size == 2) - res = setimpl (added[0], added[1]); - else -#endif - { - sortlits (added, size); - - if (learned) - { - if (lhead == eol) - { - ENLARGE (lclauses, lhead, eol); - - /* A very difficult to find bug, which only occurs if the - * learned clauses stack is immediately allocated before the - * original clauses stack without padding. In this case, we - * have 'SOC == EOC', which terminates all loops using the - * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately. - * Unfortunately this occurred in 'fix_clause_lits' after - * using a recent version of the memory allocator of 'Google' - * perftools in the context of one large benchmark for - * 'boolector'. - */ - if (eol == oclauses) - ENLARGE (lclauses, lhead, eol); - } - - idx = LIDX2IDX (lhead - lclauses); - } - else - { - if (ohead == eoo) - { - ENLARGE (oclauses, ohead, eoo); - if (eol == oclauses) - ENLARGE (oclauses, ohead, eoo); /* dito */ - } - - idx = OIDX2IDX (ohead - oclauses); - } - - assert (eol != oclauses); /* dito */ - - res = new_clause (size, learned); - -#if !defined(NDEBUG) && defined(TRACE) - if (trace) - assert (CLS2IDX (res) == idx); -#endif - if (learned) - *lhead++ = res; - else - *ohead++ = res; - -#if !defined(NDEBUG) && defined(TRACE) - if (trace && learned) - assert (zhead - zhains == lhead - lclauses); -#endif - assert (lhead != oclauses); /* dito */ - } - - if (learned && rup) - { - if (!rupstarted) - { - write_rup_header (rup); - rupstarted = 1; - } - } - - num_true = num_undef = num_false = 0; - - q = res->lits; - for (p = added; p < ahead; p++) - { - lit = *p; - *q++ = lit; - - if (learned && rup) - { - write_int (lit2int (lit), rup); - fputc (' ', rup); - } - - val = lit->val; - - num_true += (val == TRUE); - num_undef += (val == UNDEF); - num_false += (val == FALSE); - - v = LIT2VAR (lit); - } - assert (num_false + num_true + num_undef == size); - - if (learned && rup) - fputs ("0\n", rup); - - ahead = added; /* reset */ - - if (size > 0) - { - connect_head_tail (res->lits[0], res); - if (size > 1) - connect_head_tail (res->lits[1], res); - } - - if (size == 0) - { - if (!mtcls) - mtcls = res; - } - -#ifdef NO_BINARY_CLAUSES - if (size != 2) -#endif -#ifndef NDEBUG - res->connected = 1; -#endif - - LOG (fprintf (out, "%s%s ", prefix, learned ? "learned" : "original"); - dumpclsnl (res)); - - /* Shrink clause by resolving it against top level assignments. - */ - if (!level && num_false > 0) - { - assert (ahead == added); - assert (rhead == resolved); - - count_resolved = 1; - add_antecedent (res); - - end = end_of_lits (res); - for (p = res->lits; p < end; p++) - { - lit = *p; - v = LIT2VAR (lit); - use_var (v); - - if (lit->val == FALSE) - { - add_antecedent (v->reason); - count_resolved++; - } - else - add_lit (lit); - } - - assert (count_resolved >= 2); - - learned = 1; -#ifdef NO_BINARY_CLAUSES - if (res == &impl) - resetimpl (); -#endif - goto REENTER; /* and return simplified clause */ - } - - if (!num_true && num_undef == 1) /* unit clause */ - { - lit = 0; - for (p = res->lits; p < res->lits + size; p++) - { - if ((*p)->val == UNDEF) - lit = *p; - - v = LIT2VAR (*p); - use_var (v); - } - assert (lit); - - reason = res; -#ifdef NO_BINARY_CLAUSES - if (size == 2) - { - Lit * other = res->lits[0]; - if (other == lit) - other = res->lits[1]; - - assert (other->val == FALSE); - reason = LIT2REASON (NOTLIT (other)); - } -#endif - assign_forced (lit, reason); - num_true++; - } - - if (num_false == size && !conflict) - { -#ifdef NO_BINARY_CLAUSES - if (res == &impl) - conflict = setcimpl (res->lits[0], res->lits[1]); - else -#endif - conflict = res; - } - - if (!learned && !num_true && num_undef) - incjwh (res); - //FIXME: perhaps sketchy unsound hack -/* #ifdef NO_BINARY_CLAUSES */ -/* if (res == &impl) */ -/* resetimpl (); */ -/* #endif */ - return res; -} - -static int -trivial_clause (void) -{ - Lit **p, **q, *prev; - Var *v; - - sort (Lit *, cmp_ptr, added, ahead - added); - - prev = 0; - q = added; - for (p = q; p < ahead; p++) - { - Lit *this = *p; - - v = LIT2VAR (this); - - if (prev == this) /* skip repeated literals */ - continue; - - /* Top level satisfied ? - */ - if (this->val == TRUE && !v->level) - return 1; - - if (prev == NOTLIT (this))/* found pair of dual literals */ - return 1; - - *q++ = prev = this; - } - - ahead = q; /* shrink */ - - return 0; -} - -static void -simplify_and_add_original_clause (void) -{ - Cls * cls; - - if (trivial_clause ()) - { - ahead = added; - - if (ohead == eoo) - ENLARGE (oclauses, ohead, eoo); - - *ohead++ = 0; - - addedclauses++; - oadded++; - } - else - { - cls = add_simplified_clause (0); -#ifdef NO_BINARY_CLAUSES - if (cls == &impl) - resetimpl (); -#endif - } -} - -#ifndef NADC - -static void -add_ado (void) -{ - unsigned len = ahead - added; - Lit ** ado, ** p, ** q, *lit; - Var * v, * u; - -#ifdef TRACE - assert (!trace); -#endif - - ABORTIF (ados < hados && llength (ados[0]) != len, - "internal: non matching all different constraint object lengths"); - - if (hados == eados) - ENLARGE (ados, hados, eados); - - NEWN (ado, len + 1); - *hados++ = ado; - - p = added; - q = ado; - u = 0; - while (p < ahead) - { - lit = *p++; - v = LIT2VAR (lit); - ABORTIF (v->inado, - "internal: variable in multiple all different objects"); - v->inado = ado; - if (!u && !lit->val) - u = v; - *q++ = lit; - } - - assert (q == ado + len); - *q++ = 0; - - /* TODO simply do a conflict test as in propado */ - - ABORTIF (!u, - "internal: " - "adding fully instantiated all different object not implemented yet"); - - assert (u); - assert (u->inado == ado); - assert (!u->ado); - u->ado = ado; - - ahead = added; -} - -#endif - -static void -hdown (Rnk * r) -{ - unsigned end, rpos, cpos, opos; - Rnk *child, *other; - - assert (r->pos > 0); - assert (heap[r->pos] == r); - - end = hhead - heap; - rpos = r->pos; - - for (;;) - { - cpos = 2 * rpos; - if (cpos >= end) - break; - - opos = cpos + 1; - child = heap[cpos]; - - if (cmp_rnk (r, child) < 0) - { - if (opos < end) - { - other = heap[opos]; - - if (cmp_rnk (child, other) < 0) - { - child = other; - cpos = opos; - } - } - } - else if (opos < end) - { - child = heap[opos]; - - if (cmp_rnk (r, child) >= 0) - break; - - cpos = opos; - } - else - break; - - heap[rpos] = child; - child->pos = rpos; - rpos = cpos; - } - - r->pos = rpos; - heap[rpos] = r; -} - -static Rnk * -htop (void) -{ - assert (hhead > heap); - return heap[1]; -} - -static Rnk * -hpop (void) -{ - Rnk *res, *last; - unsigned end; - - assert (hhead > heap); - - res = heap[1]; - res->pos = 0; - - end = --hhead - heap; - if (end == 1) - return res; - - last = heap[end]; - - heap[last->pos = 1] = last; - hdown (last); - - return res; -} - -inline static void -hpush (Rnk * r) -{ - assert (!r->pos); - - if (hhead == eoh) - ENLARGE (heap, hhead, eoh); - - r->pos = hhead++ - heap; - heap[r->pos] = r; - hup (r); -} - -static void -fix_trail_lits (long delta) -{ - Lit **p; - for (p = trail; p < thead; p++) - *p += delta; -} - -#ifdef NO_BINARY_CLAUSES -static void -fix_impl_lits (long delta) -{ - Ltk * s; - Lit ** p; - - for (s = impls + 2; s < impls + 2 * max_var; s++) - for (p = s->start; p < s->start + s->count; p++) - *p += delta; -} -#endif - -static void -fix_clause_lits (long delta) -{ - Cls **p, *clause; - Lit **q, *lit, **eol; - - for (p = SOC; p != EOC; p = NXC (p)) - { - clause = *p; - if (!clause) - continue; - - q = clause->lits; - eol = end_of_lits (clause); - while (q < eol) - { - assert (q - clause->lits <= (int) clause->size); - lit = *q; - lit += delta; - *q++ = lit; - } - } -} - -static void -fix_added_lits (long delta) -{ - Lit **p; - for (p = added; p < ahead; p++) - *p += delta; -} - -static void -fix_assumed_lits (long delta) -{ - Lit **p; - for (p = als; p < alshead; p++) - *p += delta; -} - -static void -fix_heap_rnks (long delta) -{ - Rnk **p; - - for (p = heap + 1; p < hhead; p++) - *p += delta; -} - -#ifndef NADC - -static void -fix_ado (long delta, Lit ** ado) -{ - Lit ** p; - for (p = ado; *p; p++) - *p += delta; -} - -static void -fix_ados (long delta) -{ - Lit *** p; - - for (p = ados; p < hados; p++) - fix_ado (delta, *p); -} - -#endif - -static void -enlarge (unsigned new_size_vars) -{ - long rnks_delta, lits_delta, vars_delta; - Lit *old_lits = lits; - Rnk *old_rnks = rnks; - Var *old_vars = vars; - - RESIZEN (lits, 2 * size_vars, 2 * new_size_vars); - RESIZEN (jwh, 2 * size_vars, 2 * new_size_vars); - RESIZEN (htps, 2 * size_vars, 2 * new_size_vars); -#ifndef NDSC - RESIZEN (dhtps, 2 * size_vars, 2 * new_size_vars); -#endif - RESIZEN (impls, 2 * size_vars, 2 * new_size_vars); - RESIZEN (vars, size_vars, new_size_vars); - RESIZEN (rnks, size_vars, new_size_vars); - - lits_delta = lits - old_lits; - rnks_delta = rnks - old_rnks; - vars_delta = vars - old_vars; - - fix_trail_lits (lits_delta); - fix_clause_lits (lits_delta); - fix_added_lits (lits_delta); - fix_assumed_lits (lits_delta); -#ifdef NO_BINARY_CLAUSES - fix_impl_lits (lits_delta); -#endif -#ifndef NADC - fix_ados (lits_delta); -#endif - fix_heap_rnks (rnks_delta); - assert (mhead == marked); - - size_vars = new_size_vars; -} - -static void -unassign (Lit * lit) -{ - Cls *reason; - Var *v; - Rnk *r; - - assert (lit->val == TRUE); - - LOG (fprintf (out, "%sunassign %d\n", prefix, lit2int (lit))); - - v = LIT2VAR (lit); - reason = v->reason; - -#ifdef NO_BINARY_CLAUSES - assert (reason != &impl); - if (ISLITREASON (reason)) - { - /* DO NOTHING */ - } - else -#endif - if (reason) - { - assert (reason->locked); - reason->locked = 0; - if (reason->learned && reason->size > 2) - { - assert (llocked > 0); - llocked--; - } - } - - lit->val = UNDEF; - NOTLIT (lit)->val = UNDEF; - - r = VAR2RNK (v); - if (!r->pos) - hpush (r); - -#ifndef NDSC - { - Cls * p, * next, ** q; - - q = LIT2DHTPS (lit); - p = *q; - *q = 0; - - while (p) - { - Lit * other = p->lits[0]; - - if (other == lit) - { - other = p->lits[1]; - q = p->next + 1; - } - else - { - assert (p->lits[1] == lit); - q = p->next; - } - - next = *q; - *q = *LIT2HTPS (other); - *LIT2HTPS (other) = p; - p = next; - } - } -#endif - -#ifndef NADC - if (v->adotabpos) - { - assert (nadotab); - assert (*v->adotabpos == v->ado); - - *v->adotabpos = 0; - v->adotabpos = 0; - - nadotab--; - } -#endif -} - -static Cls * -var2reason (Var * var) -{ - Cls * res = var->reason; -#ifdef NO_BINARY_CLAUSES - Lit * this, * other; - if (ISLITREASON (res)) - { - this = VAR2LIT (var); - if (this->val == FALSE) - this = NOTLIT (this); - - other = REASON2LIT (res); - assert (other->val == TRUE); - assert (this->val == TRUE); - res = setimpl (NOTLIT (other), this); - } -#endif - return res; -} - -static void -mark_clause_to_be_collected (Cls * cls) -{ - assert (!cls->collect); - cls->collect = 1; -} - -static void -undo (unsigned new_level) -{ - Lit *lit; - Var *v; - - while (thead > trail) - { - lit = *--thead; - v = LIT2VAR (lit); - if (v->level == new_level) - { - thead++; /* fix pre decrement */ - break; - } - - unassign (lit); - } - - level = new_level; - ttail = thead; - ttail2 = thead; -#ifndef NADC - ttailado = thead; -#endif - -#ifdef NO_BINARY_CLAUSES - if (conflict == &cimpl) - resetcimpl (); -#endif -#ifndef NADC - if (conflict && conflict == adoconflict) - resetadoconflict (); -#endif - conflict = mtcls; - if (level < adecidelevel) - { - assert (als < alshead); - adecidelevel = 0; - alstail = als; - } - LOG (fprintf (out, "%sback to level %u\n", prefix, level)); -} - -#ifndef NDEBUG - -static int -clause_satisfied (Cls * cls) -{ - Lit **p, **eol, *lit; - - eol = end_of_lits (cls); - for (p = cls->lits; p < eol; p++) - { - lit = *p; - if (lit->val == TRUE) - return 1; - } - - return 0; -} - -static void -original_clauses_satisfied (void) -{ - Cls **p, *cls; - - for (p = oclauses; p < ohead; p++) - { - cls = *p; - - if (!cls) - continue; - - if (cls->learned) - continue; - - assert (clause_satisfied (cls)); - } -} - -static void -assumptions_satisfied (void) -{ - Lit *lit, ** p; - - for (p = als; p < alshead; p++) - { - lit = *p; - assert (lit->val == TRUE); - } -} - -#endif - -static void -sflush (void) -{ - double now = picosat_time_stamp (); - double delta = now - entered; - delta = (delta < 0) ? 0 : delta; - seconds += delta; - entered = now; -} - -static double -mb (void) -{ - return current_bytes / (double) (1 << 20); -} - -static double -avglevel (void) -{ - return decisions ? levelsum / decisions : 0.0; -} - -static void -rheader (void) -{ - assert (lastrheader <= reports); - - if (lastrheader == reports) - return; - - lastrheader = reports; - - fprintf (out, "%s\n", prefix); - fprintf (out, "%s %s\n", prefix, rline[0]); - fprintf (out, "%s %s\n", prefix, rline[1]); - fprintf (out, "%s\n", prefix); -} - -static unsigned -dynamic_flips_per_assignment_per_mille (void) -{ - assert (FFLIPPEDPREC >= 1000); - return sdflips / (FFLIPPEDPREC / 1000); -} - -#ifdef NLUBY - -static int -high_agility (void) -{ - return dynamic_flips_per_assignment_per_mille () >= 200; -} - -static int -very_high_agility (void) -{ - return dynamic_flips_per_assignment_per_mille () >= 250; -} - -#else - -static int -medium_agility (void) -{ - return dynamic_flips_per_assignment_per_mille () >= 230; -} - -#endif - -static void -relemdata (void) -{ - char *p; - int x; - - if (reports < 0) - { - /* strip trailing white space - */ - for (x = 0; x <= 1; x++) - { - p = rline[x] + strlen (rline[x]); - while (p-- > rline[x]) - { - if (*p != ' ') - break; - - *p = 0; - } - } - - rheader (); - } - else - fputc ('\n', out); - - rcount = 0; -} - -static void -relemhead (const char * name, int fp, double val) -{ - int x, y, len, size; - const char *fmt; - unsigned tmp, e; - - if (reports < 0) - { - x = rcount & 1; - y = (rcount / 2) * 12 + x * 6; - - if (rcount == 1) - sprintf (rline[1], "%6s", ""); - - len = strlen (name); - while (szrline <= len + y + 1) - { - size = szrline ? 2 * szrline : 128; - rline[0] = resize (rline[0], szrline, size); - rline[1] = resize (rline[1], szrline, size); - szrline = size; - } - - fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s"; - sprintf (rline[x] + y, fmt, name, ""); - } - else if (val < 0) - { - assert (fp); - - if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0) - { - fprintf (out, "-%4.1f ", -tmp / 10.0); - } - else - { - tmp = -val / 10.0 + 0.5; - e = 1; - while (tmp >= 100) - { - tmp /= 10; - e++; - } - - fprintf (out, "-%2ue%u ", tmp, e); - } - } - else - { - if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000) - { - fprintf (out, "%5.1f ", tmp / 10.0); - } - else if (!fp && (tmp = val) < 100000) - { - fprintf (out, "%5u ", tmp); - } - else - { - tmp = val / 10.0 + 0.5; - e = 1; - - while (tmp >= 1000) - { - tmp /= 10; - e++; - } - - fprintf (out, "%3ue%u ", tmp, e); - } - } - - rcount++; -} - -inline static void -relem (const char *name, int fp, double val) -{ - if (name) - relemhead (name, fp, val); - else - relemdata (); -} - -static unsigned -reduce_limit_on_lclauses (void) -{ - unsigned res = lreduce; - res += llocked; - return res; -} - -static void -report (int level, char type) -{ - int rounds; - - if (verbosity < level) - return; - - sflush (); - - if (!reports) - reports = -1; - - for (rounds = (reports < 0) ? 2 : 1; rounds; rounds--) - { - if (reports >= 0) - fprintf (out, "%s%c ", prefix, type); - - relem ("seconds", 1, seconds); - relem ("level", 1, avglevel ()); - assert (fixed <= max_var); - relem ("variables", 0, max_var - fixed); - relem ("used", 1, PERCENT (vused, max_var)); - relem ("original", 0, noclauses); - relem ("conflicts", 0, conflicts); - //relem ("decisions", 0, decisions); - // relem ("conf/dec", 1, PERCENT(conflicts,decisions)); - // relem ("limit", 0, reduce_limit_on_lclauses ()); - relem ("learned", 0, nlclauses); - // relem ("limit", 1, PERCENT (nlclauses, reduce_limit_on_lclauses ())); - relem ("limit", 0, lreduce); -#ifdef STATS - relem ("learning", 1, PERCENT (llused, lladded)); -#endif - relem ("agility", 1, dynamic_flips_per_assignment_per_mille () / 10.0); - // relem ("original", 0, noclauses); - relem ("MB", 1, mb ()); - // relem ("lladded", 0, lladded); - // relem ("llused", 0, llused); - - relem (0, 0, 0); - - reports++; - } - - /* Adapt this to the number of rows in your terminal. - */ - #define ROWS 25 - - if (reports % (ROWS - 3) == (ROWS - 4)) - rheader (); - - fflush (out); -} - -static int -bcp_queue_is_empty (void) -{ - if (ttail != thead) - return 0; - - if (ttail2 != thead) - return 0; - -#ifndef NADC - if (ttailado != thead) - return 0; -#endif - - return 1; -} - -static int -satisfied (void) -{ - assert (!mtcls); - assert (!failed_assumption); - if (alstail < alshead) - return 0; - assert (!conflict); - assert (bcp_queue_is_empty ()); - return thead == trail + max_var; /* all assigned */ -} - -static void -vrescore (void) -{ - Rnk *p, *eor = rnks + max_var; - for (p = rnks + 1; p <= eor; p++) - if (p->score != INFFLT) - p->score = mulflt (p->score, ilvinc); - vinc = mulflt (vinc, ilvinc);; -#ifdef VISCORES - nvinc = mulflt (nvinc, lscore);; -#endif -} - -static void -inc_score (Var * v) -{ - Flt score; - Rnk *r; - -#ifndef NFL - if (simplifying) - return; -#endif - - if (!v->level) - return; - - r = VAR2RNK (v); - score = r->score; - - assert (score != INFFLT); - - score = addflt (score, vinc); - assert (score < INFFLT); - r->score = score; - if (r->pos > 0) - hup (r); - - if (score > lscore) - vrescore (); -} - -static void -inc_activity (Cls * cls) -{ - Act *p; - - if (!cls->learned) - return; - - if (cls->size <= 2) - return; - - p = CLS2ACT (cls); - *p = addflt (*p, cinc); -} - -static unsigned -hashlevel (unsigned l) -{ - return 1u << (l & 31); -} - -static void -push (Var * v) -{ - if (dhead == eod) - ENLARGE (dfs, dhead, eod); - - *dhead++ = v; -} - -static Var * -pop (void) -{ - assert (dfs < dhead); - return *--dhead; -} - -static void -analyze (void) -{ - unsigned open, minlevel, siglevels, l, old, i, orig; - Lit *this, *other, **p, **q, **eol; - Var *v, *u, **m, *start, *uip; - Cls *c; - - assert (conflict); - - assert (ahead == added); - assert (mhead == marked); - assert (rhead == resolved); - - /* 2. Search for First UIP variable and mark all resolved variables. At - * the same time determine the minimum decision level involved. Increase - * activities of resolved variables. - */ - q = thead; - open = 0; - minlevel = level; - siglevels = 0; - uip = 0; - - c = conflict; - - for (;;) - { - add_antecedent (c); - inc_activity (c); - eol = end_of_lits (c); - for (p = c->lits; p < eol; p++) - { - other = *p; - - if (other->val == TRUE) - continue; - - assert (other->val == FALSE); - - u = LIT2VAR (other); - if (u->mark) - continue; - - u->mark = 1; - inc_score (u); - use_var (u); - - if (u->level == level) - { - open++; - } - else - { - push_var_as_marked (u); - - if (u->level) - { - /* The statistics counter 'nonminimizedllits' sums up the - * number of literals that would be added if only the - * 'first UIP' scheme for learned clauses would be used - * and no clause minimization. - */ - nonminimizedllits++; - - if (u->level < minlevel) - minlevel = u->level; - - siglevels |= hashlevel (u->level); - } - else - { - assert (!u->level); - assert (u->reason); - } - } - } - - do - { - if (q == trail) - { - uip = 0; - goto DONE_FIRST_UIP; - } - - this = *--q; - uip = LIT2VAR (this); - } - while (!uip->mark); - - uip->mark = 0; - - c = var2reason (uip); -#ifdef NO_BINARY_CLAUSES - if (c == &impl) - resetimpl (); -#endif - open--; - if ((!open && level) || !c) - break; - - assert (c); - } - -DONE_FIRST_UIP: - - if (uip) - { - assert (level); - this = VAR2LIT (uip); - this += (this->val == TRUE); - nonminimizedllits++; - minimizedllits++; - add_lit (this); -#ifdef STATS - if (uip->reason) - uips++; -#endif - } - else - assert (!level); - - /* 3. Try to mark more intermediate variables, with the goal to minimize - * the conflict clause. This is a DFS from already marked variables - * backward through the implication graph. It tries to reach other marked - * variables. If the search reaches an unmarked decision variable or a - * variable assigned below the minimum level of variables in the first uip - * learned clause or a level on which no variable has been marked, then - * the variable from which the DFS is started is not redundant. Otherwise - * the start variable is redundant and will eventually be removed from the - * learned clause in step 4. We initially implemented BFS, but then - * profiling revelead that this step is a bottle neck for certain - * incremental applications. After switching to DFS this hot spot went - * away. - */ - orig = mhead - marked; - for (i = 0; i < orig; i++) - { - start = marked[i]; - - assert (start->mark); - assert (start != uip); - assert (start->level < level); - - if (!start->reason) - continue; - - old = mhead - marked; - assert (dhead == dfs); - push (start); - - while (dhead > dfs) - { - u = pop (); - assert (u->mark); - - c = var2reason (u); -#ifdef NO_BINARY_CLAUSES - if (c == &impl) - resetimpl (); -#endif - if (!c || - ((l = u->level) && - (l < minlevel || ((hashlevel (l) & ~siglevels))))) - { - while (mhead > marked + old) /* reset all marked */ - (*--mhead)->mark = 0; - - dhead = dfs; /* and DFS stack */ - break; - } - - eol = end_of_lits (c); - for (p = c->lits; p < eol; p++) - { - v = LIT2VAR (*p); - if (v->mark) - continue; - - mark_var (v); - push (v); - } - } - } - - for (m = marked; m < mhead; m++) - { - v = *m; - - assert (v->mark); - assert (!v->resolved); - - use_var (v); - - c = var2reason (v); - if (!c) - continue; - -#ifdef NO_BINARY_CLAUSES - if (c == &impl) - resetimpl (); -#endif - eol = end_of_lits (c); - for (p = c->lits; p < eol; p++) - { - other = *p; - - u = LIT2VAR (other); - if (!u->level) - continue; - - if (!u->mark) /* 'MARKTEST' */ - break; - } - - if (p != eol) - continue; - - add_antecedent (c); - v->resolved = 1; - } - - for (m = marked; m < mhead; m++) - { - v = *m; - - assert (v->mark); - v->mark = 0; - - if (v->resolved) - { - v->resolved = 0; - continue; - } - - this = VAR2LIT (v); - if (this->val == TRUE) - this++; /* actually NOTLIT */ - - add_lit (this); - minimizedllits++; - } - - assert (ahead <= eoa); - assert (rhead <= eor); - - mhead = marked; -} - -static void -fanalyze (void) -{ - Lit ** eol, ** p, * lit; - Cls * cls, * reason; - Var * v, * u; - int next; - - double start = picosat_time_stamp (); - - assert (failed_assumption); - assert (failed_assumption->val == FALSE); - - v = LIT2VAR (failed_assumption); - reason = var2reason (v); - if (!reason) return; -#ifdef NO_BINARY_CLAUSES - if (reason == &impl) - resetimpl (); -#endif - - eol = end_of_lits (reason); - for (p = reason->lits; p != eol; p++) - { - lit = *p; - u = LIT2VAR (lit); - if (u == v) continue; - if (u->reason) break; - } - if (p == eol) return; - - assert (ahead == added); - assert (mhead == marked); - assert (rhead == resolved); - - next = 0; - mark_var (v); - add_lit (NOTLIT (failed_assumption)); - - do - { - v = marked[next++]; - use_var (v); - if (v->reason) - { - reason = var2reason (v); -#ifdef NO_BINARY_CLAUSES - if (reason == &impl) - resetimpl (); -#endif - add_antecedent (reason); - eol = end_of_lits (reason); - for (p = reason->lits; p != eol; p++) - { - lit = *p; - u = LIT2VAR (lit); - if (u == v) continue; - if (u->mark) continue; - mark_var (u); - } - } - else - { - lit = VAR2LIT (v); - if (lit->val == TRUE) lit = NOTLIT (lit); - add_lit (lit); - } - } - while (marked + next < mhead); - - cls = add_simplified_clause (1); - v = LIT2VAR (failed_assumption); - reason = var2reason (v); -#ifdef NO_BINARY_CLAUSES - if (reason == &impl) - resetimpl (); - else -#endif - { - assert (reason->locked); - reason->locked = 0; - } - if (reason->learned && reason->size > 2) - { - assert (llocked > 0); - llocked--; - } - v->reason = cls; - assert (cls->learned); - assert (!cls->locked); - cls->locked = 1; - if (cls->size > 2) - { - llocked++; - assert (llocked > 0); - } - - while (mhead > marked) - (*--mhead)->mark = 0; - - if (verbosity) - fprintf (out, "%sfanalyze took %.1f seconds\n", - prefix, picosat_time_stamp () - start); -} - -/* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in - * which 'this' occurs. - */ -inline static void -prop2 (Lit * this) -{ -#ifdef NO_BINARY_CLAUSES - Lit ** l, ** start; - Ltk * lstk; -#else - Cls * cls, ** p; - Cls * next; -#endif - Lit * other; - Val tmp; - - assert (this->val == FALSE); - -#ifdef NO_BINARY_CLAUSES - lstk = LIT2IMPLS (this); - start = lstk->start; - l = start + lstk->count; - while (l != start) - { -#ifdef STATS - /* The counter 'visits' is the number of clauses that are - * visited during propagations of assignments. - */ - visits++; - bvisits++; -#endif - other = *--l; - tmp = other->val; - - if (tmp == TRUE) - { -#ifdef STATS - othertrue++; - othertrue2++; - if (LIT2VAR (other)->level < level) - othertrue2u++; -#endif - continue; - } - - if (tmp != FALSE) - { - assign_forced (other, LIT2REASON (NOTLIT(this))); - continue; - } - - if (conflict == &cimpl) - resetcimpl (); - conflict = setcimpl (this, other); - } -#else - /* Traverse all binary clauses with 'this'. Head/Tail pointers for binary - * clauses do not have to be modified here. - */ - p = LIT2IMPLS (this); - for (cls = *p; cls; cls = next) - { -#ifdef STATS - visits++; - bvisits++; -#endif - assert (!cls->collect); -#ifdef TRACE - assert (!cls->collected); -#endif - assert (cls->size == 2); - - other = cls->lits[0]; - if (other == this) - { - next = cls->next[0]; - other = cls->lits[1]; -#ifdef STATS -#endif - } - else - next = cls->next[1]; - - tmp = other->val; - - if (tmp == TRUE) - { -#ifdef STATS - othertrue++; - othertrue2++; - if (LIT2VAR (other)->level < level) - othertrue2u++; -#endif - continue; - } - - if (tmp == FALSE) - conflict = cls; - else - assign_forced (other, cls); /* unit clause */ - } -#endif /* !defined(NO_BINARY_CLAUSES) */ -} - -#ifndef NDSC -static int -should_disconnect_head_tail (Lit * lit) -{ - unsigned lit_level; - Var * v; - - assert (lit->val == TRUE); - - v = LIT2VAR (lit); - lit_level = v->level; - - if (!lit_level) - return 1; - -#ifndef NFL - if (simplifying) - return 0; -#endif - - return lit_level < level; -} -#endif - -inline static void -propl (Lit * this) -{ - Lit **l, *other, *prev, *new_lit, **eol; - Cls *next, **htp_ptr, **new_htp_ptr; - Cls *cls; -#ifdef STATS - unsigned size; -#endif - - htp_ptr = LIT2HTPS (this); - assert (this->val == FALSE); - - /* Traverse all non binary clauses with 'this'. Head/Tail pointers are - * updated as well. - */ - for (cls = *htp_ptr; cls; cls = next) - { -#ifdef STATS - visits++; - size = cls->size; - if (size == 2) - bvisits++; - else if (size >= 3) - { - traversals++; /* other is dereferenced at least */ - - if (size == 3) - tvisits++; - else if (size >= 4) - { - lvisits++; - ltraversals++; - } - } -#endif -#ifdef TRACE - assert (!cls->collected); -#endif - assert (cls->size > 0); - - /* With assumptions we need to traverse unit clauses as well. - */ - if (cls->size == 1) - { - assert (!conflict); - conflict = cls; - break; - } - - other = cls->lits[0]; - if (other != this) - { - cls->lits[0] = this; - cls->lits[1] = other; - next = cls->next[1]; - cls->next[1] = cls->next[0]; - cls->next[0] = next; - } - else - { - other = cls->lits[1]; - next = cls->next[0]; - } - assert (other == cls->lits[1]); - assert (this == cls->lits[0]); - assert (next == cls->next[0]); - assert (!cls->collect); - - if (other->val == TRUE) - { -#ifdef STATS - othertrue++; - othertruel++; -#endif -#ifndef NDSC - if (should_disconnect_head_tail (other)) - { - new_htp_ptr = LIT2DHTPS (other); - cls->next[0] = *new_htp_ptr; - *new_htp_ptr = cls; -#ifdef STATS - othertruelu++; -#endif - *htp_ptr = next; - continue; - } -#endif - htp_ptr = cls->next; - continue; - } - - l = cls->lits + 1; - eol = cls->lits + cls->size; - prev = this; - - while (++l != eol) - { -#ifdef STATS - if (size >= 3) - { - traversals++; - if (size > 3) - ltraversals++; - } -#endif - new_lit = *l; - *l = prev; - prev = new_lit; - if (new_lit->val != FALSE) break; - } - - if (l == eol) - { - while (l > cls->lits + 2) - { - new_lit = *--l; - *l = prev; - prev = new_lit; - } - assert (cls->lits[0] == this); - - assert (other == cls->lits[1]); - if (other->val == FALSE) /* found conflict */ - { - assert (!conflict); - conflict = cls; - return; - } - - assign_forced (other, cls); /* unit clause */ - htp_ptr = cls->next; - } - else - { - assert (new_lit->val == TRUE || new_lit->val == UNDEF); - cls->lits[0] = new_lit; - // *l = this; - new_htp_ptr = LIT2HTPS (new_lit); - cls->next[0] = *new_htp_ptr; - *new_htp_ptr = cls; - *htp_ptr = next; - } - } -} - -#ifndef NADC - -static unsigned primes[] = { 996293, 330643, 753947, 500873 }; - -#define PRIMES ((sizeof primes)/sizeof *primes) - -static unsigned -hash_ado (Lit ** ado, unsigned salt) -{ - unsigned i, res, tmp; - Lit ** p, * lit; - - assert (salt < PRIMES); - - i = salt; - res = 0; - - for (p = ado; (lit = *p); p++) - { - assert (lit->val); - - tmp = res >> 31; - res <<= 1; - - if (lit->val > 0) - res |= 1; - - assert (i < PRIMES); - res *= primes[i++]; - if (i == PRIMES) - i = 0; - - res += tmp; - } - - return res & (szadotab - 1); -} - -static unsigned -cmp_ado (Lit ** a, Lit ** b) -{ - Lit ** p, ** q, * l, * k; - int res; - - for (p = a, q = b; (l = *p); p++, q++) - { - k = *q; - assert (k); - if ((res = (l->val - k->val))) - return res; - } - - assert (!*q); - - return 0; -} - -static Lit *** -find_ado (Lit ** ado) -{ - Lit *** res, ** other; - unsigned pos, delta; - - pos = hash_ado (ado, 0); - assert (pos < szadotab); - res = adotab + pos; - - other = *res; - if (!other || !cmp_ado (other, ado)) - return res; - - delta = hash_ado (ado, 1); - if (!(delta & 1)) - delta++; - - assert (delta & 1); - assert (delta < szadotab); - - for (;;) - { - pos += delta; - if (pos >= szadotab) - pos -= szadotab; - - assert (pos < szadotab); - res = adotab + pos; - other = *res; - if (!other || !cmp_ado (other, ado)) - return res; - } -} - -static void -enlarge_adotab (void) -{ - /* TODO make this generic */ - - ABORTIF (szadotab, - "internal: all different objects table needs larger initial size"); - assert (!nadotab); - szadotab = 10000; - NEWN (adotab, szadotab); - CLRN (adotab, szadotab); -} - -static int -propado (Var * v) -{ - Lit ** p, ** q, *** adotabpos, **ado, * lit; - Var * u; - - if (level && adodisabled) - return 1; - - assert (!conflict); - assert (!adoconflict); - assert (VAR2LIT (v)->val != UNDEF); - assert (!v->adotabpos); - - if (!v->ado) - return 1; - - assert (v->inado); - - for (p = v->ado; (lit = *p); p++) - if (lit->val == UNDEF) - { - u = LIT2VAR (lit); - assert (!u->ado); - u->ado = v->ado; - v->ado = 0; - - return 1; - } - - if (4 * nadotab >= 3 * szadotab) /* at least 75% filled */ - enlarge_adotab (); - - adotabpos = find_ado (v->ado); - ado = *adotabpos; - - if (!ado) - { - nadotab++; - v->adotabpos = adotabpos; - *adotabpos = v->ado; - return 1; - } - - assert (ado != v->ado); - - adoconflict = new_clause (2 * llength (ado), 1); - q = adoconflict->lits; - - for (p = ado; (lit = *p); p++) - *q++ = lit->val == FALSE ? lit : NOTLIT (lit); - - for (p = v->ado; (lit = *p); p++) - *q++ = lit->val == FALSE ? lit : NOTLIT (lit); - - assert (q == ENDOFCLS (adoconflict)); - conflict = adoconflict; - adoconflicts++; - return 0; -} - -#endif - -static void -bcp (void) -{ - int props = 0; - assert (!conflict); - - if (mtcls || conflict) - return; - - for (;;) - { - if (ttail2 < thead) /* prioritize implications */ - { - props++; - prop2 (NOTLIT (*ttail2++)); - } - else if (ttail < thead) /* unit clauses or clauses with length > 2 */ - { - if (conflict) break; - propl (NOTLIT (*ttail++)); - if (conflict) break; - } -#ifndef NADC - else if (ttailado < thead) - { - if (conflict) break; - propado (LIT2VAR (*ttailado++)); - if (conflict) break; - } -#endif - else - break; /* all assignments propagated, so break */ - } - - propagations += props; -} - -/* This version of 'drive' is independent of the global variable 'level' and - * thus even works if we resolve ala 'relsat' without driving an assignment. - */ -static unsigned -drive (void) -{ - Var *v, *first, *second; - Lit **p; - - first = 0; - for (p = added; p < ahead; p++) - { - v = LIT2VAR (*p); - if (!first || v->level > first->level) - first = v; - } - - if (!first) - return 0; - - second = 0; - for (p = added; p < ahead; p++) - { - v = LIT2VAR (*p); - - if (v->level == first->level) - continue; - - if (!second || v->level > second->level) - second = v; - } - - if (!second) - return 0; - - return second->level; -} - -#ifdef VISCORES - -static void -viscores (void) -{ - Rnk *p, *eor = rnks + max_var; - char name[100], cmd[200]; - FILE * data; - Flt s; - int i; - - for (p = rnks + 1; p <= eor; p++) - { - s = p->score; - if (s == INFFLT) - continue; - s = mulflt (s, nvinc); - assert (flt2double (s) <= 1.0); - } - - sprintf (name, "/tmp/picosat-viscores/data/%08u", conflicts); - sprintf (cmd, "sort -n|nl>%s", name); - - data = popen (cmd, "w"); - for (p = rnks + 1; p <= eor; p++) - { - s = p->score; - if (s == INFFLT) - continue; - s = mulflt (s, nvinc); - fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - rnks)); - } - fflush (data); - pclose (data); - - for (i = 0; i < 8; i++) - { - sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i); - system (cmd); - } - - fprintf (fviscores, "set title \"%u\"\n", conflicts); - fprintf (fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", max_var); - - for (i = 0; i < 8; i++) - fprintf (fviscores, - ", \"%s.%d\" using 1:2:3 with labels tc lt %d", - name, i, i + 1); - - fputc ('\n', fviscores); - fflush (fviscores); -#ifndef WRITEGIF - usleep (50000); /* refresh rate of 20 Hz */ -#endif -} - -#endif - -static void -crescore (void) -{ - Cls **p, *cls; - Act *a; - Flt factor; - int l = log2flt (cinc); - assert (l > 0); - factor = base2flt (1, -l); - - for (p = lclauses; p != lhead; p++) - { - cls = *p; - - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - assert (cls->learned); - - if (cls->size <= 2) - continue; - - a = CLS2ACT (cls); - *a = mulflt (*a, factor); - } - - cinc = mulflt (cinc, factor); -} - -static void -inc_vinc (void) -{ -#ifdef VISCORES - nvinc = mulflt (nvinc, fvinc); -#endif - vinc = mulflt (vinc, ifvinc); -} - -inline static void -inc_max_var (void) -{ - Lit *lit; - Rnk *r; - Var *v; - - assert (max_var < size_vars); - - max_var++; /* new index of variable */ - assert (max_var); /* no unsigned overflow */ - - if (max_var == size_vars) - enlarge (size_vars + (size_vars + 3) / 4); /* increase by 25% */ - - assert (max_var < size_vars); - - lit = lits + 2 * max_var; - lit[0].val = lit[1].val = UNDEF; - - memset (htps + 2 * max_var, 0, 2 * sizeof *htps); -#ifndef NDSC - memset (dhtps + 2 * max_var, 0, 2 * sizeof *dhtps); -#endif - memset (impls + 2 * max_var, 0, 2 * sizeof *impls); - memset (jwh + 2 * max_var, 0, 2 * sizeof *jwh); - - v = vars + max_var; /* initialize variable components */ - CLR (v); - - r = rnks + max_var; /* initialize rank */ - CLR (r); - - hpush (r); -} - -static void -force (Cls * cls) -{ - Lit ** p, ** eol, * lit, * forced; - Cls * reason; - Var *v; - - forced = 0; - reason = cls; - - eol = end_of_lits (cls); - for (p = cls->lits; p < eol; p++) - { - lit = *p; - if (lit->val == UNDEF) - { - assert (!forced); - forced = lit; -#ifdef NO_BINARY_CLAUSES - if (cls == &impl) - reason = LIT2REASON (NOTLIT (p[p == cls->lits ? 1 : -1])); -#endif - } - else - assert (lit->val == FALSE); - } - -#ifdef NO_BINARY_CLAUSES - if (cls == &impl) - resetimpl (); -#endif - if (!forced) - return; - - assign_forced (forced, reason); - v = LIT2VAR (forced); -} - -static void -inc_lreduce (void) -{ -#ifdef STATS - inclreduces++; -#endif - lreduce *= FREDUCE; - lreduce /= 100; - report (1, '+'); -} - -static void -backtrack (void) -{ - unsigned new_level; - Cls * cls; - - conflicts++; - LOG (fprintf (out, "%sconflict ", prefix); dumpclsnl (conflict)); - - analyze (); - new_level = drive (); - // TODO: why not? assert (new_level != 1 || (ahead - added) == 2); - cls = add_simplified_clause (1); - undo (new_level); - force (cls); - - if ( -#ifndef NFL - !simplifying && -#endif - !--lreduceadjustcnt) - { - lreduceadjustinc *= 15; - lreduceadjustinc /= 10; - lreduceadjustcnt = lreduceadjustinc; - inc_lreduce (); - } - - if (verbosity >= 4 && !(conflicts % 1000)) - report (4, 'C'); -} - -static void -inc_cinc (void) -{ - cinc = mulflt (cinc, fcinc); - if (lcinc < cinc) - crescore (); -} - -static void -incincs (void) -{ - inc_vinc (); - inc_cinc (); -#ifdef VISCORES - viscores (); -#endif -} - -static void -disconnect_clause (Cls * cls) -{ - assert (cls->connected); - - if (cls->size > 2) - { - if (cls->learned) - { - assert (nlclauses > 0); - nlclauses--; - - assert (llits >= cls->size); - llits -= cls->size; - } - else - { - assert (noclauses > 0); - noclauses--; - - assert (olits >= cls->size); - olits -= cls->size; - } - } - -#ifndef NDEBUG - cls->connected = 0; -#endif -} - -static int -clause_is_toplevel_satisfied (Cls * cls) -{ - Lit *lit, **p, **eol = end_of_lits (cls); - Var *v; - - for (p = cls->lits; p < eol; p++) - { - lit = *p; - if (lit->val == TRUE) - { - v = LIT2VAR (lit); - if (!v->level) - return 1; - } - } - - return 0; -} - -static int -collect_clause (Cls * cls) -{ - assert (cls->collect); - cls->collect = 0; - -#ifdef TRACE - assert (!cls->collected); - cls->collected = 1; -#endif - disconnect_clause (cls); - -#ifdef TRACE - if (trace && (!cls->learned || cls->used)) - return 0; -#endif - delete_clause (cls); - - return 1; -} - -static size_t -collect_clauses (void) -{ - Cls *cls, **p, **q, * next; - Lit * lit, * eol; - size_t res; - Var * v; - int i; - - res = current_bytes; - - eol = lits + 2 * max_var + 1; - for (lit = lits + 2; lit <= eol; lit++) - { - for (i = 0; i <= 1; i++) - { - if (i) - { -#ifdef NO_BINARY_CLAUSES - Ltk * lstk = LIT2IMPLS (lit); - Lit ** r, ** s; - r = lstk->start; - for (s = r; s < lstk->start + lstk->count; s++) - { - Lit * other = *s; - Var *v = LIT2VAR (other); - if (v->level || other->val != TRUE) - *r++ = other; - } - lstk->count = r - lstk->start; - continue; -#else - p = LIT2IMPLS (lit); -#endif - } - else - p = LIT2HTPS (lit); - - for (cls = *p; cls; cls = next) - { - q = cls->next; - if (cls->lits[0] != lit) - q++; - - next = *q; - if (cls->collect) - *p = next; - else - p = q; - } - } - } - -#ifndef NDSC - for (lit = lits + 2; lit <= eol; lit++) - { - p = LIT2DHTPS (lit); - while ((cls = *p)) - { - Lit * other = cls->lits[0]; - if (other == lit) - { - q = cls->next + 1; - } - else - { - assert (cls->lits[1] == lit); - q = cls->next; - } - - if (cls->collect) - *p = *q; - else - p = q; - } - } -#endif - - for (v = vars + 1; v <= vars + max_var; v++) - { - cls = v->reason; - if (!cls) - continue; - -#ifdef NO_BINARY_CLAUSES - if (ISLITREASON (cls)) - continue; -#endif - if (cls->collect) - v->reason = 0; - } - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - - if (!cls) - continue; - - if (!cls->collect) - continue; - - if (collect_clause (cls)) - *p = 0; - } - -#ifdef TRACE - if (!trace) -#endif - { - q = oclauses; - for (p = q; p < ohead; p++) - if ((cls = *p)) - *q++ = cls; - ohead = q; - - q = lclauses; - for (p = q; p < lhead; p++) - if ((cls = *p)) - *q++ = cls; - lhead = q; - } - - assert (current_bytes <= res); - res -= current_bytes; - recycled += res; - - LOG (fprintf (out, "%scollected %ld bytes\n", prefix, res)); - - return res; -} - -static int -need_to_reduce (void) -{ - return nlclauses >= reduce_limit_on_lclauses (); -} - -#ifdef NLUBY - -static void -inc_drestart (void) -{ - drestart *= FRESTART; - drestart /= 100; - - if (drestart >= MAXRESTART) - drestart = MAXRESTART; -} - -static void -inc_ddrestart (void) -{ - ddrestart *= FRESTART; - ddrestart /= 100; - - if (ddrestart >= MAXRESTART) - ddrestart = MAXRESTART; -} - -#else - -static int -luby (int i) -{ - int k; - for (k = 1; k < 32; k++) - if (i == (1 << k) - 1) - return 1 << (k - 1); - - for (k = 1;; k++) - if ((1 << (k - 1)) <= i && i < (1 << k) - 1) - return luby (i - (1 << (k-1)) + 1); -} - -#endif - -#ifndef NLUBY -static void -inc_lrestart (int skip) -{ - unsigned delta; - - delta = 100 * luby (++lubycnt); - lrestart = conflicts + delta; - - if (waslubymaxdelta) - report (1, skip ? 'N' : 'R'); - else - report (2, skip ? 'n' : 'r'); - - if (delta > lubymaxdelta) - { - lubymaxdelta = delta; - waslubymaxdelta = 1; - } - else - waslubymaxdelta = 0; -} -#endif - -static void -init_restart (void) -{ -#ifdef NLUBY - /* TODO: why is it better in incremental usage to have smaller initial - * outer restart interval? - */ - ddrestart = calls > 1 ? MINRESTART : 1000; - drestart = MINRESTART; - lrestart = conflicts + drestart; -#else - lubycnt = 0; - lubymaxdelta = 0; - waslubymaxdelta = 0; - inc_lrestart (0); -#endif -} - -static void -restart (void) -{ - int skip; -#ifdef NLUBY - char kind; - int outer; - - inc_drestart (); - outer = (drestart >= ddrestart); - - if (outer) - skip = very_high_agility (); - else - skip = high_agility (); -#else - skip = medium_agility (); -#endif - -#ifdef STATS - if (skip) - skippedrestarts++; -#endif - - assert (conflicts >= lrestart); - - if (!skip) - { - restarts++; - assert (level > 1); - LOG (fprintf (out, "%srestart %u\n", prefix, restarts)); - undo (0); - } - -#ifdef NLUBY - if (outer) - { - kind = skip ? 'N' : 'R'; - inc_ddrestart (); - drestart = MINRESTART; - } - else if (skip) - { - kind = 'n'; - } - else - { - kind = 'r'; - } - - assert (drestart <= MAXRESTART); - lrestart = conflicts + drestart; - assert (lrestart > conflicts); - - report (outer ? 1 : 2, kind); -#else - inc_lrestart (skip); -#endif -} - -inline static void -assign_decision (Lit * lit) -{ - assert (!conflict); - - level++; - - LOG (fprintf (out, "%snew level %u\n", prefix, level)); - LOG (fprintf (out, - "%sassign %d at level %d <= DECISION\n", - prefix, lit2int (lit), level)); - - assign (lit, 0); -} - -#ifndef NFL - -static int -lit_has_binary_clauses (Lit * lit) -{ -#ifdef NO_BINARY_CLAUSES - Ltk* lstk = LIT2IMPLS (lit); - return lstk->count != 0; -#else - return *LIT2IMPLS (lit) != 0; -#endif -} - -static void -flbcp (void) -{ -#ifdef STATS - unsigned long long propagaions_before_bcp = propagations; -#endif - bcp (); -#ifdef STATS - flprops += propagations - propagaions_before_bcp; -#endif -} - -inline static int -cmp_inverse_rnk (Rnk * a, Rnk * b) -{ - return -cmp_rnk (a, b); -} - -inline static Flt -rnk2jwh (Rnk * r) -{ - Flt res, sum, pjwh, njwh; - Lit * plit, * nlit; - - plit = RNK2LIT (r); - nlit = plit + 1; - - pjwh = *LIT2JWH (plit); - njwh = *LIT2JWH (nlit); - - res = mulflt (pjwh, njwh); - - sum = addflt (pjwh, njwh); - sum = mulflt (sum, base2flt (1, -10)); - res = addflt (res, sum); - - return res; -} - -static int -cmp_inverse_jwh_rnk (Rnk * r, Rnk * s) -{ - Flt a = rnk2jwh (r); - Flt b = rnk2jwh (s); - int res = cmpflt (a, b); - - if (res) - return -res; - - return cmp_inverse_rnk (r, s); -} - -static void -faillits (void) -{ - unsigned i, j, old_trail_count, common, saved_count; - unsigned new_saved_size, oldladded = ladded; - unsigned long long limit, delta; - Lit * lit, * other, * pivot; - int new_trail_count; - Rnk * r, ** p, ** q; - Var * v; - - if (heap + 1 >= hhead) - return; - - if (propagations < fllimit) - return; - - flcalls++; -#ifdef STATSA - flrounds++; -#endif - delta = propagations/10; - if (delta >= 100*1000*1000) delta = 100*1000*1000; - else if (delta <= 100*1000) delta = 100*1000; - - limit = propagations + delta; - fllimit = propagations; - - assert (!level); - assert (simplifying); - - if (flcalls <= 1) - sort (Rnk *, cmp_inverse_jwh_rnk, heap + 1, hhead - (heap + 1)); - else - sort (Rnk *, cmp_inverse_rnk, heap + 1, hhead - (heap + 1)); - - i = 1; /* NOTE: heap starts at position '1' */ - - while (propagations < limit) - { - if (heap + i == hhead) - { - if (ladded == oldladded) - break; - - i = 1; -#ifdef STATS - flrounds++; -#endif - oldladded = ladded; - } - - assert (heap + i < hhead); - - r = heap[i++]; - lit = RNK2LIT (r); - - if (lit->val) - continue; - - if (!lit_has_binary_clauses (NOTLIT (lit))) - { -#ifdef STATS - flskipped++; -#endif - continue; - } - -#ifdef STATS - fltried++; -#endif - LOG (fprintf (out, "%strying %d as failed literal\n", - prefix, lit2int (lit))); - - assign_decision (lit); - old_trail_count = thead - trail; - flbcp (); - - if (conflict) - { -EXPLICITLY_FAILED_LITERAL: - LOG (fprintf (out, "%sfound explicitly failed literal %d\n", - prefix, lit2int (lit))); - - failedlits++; - efailedlits++; - - backtrack (); - flbcp (); - - if (!conflict) - continue; - -CONTRADICTION: - assert (!level); - backtrack (); - assert (mtcls); - - goto RETURN; - } - - if (propagations >= limit) - { - undo (0); - break; - } - - lit = NOTLIT (lit); - - if (!lit_has_binary_clauses (NOTLIT (lit))) - { -#ifdef STATS - flskipped++; -#endif - undo (0); - continue; - } - -#ifdef STATS - fltried++; -#endif - LOG (fprintf (out, "%strying %d as failed literals\n", - prefix, lit2int (lit))); - - new_trail_count = thead - trail; - saved_count = new_trail_count - old_trail_count; - - if (saved_count > saved_size) - { - new_saved_size = saved_size ? 2 * saved_size : 1; - while (saved_count > new_saved_size) - new_saved_size *= 2; - - RESIZEN (saved, saved_size, new_saved_size); - saved_size = new_saved_size; - } - - for (j = 0; j < saved_count; j++) - { - other = trail[old_trail_count + j]; - saved[j] = trail[old_trail_count + j]; - } - - undo (0); - - assign_decision (lit); - flbcp (); - - if (conflict) - goto EXPLICITLY_FAILED_LITERAL; - - pivot = (thead - trail <= new_trail_count) ? lit : NOTLIT (lit); - - common = 0; - for (j = 0; j < saved_count; j++) - if ((other = saved[j])->val == TRUE) - saved[common++] = other; - - undo (0); - - LOG (if (common) - fprintf (out, - "%sfound %d literals implied by %d and %d\n", - prefix, common, - lit2int (NOTLIT (lit)), lit2int (lit))); - - for (j = 0; - j < common - /* TODO: For some Velev benchmarks, extracting the common implicit - * failed literals took quite some time. This needs to be fixed by - * a dedicated analyzer. Up to then we bound the number of - * propagations in this loop as well. - */ - && propagations < limit + delta - ; j++) - { - other = saved[j]; - - if (other->val == TRUE) - continue; - - assert (!other->val); - - LOG (fprintf (out, - "%sforcing %d as forced implicitly failed literal\n", - prefix, lit2int (other))); - - assert (pivot != NOTLIT (other)); - assert (pivot != other); - - assign_decision (NOTLIT (other)); - flbcp (); - - assert (level == 1); - - if (conflict) - { - backtrack (); - assert (!level); - } - else - { - assign_decision (pivot); - flbcp (); - - backtrack (); - - if (level) - { - assert (level == 1); - - flbcp (); - - if (conflict) - { - backtrack (); - assert (!level); - } - else - { - assign_decision (NOTLIT (pivot)); - flbcp (); - backtrack (); - - if (level) - { - assert (level == 1); - flbcp (); - - if (!conflict) - { -#ifdef STATS - floopsed++; -#endif - undo (0); - continue; - } - - backtrack (); - } - - assert (!level); - } - - assert (!level); - } - } - assert (!level); - flbcp (); - - failedlits++; - ifailedlits++; - - if (conflict) - goto CONTRADICTION; - } - } - - fllimit += 9 * (propagations - fllimit); /* 10% for failed literals */ - -RETURN: - - /* First flush top level assigned literals. Those are prohibited from - * being pushed up the heap during 'faillits' since 'simplifying' is set. - */ - assert (heap < hhead); - for (p = q = heap + 1; p < hhead; p++) - { - r = *p; - v = vars + (r - rnks); - lit = RNK2LIT (r); - if (lit->val) - r->pos = 0; - else - *q++ = r; - } - - /* Then resort with respect to EVSIDS score and fix positions. - */ - sort (Rnk *, cmp_inverse_rnk, heap + 1, hhead - (heap + 1)); - for (p = heap + 1; p < hhead; p++) - (*p)->pos = p - heap; -} - -#endif - -static void -simplify (void) -{ - unsigned collect, delta; - size_t bytes_collected; - Cls **p, *cls; - - assert (!mtcls); - assert (!satisfied ()); - assert (lsimplify <= propagations); - assert (fsimplify <= fixed); - -#ifndef NFL - if (level) - undo (0); - - simplifying = 1; - faillits (); - simplifying = 0; - - if (mtcls) - return; -#endif - - collect = 0; - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - - if (cls->locked) - continue; - - assert (!cls->collect); - if (clause_is_toplevel_satisfied (cls)) - { - mark_clause_to_be_collected (cls); - collect++; - } - } - - if (collect) - { - bytes_collected = collect_clauses (); -#ifdef STATS - srecycled += bytes_collected; -#endif - } - - delta = 10 * (olits + llits) + 100000; - if (delta > 2000000) - delta = 2000000; - lsimplify = propagations + delta; - fsimplify = fixed; - simps++; - - report (1, 's'); -} - -static void -iteration (void) -{ - assert (!level); - assert (bcp_queue_is_empty ()); - assert (isimplify < fixed); - - iterations++; - report (2, 'i'); -#ifdef NLUBY - drestart = MINRESTART; - lrestart = conflicts + drestart; -#else - init_restart (); -#endif - isimplify = fixed; -} - -static int -cmp_activity (Cls * c, Cls * d) -{ - Act a; - Act b; - - assert (c->learned); - assert (d->learned); - - a = *CLS2ACT (c); - b = *CLS2ACT (d); - - if (a < b) - return -1; - - if (b < a) - return 1; - - /* Prefer shorter clauses. - */ - if (c->size < d->size) - return 1; - - if (c->size > d->size) - return -1; - - return 0; -} - -static void -reduce (unsigned percentage) -{ - unsigned rcount, lcollect, collect, target, ld; - size_t bytes_collected; - Cls **p, *cls; - Act minact; - - lastreduceconflicts = conflicts; - - assert (percentage <= 100); - LOG (fprintf (out, - "%sreducing %u%% learned clauses\n", - prefix, percentage)); - - while (nlclauses - llocked > (unsigned)(eor - resolved)) - ENLARGE (resolved, rhead, eor); - - collect = 0; - lcollect = 0; - - for (p = ((fsimplify < fixed) ? SOC : lclauses); p != EOC; p = NXC (p)) - { - cls = *p; - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - - if (cls->locked) - continue; - - assert (!cls->collect); - if (fsimplify < fixed && clause_is_toplevel_satisfied (cls)) - { - mark_clause_to_be_collected (cls); - collect++; - - if (cls->learned && cls->size > 2) - lcollect++; - - continue; - } - - if (cls->fixed) - continue; - - if (!cls->learned) - continue; - - if (cls->size <= 2) - continue; - - assert (rhead < eor); - *rhead++ = cls; - } - assert (rhead <= eor); - - fsimplify = fixed; - - rcount = rhead - resolved; - sort (Cls *, cmp_activity, resolved, rcount); - - assert (nlclauses >= lcollect); - target = nlclauses - lcollect + 1; - - for (ld = 1; ld < 32 && ((unsigned) (1 << ld)) < target; ld++) - ; - minact = mulflt (cinc, base2flt (1, -ld)); - - target = (percentage * target + 99) / 100; - - if (target >= rcount) - { - target = rcount; - } - else if (*CLS2ACT (resolved[target]) < minact) - { - /* If the distribution of clause activities is skewed and the median - * is actually below the maximum average activity, then we collect all - * clauses below this activity. - */ - while (++target < rcount && *CLS2ACT (resolved[target]) < minact) - ; - } - else - { - while (target > 0 && - !cmp_activity (resolved[target - 1], resolved[target])) - target--; - } - - rhead = resolved + target; - while (rhead > resolved) - { - cls = *--rhead; - mark_clause_to_be_collected (cls); - - collect++; - if (cls->learned && cls->size > 2) /* just for consistency */ - lcollect++; - } - - if (collect) - { - reductions++; - bytes_collected = collect_clauses (); -#ifdef STATS - rrecycled += bytes_collected; -#endif - report (2, '-'); - } - - if (!lcollect) - inc_lreduce (); /* avoid dead lock */ - - assert (rhead == resolved); -} - -static void -init_reduce (void) -{ - lreduce = loadded / 2; - - if (lreduce < 100) - lreduce = 100; - -#if 0 - if (lreduce > 10000) - lreduce = 10000; -#endif - - if (verbosity) - fprintf (out, - "%s\n%sinitial reduction limit %u clauses\n%s\n", - prefix, prefix, lreduce, prefix); -} - -static unsigned -rng (void) -{ - unsigned res = srng; - srng *= 1664525u; - srng += 1013904223u; - NOLOG (fprintf (out, "%srng () = %u\n", prefix, res)); - return res; -} - -static unsigned -rrng (unsigned low, unsigned high) -{ - unsigned long long tmp; - unsigned res, elements; - assert (low <= high); - elements = high - low + 1; - tmp = rng (); - tmp *= elements; - tmp >>= 32; - tmp += low; - res = tmp; - NOLOG (fprintf (out, "%srrng (%u, %u) = %u\n", prefix, low, high, res)); - assert (low <= res); - assert (res <= high); - return res; -} - -static Lit * -decide_phase (Lit * lit) -{ - Lit * not_lit = NOTLIT (lit); - Var *v = LIT2VAR (lit); - - assert (LIT2SGN (lit) > 0); - if (!v->assigned) - { -#ifdef STATS - staticphasedecisions++; -#endif - if (defaultphase == 1) - { - /* assign to TRUE */ - } - else if (defaultphase == 0) - { - /* assign to FALSE */ - lit = not_lit; - } - else if (defaultphase == 3) - { - /* randomly assign default phase */ - if (rrng (1, 2) != 2) - lit = not_lit; - } - else if (*LIT2JWH(lit) <= *LIT2JWH (not_lit)) - { - /* assign to FALSE (Jeroslow-Wang says there are more short - * clauses with negative occurence of this variable, so satisfy - * those, to minimize BCP) - */ - lit = not_lit; - } - else - { - /* assign to TRUE (... but strictly more positive occurrences) */ - } - } - else - { - /* repeat last phase: phase saving heuristic */ - - if (v->phase) - { - /* assign to TRUE (last phase was TRUE as well) */ - } - else - { - /* assign to FALSE (last phase was FALSE as well) */ - lit = not_lit; - } - } - - return lit; -} - -static unsigned -gcd (unsigned a, unsigned b) -{ - unsigned tmp; - - assert (a); - assert (b); - - if (a < b) - { - tmp = a; - a = b; - b = tmp; - } - - while (b) - { - assert (a >= b); - tmp = b; - b = a % b; - a = tmp; - } - - return a; -} - -static Lit * -rdecide (void) -{ - unsigned idx, delta, spread; - Lit * res; - - spread = RDECIDE; - if (rrng (1, spread) != 2) - return 0; - - assert (1 <= max_var); - idx = rrng (1, max_var); - res = int2lit (idx); - - if (res->val != UNDEF) - { - delta = rrng (1, max_var); - while (gcd (delta, max_var) != 1) - delta--; - - assert (1 <= delta); - assert (delta <= max_var); - - do { - idx += delta; - if (idx > max_var) - idx -= max_var; - res = int2lit (idx); - } while (res->val != UNDEF); - } - -#ifdef STATS - rdecisions++; -#endif - res = decide_phase (res); - LOG (fprintf (out, "%srdecide %d\n", prefix, lit2int (res))); - - return res; -} - -static Lit * -sdecide (void) -{ - Rnk *r, * tmp; - Lit *res; - - for (;;) - { - r = htop (); - res = RNK2LIT (r); - if (res->val == UNDEF) break; - tmp = hpop (); - assert (tmp == r); - NOLOG (fprintf (out, - "%shpop %u %u %u\n", - prefix, r - rnks, - FLTMANTISSA(r->score), - FLTEXPONENT(r->score))); - } - -#ifdef STATS - sdecisions++; -#endif - res = decide_phase (res); - - LOG (fprintf (out, "%ssdecide %d\n", prefix, lit2int (res))); - - return res; -} - -static Lit * -adecide (void) -{ - Lit *lit; - Var * v; - - assert (als < alshead); - assert (!failed_assumption); - - while (alstail < alshead) - { - lit = *alstail++; - - if (lit->val == FALSE) - { - failed_assumption = lit; - v = LIT2VAR (lit); - - use_var (v); - - LOG (fprintf (out, "%sfirst failed assumption %d\n", - prefix, lit2int (failed_assumption))); - fanalyze (); - return 0; - } - - if (lit->val == TRUE) - { - v = LIT2VAR (lit); - if (v->level > adecidelevel) - adecidelevel = v->level; - continue; - } - -#ifdef STATS - assumptions++; -#endif - LOG (fprintf (out, "%sadecide %d\n", prefix, lit2int (lit))); - adecidelevel = level + 1; - - return lit; - } - - return 0; -} - -static void -decide (void) -{ - Lit * lit; - - assert (!satisfied ()); - assert (!conflict); - - if (alstail < alshead && (lit = adecide ())) - ; - else if (failed_assumption) - return; - else if (satisfied ()) - return; - else if (!(lit = rdecide ())) - lit = sdecide (); - - assert (lit); - assign_decision (lit); - - levelsum += level; - decisions++; -} - -static int -sat (int l) -{ - int count = 0, backtracked; - - if (!conflict) - bcp (); - - if (conflict) - backtrack (); - - if (mtcls) - return PICOSAT_UNSATISFIABLE; - - if (satisfied ()) - goto SATISFIED; - - if (lsimplify <= propagations) - simplify (); - - if (mtcls) - return PICOSAT_UNSATISFIABLE; - - if (satisfied ()) - goto SATISFIED; - - init_restart (); - - isimplify = fixed; - backtracked = 0; - - for (;;) - { - if (!conflict) - bcp (); - - if (conflict) - { - incincs (); - backtrack (); - - if (mtcls) - return PICOSAT_UNSATISFIABLE; - backtracked = 1; - continue; - } - - if (satisfied ()) - { -SATISFIED: -#ifndef NDEBUG - original_clauses_satisfied (); - assumptions_satisfied (); -#endif - return PICOSAT_SATISFIABLE; - } - - if (backtracked) - { - backtracked = 0; - if (!level && isimplify < fixed) - iteration (); - } - - if (l >= 0 && count >= l) /* decision limit reached ? */ - return PICOSAT_UNKNOWN; - - if (propagations >= lpropagations)/* propagation limit reached ? */ - return PICOSAT_UNKNOWN; - -#ifndef NADC - if (!adodisabled && adoconflicts >= adoconflictlimit) - { - assert (bcp_queue_is_empty ()); - return PICOSAT_UNKNOWN; - } -#endif - - if (fsimplify < fixed && lsimplify <= propagations) - { - simplify (); - if (!bcp_queue_is_empty ()) - continue; -#ifndef NFL - if (mtcls) - return PICOSAT_UNSATISFIABLE; - - if (satisfied ()) - return PICOSAT_SATISFIABLE; - - assert (!level); -#endif - } - - if (!lreduce) - init_reduce (); - - if (need_to_reduce ()) - reduce (50); - - if (conflicts >= lrestart && level > 2) - restart (); - - decide (); - if (failed_assumption) - return PICOSAT_UNSATISFIABLE; - count++; - } -} - -static void -rebias (void) -{ - Cls ** p, * c; - Var * v; - - for (v = vars + 1; v <= vars + max_var; v++) - v->assigned = 0; - - memset (jwh, 0, 2 * (max_var + 1) * sizeof *jwh); - - for (p = oclauses; p < ohead; p++) - { - c = *p; - - if (!c) - continue; - - if (c->learned) - continue; - - incjwh (c); - } -} - -#ifdef TRACE - -static unsigned -core (void) -{ - unsigned idx, prev, this, delta, i, lcore, vcore; - unsigned *stack, *shead, *eos; - Lit **q, **eol, *lit; - Cls *cls, *reason; - Znt *p, byte; - Zhn *zhain; - Var *v; - - assert (trace); - - assert (mtcls || failed_assumption); - if (ocore >= 0) - return ocore; - - lcore = ocore = vcore = 0; - - stack = shead = eos = 0; - ENLARGE (stack, shead, eos); - - if (mtcls) - { - idx = CLS2IDX (mtcls); - *shead++ = idx; - } - else - { - assert (failed_assumption); - v = LIT2VAR (failed_assumption); - reason = v->reason; - assert (reason); - idx = CLS2IDX (reason); - *shead++ = idx; - } - - while (shead > stack) - { - idx = *--shead; - zhain = IDX2ZHN (idx); - - if (zhain) - { - if (zhain->core) - continue; - - zhain->core = 1; - lcore++; - - cls = IDX2CLS (idx); - if (cls) - { - assert (!cls->core); - cls->core = 1; - } - - i = 0; - delta = 0; - prev = 0; - for (p = zhain->znt; (byte = *p); p++, i += 7) - { - delta |= (byte & 0x7f) << i; - if (byte & 0x80) - continue; - - this = prev + delta; - assert (prev < this); /* no overflow */ - - if (shead == eos) - ENLARGE (stack, shead, eos); - *shead++ = this; - - prev = this; - delta = 0; - i = -7; - } - } - else - { - cls = IDX2CLS (idx); - - assert (cls); - assert (!cls->learned); - - if (cls->core) - continue; - - cls->core = 1; - ocore++; - - eol = end_of_lits (cls); - for (q = cls->lits; q < eol; q++) - { - lit = *q; - v = LIT2VAR (lit); - if (v->core) - continue; - - v->core = 1; - vcore++; - - if (!failed_assumption) continue; - if (lit != failed_assumption) continue; - - reason = v->reason; - if (!reason) continue; - if (reason->core) continue; - - idx = CLS2IDX (reason); - if (shead == eos) - ENLARGE (stack, shead, eos); - *shead++ = idx; - } - } - } - - DELETEN (stack, eos - stack); - - if (verbosity) - fprintf (out, - "%s%u core variables out of %u (%.1f%%)\n" - "%s%u core original clauses out of %u (%.1f%%)\n" - "%s%u core learned clauses out of %u (%.1f%%)\n", - prefix, vcore, max_var, PERCENT (vcore, max_var), - prefix, ocore, oadded, PERCENT (ocore, oadded), - prefix, lcore, ladded, PERCENT (lcore, ladded)); - - return ocore; -} - -static void -write_unsigned (unsigned d, FILE * file) -{ - static char write_unsigned_buffer[20]; - unsigned tmp; - char * res; - - assert (sizeof d <= 4); - - res = write_unsigned_buffer + sizeof write_unsigned_buffer; - *--res = 0; - tmp = d; - do { - assert (res > write_unsigned_buffer); - *--res = '0' + (tmp % 10); - tmp /= 10; - } while (tmp); - - fputs (res, file); -} - -static void -trace_lits (Cls * cls, FILE * file) -{ - Lit **p, **eol = end_of_lits (cls); - - assert (cls); - assert (cls->core); - - for (p = cls->lits; p < eol; p++) - { - write_int (LIT2INT (*p), file); - fputc (' ', file); - } - - fputc ('0', file); -} - -static void -write_idx (unsigned idx, FILE * file) -{ - write_unsigned (EXPORTIDX (idx), file); -} - -static void -trace_clause (unsigned idx, Cls * cls, FILE * file, int fmt) -{ - assert (cls); - assert (cls->core); - assert (fmt == RUP_TRACE_FMT || !cls->learned); - assert (CLS2IDX (cls) == idx); - - if (fmt != RUP_TRACE_FMT) - { - write_idx (idx, file); - fputc (' ', file); - } - - trace_lits (cls, file); - - if (fmt != RUP_TRACE_FMT) - fputs (" 0", file); - - fputc ('\n', file); -} - -static void -trace_zhain (unsigned idx, Zhn * zhain, FILE * file, int fmt) -{ - unsigned prev, this, delta, i; - Znt *p, byte; - Cls * cls; - - assert (zhain); - assert (zhain->core); - - write_idx (idx, file); - fputc (' ', file); - - if (fmt == EXTENDED_TRACECHECK_TRACE_FMT) - { - cls = IDX2CLS (idx); - assert (cls); - trace_lits (cls, file); - } - else - { - assert (fmt == COMPACT_TRACECHECK_TRACE_FMT); - putc ('*', file); - } - - i = 0; - delta = 0; - prev = 0; - - for (p = zhain->znt; (byte = *p); p++, i += 7) - { - delta |= (byte & 0x7f) << i; - if (byte & 0x80) - continue; - - this = prev + delta; - - putc (' ', file); - write_idx (this, file); - - prev = this; - delta = 0; - i = -7; - } - - fputs (" 0\n", file); -} - -static void -write_core (FILE * file) -{ - Lit **q, **eol; - Cls **p, *cls; - - fprintf (file, "p cnf %u %u\n", max_var, core ()); - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - - if (!cls || cls->learned || !cls->core) - continue; - - eol = end_of_lits (cls); - for (q = cls->lits; q < eol; q++) - { - write_int (LIT2INT (*q), file); - fputc (' ', file); - } - - fputs ("0\n", file); - } -} - -#endif - -static void -write_trace (FILE * file, int fmt) -{ -#ifdef TRACE - Cls *cls, ** p; - Zhn *zhain; - unsigned i; - - core (); - - if (fmt == RUP_TRACE_FMT) - { - rupvariables = picosat_variables (), - rupclauses = picosat_added_original_clauses (); - write_rup_header (file); - } - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - - if (oclauses <= p && p < eoo) - { - i = OIDX2IDX (p - oclauses); - assert (!cls || CLS2IDX (cls) == i); - } - else - { - assert (lclauses <= p && p < eol); - i = LIDX2IDX (p - lclauses); - } - - zhain = IDX2ZHN (i); - - if (zhain) - { - if (zhain->core) - { - if (fmt == RUP_TRACE_FMT) - trace_clause (i, cls, file, fmt); - else - trace_zhain (i, zhain, file, fmt); - } - } - else if (cls) - { - if (fmt != RUP_TRACE_FMT && cls) - { - if (cls->core) - trace_clause (i, cls, file, fmt); - } - } - } -#else - (void) file; - (void) fmt; -#endif -} - -static void -write_core_wrapper (FILE * file, int fmt) -{ - (void) fmt; -#ifdef TRACE - write_core (file); -#else - (void) file; -#endif -} - -static Lit * -import_lit (int lit) -{ - ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal"); - - while (abs (lit) > (int) max_var) - inc_max_var (); - - return int2lit (lit); -} - -#ifdef TRACE -static void -reset_core (void) -{ - Cls ** p, * c; - Zhn ** q, * z; - unsigned i; - - for (i = 1; i <= max_var; i++) - vars[i].core = 0; - - for (p = SOC; p != EOC; p = NXC (p)) - if ((c = *p)) - c->core = 0; - - for (q = zhains; q != zhead; q++) - if ((z = *q)) - z->core = 0; - - ocore = -1; -} -#endif - -static void -reset_assumptions (void) -{ - Lit ** p; - - failed_assumption = 0; - - if (extracted_all_failed_assumptions) - { - for (p = als; p < alshead; p++) - LIT2VAR (*p)->failed = 0; - - extracted_all_failed_assumptions = 0; - } - - alstail = alshead = als; - adecidelevel = 0; -} - -static void -check_ready (void) -{ - ABORTIF (state == RESET, "API usage: uninitialized"); -} - -static void -check_sat_state (void) -{ - ABORTIF (state != SAT, "API usage: expected to be in SAT state"); -} - -static void -check_unsat_state (void) -{ - ABORTIF (state != UNSAT, "API usage: expected to be in UNSAT state"); -} - -static void -check_sat_or_unsat_or_unknown_state (void) -{ - ABORTIF (state != SAT && state != UNSAT && state != UNKNOWN, - "API usage: expected to be in SAT, UNSAT, or UNKNOWN state"); -} - -static void -reset_incremental_usage (void) -{ - unsigned num_non_false; - Lit * lit, ** q; - - check_sat_or_unsat_or_unknown_state (); - - LOG (fprintf (out, "%sRESET incremental usage\n", prefix)); - - if (level) - undo (0); - - reset_assumptions (); - - if (conflict) - { - num_non_false = 0; - for (q = conflict->lits; q < end_of_lits (conflict); q++) - { - lit = *q; - if (lit->val != FALSE) - num_non_false++; - } - - // assert (num_non_false >= 2); // TODO: why this assertion? -#ifdef NO_BINARY_CLAUSES - if (conflict == &cimpl) - resetcimpl (); -#endif -#ifndef NADC - if (conflict == adoconflict) - resetadoconflict (); -#endif - conflict = 0; - } - -#ifdef TRACE - reset_core (); -#endif - - saved_flips = flips; - min_flipped = UINT_MAX; - saved_max_var = max_var; - - state = READY; -} - -static void -enter (void) -{ - if (nentered++) - return; - - check_ready (); - entered = picosat_time_stamp (); -} - -static void -leave (void) -{ - assert (nentered); - if (--nentered) - return; - - sflush (); -} - -static void -check_trace_support_and_execute (FILE * file, void (*f)(FILE*,int), int fmt) -{ - check_ready (); - check_unsat_state (); -#ifdef TRACE - ABORTIF (!trace, "API usage: tracing disabled"); - enter (); - f (file, fmt); - leave (); -#else - (void) file; - (void) fmt; - (void) f; - ABORT ("compiled without trace support"); -#endif -} - -static void -extract_all_failed_assumptions (void) -{ - Lit ** p, ** eol; - Var * v, * u; - int pos; - Cls * c; - - assert (!extracted_all_failed_assumptions); - - assert (failed_assumption); - assert (mhead == marked); - - if (marked == eom) - ENLARGE (marked, mhead, eom); - - v = LIT2VAR (failed_assumption); - mark_var (v); - pos = 0; - - while (pos < mhead - marked) - { - v = marked[pos++]; - assert (v->mark); - c = var2reason (v); - if (!c) - continue; - eol = end_of_lits (c); - for (p = c->lits; p < eol; p++) - { - u = LIT2VAR (*p); - if (!u->mark) - mark_var (u); - } - } - - for (p = als; p < alshead; p++) - { - u = LIT2VAR (*p); - if (!u->mark) continue; - u->failed = 1; - LOG (fprintf (out, "%sfailed assumption %d\n", prefix, lit2int (*p))); - } - - while (mhead > marked) - (*--mhead)->mark = 0; - - extracted_all_failed_assumptions = 1; -} - -const char * -picosat_copyright (void) -{ - return "Copyright (c) 2006 - 2010 Armin Biere JKU Linz"; -} - -void -picosat_init (void) -{ - init (); -} - -void -picosat_adjust (int new_max_var) -{ - unsigned new_size_vars; - - enter (); - - new_max_var = abs (new_max_var); - new_size_vars = new_max_var + 1; - - if (size_vars < new_size_vars) - enlarge (new_size_vars); - - while (max_var < (unsigned) new_max_var) - inc_max_var (); - - leave (); -} - -int -picosat_inc_max_var (void) -{ - if (measurealltimeinlib) - enter (); - else - check_ready (); - - inc_max_var (); - - if (measurealltimeinlib) - leave (); - - return max_var; -} - -void -picosat_set_verbosity (int new_verbosity_level) -{ - check_ready (); - verbosity = new_verbosity_level; -} - -int -picosat_enable_trace_generation (void) -{ - int res = 0; - check_ready (); -#ifdef TRACE - ABORTIF (addedclauses, - "API usage: trace generation enabled after adding clauses"); - res = trace = 1; -#endif - return res; -} - -void -picosat_set_incremental_rup_file (FILE * rup_file, int m, int n) -{ - check_ready (); - assert (!rupstarted); - rup = rup_file; - rupvariables = m; - rupclauses = n; -} - -void -picosat_set_output (FILE * output_file) -{ - check_ready (); - out = output_file; -} - -void -picosat_measure_all_calls (void) -{ - check_ready (); - measurealltimeinlib = 1; -} - -void -picosat_set_prefix (const char * str) -{ - check_ready (); - new_prefix (str); -} - -void -picosat_set_seed (unsigned s) -{ - check_ready (); - srng = s; -} - -void -picosat_reset (void) -{ - check_ready (); - reset (); -} - -int -picosat_add (int int_lit) -{ - int res = oadded; - Lit *lit; - - if (measurealltimeinlib) - enter (); - else - check_ready (); - - ABORTIF (rup && rupstarted && oadded >= (unsigned)rupclauses, - "API usage: adding too many clauses after RUP header written"); -#ifndef NADC - ABORTIF (addingtoado, - "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed"); -#endif - if (state != READY) - reset_incremental_usage (); - - lit = import_lit (int_lit); - - if (int_lit) - add_lit (lit); - else - simplify_and_add_original_clause (); - - if (measurealltimeinlib) - leave (); - - return res; -} - -void -picosat_add_ado_lit (int external_lit) -{ -#ifndef NADC - Lit * internal_lit; - - if (measurealltimeinlib) - enter (); - else - check_ready (); - - if (state != READY) - reset_incremental_usage (); - - ABORTIF (!addingtoado && ahead > added, - "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed"); - - if (external_lit) - { - addingtoado = 1; - internal_lit = import_lit (external_lit); - add_lit (internal_lit); - } - else - { - addingtoado = 0; - add_ado (); - } - if (measurealltimeinlib) - leave (); -#else - (void) external_lit; - ABORT ("compiled without all different constraint support"); -#endif -} - -void -picosat_assume (int int_lit) -{ - Lit *lit; - - if (measurealltimeinlib) - enter (); - else - check_ready (); - - if (state != READY) - reset_incremental_usage (); - - lit = import_lit (int_lit); - if (alshead == eoals) - { - assert (alstail == als); - ENLARGE (als, alshead, eoals); - alstail = als; - } - - *alshead++ = lit; - LOG (fprintf (out, "%sassumption %d\n", prefix, int_lit)); - - if (measurealltimeinlib) - leave (); -} - -int -picosat_sat (int l) -{ - int res; - char ch; - - enter (); - - calls++; - LOG (fprintf (out, "%sSTART call %u\n", prefix, calls)); - - if (added < ahead) - { -#ifndef NADC - if (addingtoado) - ABORT ("API usage: incomplete all different constraint"); - else -#endif - ABORT ("API usage: incomplete clause"); - } - - if (state != READY) - reset_incremental_usage (); - - res = sat (l); - - assert (state == READY); - - switch (res) - { - case PICOSAT_UNSATISFIABLE: - ch = '0'; - state = UNSAT; - break; - case PICOSAT_SATISFIABLE: - ch = '1'; - state = SAT; - break; - default: - ch = '?'; - state = UNKNOWN; - break; - } - - if (verbosity) - { - report (1, ch); - rheader (); - } - - leave (); - LOG (fprintf (out, "%sEND call %u\n", prefix, calls)); - - last_sat_call_result = res; - - return res; -} - -int -picosat_res (void) -{ - return last_sat_call_result; -} - -int -picosat_deref (int int_lit) -{ - Lit *lit; - - check_ready (); - check_sat_state (); - ABORTIF (!int_lit, "API usage: can not deref zero literal"); - ABORTIF (mtcls, "API usage: deref after empty clause generated"); - -#ifdef STATS - derefs++; -#endif - - if (abs (int_lit) > (int) max_var) - return 0; - - lit = int2lit (int_lit); - - if (lit->val == TRUE) - return 1; - - if (lit->val == FALSE) - return -1; - - return 0; -} - -int -picosat_deref_toplevel (int int_lit) -{ - Lit *lit; - Var * v; - - check_ready (); - ABORTIF (!int_lit, "API usage: can not deref zero literal"); - ABORTIF (mtcls, "API usage: deref after empty clause generated"); - -#ifdef STATS - derefs++; -#endif - if (abs (int_lit) > (int) max_var) - return 0; - - lit = int2lit (int_lit); - - v = LIT2VAR (lit); - if (v->level > 0) - return 0; - - if (lit->val == TRUE) - return 1; - - if (lit->val == FALSE) - return -1; - - return 0; -} - -int -picosat_inconsistent (void) -{ - check_ready (); - return mtcls != 0; -} - -int -picosat_corelit (int int_lit) -{ - int res; - - check_ready (); - check_unsat_state (); - ABORTIF (!int_lit, "API usage: zero literal can not be in core"); - - assert (mtcls || failed_assumption); - - res = 0; - -#ifdef TRACE - { - ABORTIF (!trace, "tracing disabled"); - if (measurealltimeinlib) - enter (); - core (); - if (abs (int_lit) <= (int) max_var) - res = vars[abs (int_lit)].core; - assert (!res || failed_assumption || vars[abs (int_lit)].used); - if (measurealltimeinlib) - leave (); - } -#else - ABORT ("compiled without trace support"); -#endif - - return res; -} - -int -picosat_coreclause (int ocls) -{ - int res; - - check_ready (); - check_unsat_state (); - - ABORTIF (ocls < 0, "API usage: negative original clause index"); - ABORTIF (ocls >= (int)oadded, "API usage: original clause index exceeded"); - - assert (mtcls || failed_assumption); - - res = 0; - -#ifdef TRACE - { - Cls ** clsptr, * cls; - - ABORTIF (!trace, "tracing disabled"); - if (measurealltimeinlib) - enter (); - core (); - clsptr = oclauses + ocls; - assert (clsptr < ohead); - cls = *clsptr; - if (cls) - res = cls->core; - if (measurealltimeinlib) - leave (); - } -#else - ABORT ("compiled without trace support"); -#endif - - return res; -} - -int -picosat_failed_assumption (int int_lit) -{ - Lit * lit; - Var * v; - ABORTIF (!int_lit, "API usage: zero literal as assumption"); - check_ready (); - check_unsat_state (); - if (mtcls) - return 0; - assert (failed_assumption); - if (abs (int_lit) > (int) max_var) - return 0; - if (!extracted_all_failed_assumptions) - extract_all_failed_assumptions (); - lit = import_lit (int_lit); - v = LIT2VAR (lit); - return v->failed; -} - -const int * -picosat_failed_assumptions (void) -{ - Lit ** p, * lit; - Var * v; - int ilit; - - falshead = fals; - check_ready (); - check_unsat_state (); - if (!mtcls) - { - assert (failed_assumption); - if (!extracted_all_failed_assumptions) - extract_all_failed_assumptions (); - - for (p = als; p < alshead; p++) - { - lit = *p; - v = LIT2VAR (*p); - if (!v->failed) - continue; - ilit = LIT2INT (lit); - if (falshead == eofals) - ENLARGE (fals, falshead, eofals); - *falshead++ = ilit; - } - } - if (falshead == eofals) - ENLARGE (fals, falshead, eofals); - *falshead++ = 0; - return fals; -} - -static const char * enumstr (int i) { - int last = i % 10; - if (last == 1) return "st"; - if (last == 2) return "nd"; - if (last == 3) return "rd"; - return "th"; -} - -const int * -picosat_mus_assumptions (void * s, void (*cb)(void*,const int*), int fix) -{ - int i, j, ilit, len, oldlen, norig = alshead - als, nwork, * work, res; - signed char * redundant; - Lit ** p, * lit; - int failed; - Var * v; - - check_ready (); - check_unsat_state (); - len = 0; - if (!mtcls) - { - assert (failed_assumption); - if (!extracted_all_failed_assumptions) - extract_all_failed_assumptions (); - - for (p = als; p < alshead; p++) - if (LIT2VAR (*p)->failed) - len++; - } - - if (mass) - DELETEN (mass, szmass); - szmass = len + 1; - NEWN (mass, szmass); - - i = 0; - for (p = als; p < alshead; p++) - { - lit = *p; - v = LIT2VAR (lit); - if (!v->failed) - continue; - ilit = LIT2INT (lit); - assert (i < len); - mass[i++] = ilit; - } - assert (i == len); - mass[i] = 0; - if (verbosity) - fprintf (out, - "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n", - prefix, len, norig, PERCENT (len, norig)); - if (cb) - cb (s, mass); - - nwork = len; - NEWN (work, nwork); - for (i = 0; i < len; i++) - work[i] = mass[i]; - - NEWN (redundant, nwork); - CLRN (redundant, nwork); - - for (i = 0; i < nwork; i++) - { - if (redundant[i]) - continue; - - if (verbosity > 1) - fprintf (out, - "%strying to drop %d%s assumption %d\n", - prefix, i, enumstr (i), work[i]); - for (j = 0; j < nwork; j++) - if (i != j && !redundant[j]) - picosat_assume (work[j]); - - res = picosat_sat (-1); - if (res == 10) - { - if (verbosity > 1) - fprintf (out, - "%sfailed to drop %d%s assumption %d\n", - prefix, i, enumstr (i), work[i]); - - if (fix) - { - picosat_add (work[i]); - picosat_add (0); - } - } - else - { - assert (res == 20); - if (verbosity > 1) - fprintf (out, - "%ssuceeded to drop %d%s assumption %d\n", - prefix, i, enumstr (i), work[i]); - redundant[i] = 1; - for (j = 0; j < nwork; j++) - { - failed = picosat_failed_assumption (work[j]); - if (j <= i) - { - assert (redundant[j] == !failed); - continue; - } - - if (!failed) - { - redundant[j] = -1; - if (verbosity > 1) - fprintf (out, - "%salso suceeded to drop %d%s assumption %d\n", - prefix, j, enumstr (j), work[j]); - } - } - - oldlen = len; - len = 0; - for (j = 0; j < nwork; j++) - if (!redundant[j]) - mass[len++] = work[j]; - mass[len] = 0; - assert (len < oldlen); - - if (fix) - { - picosat_add (-work[i]); - picosat_add (0); - } - -#ifndef NDEBUG - for (j = 0; j <= i; j++) - assert (redundant[j] >= 0); -#endif - for (j = i + 1; j < nwork; j++) - { - if (redundant[j] >= 0) - continue; - - if (fix) - { - picosat_add (-work[j]); - picosat_add (0); - } - - redundant[j] = 1; - } - - if (verbosity) - fprintf (out, - "%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n", - prefix, len, norig, PERCENT (len, norig)); - if (cb) - cb (s, mass); - } - } - - DELETEN (work, nwork); - DELETEN (redundant, nwork); - - if (verbosity) - fprintf (out, "%sreinitializaing unsat state", prefix); - for (i = 0; i < len; i++) - picosat_assume (mass[i]); - res = picosat_sat (-1); - assert (res == 20); - - return mass; -} - -int -picosat_usedlit (int int_lit) -{ - int res; - check_ready (); - check_sat_or_unsat_or_unknown_state (); - ABORTIF (!int_lit, "API usage: zero literal can not be used"); - int_lit = abs (int_lit); - res = (int_lit <= (int) max_var) ? vars[int_lit].used : 0; - return res; -} - -void -picosat_write_clausal_core (FILE * file) -{ - check_trace_support_and_execute (file, write_core_wrapper, 0); -} - -void -picosat_write_compact_trace (FILE * file) -{ - check_trace_support_and_execute (file, write_trace, - COMPACT_TRACECHECK_TRACE_FMT); -} - -void -picosat_write_extended_trace (FILE * file) -{ - check_trace_support_and_execute (file, write_trace, - EXTENDED_TRACECHECK_TRACE_FMT); -} - -void -picosat_write_rup_trace (FILE * file) -{ - check_trace_support_and_execute (file, write_trace, RUP_TRACE_FMT); -} - -size_t -picosat_max_bytes_allocated (void) -{ - check_ready (); - return max_bytes; -} - -void -picosat_set_propagation_limit (unsigned long long l) -{ - lpropagations = l; -} - -unsigned long long -picosat_propagations (void) -{ - return propagations; -} - -int -picosat_variables (void) -{ - check_ready (); - return (int) max_var; -} - -int -picosat_added_original_clauses (void) -{ - check_ready (); - return (int) oadded; -} - -void -picosat_stats (void) -{ - unsigned redlits; -#ifdef STATS - check_ready (); - assert (sdecisions + rdecisions + assumptions == decisions); -#endif - if (calls > 1) - fprintf (out, "%s%u calls\n", prefix, calls); - fprintf (out, "%s%u iterations\n", prefix, iterations); - fprintf (out, "%s%u restarts", prefix, restarts); -#ifdef STATS - fprintf (out, " (%u skipped)", skippedrestarts); -#endif - fputc ('\n', out); -#ifndef NFL - fprintf (out, "%s%u failed literals", prefix, failedlits); -#ifdef STATS - fprintf (out, - ", %u calls, %u rounds, %llu propagations", - flcalls, flrounds, flprops); -#endif - fputc ('\n', out); -#ifdef STATS - fprintf (out, - "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n", - prefix, - ifailedlits, PERCENT (ifailedlits, failedlits), - floopsed, fltried, flskipped); -#endif -#endif - fprintf (out, "%s%u conflicts", prefix, conflicts); -#ifdef STATS - fprintf (out, " (%u uips = %.1f%%)\n", uips, PERCENT(uips,conflicts)); -#else - fputc ('\n', out); -#endif -#ifndef NADC - fprintf (out, "%s%u adc conflicts\n", prefix, adoconflicts); -#endif -#ifdef STATS - fprintf (out, "%s%llu dereferenced literals\n", prefix, derefs); -#endif - fprintf (out, "%s%u decisions", prefix, decisions); -#ifdef STATS - fprintf (out, " (%u random = %.2f%%", - rdecisions, PERCENT (rdecisions, decisions)); - fprintf (out, ", %u assumptions", assumptions); - fputc (')', out); -#endif - fputc ('\n', out); -#ifdef STATS - fprintf (out, - "%s%u static phase decisions (%.1f%% of all variables)\n", - prefix, - staticphasedecisions, PERCENT (staticphasedecisions, max_var)); -#endif - fprintf (out, "%s%u fixed variables\n", prefix, fixed); - assert (nonminimizedllits >= minimizedllits); - redlits = nonminimizedllits - minimizedllits; - fprintf (out, "%s%u learned literals\n", prefix, llitsadded); - fprintf (out, "%s%.1f%% deleted literals\n", - prefix, PERCENT (redlits, nonminimizedllits)); - -#ifdef STATS -#ifndef NO_BINARY_CLAUSES - fprintf (out, - "%s%llu antecedents (%.1f antecedents per clause", - prefix, antecedents, AVERAGE (antecedents, conflicts)); -#endif -#ifdef TRACE - if (trace) - fprintf (out, ", %.1f bytes/antecedent)", AVERAGE (znts, antecedents)); -#endif -#if !defined(NO_BINARY_CLAUSES) || defined(TRACE) - fputs (")\n", out); -#endif - - fprintf (out, "%s%llu propagations (%.1f propagations per decision)\n", - prefix, propagations, AVERAGE (propagations, decisions)); - fprintf (out, "%s%llu visits (%.1f per propagation)\n", - prefix, visits, AVERAGE (visits, propagations)); - fprintf (out, - "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n", - prefix, bvisits, - PERCENT (bvisits, visits), - AVERAGE (bvisits, propagations)); - fprintf (out, - "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n", - prefix, tvisits, - PERCENT (tvisits, visits), - AVERAGE (tvisits, propagations)); - fprintf (out, - "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n", - prefix, lvisits, - PERCENT (lvisits, visits), - AVERAGE (lvisits, propagations)); - fprintf (out, "%s%llu other true (%.1f%% of visited clauses)\n", - prefix, othertrue, PERCENT (othertrue, visits)); - fprintf (out, - "%s%llu other true in binary clauses (%.1f%%)" - ", %llu upper (%.1f%%)\n", - prefix, othertrue2, PERCENT (othertrue2, othertrue), - othertrue2u, PERCENT (othertrue2u, othertrue2)); - fprintf (out, - "%s%llu other true in large clauses (%.1f%%)" - ", %llu upper (%.1f%%)\n", - prefix, othertruel, PERCENT (othertruel, othertrue), - othertruelu, PERCENT (othertruelu, othertruel)); - fprintf (out, "%s%llu ternary and large traversals (%.1f per visit)\n", - prefix, traversals, AVERAGE (traversals, visits)); - fprintf (out, "%s%llu large traversals (%.1f per large visit)\n", - prefix, ltraversals, AVERAGE (ltraversals, lvisits)); - fprintf (out, "%s%llu assignments\n", prefix, assignments); -#else - fprintf (out, "%s%llu propagations\n", prefix, picosat_propagations ()); -#endif - fprintf (out, "%s%.1f%% variables used\n", prefix, PERCENT (vused, max_var)); - - sflush (); - fprintf (out, "%s%.1f seconds in library\n", prefix, seconds); - fprintf (out, "%s%.1f megaprops/second\n", - prefix, AVERAGE (propagations / 1e6f, seconds)); -#ifdef STATS - fprintf (out, "%s%.1f million visits per second\n", - prefix, AVERAGE (visits / 1e6f, seconds)); - fprintf (out, - "%srecycled %.1f MB in %u reductions\n", - prefix, rrecycled / (double) (1 << 20), reductions); - fprintf (out, - "%srecycled %.1f MB in %u simplifications\n", - prefix, srecycled / (double) (1 << 20), simps); -#else - fprintf (out, "%s%u simplifications\n", prefix, simps); - fprintf (out, "%s%u reductions\n", prefix, reductions); - fprintf (out, "%s%.1f MB recycled\n", prefix, recycled / (double) (1 << 20)); -#endif - fprintf (out, "%s%.1f MB maximally allocated\n", - prefix, picosat_max_bytes_allocated () / (double) (1 << 20)); -} - -#ifndef NGETRUSAGE -#include <sys/time.h> -#include <sys/resource.h> -#include <sys/unistd.h> -#endif - -double -picosat_time_stamp (void) -{ - double res = -1; -#ifndef NGETRUSAGE - struct rusage u; - res = 0; - if (!getrusage (RUSAGE_SELF, &u)) - { - res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec; - res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec; - } -#endif - return res; -} - -double -picosat_seconds (void) -{ - check_ready (); - return seconds; -} - -void -picosat_print (FILE * file) -{ -#ifdef NO_BINARY_CLAUSES - Lit * lit, *other, * last; - Ltk * stack; -#endif - Lit **q, **eol; - Cls **p, *cls; - unsigned n; - - if (measurealltimeinlib) - enter (); - else - check_ready (); - - n = 0; - n += alshead - als; - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - n++; - } - -#ifdef NO_BINARY_CLAUSES - last = int2lit (-max_var); - for (lit = int2lit (1); lit <= last; lit++) - { - stack = LIT2IMPLS (lit); - eol = stack->start + stack->count; - for (q = stack->start; q < eol; q++) - if (*q >= lit) - n++; - } -#endif - - fprintf (file, "p cnf %d %u\n", max_var, n); - - for (p = SOC; p != EOC; p = NXC (p)) - { - cls = *p; - if (!cls) - continue; - -#ifdef TRACE - if (cls->collected) - continue; -#endif - - eol = end_of_lits (cls); - for (q = cls->lits; q < eol; q++) - { - write_int (lit2int (*q), file); - fputc (' ', file); - } - - fputs ("0\n", file); - } - -#ifdef NO_BINARY_CLAUSES - last = int2lit (-max_var); - for (lit = int2lit (1); lit <= last; lit++) - { - stack = LIT2IMPLS (lit); - eol = stack->start + stack->count; - for (q = stack->start; q < eol; q++) - if ((other = *q) >= lit) - fprintf (file, "%d %d 0\n", lit2int (lit), lit2int (other)); - } -#endif - - { - Lit **r; - for (r = als; r < alshead; r++) - fprintf (file, "%d 0\n", lit2int (*r)); - } - - fflush (file); - - if (measurealltimeinlib) - leave (); -} - -void -picosat_enter (void) -{ - enter (); -} - -void -picosat_leave (void) -{ - leave (); -} - -void -picosat_message (int level, const char * fmt, ...) -{ - va_list ap; - - if (level > verbosity) - return; - - fputs (prefix, out); - va_start (ap, fmt); - vfprintf (out, fmt, ap); - va_end (ap); - fputc ('\n', out); -} - -int -picosat_changed (void) -{ - int res; - - check_ready (); - check_sat_state (); - - res = (min_flipped <= saved_max_var); - assert (!res || saved_flips != flips); - - return res; -} - -static void -setemgr (void * nmgr) -{ - ABORTIF (emgr && emgr != nmgr, - "API usage: mismatched external memory managers"); - emgr = nmgr; -} - -void -picosat_set_new (void * nmgr, void * (*nnew)(void*,size_t)) -{ - ABORTIF (state != RESET, - "API usage: 'picosat_set_new' after 'picosat_init'"); - enew = nnew; - setemgr (nmgr); -} - -void -picosat_set_resize (void * nmgr, void * (*nresize)(void*,void*,size_t,size_t)) -{ - ABORTIF (state != RESET, - "API usage: 'picosat_set_resize' after 'picosat_init'"); - eresize = nresize; - setemgr (nmgr); -} - -void -picosat_set_delete (void * nmgr, void (*ndelete)(void*,void*,size_t)) -{ - ABORTIF (state != RESET, - "API usage: 'picosat_set_delete' after 'picosat_init'"); - edelete = ndelete; - setemgr (nmgr); -} - -void -picosat_reset_phases (void) -{ - rebias (); -} - -void -picosat_reset_scores (void) -{ - Rnk * r; - hhead = heap + 1; - for (r = rnks + 1; r <= rnks + max_var; r++) - { - CLR (r); - hpush (r); - } -} - -void -picosat_remove_learned (unsigned percentage) -{ - reset_incremental_usage (); - reduce (percentage); -} - -void -picosat_set_global_default_phase (int phase) -{ - check_ready (); - ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' " - "with negative argument"); - ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' " - "with argument > 3"); - defaultphase = phase; -} - -void -picosat_set_default_phase_lit (int int_lit, int phase) -{ - unsigned newphase; - Lit * lit; - Var * v; - - check_ready (); - - lit = import_lit (int_lit); - v = LIT2VAR (lit); - - if (phase) - { - newphase = (int_lit < 0) == (phase < 0); - v->phase = newphase; - v->assigned = 1; - } - else - v->assigned = 0; -} - -void -picosat_set_more_important_lit (int int_lit) -{ - Lit * lit; - Var * v; - Rnk * r; - - check_ready (); - - lit = import_lit (int_lit); - v = LIT2VAR (lit); - r = VAR2RNK (v); - - ABORTIF (r->lessimportant, "can not mark variable more and less important"); - - if (r->moreimportant) - return; - - r->moreimportant = 1; - - if (r->pos) - hup (r); -} - -void -picosat_set_less_important_lit (int int_lit) -{ - Lit * lit; - Var * v; - Rnk * r; - - check_ready (); - - lit = import_lit (int_lit); - v = LIT2VAR (lit); - r = VAR2RNK (v); - - ABORTIF (r->moreimportant, "can not mark variable more and less important"); - - if (r->lessimportant) - return; - - r->lessimportant = 1; - - if (r->pos) - hup (r); -} - -#ifndef NADC - -unsigned -picosat_ado_conflicts (void) -{ - check_ready (); - return adoconflicts; -} - -void -picosat_disable_ado (void) -{ - check_ready (); - assert (!adodisabled); - adodisabled = 1; -} - -void -picosat_enable_ado (void) -{ - check_ready (); - assert (adodisabled); - adodisabled = 0; -} - -void -picosat_set_ado_conflict_limit (unsigned newadoconflictlimit) -{ - check_ready (); - adoconflictlimit = newadoconflictlimit; -} - -#endif - -int -picosat_haveados (void) -{ -#ifndef NADC - return 1; -#else - return 0; -#endif -} diff --git a/src/prop/bvpicosat/picosat.h b/src/prop/bvpicosat/picosat.h deleted file mode 100644 index e2b5f3752..000000000 --- a/src/prop/bvpicosat/picosat.h +++ /dev/null @@ -1,484 +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. -****************************************************************************/ - -#ifdef __cplusplus -extern "C" { -#endif - -#ifndef picosat_h_INCLUDED -#define picosat_h_INCLUDED - -/*------------------------------------------------------------------------*/ - -#include <stdlib.h> -#include <stdio.h> - -/*------------------------------------------------------------------------*/ -/* These are the return values for 'picosat_sat' as for instance - * standardized by the output format of the SAT competition. - */ -#define PICOSAT_UNKNOWN 0 -#define PICOSAT_SATISFIABLE 10 -#define PICOSAT_UNSATISFIABLE 20 - -/*------------------------------------------------------------------------*/ - - - - -const char *picosat_version (void); -const char *picosat_config (void); -const char *picosat_copyright (void); - -/*------------------------------------------------------------------------*/ -/* You can make picosat use an external memory manager instead of the one - * provided by LIBC. But then you need to call these three function before - * 'picosat_init'. The memory manager functions here all have an additional - * first argument which is a pointer to the memory manager, but otherwise - * are supposed to work as their LIBC counter parts 'malloc', 'realloc' and - * 'free'. As exception the 'resize' and 'delete' function have as third - * argument the number of bytes of the block given as second argument. - */ -void picosat_set_new (void * mgr, void * (*)(void *, size_t)); -void picosat_set_resize (void *, void * (*)(void *, void *, size_t, size_t)); -void picosat_set_delete (void *, void (*)(void *, void *, size_t)); - -/*------------------------------------------------------------------------*/ - -void picosat_init (void); /* constructor */ -void picosat_reset (void); /* destructor */ - -/*------------------------------------------------------------------------*/ -/* The following five functions are essentially parameters to 'init', and - * thus should be called right after 'picosat_init' before doing anything - * else. You should not call any of them after adding a literal. - */ - -/* Set output file, default is 'stdout'. - */ -void picosat_set_output (FILE *); - -/* Measure all time spent in all calls in the solver. By default only the - * time spent in 'picosat_sat' is measured. Enabling this function may for - * instance tripple the time needed to add large CNFs, since every call to - * 'picosat_add' will trigger a call to 'getrusage'. - */ -void picosat_measure_all_calls (void); - -/* Set the prefix used for printing verbose messages and statistics. - * Default is "c ". - */ -void picosat_set_prefix (const char *); - -/* The function 'picosat_set_incremental_rup_file' produces - * a proof trace in RUP format on the fly. The resulting RUP file may - * contain learned clauses that are not actual in the clausal core. - */ - -/* Set verbosity level. A verbosity level of 1 and above prints more and - * more detailed progress reports on the output file, set by - * 'picosat_set_output'. Verbose messages are prefixed with the string set - * by 'picosat_set_prefix'. - */ -void picosat_set_verbosity (int new_verbosity_level); - -/* Set default initial phase: - * - * 0 = false - * 1 = true - * 2 = Jeroslow-Wang (default) - * 3 = random initial phase - * - * After a variable has been assigned the first time, it will always - * be assigned the previous value if it is picked as decision variable. - * The initial assignment can be choosen with this function. - */ -void picosat_set_global_default_phase (int); - -/* Set next/initial phase of a particular variable if picked as decision - * variable. Second argument 'phase' has the following meaning: - * - * negative = next value if picked as decision variable is false - * - * positive = next value if picked as decision variable is true - * - * 0 = use global default phase as next value and - * assume 'lit' was never assigned - * - * Again if 'lit' is assigned afterwards through a forced assignment, - * then this forced assignment is the next phase if this variable is - * used as decision variable. - */ -void picosat_set_default_phase_lit (int lit, int phase); - -/* You can reset all phases by the following function. - */ -void picosat_reset_phases (void); - -/* Scores can be erased as well. Not however, that even after erasing - * scores and phases, learned clauses are kept. In addition head tail - * pointers for literals are not moved either. So expect to be a difference - * between calling the solver in incremental mode or with a fresh copy of - * the CNF. - */ -void picosat_reset_scores (void); - -/* Reset assignment if in SAT state and then remove the given percentage of - * less active (large) learned clauses. If you specify 100% all large - * learned clauses are removed. - */ -void picosat_remove_learned (unsigned percentage); - -/* Set some variables to be more important than others. These variables are - * always used as decisions before other variables are used. Dually there - * is a set of variables that is used last. The default is - * to mark all variables as being indifferent only. - */ -void picosat_set_more_important_lit (int lit); -void picosat_set_less_important_lit (int lit); - -/* Allows to print to internal 'out' file from client. - */ -void picosat_message (int verbosity_level, const char * fmt, ...); - -/* Deprecated! - */ -#define picosat_enable_verbosity() picosat_set_verbosity (1) - -/* Set a seed for the random number generator. The random number generator - * is currently just used for generating random decisions. In our - * experiments having random decisions did not really help on industrial - * examples, but was rather helpful to randomize the solver in order to - * do proper benchmarking of different internal parameter sets. - */ -void picosat_set_seed (unsigned random_number_generator_seed); - -/* If you ever want to extract cores or proof traces with the current - * instance of PicoSAT initialized with 'picosat_init', then make sure to - * call 'picosat_enable_trace_generation' right after 'picosat_init'. This - * is not necessary if you only use 'picosat_set_incremental_rup_file'. - * - * NOTE, trace generation code is not necessarily included, e.g. if you - * configure picosat with full optimzation as './configure -O' or with - * './configure --no-trace'. This speeds up the solver slightly. Then you - * you do not get any results by trying to generate traces. - * - * The return value is non-zero if code for generating traces is including - * and it is zero if traces can not be generated. - */ -int picosat_enable_trace_generation (void); - -/* You can dump proof traces in RUP format incrementally even without - * keeping the proof trace in memory. The advantage is a reduction of - * memory usage, but the dumped clauses do not necessarily belong to the - * clausal core. Beside the file the additional parameters denotes the - * maximal number of variables and the number of original clauses. - */ -void picosat_set_incremental_rup_file (FILE * file, int m, int n); - -/*------------------------------------------------------------------------*/ -/* This function returns the next available unused variable index and - * allocates a variable for it even though this variable does not occur as - * assumption, nor in a clause or any other constraints. In future calls to - * 'picosat_sat', 'picosat_deref' and particularly for 'picosat_changed', - * this variable is treated as if it had been used. - */ -int picosat_inc_max_var (void); - -/*------------------------------------------------------------------------*/ -/* If you know a good estimate on how many variables you are going to use - * then calling this function before adding literals will result in less - * resizing of the variable table. But this is just a minor optimization. - * Beside exactly allocating enough variables it has the same effect as - * calling 'picosat_inc_max_var'. - */ -void picosat_adjust (int max_idx); - -/*------------------------------------------------------------------------*/ -/* Statistics. - */ -int picosat_variables (void); /* p cnf <m> n */ -int picosat_added_original_clauses (void); /* p cnf m <n> */ -size_t picosat_max_bytes_allocated (void); -double picosat_time_stamp (void); /* ... in process */ -void picosat_stats (void); /* > output file */ -unsigned long long picosat_propagations (void); /* #propagations */ - -/* The time spent in the library or in 'picosat_sat'. The former is only - * returned if, right after initialization 'picosat_measure_all_calls' - * is called. - */ -double picosat_seconds (void); - -/*------------------------------------------------------------------------*/ -/* Add a literal of the next clause. A zero terminates the clause. The - * solver is incremental. Adding a new literal will reset the previous - * assignment. The return value is the original clause index to which - * this literal respectively the trailing zero belong starting at 0. - */ -int picosat_add (int lit); - -/* Print the CNF to the given file in DIMACS format. - */ -void picosat_print (FILE *); - -/* You can add arbitrary many assumptions before the next 'picosat_sat'. - * This is similar to the using assumptions in MiniSAT, except that you do - * not have to collect all your assumptions yourself. In PicoSAT you can - * add one after the other before the next call to 'picosat_sat'. - * - * These assumptions can be seen as adding unit clauses with those - * assumptions as literals. However these assumption clauses are only valid - * for exactly the next call to 'picosat_sat'. And will be removed - * afterwards, e.g. in future calls to 'picosat_sat' after the next one they - * are not assumed, unless they are assumed again trough 'picosat_assume'. - * - * More precisely, assumptions actually remain valid even after the next - * call to 'picosat_sat' returns. Valid means they remain 'assumed' until a - * call to 'picosat_add', 'picosat_assume', or another 'picosat_sat, - * following the first 'picosat_sat'. They need to stay valid for - * 'picosat_failed_assumption' to return correct values. - * - * Example: - * - * picosat_assume (1); // assume unit clause '1 0' - * picosat_assume (-2); // additionally assume clause '-2 0' - * res = picosat_sat (1000); // assumes 1 and -2 to hold - * // 1000 decisions max. - * - * if (res == PICOSAT_UNSATISFIABLE) - * { - * if (picosat_failed_assumption (1)) - * // unit clause '1 0' was necessary to derive UNSAT - * - * if (picosat_failed_assumption (-2)) - * // unit clause '-2 0' was necessary to derive UNSAT - * - * // at least one but also both could be necessary - * - * picosat_assume (17); // previous assumptions are removed - * // now assume unit clause '17 0' for - * // the next call to 'picosat_sat' - * - * // adding a new clause, actually the first literal of - * // a clause would also make the assumptions used in the previous - * // call to 'picosat_sat' invalid. - * - * // The first two assumptions above are not assumed anymore. Only - * // the assumptions, since the last call to 'picosat_sat' returned - * // are assumed, e.g. the unit clause '17 0'. - * - * res = picosat_sat (-1); - * } - * else if (res == PICOSAT_SATISFIABLE) - * { - * // now the assignment is valid and we can call 'picosat_deref' - * - * assert (picosat_deref (1) == 1)); - * assert (picosat_deref (-2) == 1)); - * - * val = picosat_deref (15); - * - * // previous two assumptions are still valid - * - * // would become invalid if 'picosat_add' or 'picosat_assume' is - * // called here, but we immediately call 'picosat_sat'. Now when - * // entering 'picosat_sat' the solver nows that the previous call - * // returned SAT and it can savely reset the previous assumptions - * - * res = picosat_sat (-1); - * } - * else - * { - * assert (res == PICOSAT_UNKNOWN); - * - * // assumptions valid, but assignment invalid - * // except for top level assigned literals which - * // necessarily need to have this value if the formula is SAT - * - * // as above the solver nows that the previous call returned UNKWOWN - * // and will before doing anything else reset assumptions - * - * picosat_sat (-1); - * } - */ -void picosat_assume (int lit); - -/*------------------------------------------------------------------------*/ -/* This is an experimental feature for handling 'all different constraints' - * (ADC). Currently only one global ADC can be handled. The bit-width of - * all the bit-vectors entered in this ADC (stored in 'all different - * objects' or ADOs) has to be identical. - * - * TODO: also handle top level assigned literals here. - */ -void picosat_add_ado_lit (int); - -/*------------------------------------------------------------------------*/ -/* Call the main SAT routine. A negative decision limit sets no limit on - * the number of decisions. The return values are as above, e.g. - * 'PICOSAT_UNSATISFIABLE', 'PICOSAT_SATISFIABLE', or 'PICOSAT_UNKNOWN'. - */ -int picosat_sat (int decision_limit); - -/* As alternative to a decision limit you can use the number of propagations - * as limit. This is more linearly related to execution time. - */ -void picosat_set_propagation_limit (unsigned long long limit); - -/* Return last result of calling 'picosat_sat' or '0' if not called. - */ -int picosat_res (); - -/* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then - * the satisfying assignment can be obtained by 'dereferencing' literals. - * The value of the literal is return as '1' for 'true', '-1' for 'false' - * and '0' for an unknown value. - */ -int picosat_deref (int lit); - -/* Same as before but just returns true resp. false if the literals is - * forced to this assignment at the top level. This function does not - * require that 'picosat_sat' was called and also does not internally reset - * incremental usage. - */ -int picosat_deref_toplevel (int lit); - -/* Returns non zero if the CNF is unsatisfiable because an empty clause was - * added or derived. - */ -int picosat_inconsistent (void); - -/* Returns non zero if the literal is a failed assumption, which is defined - * as an assumption used to derive unsatisfiability. This is as accurate as - * generating core literals, but still of course is an overapproximation of - * the set of assumptions really necessary. The technique does not need - * clausal core generation nor tracing to be enabled and thus can be much - * more effectice. The function can only be called as long the current - * assumptions are valid. See 'picosat_assume' for more details. - */ -int picosat_failed_assumption (int lit); - -/* Returns a zero terminated list of failed assumption in the last call to - * 'picosat_sat'. The pointer is valid until the next call to - * 'picosat_sat' or 'picosat_failed_assumptions'. It only makes sense if the - * last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'. - */ -const int * picosat_failed_assumptions (void); - -/* Returns a zero terminated minimized list of failed assumption for the last - * call to 'picosat_sat'. The pointer is valid until the next call to this - * function or 'picosat_sat' or 'picosat_mus_assumptions'. It only makes sense - * if the last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'. - * - * The - * call back function is called for all succesful simplification attempts. The - * first argument of the call back function is the state given as first - * argument to 'picosat_mus_assumptions'. The second argument to the call back - * function is the new reduced list of failed assumptions. - * - * This function will call 'picosat_assume' and 'picosat_sat' internally but - * before returning reestablish a proper UNSAT state, e.g. - * 'picosat_failed_assumption' will work afterwards as expected. - * - * The last argument if non zero fixes assumptions. In particular, if an - * assumption can not be removed it is permanently assigned true, otherwise - * if it turns out to be redundant it is permanently assumed to be false. - */ -const int * picosat_mus_assumptions (void *, void(*)(void*,const int*),int); - -/*------------------------------------------------------------------------*/ -/* Assume that a previous call to 'picosat_sat' in incremental usage, - * returned 'SATISFIABLE'. Then a couple of clauses and optionally new - * variables were added (a new variable is a variable that has an index - * larger then the maximum variable added so far). The next call to - * 'picosat_sat' also returns 'SATISFIABLE'. If this function - * 'picosat_changed' returns '0', then the assignment to the old variables - * did not change. Otherwise it may have changed. The return value to - * this function is only valid until new clauses are added through - * 'picosat_add', an assumption is made through 'picosat_assume', or again - * 'picosat_sat' is called. This is the same assumption as for - * 'picosat_deref'. - * - * TODO currently this function may also return a non zero value even if the - * old assignment did not change, because it only checks whether the - * assignment of at least one old variable was flipped at least once during - * the search. In principle it should be possible to be exact in the other - * direcetion as well by using a counter of variables that have an odd - * number of flips. But this is not implemented yet. - */ -int picosat_changed (void); - -/*------------------------------------------------------------------------*/ -/* The following six functions internally extract the variable and clausal - * core and thus require trace generation to be enabled with - * 'picosat_enable_trace_generation' right after calling 'picosat_init'. - * - * TODO: using these functions in incremental mode with failed assumptions - * has only been tested for 'picosat_corelit' thoroughly. The others may - * only work in non-incremental mode or without using 'picosat_assume'. - */ - -/* This function determines whether the i'th added original clause is in the - * core. The 'i' is the return value of 'picosat_add', which starts at zero - * and is incremented by one after a original clause is added (that is after - * 'picosat_add (0)'). For the index 'i' the following has to hold: - * - * 0 <= i < picosat_added_original_clauses () - */ -int picosat_coreclause (int i); - -/* This function gives access to the variable core, which is made up of the - * variables that were resolved in deriving the empty clauses. - */ -int picosat_corelit (int lit); - -/* Write the clauses that were used in deriving the empty clause to a file - * in DIMACS format. - */ -void picosat_write_clausal_core (FILE * core_file); - -/* Write a proof trace in TraceCheck format to a file. - */ -void picosat_write_compact_trace (FILE * trace_file); -void picosat_write_extended_trace (FILE * trace_file); - -/* Write a RUP trace to a file. This trace file contains only the learned - * core clauses while this is not necessarily the case for the RUP file - * obtained with 'picosat_set_incremental_rup_file'. - */ -void picosat_write_rup_trace (FILE * trace_file); - -/*------------------------------------------------------------------------*/ -/* Keeping the proof trace around is not necessary if an over-approximation - * of the core is enough. A literal is 'used' if it was involved in a - * resolution to derive a learned clause. The core literals are necessarily - * a subset of the 'used' literals. - */ - -int picosat_usedlit (int lit); -/*------------------------------------------------------------------------*/ -#endif - -#ifdef __cplusplus -} -#endif /* extern "C" */ diff --git a/src/prop/bvpicosat/version.c b/src/prop/bvpicosat/version.c deleted file mode 100644 index 71c322bd7..000000000 --- a/src/prop/bvpicosat/version.c +++ /dev/null @@ -1,14 +0,0 @@ -#include "config.h" - -const char * -picosat_version (void) -{ - return PICOSAT_VERSION; -} - -const char * -picosat_config (void) -{ - return PICOSAT_CC " " PICOSAT_CFLAGS; -} - diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f2557a303..9f49d81a2 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -68,7 +68,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { } else { Assert(c.size() > 1); NodeBuilder<> b(kind::OR); - for(int i = 0; i < c.size(); ++i) { + for(unsigned i = 0; i < c.size(); ++i) { b << getNode(c[i]); } Node n = b; diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 85e1b9750..9cd0d8848 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -83,9 +83,24 @@ const Lit lit_Error = { -1 }; // } // does enough constant propagation to produce sensible code, and this appears to be somewhat // fragile unfortunately. -#define l_True (Minisat::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants. -#define l_False (Minisat::lbool((uint8_t)1)) -#define l_Undef (Minisat::lbool((uint8_t)2)) +/* + This is to avoid multiple definitions of l_True, l_False and l_Undef if using multiple copies of + Minisat. + IMPORTANT: if we you change the value of the constants so that it is not the same in all copies + of Minisat this breaks! + */ + +#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/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index faf3c67f9..5d8c2850e 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -96,7 +96,7 @@ template<class T> void vec<T>::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 - if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) + if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) throw OutOfMemoryException(); } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 97f5c2265..e9116001f 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -121,7 +121,7 @@ class SimpSolver : public Solver { bool operator()(Var x, Var y) const { int c_x = cost(x); int c_y = cost(y); - return c_x < c_y || c_x == c_y && x < y; } + return c_x < c_y || (c_x == c_y && x < y); } }; struct ClauseDeleted { diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index d2611be94..5e061f2e7 100644 --- a/src/prop/minisat/utils/Options.h +++ b/src/prop/minisat/utils/Options.h @@ -60,7 +60,7 @@ class Option struct OptionLt { bool operator()(const Option* x, const Option* y) { int test1 = strcmp(x->category, y->category); - return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; + return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); } }; diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp index 1c1251545..9391acbe5 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_module.cpp @@ -24,6 +24,13 @@ #include "expr/expr_stream.h" #include "prop/sat.h" +// DPLLT Minisat +#include "prop/minisat/simp/SimpSolver.h" + +// BV Minisat +#include "prop/bvminisat/simp/SimpSolver.h" + + using namespace std; namespace CVC4 { @@ -41,6 +48,10 @@ MinisatSatSolver::MinisatSatSolver() : d_statistics.init(d_minisat); } +MinisatSatSolver::~MinisatSatSolver() { + delete d_minisat; +} + void MinisatSatSolver::addClause(SatClause& clause, bool removable) { Debug("sat::minisat") << "Add clause " << clause <<"\n"; BVMinisat::vec<BVMinisat::Lit> minisat_clause; @@ -173,7 +184,7 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause, for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); } - Assert(clause.size() == minisat_clause.size()); + Assert(clause.size() == (unsigned)minisat_clause.size()); } void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, @@ -181,10 +192,64 @@ void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); } - Assert(clause.size() == sat_clause.size()); + Assert((unsigned)clause.size() == sat_clause.size()); } +// Satistics for MinisatSatSolver + +MinisatSatSolver::Statistics::Statistics() : + d_statStarts("theory::bv::bvminisat::starts"), + d_statDecisions("theory::bv::bvminisat::decisions"), + d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::bvminisat::propagations"), + d_statConflicts("theory::bv::bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::bvminisat::max_literals"), + d_statTotLiterals("theory::bv::bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") +{ + StatisticsRegistry::registerStat(&d_statStarts); + StatisticsRegistry::registerStat(&d_statDecisions); + StatisticsRegistry::registerStat(&d_statRndDecisions); + StatisticsRegistry::registerStat(&d_statPropagations); + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statClausesLiterals); + StatisticsRegistry::registerStat(&d_statLearntsLiterals); + StatisticsRegistry::registerStat(&d_statMaxLiterals); + StatisticsRegistry::registerStat(&d_statTotLiterals); + StatisticsRegistry::registerStat(&d_statEliminatedVars); +} + +MinisatSatSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_statStarts); + StatisticsRegistry::unregisterStat(&d_statDecisions); + StatisticsRegistry::unregisterStat(&d_statRndDecisions); + StatisticsRegistry::unregisterStat(&d_statPropagations); + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statClausesLiterals); + StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); + StatisticsRegistry::unregisterStat(&d_statMaxLiterals); + StatisticsRegistry::unregisterStat(&d_statTotLiterals); + StatisticsRegistry::unregisterStat(&d_statEliminatedVars); +} + +void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ + d_statStarts.setData(minisat->starts); + d_statDecisions.setData(minisat->decisions); + d_statRndDecisions.setData(minisat->rnd_decisions); + d_statPropagations.setData(minisat->propagations); + d_statConflicts.setData(minisat->conflicts); + d_statClausesLiterals.setData(minisat->clauses_literals); + d_statLearntsLiterals.setData(minisat->learnts_literals); + d_statMaxLiterals.setData(minisat->max_literals); + d_statTotLiterals.setData(minisat->tot_literals); + d_statEliminatedVars.setData(minisat->eliminated_vars); +} + + + //// DPllMinisatSatSolver DPLLMinisatSatSolver::DPLLMinisatSatSolver() : @@ -238,7 +303,7 @@ void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); } - Assert(clause.size() == minisat_clause.size()); + Assert(clause.size() == (unsigned)minisat_clause.size()); } void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, @@ -246,7 +311,7 @@ void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); } - Assert(clause.size() == sat_clause.size()); + Assert((unsigned)clause.size() == sat_clause.size()); } @@ -341,6 +406,59 @@ void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { d_minisat->renewVar(toMinisatLit(lit), level); } +/// Statistics for DPLLMinisatSatSolver + +DPLLMinisatSatSolver::Statistics::Statistics() : + d_statStarts("sat::starts"), + d_statDecisions("sat::decisions"), + d_statRndDecisions("sat::rnd_decisions"), + d_statPropagations("sat::propagations"), + d_statConflicts("sat::conflicts"), + d_statClausesLiterals("sat::clauses_literals"), + d_statLearntsLiterals("sat::learnts_literals"), + d_statMaxLiterals("sat::max_literals"), + d_statTotLiterals("sat::tot_literals") +{ + StatisticsRegistry::registerStat(&d_statStarts); + StatisticsRegistry::registerStat(&d_statDecisions); + StatisticsRegistry::registerStat(&d_statRndDecisions); + StatisticsRegistry::registerStat(&d_statPropagations); + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statClausesLiterals); + StatisticsRegistry::registerStat(&d_statLearntsLiterals); + StatisticsRegistry::registerStat(&d_statMaxLiterals); + StatisticsRegistry::registerStat(&d_statTotLiterals); +} +DPLLMinisatSatSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_statStarts); + StatisticsRegistry::unregisterStat(&d_statDecisions); + StatisticsRegistry::unregisterStat(&d_statRndDecisions); + StatisticsRegistry::unregisterStat(&d_statPropagations); + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statClausesLiterals); + StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); + StatisticsRegistry::unregisterStat(&d_statMaxLiterals); + StatisticsRegistry::unregisterStat(&d_statTotLiterals); +} +void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ + d_statStarts.setData(d_minisat->starts); + d_statDecisions.setData(d_minisat->decisions); + d_statRndDecisions.setData(d_minisat->rnd_decisions); + d_statPropagations.setData(d_minisat->propagations); + d_statConflicts.setData(d_minisat->conflicts); + d_statClausesLiterals.setData(d_minisat->clauses_literals); + d_statLearntsLiterals.setData(d_minisat->learnts_literals); + d_statMaxLiterals.setData(d_minisat->max_literals); + d_statTotLiterals.setData(d_minisat->tot_literals); +} + + +/* + + SatSolverFactory + + */ + MinisatSatSolver* SatSolverFactory::createMinisat() { return new MinisatSatSolver(); } diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h index 94e39e5c6..320dfe09b 100644 --- a/src/prop/sat_module.h +++ b/src/prop/sat_module.h @@ -24,17 +24,24 @@ #include <stdint.h> #include "util/options.h" #include "util/stats.h" - +#include "context/cdlist.h" // DPLLT Minisat -#include "prop/minisat/core/Solver.h" #include "prop/minisat/core/SolverTypes.h" -#include "prop/minisat/simp/SimpSolver.h" // BV Minisat -#include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/core/SolverTypes.h" -#include "prop/bvminisat/simp/SimpSolver.h" + + +namespace Minisat{ +class Solver; +class SimpSolver; +} + +namespace BVMinisat{ +class Solver; +class SimpSolver; +} namespace CVC4 { @@ -155,7 +162,7 @@ class MinisatSatSolver: public BVSatSolverInterface { MinisatSatSolver(); public: - ~MinisatSatSolver() {delete d_minisat;} + ~MinisatSatSolver(); void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); @@ -188,7 +195,6 @@ public: static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); - class Statistics { public: ReferenceStat<uint64_t> d_statStarts, d_statDecisions; @@ -197,54 +203,9 @@ public: ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat<uint64_t> d_statTotLiterals; ReferenceStat<int> d_statEliminatedVars; - Statistics() : - d_statStarts("theory::bv::bvminisat::starts"), - d_statDecisions("theory::bv::bvminisat::decisions"), - d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::bvminisat::propagations"), - d_statConflicts("theory::bv::bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::bvminisat::max_literals"), - d_statTotLiterals("theory::bv::bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") - { - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - StatisticsRegistry::registerStat(&d_statEliminatedVars); - } - ~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - StatisticsRegistry::unregisterStat(&d_statEliminatedVars); - } - - void init(BVMinisat::SimpSolver* minisat){ - d_statStarts.setData(minisat->starts); - d_statDecisions.setData(minisat->decisions); - d_statRndDecisions.setData(minisat->rnd_decisions); - d_statPropagations.setData(minisat->propagations); - d_statConflicts.setData(minisat->conflicts); - d_statClausesLiterals.setData(minisat->clauses_literals); - d_statLearntsLiterals.setData(minisat->learnts_literals); - d_statMaxLiterals.setData(minisat->max_literals); - d_statTotLiterals.setData(minisat->tot_literals); - d_statEliminatedVars.setData(minisat->eliminated_vars); - } + Statistics(); + ~Statistics(); + void init(BVMinisat::SimpSolver* minisat); }; Statistics d_statistics; @@ -252,31 +213,6 @@ public: }; -// class PicosatSatSolver: public SatSolverInterface { - -// public: -// PicosatSatSolver(); - -// void addClause(SatClause& clause, bool removable); - -// SatVariable newVar(bool theoryAtom = false); - -// void markUnremovable(SatLiteral lit); - -// SatLiteralValue solve(unsigned long& resource = 0); - -// SatLiteralValue solve(const std::vector<SatLiteral>& assumptions); - -// void interrupt(); - -// SatLiteralValue value(SatLiteral l); - -// SatLiteralValue modelValue(SatLiteral l); - -// }; - - - class DPLLMinisatSatSolver : public DPLLSatSolverInterface { /** The SatSolver used */ @@ -338,49 +274,9 @@ public: ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat<uint64_t> d_statTotLiterals; public: - Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") - { - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - } - ~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - } - void init(Minisat::SimpSolver* d_minisat){ - d_statStarts.setData(d_minisat->starts); - d_statDecisions.setData(d_minisat->decisions); - d_statRndDecisions.setData(d_minisat->rnd_decisions); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); - } + Statistics(); + ~Statistics(); + void init(Minisat::SimpSolver* d_minisat); }; Statistics d_statistics; @@ -391,8 +287,6 @@ class SatSolverFactory { public: static MinisatSatSolver* createMinisat(); static DPLLMinisatSatSolver* createDPLLMinisat(); - //static PicosatSatSolver* createPicosat(); - //static DPLLPicosatSatSolver* createDPLLPicosat(context::Context* context); }; }/* prop namespace */ diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index b0a02c0a5..6967bff98 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -55,13 +55,13 @@ void inline extractBits(const Bits& b, Bits& dest, unsigned lo, unsigned hi) { } void inline negateBits(const Bits& bits, Bits& negated_bits) { - for(int i = 0; i < bits.size(); ++i) { + for(unsigned i = 0; i < bits.size(); ++i) { negated_bits.push_back(utils::mkNot(bits[i])); } } bool inline isZero(const Bits& bits) { - for(int i = 0; i < bits.size(); ++i) { + for(unsigned i = 0; i < bits.size(); ++i) { if(bits[i] != mkFalse()) { return false; } @@ -323,7 +323,6 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { Assert(node.getKind() == kind::CONST_BITVECTOR); Assert(bits.size() == 0); - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0; i < utils::getSize(node); ++i) { Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); if(bit == Integer(0)){ @@ -690,12 +689,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { res = a; Bits prev_res; - for(int s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < b.size(); ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; int threshold = pow(2, s); - for(int i = 0; i < a.size(); ++i) { + for(unsigned i = 0; i < a.size(); ++i) { if (i + threshold >= a.size()) { // if b[s] is true then we must have shifted by at least 2^b bits so // all bits above 2^s will be 0, otherwise just use previous shift value @@ -723,12 +722,12 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { TNode sign_bit = a.back(); Bits prev_res; - for(int s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < b.size(); ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; int threshold = pow(2, s); - for(int i = 0; i < a.size(); ++i) { + for(unsigned i = 0; i < a.size(); ++i) { if (i + threshold >= a.size()) { // if b[s] is true then we must have shifted by at least 2^b bits so // all bits above 2^s will be the sign bit, otherwise just use previous shift value diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index 22a679693..97e886db2 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -64,6 +64,11 @@ Bitblaster::Bitblaster(context::Context* c) : initTermBBStrategies(); } +Bitblaster::~Bitblaster() { + delete d_cnfStream; + delete d_satSolver; +} + /** * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 9844cd982..ee48dbef4 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -109,11 +109,7 @@ public: public: Bitblaster(context::Context* c); - ~Bitblaster() { - delete d_cnfStream; - delete d_satSolver; - } - + ~Bitblaster(); void assertToSat(TNode node); bool solve(); void bitblast(TNode node); |