Commits

art_haali committed b92436f

minisat back

Comments (0)

Files changed (30)

benchmarking/ext_tools/ic3-ref/minisat/CMakeLists.txt

+cmake_minimum_required(VERSION 2.6 FATAL_ERROR)
+
+project(minisat)
+
+#--------------------------------------------------------------------------------------------------
+# Configurable options:
+
+option(STATIC_BINARIES "Link binaries statically." ON)
+option(USE_SORELEASE   "Use SORELEASE in shared library filename." ON)
+
+#--------------------------------------------------------------------------------------------------
+# Library version:
+
+set(MINISAT_SOMAJOR   2)
+set(MINISAT_SOMINOR   1)
+set(MINISAT_SORELEASE 0)
+
+# Compute VERSION and SOVERSION:
+if (USE_SORELEASE)
+  set(MINISAT_VERSION ${MINISAT_SOMAJOR}.${MINISAT_SOMINOR}.${MINISAT_SORELEASE})
+else()
+  set(MINISAT_VERSION ${MINISAT_SOMAJOR}.${MINISAT_SOMINOR})
+endif()
+set(MINISAT_SOVERSION ${MINISAT_SOMAJOR})
+
+#--------------------------------------------------------------------------------------------------
+# Dependencies:
+
+find_package(ZLIB)
+include_directories(${ZLIB_INCLUDE_DIR})
+include_directories(${minisat_SOURCE_DIR})
+
+#--------------------------------------------------------------------------------------------------
+# Compile flags:
+
+add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS)
+
+#--------------------------------------------------------------------------------------------------
+# Build Targets:
+
+set(MINISAT_LIB_SOURCES
+    minisat/utils/Options.cc
+    minisat/utils/System.cc
+    minisat/core/Solver.cc
+    minisat/simp/SimpSolver.cc)
+
+add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES})
+add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES})
+
+target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY})
+target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY})
+
+add_executable(minisat_core minisat/core/Main.cc)
+add_executable(minisat_simp minisat/simp/Main.cc)
+
+if(STATIC_BINARIES)
+  target_link_libraries(minisat_core minisat-lib-static)
+  target_link_libraries(minisat_simp minisat-lib-static)
+else()
+  target_link_libraries(minisat_core minisat-lib-shared)
+  target_link_libraries(minisat_simp minisat-lib-shared)
+endif()
+
+set_target_properties(minisat-lib-static PROPERTIES OUTPUT_NAME "minisat")
+set_target_properties(minisat-lib-shared
+  PROPERTIES
+    OUTPUT_NAME "minisat" 
+    VERSION ${MINISAT_VERSION}
+    SOVERSION ${MINISAT_SOVERSION})
+
+set_target_properties(minisat_simp       PROPERTIES OUTPUT_NAME "minisat")
+
+#--------------------------------------------------------------------------------------------------
+# Installation targets:
+
+install(TARGETS minisat-lib-static minisat-lib-shared minisat_core minisat_simp 
+        RUNTIME DESTINATION bin
+        LIBRARY DESTINATION lib
+        ARCHIVE DESTINATION lib)
+
+install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp
+        DESTINATION include/minisat
+        FILES_MATCHING PATTERN "*.h")

benchmarking/ext_tools/ic3-ref/minisat/LICENSE

+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  Niklas Sorensson
+
+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.

benchmarking/ext_tools/ic3-ref/minisat/Makefile

+###################################################################################################
+
+.PHONY:	r d p sh cr cd cp csh lr ld lp lsh config all install install-headers install-lib\
+        install-bin clean distclean
+all:	r lr lsh
+
+## Load Previous Configuration ####################################################################
+
+-include config.mk
+
+## Configurable options ###########################################################################
+
+# Directory to store object files, libraries, executables, and dependencies:
+BUILD_DIR      ?= build
+
+# Include debug-symbols in release builds
+MINISAT_RELSYM ?= -g
+
+# Sets of compile flags for different build types
+MINISAT_REL    ?= -O3 -D NDEBUG
+MINISAT_DEB    ?= -O0 -D DEBUG 
+MINISAT_PRF    ?= -O3 -D NDEBUG
+MINISAT_FPIC   ?= -fpic
+
+# GNU Standard Install Prefix
+prefix         ?= /usr/local
+
+## Write Configuration  ###########################################################################
+
+config:
+	@( echo 'BUILD_DIR?=$(BUILD_DIR)'           ; \
+	   echo 'MINISAT_RELSYM?=$(MINISAT_RELSYM)' ; \
+	   echo 'MINISAT_REL?=$(MINISAT_REL)'       ; \
+	   echo 'MINISAT_DEB?=$(MINISAT_DEB)'       ; \
+	   echo 'MINISAT_PRF?=$(MINISAT_PRF)'       ; \
+	   echo 'MINISAT_FPIC?=$(MINISAT_FPIC)'     ; \
+	   echo 'prefix?=$(prefix)'                 ) > config.mk
+
+## Configurable options end #######################################################################
+
+INSTALL ?= install
+
+# GNU Standard Install Variables
+exec_prefix ?= $(prefix)
+includedir  ?= $(prefix)/include
+bindir      ?= $(exec_prefix)/bin
+libdir      ?= $(exec_prefix)/lib
+datarootdir ?= $(prefix)/share
+mandir      ?= $(datarootdir)/man
+
+# Target file names
+MINISAT      = minisat#       Name of MiniSat main executable.
+MINISAT_CORE = minisat_core#  Name of simplified MiniSat executable (only core solver support).
+MINISAT_SLIB = lib$(MINISAT).a#  Name of MiniSat static library.
+MINISAT_DLIB = lib$(MINISAT).so# Name of MiniSat shared library.
+
+# Shared Library Version
+SOMAJOR=2
+SOMINOR=1
+SORELEASE?=.0#   Declare empty to leave out from library file name.
+
+MINISAT_CXXFLAGS = -I. -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wall -Wno-parentheses -Wextra
+MINISAT_LDFLAGS  = -Wall -lz
+
+ECHO=@echo
+ifeq ($(VERB),)
+VERB=@
+else
+VERB=
+endif
+
+SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc)
+HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h)
+OBJS = $(filter-out %Main.o, $(SRCS:.cc=.o))
+
+r:	$(BUILD_DIR)/release/bin/$(MINISAT)
+d:	$(BUILD_DIR)/debug/bin/$(MINISAT)
+p:	$(BUILD_DIR)/profile/bin/$(MINISAT)
+sh:	$(BUILD_DIR)/dynamic/bin/$(MINISAT)
+
+cr:	$(BUILD_DIR)/release/bin/$(MINISAT_CORE)
+cd:	$(BUILD_DIR)/debug/bin/$(MINISAT_CORE)
+cp:	$(BUILD_DIR)/profile/bin/$(MINISAT_CORE)
+csh:	$(BUILD_DIR)/dynamic/bin/$(MINISAT_CORE)
+
+lr:	$(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
+ld:	$(BUILD_DIR)/debug/lib/$(MINISAT_SLIB)
+lp:	$(BUILD_DIR)/profile/lib/$(MINISAT_SLIB)
+lsh:	$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
+
+## Build-type Compile-flags:
+$(BUILD_DIR)/release/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM)
+$(BUILD_DIR)/debug/%.o:				MINISAT_CXXFLAGS +=$(MINISAT_DEB) -g
+$(BUILD_DIR)/profile/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_PRF) -pg
+$(BUILD_DIR)/dynamic/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)
+
+## Build-type Link-flags:
+$(BUILD_DIR)/profile/bin/$(MINISAT):		MINISAT_LDFLAGS += -pg
+$(BUILD_DIR)/release/bin/$(MINISAT):		MINISAT_LDFLAGS += --static $(MINISAT_RELSYM)
+$(BUILD_DIR)/profile/bin/$(MINISAT_CORE):	MINISAT_LDFLAGS += -pg
+$(BUILD_DIR)/release/bin/$(MINISAT_CORE):	MINISAT_LDFLAGS += --static $(MINISAT_RELSYM)
+
+## Executable dependencies
+$(BUILD_DIR)/release/bin/$(MINISAT):	 	$(BUILD_DIR)/release/minisat/simp/Main.o $(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
+$(BUILD_DIR)/debug/bin/$(MINISAT):	 	$(BUILD_DIR)/debug/minisat/simp/Main.o $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB)
+$(BUILD_DIR)/profile/bin/$(MINISAT):	 	$(BUILD_DIR)/profile/minisat/simp/Main.o $(BUILD_DIR)/profile/lib/$(MINISAT_SLIB)
+# need the main-file be compiled with fpic?
+$(BUILD_DIR)/dynamic/bin/$(MINISAT):	 	$(BUILD_DIR)/dynamic/minisat/simp/Main.o $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
+
+## Executable dependencies (core-version)
+$(BUILD_DIR)/release/bin/$(MINISAT_CORE):	$(BUILD_DIR)/release/minisat/core/Main.o $(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
+$(BUILD_DIR)/debug/bin/$(MINISAT_CORE):	 	$(BUILD_DIR)/debug/minisat/core/Main.o $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB)
+$(BUILD_DIR)/profile/bin/$(MINISAT_CORE):	$(BUILD_DIR)/profile/minisat/core/Main.o $(BUILD_DIR)/profile/lib/$(MINISAT_SLIB)
+# need the main-file be compiled with fpic?
+$(BUILD_DIR)/dynamic/bin/$(MINISAT_CORE): 	$(BUILD_DIR)/dynamic/minisat/core/Main.o $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
+
+## Library dependencies
+$(BUILD_DIR)/release/lib/$(MINISAT_SLIB):	$(foreach o,$(OBJS),$(BUILD_DIR)/release/$(o))
+$(BUILD_DIR)/debug/lib/$(MINISAT_SLIB):		$(foreach o,$(OBJS),$(BUILD_DIR)/debug/$(o))
+$(BUILD_DIR)/profile/lib/$(MINISAT_SLIB):	$(foreach o,$(OBJS),$(BUILD_DIR)/profile/$(o))
+$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB):	$(foreach o,$(OBJS),$(BUILD_DIR)/dynamic/$(o))
+
+## Compile rules (these should be unified, buit I have not yet found a way which works in GNU Make)
+$(BUILD_DIR)/release/%.o:	%.cc
+	$(ECHO) Compiling: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $(MINISAT_CXXFLAGS) $(CXXFLAGS) -c -o $@ $< -MMD -MF $(BUILD_DIR)/release/$*.d
+
+$(BUILD_DIR)/profile/%.o:	%.cc
+	$(ECHO) Compiling: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $(MINISAT_CXXFLAGS) $(CXXFLAGS) -c -o $@ $< -MMD -MF $(BUILD_DIR)/profile/$*.d
+
+$(BUILD_DIR)/debug/%.o:	%.cc
+	$(ECHO) Compiling: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $(MINISAT_CXXFLAGS) $(CXXFLAGS) -c -o $@ $< -MMD -MF $(BUILD_DIR)/debug/$*.d
+
+$(BUILD_DIR)/dynamic/%.o:	%.cc
+	$(ECHO) Compiling: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $(MINISAT_CXXFLAGS) $(CXXFLAGS) -c -o $@ $< -MMD -MF $(BUILD_DIR)/dynamic/$*.d
+
+## Linking rule
+$(BUILD_DIR)/release/bin/$(MINISAT) $(BUILD_DIR)/debug/bin/$(MINISAT) $(BUILD_DIR)/profile/bin/$(MINISAT) $(BUILD_DIR)/dynamic/bin/$(MINISAT)\
+$(BUILD_DIR)/release/bin/$(MINISAT_CORE) $(BUILD_DIR)/debug/bin/$(MINISAT_CORE) $(BUILD_DIR)/profile/bin/$(MINISAT_CORE) $(BUILD_DIR)/dynamic/bin/$(MINISAT_CORE):
+	$(ECHO) Linking Binary: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $^ $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@
+
+## Static Library rule
+%/lib/$(MINISAT_SLIB):
+	$(ECHO) Linking Static Library: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(AR) -rcs $@ $^
+
+## Shared Library rule
+$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB):
+	$(ECHO) Linking Shared Library: $@
+	$(VERB) mkdir -p $(dir $@)
+	$(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -shared -Wl,-soname,$(MINISAT_DLIB).$(SOMAJOR) $^
+	$(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)
+	$(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
+
+install:	install-headers install-lib install-bin
+install-debug:	install-headers install-lib-debug
+
+install-headers:
+#       Create directories
+	$(INSTALL) -d $(DESTDIR)$(includedir)/minisat
+	for dir in mtl utils core simp; do \
+	  $(INSTALL) -d $(DESTDIR)$(includedir)/minisat/$$dir ; \
+	done
+#       Install headers
+	for h in $(HDRS) ; do \
+	  $(INSTALL) -m 644 $$h $(DESTDIR)$(includedir)/$$h ; \
+	done
+
+install-lib-debug: $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB)
+	$(INSTALL) -d $(DESTDIR)$(libdir)
+	$(INSTALL) -m 644 $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB) $(DESTDIR)$(libdir)
+
+install-lib: $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
+	$(INSTALL) -d $(DESTDIR)$(libdir)
+	$(INSTALL) -m 644 $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) $(DESTDIR)$(libdir)
+	ln -sf $(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) $(DESTDIR)$(libdir)/$(MINISAT_DLIB).$(SOMAJOR)
+	ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(DESTDIR)$(libdir)/$(MINISAT_DLIB)
+	$(INSTALL) -m 644 $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) $(DESTDIR)$(libdir)
+
+install-bin: $(BUILD_DIR)/dynamic/bin/$(MINISAT)
+	$(INSTALL) -d $(DESTDIR)$(bindir)
+	$(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir)
+
+clean:
+	rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
+          $(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
+	  $(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \
+	  $(foreach t, release debug profile, $(BUILD_DIR)/$t/lib/$(MINISAT_SLIB)) \
+	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
+	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
+	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
+
+distclean:	clean
+	rm -f config.mk
+
+## Include generated dependencies
+-include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/release/$s)
+-include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/debug/$s)
+-include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/profile/$s)
+-include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/dynamic/$s)

benchmarking/ext_tools/ic3-ref/minisat/README

+================================================================================
+Quick Install
+
+- Decide where to install the files . The simplest approach is to use
+  GNU standard locations and just set a "prefix" for the root install
+  directory (reffered to as $PREFIX below). More control can be
+  achieved by overriding other of the GNU standard install locations
+  (includedir, bindir, etc). Configuring with just a prefix:
+
+  > make config prefix=$PREFIX
+
+- Compiling and installing:
+
+  > make install
+
+================================================================================
+Configuration
+
+- Multiple configuration steps can be joined into one call to "make
+  config" by appending multiple variable assignments on the same line.
+
+- The configuration is stored in the file "config.mk". Look here if
+  you want to know what the current configuration looks like.
+
+- To reset from defaults simply remove the "config.mk" file or call
+  "make distclean".
+
+- Recompilation can be done without the configuration step.
+
+  [ TODO: describe configartion possibilities for compile flags / modes ]
+
+================================================================================
+Building
+
+  [ TODO: describe seperate build modes ]
+
+================================================================================
+Install
+
+  [ TODO: ? ]
+
+================================================================================
+Directory Overview:
+
+minisat/mtl/            Mini Template Library
+minisat/utils/          Generic helper code (I/O, Parsing, CPU-time, etc)
+minisat/core/           A core version of the solver
+minisat/simp/           An extended solver with simplification capabilities
+doc/                    Documentation
+README
+LICENSE
+
+================================================================================
+Examples:
+
+Run minisat with same heuristics as version 2.0:
+
+> minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02

benchmarking/ext_tools/ic3-ref/minisat/doc/ReleaseNotes-2.2.0.txt

+Release Notes for MiniSat 2.2.0
+===============================
+
+Changes since version 2.0:
+
+ * Started using a more standard release numbering.
+
+ * Includes some now well-known heuristics: phase-saving and luby
+   restarts. The old heuristics are still present and can be activated
+   if needed.
+
+ * Detection/Handling of out-of-memory and vector capacity
+   overflow. This is fairly new and relatively untested.
+
+ * Simple resource controls: CPU-time, memory, number of
+   conflicts/decisions.
+
+ * CPU-time limiting is implemented by a more general, but simple,
+   asynchronous interruption feature. This means that the solving
+   procedure can be interrupted from another thread or in a signal
+   handler.
+
+ * Improved portability with respect to building on Solaris and with
+   Visual Studio. This is not regularly tested and chances are that
+   this have been broken since, but should be fairly easy to fix if
+   so.
+
+ * Changed C++ file-extention to the less problematic ".cc".
+
+ * Source code is now namespace-protected
+
+ * Introducing a new Clause Memory Allocator that brings reduced
+   memory consumption on 64-bit architechtures and improved
+   performance (to some extent). The allocator uses a region-based
+   approach were all references to clauses are represented as a 32-bit
+   index into a global memory region that contains all clauses. To
+   free up and compact memory it uses a simple copying garbage
+   collector.
+
+ * Improved unit-propagation by Blocking Literals. For each entry in
+   the watcher lists, pair the pointer to a clause with some
+   (arbitrary) literal from the clause. The idea is that if the
+   literal is currently true (i.e. the clause is satisfied) the
+   watchers of the clause does not need to be altered. This can thus
+   be detected without touching the clause's memory at all. As often
+   as can be done cheaply, the blocking literal for entries to the
+   watcher list of a literal 'p' is set to the other literal watched
+   in the corresponding clause.
+
+ * Basic command-line/option handling system. Makes it easy to specify
+   options in the class that they affect, and whenever that class is
+   used in an executable, parsing of options and help messages are
+   brought in automatically.
+
+ * General clean-up and various minor bug-fixes.
+
+ * Changed implementation of variable-elimination/model-extension:
+    
+     - The interface is changed so that arbitrary remembering is no longer
+       possible. If you need to mention some variable again in the future,
+       this variable has to be frozen.
+    
+     - When eliminating a variable, only clauses that contain the variable
+       with one sign is necessary to store. Thereby making the other sign
+       a "default" value when extending models.
+    
+     - The memory consumption for eliminated clauses is further improved
+       by storing all eliminated clauses in a single contiguous vector.
+
+  * Some common utility code (I/O, Parsing, CPU-time, etc) is ripped
+    out and placed in a separate "utils" directory.
+
+  * The DIMACS parse is refactored so that it can be reused in other
+    applications (not very elegant, but at least possible).
+
+  * Some simple improvements to scalability of preprocessing, using
+    more lazy clause removal from data-structures and a couple of
+    ad-hoc limits (the longest clause that can be produced in variable
+    elimination, and the longest clause used in backward subsumption).

benchmarking/ext_tools/ic3-ref/minisat/github_version

+the hash of the commit we use is 
+37dc6c67e2af26379d88ce349eb9c4c6160e8543
+

benchmarking/ext_tools/ic3-ref/minisat/minisat/core/Dimacs.h

+/****************************************************************************************[Dimacs.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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.
+**************************************************************************************************/
+
+#ifndef Minisat_Dimacs_h
+#define Minisat_Dimacs_h
+
+#include <stdio.h>
+
+#include "minisat/utils/ParseUtils.h"
+#include "minisat/core/SolverTypes.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// DIMACS Parser:
+
+template<class B, class Solver>
+static void readClause(B& in, Solver& S, vec<Lit>& lits) {
+    int     parsed_lit, var;
+    lits.clear();
+    for (;;){
+        parsed_lit = parseInt(in);
+        if (parsed_lit == 0) break;
+        var = abs(parsed_lit)-1;
+        while (var >= S.nVars()) S.newVar();
+        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
+    }
+}
+
+template<class B, class Solver>
+static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
+    vec<Lit> lits;
+    int vars    = 0;
+    int clauses = 0;
+    int cnt     = 0;
+    for (;;){
+        skipWhitespace(in);
+        if (*in == EOF) break;
+        else if (*in == 'p'){
+            if (eagerMatch(in, "p cnf")){
+                vars    = parseInt(in);
+                clauses = parseInt(in);
+                // SATRACE'06 hack
+                // if (clauses > 4000000)
+                //     S.eliminate(true);
+            }else{
+                printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+            }
+        } else if (*in == 'c' || *in == 'p')
+            skipLine(in);
+        else{
+            cnt++;
+            readClause(in, S, lits);
+            S.addClause_(lits); }
+    }
+    if (strictp && cnt != clauses)
+        printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+    StreamBuffer in(input_stream);
+    parse_DIMACS_main(in, S, strictp); }
+
+//=================================================================================================
+}
+
+#endif

benchmarking/ext_tools/ic3-ref/minisat/minisat/core/Main.cc

+/*****************************************************************************************[Main.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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 <errno.h>
+#include <zlib.h>
+
+#include "minisat/utils/System.h"
+#include "minisat/utils/ParseUtils.h"
+#include "minisat/utils/Options.h"
+#include "minisat/core/Dimacs.h"
+#include "minisat/core/Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+
+
+static Solver* solver;
+// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
+// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
+static void SIGINT_interrupt(int) { solver->interrupt(); }
+
+// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
+// destructors and may cause deadlocks if a malloc/free function happens to be running (these
+// functions are guarded by locks for multithreaded use).
+static void SIGINT_exit(int) {
+    printf("\n"); printf("*** INTERRUPTED ***\n");
+    if (solver->verbosity > 0){
+        solver->printStats();
+        printf("\n"); printf("*** INTERRUPTED ***\n"); }
+    _exit(1); }
+
+
+//=================================================================================================
+// Main:
+
+
+int main(int argc, char** argv)
+{
+    try {
+        setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
+        setX86FPUPrecision();
+
+        // Extra options:
+        //
+        IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+        IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", 0, IntRange(0, INT32_MAX));
+        IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, INT32_MAX));
+        BoolOption   strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false);
+        
+        parseOptions(argc, argv, true);
+
+        Solver S;
+        double initial_time = cpuTime();
+
+        S.verbosity = verb;
+        
+        solver = &S;
+        // Use signal handlers that forcibly quit until the solver will be able to respond to
+        // interrupts:
+        sigTerm(SIGINT_exit);
+
+        // Try to set resource limits:
+        if (cpu_lim != 0) limitTime(cpu_lim);
+        if (mem_lim != 0) limitMemory(mem_lim);
+        
+        if (argc == 1)
+            printf("Reading from standard input... Use '--help' for help.\n");
+        
+        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
+        if (in == NULL)
+            printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
+        
+        if (S.verbosity > 0){
+            printf("============================[ Problem Statistics ]=============================\n");
+            printf("|                                                                             |\n"); }
+        
+        parse_DIMACS(in, S, (bool)strictp);
+        gzclose(in);
+        FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+        
+        if (S.verbosity > 0){
+            printf("|  Number of variables:  %12d                                         |\n", S.nVars());
+            printf("|  Number of clauses:    %12d                                         |\n", S.nClauses()); }
+        
+        double parsed_time = cpuTime();
+        if (S.verbosity > 0){
+            printf("|  Parse time:           %12.2f s                                       |\n", parsed_time - initial_time);
+            printf("|                                                                             |\n"); }
+ 
+        // Change to signal-handlers that will only notify the solver and allow it to terminate
+        // voluntarily:
+        sigTerm(SIGINT_interrupt);
+       
+        if (!S.simplify()){
+            if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+            if (S.verbosity > 0){
+                printf("===============================================================================\n");
+                printf("Solved by unit propagation\n");
+                S.printStats();
+                printf("\n"); }
+            printf("UNSATISFIABLE\n");
+            exit(20);
+        }
+        
+        vec<Lit> dummy;
+        lbool ret = S.solveLimited(dummy);
+        if (S.verbosity > 0){
+            S.printStats();
+            printf("\n"); }
+        printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
+        if (res != NULL){
+            if (ret == l_True){
+                fprintf(res, "SAT\n");
+                for (int i = 0; i < S.nVars(); i++)
+                    if (S.model[i] != l_Undef)
+                        fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
+                fprintf(res, " 0\n");
+            }else if (ret == l_False)
+                fprintf(res, "UNSAT\n");
+            else
+                fprintf(res, "INDET\n");
+            fclose(res);
+        }
+        
+#ifdef NDEBUG
+        exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
+#else
+        return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+#endif
+    } catch (OutOfMemoryException&){
+        printf("===============================================================================\n");
+        printf("INDETERMINATE\n");
+        exit(0);
+    }
+}

benchmarking/ext_tools/ic3-ref/minisat/minisat/core/Solver.cc

+/***************************************************************************************[Solver.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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 <math.h>
+
+#include "minisat/mtl/Alg.h"
+#include "minisat/mtl/Sort.h"
+#include "minisat/utils/System.h"
+#include "minisat/core/Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "CORE";
+
+static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
+static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
+static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
+static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
+static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
+static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
+static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
+static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));
+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
+static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption     opt_min_learnts_lim   (_cat, "min-learnts", "Minimum learnt clause limit",  0, IntRange(0, INT32_MAX));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+Solver::Solver() :
+
+    // Parameters (user settable):
+    //
+    verbosity        (0)
+  , var_decay        (opt_var_decay)
+  , clause_decay     (opt_clause_decay)
+  , random_var_freq  (opt_random_var_freq)
+  , random_seed      (opt_random_seed)
+  , luby_restart     (opt_luby_restart)
+  , ccmin_mode       (opt_ccmin_mode)
+  , phase_saving     (opt_phase_saving)
+  , rnd_pol          (false)
+  , rnd_init_act     (opt_rnd_init_act)
+  , garbage_frac     (opt_garbage_frac)
+  , min_learnts_lim  (opt_min_learnts_lim)
+  , restart_first    (opt_restart_first)
+  , restart_inc      (opt_restart_inc)
+
+    // Parameters (the rest):
+    //
+  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
+
+    // Parameters (experimental):
+    //
+  , learntsize_adjust_start_confl (100)
+  , learntsize_adjust_inc         (1.5)
+
+    // Statistics: (formerly in 'SolverStats')
+    //
+  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
+  , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+
+  , watches            (WatcherDeleted(ca))
+  , order_heap         (VarOrderLt(activity))
+  , ok                 (true)
+  , cla_inc            (1)
+  , var_inc            (1)
+  , qhead              (0)
+  , simpDB_assigns     (-1)
+  , simpDB_props       (0)
+  , progress_estimate  (0)
+  , remove_satisfied   (true)
+  , next_var           (0)
+
+    // Resource constraints:
+    //
+  , conflict_budget    (-1)
+  , propagation_budget (-1)
+  , asynch_interrupt   (false)
+{}
+
+
+Solver::~Solver()
+{
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
+//
+Var Solver::newVar(lbool upol, bool dvar)
+{
+    Var v;
+    if (free_vars.size() > 0){
+        v = free_vars.last();
+        free_vars.pop();
+    }else
+        v = next_var++;
+
+    watches  .init(mkLit(v, false));
+    watches  .init(mkLit(v, true ));
+    assigns  .insert(v, l_Undef);
+    vardata  .insert(v, mkVarData(CRef_Undef, 0));
+    activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);
+    seen     .insert(v, 0);
+    polarity .insert(v, true);
+    user_pol .insert(v, upol);
+    decision .reserve(v);
+    trail    .capacity(v+1);
+    setDecisionVar(v, dvar);
+    return v;
+}
+
+
+// Note: at the moment, only unassigned variable will be released (this is to avoid duplicate
+// releases of the same variable).
+void Solver::releaseVar(Lit l)
+{
+    if (value(l) == l_Undef){
+        addClause(l);
+        released_vars.push(var(l));
+    }
+}
+
+
+bool Solver::addClause_(vec<Lit>& ps)
+{
+    assert(decisionLevel() == 0);
+    if (!ok) return false;
+
+    // Check if clause is satisfied and remove false/duplicate literals:
+    sort(ps);
+    Lit p; int i, j;
+    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
+        if (value(ps[i]) == l_True || ps[i] == ~p)
+            return true;
+        else if (value(ps[i]) != l_False && ps[i] != p)
+            ps[j++] = p = ps[i];
+    ps.shrink(i - j);
+
+    if (ps.size() == 0)
+        return ok = false;
+    else if (ps.size() == 1){
+        uncheckedEnqueue(ps[0]);
+        return ok = (propagate() == CRef_Undef);
+    }else{
+        CRef cr = ca.alloc(ps, false);
+        clauses.push(cr);
+        attachClause(cr);
+    }
+
+    return true;
+}
+
+
+void Solver::attachClause(CRef cr){
+    const Clause& c = ca[cr];
+    assert(c.size() > 1);
+    watches[~c[0]].push(Watcher(cr, c[1]));
+    watches[~c[1]].push(Watcher(cr, c[0]));
+    if (c.learnt()) num_learnts++, learnts_literals += c.size();
+    else            num_clauses++, clauses_literals += c.size();
+}
+
+
+void Solver::detachClause(CRef cr, bool strict){
+    const Clause& c = ca[cr];
+    assert(c.size() > 1);
+    
+    // Strict or lazy detaching:
+    if (strict){
+        remove(watches[~c[0]], Watcher(cr, c[1]));
+        remove(watches[~c[1]], Watcher(cr, c[0]));
+    }else{
+        watches.smudge(~c[0]);
+        watches.smudge(~c[1]);
+    }
+
+    if (c.learnt()) num_learnts--, learnts_literals -= c.size();
+    else            num_clauses--, clauses_literals -= c.size();
+}
+
+
+void Solver::removeClause(CRef cr) {
+    Clause& c = ca[cr];
+    detachClause(cr);
+    // Don't leave pointers to free'd memory!
+    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
+    c.mark(1); 
+    ca.free(cr);
+}
+
+
+bool Solver::satisfied(const Clause& c) const {
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) == l_True)
+            return true;
+    return false; }
+
+
+// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
+//
+void Solver::cancelUntil(int level) {
+    if (decisionLevel() > level){
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+            Var      x  = var(trail[c]);
+            assigns [x] = l_Undef;
+            if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))
+                polarity[x] = sign(trail[c]);
+            insertVarOrder(x); }
+        qhead = trail_lim[level];
+        trail.shrink(trail.size() - trail_lim[level]);
+        trail_lim.shrink(trail_lim.size() - level);
+    } }
+
+
+//=================================================================================================
+// Major methods:
+
+
+Lit Solver::pickBranchLit()
+{
+    Var next = var_Undef;
+
+    // Random decision:
+    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
+        next = order_heap[irand(random_seed,order_heap.size())];
+        if (value(next) == l_Undef && decision[next])
+            rnd_decisions++; }
+
+    // Activity based decision:
+    while (next == var_Undef || value(next) != l_Undef || !decision[next])
+        if (order_heap.empty()){
+            next = var_Undef;
+            break;
+        }else
+            next = order_heap.removeMin();
+
+    // Choose polarity based on different polarity modes (global or per-variable):
+    if (next == var_Undef)
+        return lit_Undef;
+    else if (user_pol[next] != l_Undef)
+        return mkLit(next, user_pol[next] == l_True);
+    else if (rnd_pol)
+        return mkLit(next, drand(random_seed) < 0.5);
+    else
+        return mkLit(next, polarity[next]);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
+|  
+|  Description:
+|    Analyze conflict and produce a reason clause.
+|  
+|    Pre-conditions:
+|      * 'out_learnt' is assumed to be cleared.
+|      * Current decision level must be greater than root level.
+|  
+|    Post-conditions:
+|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
+|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the 
+|        rest of literals. There may be others from the same level though.
+|  
+|________________________________________________________________________________________________@*/
+void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    int pathC = 0;
+    Lit p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    int index   = trail.size() - 1;
+
+    do{
+        assert(confl != CRef_Undef); // (otherwise should be UIP)
+        Clause& c = ca[confl];
+
+        if (c.learnt())
+            claBumpActivity(c);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+            Lit q = c[j];
+
+            if (!seen[var(q)] && level(var(q)) > 0){
+                varBumpActivity(var(q));
+                seen[var(q)] = 1;
+                if (level(var(q)) >= decisionLevel())
+                    pathC++;
+                else
+                    out_learnt.push(q);
+            }
+        }
+        
+        // Select next clause to look at:
+        while (!seen[var(trail[index--])]);
+        p     = trail[index+1];
+        confl = reason(var(p));
+        seen[var(p)] = 0;
+        pathC--;
+
+    }while (pathC > 0);
+    out_learnt[0] = ~p;
+
+    // Simplify conflict clause:
+    //
+    int i, j;
+    out_learnt.copyTo(analyze_toclear);
+    if (ccmin_mode == 2){
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))
+                out_learnt[j++] = out_learnt[i];
+        
+    }else if (ccmin_mode == 1){
+        for (i = j = 1; i < out_learnt.size(); i++){
+            Var x = var(out_learnt[i]);
+
+            if (reason(x) == CRef_Undef)
+                out_learnt[j++] = out_learnt[i];
+            else{
+                Clause& c = ca[reason(var(out_learnt[i]))];
+                for (int k = 1; k < c.size(); k++)
+                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
+                        out_learnt[j++] = out_learnt[i];
+                        break; }
+            }
+        }
+    }else
+        i = j = out_learnt.size();
+
+    max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    tot_literals += out_learnt.size();
+
+    // Find correct backtrack level:
+    //
+    if (out_learnt.size() == 1)
+        out_btlevel = 0;
+    else{
+        int max_i = 1;
+        // Find the first literal assigned at the next-highest level:
+        for (int i = 2; i < out_learnt.size(); i++)
+            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
+                max_i = i;
+        // Swap-in this literal at index 1:
+        Lit p             = out_learnt[max_i];
+        out_learnt[max_i] = out_learnt[1];
+        out_learnt[1]     = p;
+        out_btlevel       = level(var(p));
+    }
+
+    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+}
+
+
+// Check if 'p' can be removed from a conflict clause.
+bool Solver::litRedundant(Lit p)
+{
+    enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };
+    assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);
+    assert(reason(var(p)) != CRef_Undef);
+
+    Clause*               c     = &ca[reason(var(p))];
+    vec<ShrinkStackElem>& stack = analyze_stack;
+    stack.clear();
+
+    for (uint32_t i = 1; ; i++){
+        if (i < (uint32_t)c->size()){
+            // Checking 'p'-parents 'l':
+            Lit l = (*c)[i];
+            
+            // Variable at level 0 or previously removable:
+            if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){
+                continue; }
+            
+            // Check variable can not be removed for some local reason:
+            if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){
+                stack.push(ShrinkStackElem(0, p));
+                for (int i = 0; i < stack.size(); i++)
+                    if (seen[var(stack[i].l)] == seen_undef){
+                        seen[var(stack[i].l)] = seen_failed;
+                        analyze_toclear.push(stack[i].l);
+                    }
+                    
+                return false;
+            }
+
+            // Recursively check 'l':
+            stack.push(ShrinkStackElem(i, p));
+            i  = 0;
+            p  = l;
+            c  = &ca[reason(var(p))];
+        }else{
+            // Finished with current element 'p' and reason 'c':
+            if (seen[var(p)] == seen_undef){
+                seen[var(p)] = seen_removable;
+                analyze_toclear.push(p);
+            }
+
+            // Terminate with success if stack is empty:
+            if (stack.size() == 0) break;
+            
+            // Continue with top element on stack:
+            i  = stack.last().i;
+            p  = stack.last().l;
+            c  = &ca[reason(var(p))];
+
+            stack.pop();
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Lit p, LSet& out_conflict)
+{
+    out_conflict.clear();
+    out_conflict.insert(p);
+
+    if (decisionLevel() == 0)
+        return;
+
+    seen[var(p)] = 1;
+
+    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
+        Var x = var(trail[i]);
+        if (seen[x]){
+            if (reason(x) == CRef_Undef){
+                assert(level(x) > 0);
+                out_conflict.insert(~trail[i]);
+            }else{
+                Clause& c = ca[reason(x)];
+                for (int j = 1; j < c.size(); j++)
+                    if (level(var(c[j])) > 0)
+                        seen[var(c[j])] = 1;
+            }
+            seen[x] = 0;
+        }
+    }
+
+    seen[var(p)] = 0;
+}
+
+
+void Solver::uncheckedEnqueue(Lit p, CRef from)
+{
+    assert(value(p) == l_Undef);
+    assigns[var(p)] = lbool(!sign(p));
+    vardata[var(p)] = mkVarData(from, decisionLevel());
+    trail.push_(p);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Clause*]
+|  
+|  Description:
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise CRef_Undef.
+|  
+|    Post-conditions:
+|      * the propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+CRef Solver::propagate()
+{
+    CRef    confl     = CRef_Undef;
+    int     num_props = 0;
+
+    while (qhead < trail.size()){
+        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
+        vec<Watcher>&  ws  = watches.lookup(p);
+        Watcher        *i, *j, *end;
+        num_props++;
+
+        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
+            // Try to avoid inspecting the clause:
+            Lit blocker = i->blocker;
+            if (value(blocker) == l_True){
+                *j++ = *i++; continue; }
+
+            // Make sure the false literal is data[1]:
+            CRef     cr        = i->cref;
+            Clause&  c         = ca[cr];
+            Lit      false_lit = ~p;
+            if (c[0] == false_lit)
+                c[0] = c[1], c[1] = false_lit;
+            assert(c[1] == false_lit);
+            i++;
+
+            // If 0th watch is true, then clause is already satisfied.
+            Lit     first = c[0];
+            Watcher w     = Watcher(cr, first);
+            if (first != blocker && value(first) == l_True){
+                *j++ = w; continue; }
+
+            // Look for new watch:
+            for (int k = 2; k < c.size(); k++)
+                if (value(c[k]) != l_False){
+                    c[1] = c[k]; c[k] = false_lit;
+                    watches[~c[1]].push(w);
+                    goto NextClause; }
+
+            // Did not find watch -- clause is unit under assignment:
+            *j++ = w;
+            if (value(first) == l_False){
+                confl = cr;
+                qhead = trail.size();
+                // Copy the remaining watches:
+                while (i < end)
+                    *j++ = *i++;
+            }else
+                uncheckedEnqueue(first, cr);
+
+        NextClause:;
+        }
+        ws.shrink(i - j);
+    }
+    propagations += num_props;
+    simpDB_props -= num_props;
+
+    return confl;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  reduceDB : ()  ->  [void]
+|  
+|  Description:
+|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
+|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt { 
+    ClauseAllocator& ca;
+    reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
+    bool operator () (CRef x, CRef y) { 
+        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
+};
+void Solver::reduceDB()
+{
+    int     i, j;
+    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
+
+    sort(learnts, reduceDB_lt(ca));
+    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
+    // and clauses with activity smaller than 'extra_lim':
+    for (i = j = 0; i < learnts.size(); i++){
+        Clause& c = ca[learnts[i]];
+        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
+            removeClause(learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+    checkGarbage();
+}
+
+
+void Solver::removeSatisfied(vec<CRef>& cs)
+{
+    int i, j;
+    for (i = j = 0; i < cs.size(); i++){
+        Clause& c = ca[cs[i]];
+        if (satisfied(c))
+            removeClause(cs[i]);
+        else{
+            // Trim clause:
+            assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);
+            for (int k = 2; k < c.size(); k++)
+                if (value(c[k]) == l_False){
+                    c[k--] = c[c.size()-1];
+                    c.pop();
+                }
+            cs[j++] = cs[i];
+        }
+    }
+    cs.shrink(i - j);
+}
+
+
+void Solver::rebuildOrderHeap()
+{
+    vec<Var> vs;
+    for (Var v = 0; v < nVars(); v++)
+        if (decision[v] && value(v) == l_Undef)
+            vs.push(v);
+    order_heap.build(vs);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplify : [void]  ->  [bool]
+|  
+|  Description:
+|    Simplify the clause database according to the current top-level assigment. Currently, the only
+|    thing done here is the removal of satisfied clauses, but more things can be put here.
+|________________________________________________________________________________________________@*/
+bool Solver::simplify()
+{
+    assert(decisionLevel() == 0);
+
+    if (!ok || propagate() != CRef_Undef)
+        return ok = false;
+
+    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
+        return true;
+
+    // Remove satisfied clauses:
+    removeSatisfied(learnts);
+    if (remove_satisfied){       // Can be turned off.
+        removeSatisfied(clauses);
+
+        // TODO: what todo in if 'remove_satisfied' is false?
+
+        // Remove all released variables from the trail:
+        for (int i = 0; i < released_vars.size(); i++){
+            assert(seen[released_vars[i]] == 0);
+            seen[released_vars[i]] = 1;
+        }
+
+        int i, j;
+        for (i = j = 0; i < trail.size(); i++)
+            if (seen[var(trail[i])] == 0)
+                trail[j++] = trail[i];
+        trail.shrink(i - j);
+        //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
+        qhead = trail.size();
+
+        for (int i = 0; i < released_vars.size(); i++)
+            seen[released_vars[i]] = 0;
+
+        // Released variables are now ready to be reused:
+        append(released_vars, free_vars);
+        released_vars.clear();
+    }
+    checkGarbage();
+    rebuildOrderHeap();
+
+    simpDB_assigns = nAssigns();
+    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
+|  
+|  Description:
+|    Search for a model the specified number of conflicts. 
+|    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
+|  
+|  Output:
+|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
+|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
+|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|________________________________________________________________________________________________@*/
+lbool Solver::search(int nof_conflicts)
+{
+    assert(ok);
+    int         backtrack_level;
+    int         conflictC = 0;
+    vec<Lit>    learnt_clause;
+    starts++;
+
+    for (;;){
+        CRef confl = propagate();
+        if (confl != CRef_Undef){
+            // CONFLICT
+            conflicts++; conflictC++;
+            if (decisionLevel() == 0) return l_False;
+
+            learnt_clause.clear();
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(backtrack_level);
+
+            if (learnt_clause.size() == 1){
+                uncheckedEnqueue(learnt_clause[0]);
+            }else{
+                CRef cr = ca.alloc(learnt_clause, true);
+                learnts.push(cr);
+                attachClause(cr);
+                claBumpActivity(ca[cr]);
+                uncheckedEnqueue(learnt_clause[0], cr);
+            }
+
+            varDecayActivity();
+            claDecayActivity();
+
+            if (--learntsize_adjust_cnt == 0){
+                learntsize_adjust_confl *= learntsize_adjust_inc;
+                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
+                max_learnts             *= learntsize_inc;
+
+                if (verbosity >= 1)
+                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
+                           (int)conflicts, 
+                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
+                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
+            }
+
+        }else{
+            // NO CONFLICT
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                cancelUntil(0);
+                return l_Undef; }
+
+            // Simplify the set of problem clauses:
+            if (decisionLevel() == 0 && !simplify())
+                return l_False;
+
+            if (learnts.size()-nAssigns() >= max_learnts)
+                // Reduce the set of learnt clauses:
+                reduceDB();
+
+            Lit next = lit_Undef;
+            while (decisionLevel() < assumptions.size()){
+                // Perform user provided assumption:
+                Lit p = assumptions[decisionLevel()];
+                if (value(p) == l_True){
+                    // Dummy decision level:
+                    newDecisionLevel();
+                }else if (value(p) == l_False){
+                    analyzeFinal(~p, conflict);
+                    return l_False;
+                }else{
+                    next = p;
+                    break;
+                }
+            }
+
+            if (next == lit_Undef){
+                // New variable decision:
+                decisions++;
+                next = pickBranchLit();
+
+                if (next == lit_Undef)
+                    // Model found:
+                    return l_True;
+            }
+
+            // Increase decision level and enqueue 'next'
+            newDecisionLevel();
+            uncheckedEnqueue(next);
+        }
+    }
+}
+
+
+double Solver::progressEstimate() const
+{
+    double  progress = 0;
+    double  F = 1.0 / nVars();
+
+    for (int i = 0; i <= decisionLevel(); i++){
+        int beg = i == 0 ? 0 : trail_lim[i - 1];
+        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
+        progress += pow(F, i) * (end - beg);
+    }
+
+    return progress / nVars();
+}
+
+/*
+  Finite subsequences of the Luby-sequence:
+
+  0: 1
+  1: 1 1 2
+  2: 1 1 2 1 1 2 4
+  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
+  ...
+
+
+ */
+
+static double luby(double y, int x){
+
+    // Find the finite subsequence that contains index 'x', and the
+    // size of that subsequence:
+    int size, seq;
+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
+
+    while (size-1 != x){
+        size = (size-1)>>1;
+        seq--;
+        x = x % size;
+    }
+
+    return pow(y, seq);
+}
+
+// NOTE: assumptions passed in member-variable 'assumptions'.
+lbool Solver::solve_()
+{
+    model.clear();
+    conflict.clear();
+    if (!ok) return l_False;
+
+    solves++;
+
+    max_learnts = nClauses() * learntsize_factor;
+    if (max_learnts < min_learnts_lim)
+        max_learnts = min_learnts_lim;
+
+    learntsize_adjust_confl   = learntsize_adjust_start_confl;
+    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
+    lbool   status            = l_Undef;
+
+    if (verbosity >= 1){
+        printf("============================[ Search Statistics ]==============================\n");
+        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
+        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
+        printf("===============================================================================\n");
+    }
+
+    // Search:
+    int curr_restarts = 0;
+    while (status == l_Undef){
+        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
+        status = search(rest_base * restart_first);
+        if (!withinBudget()) break;
+        curr_restarts++;
+    }
+
+    if (verbosity >= 1)
+        printf("===============================================================================\n");
+
+
+    if (status == l_True){
+        // Extend & copy model:
+        model.growTo(nVars());
+        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+    }else if (status == l_False && conflict.size() == 0)
+        ok = false;
+
+    cancelUntil(0);
+    return status;
+}
+
+
+bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out)
+{
+    trail_lim.push(trail.size());
+    for (int i = 0; i < assumps.size(); i++){
+        Lit a = assumps[i];
+
+        if (value(a) == l_False){
+            cancelUntil(0);
+            return false;
+        }else if (value(a) == l_Undef)
+            uncheckedEnqueue(a);
+    }
+
+    unsigned trail_before = trail.size();
+    bool     ret          = true;
+    if (propagate() == CRef_Undef){
+        out.clear();
+        for (int j = trail_before; j < trail.size(); j++)
+            out.push(trail[j]);
+    }else
+        ret = false;
+    
+    cancelUntil(0);
+    return ret;
+}
+
+//=================================================================================================
+// Writing CNF to DIMACS:
+// 
+// FIXME: this needs to be rewritten completely.
+
+static Var mapVar(Var x, vec<Var>& map, Var& max)
+{
+    if (map.size() <= x || map[x] == -1){
+        map.growTo(x+1, -1);
+        map[x] = max++;
+    }
+    return map[x];
+}
+
+
+void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
+{
+    if (satisfied(c)) return;
+
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) != l_False)
+            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
+    fprintf(f, "0\n");
+}
+
+
+void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
+{
+    FILE* f = fopen(file, "wr");
+    if (f == NULL)
+        fprintf(stderr, "could not open file %s\n", file), exit(1);
+    toDimacs(f, assumps);
+    fclose(f);
+}
+
+
+void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
+{
+    // Handle case when solver is in contradictory state:
+    if (!ok){
+        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
+        return; }
+
+    vec<Var> map; Var max = 0;
+
+    // Cannot use removeClauses here because it is not safe
+    // to deallocate them at this point. Could be improved.
+    int cnt = 0;
+    for (int i = 0; i < clauses.size(); i++)
+        if (!satisfied(ca[clauses[i]]))
+            cnt++;
+        
+    for (int i = 0; i < clauses.size(); i++)
+        if (!satisfied(ca[clauses[i]])){
+            Clause& c = ca[clauses[i]];
+            for (int j = 0; j < c.size(); j++)
+                if (value(c[j]) != l_False)
+                    mapVar(var(c[j]), map, max);
+        }
+
+    // Assumptions are added as unit clauses:
+    cnt += assumps.size();
+
+    fprintf(f, "p cnf %d %d\n", max, cnt);
+
+    for (int i = 0; i < assumps.size(); i++){
+        assert(value(assumps[i]) != l_False);
+        fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
+    }
+
+    for (int i = 0; i < clauses.size(); i++)
+        toDimacs(f, ca[clauses[i]], map, max);
+
+    if (verbosity > 0)
+        printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
+}
+
+
+void Solver::printStats() const
+{
+    double cpu_time = cpuTime();
+    double mem_used = memUsedPeak();
+    printf("restarts              : %"PRIu64"\n", starts);
+    printf("conflicts             : %-12"PRIu64"   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);
+    printf("decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);
+    printf("propagations          : %-12"PRIu64"   (%.0f /sec)\n", propagations, propagations/cpu_time);
+    printf("conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
+    printf("CPU time              : %g s\n", cpu_time);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+void Solver::relocAll(ClauseAllocator& to)
+{
+    // All watchers:
+    //
+    watches.cleanAll();
+    for (int v = 0; v < nVars(); v++)
+        for (int s = 0; s < 2; s++){
+            Lit p = mkLit(v, s);
+            vec<Watcher>& ws = watches[p];
+            for (int j = 0; j < ws.size(); j++)
+                ca.reloc(ws[j].cref, to);
+        }
+
+    // All reasons:
+    //
+    for (int i = 0; i < trail.size(); i++){
+        Var v = var(trail[i]);
+
+        // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep
+        // 'dangling' reasons here. It is safe and does not hurt.
+        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){
+            assert(!isRemoved(reason(v)));
+            ca.reloc(vardata[v].reason, to);
+        }
+    }
+
+    // All learnt:
+    //
+    int i, j;
+    for (i = j = 0; i < learnts.size(); i++)
+        if (!isRemoved(learnts[i])){
+            ca.reloc(learnts[i], to);
+            learnts[j++] = learnts[i];
+        }
+    learnts.shrink(i - j);
+
+    // All original:
+    //
+    for (i = j = 0; i < clauses.size(); i++)
+        if (!isRemoved(clauses[i])){
+            ca.reloc(clauses[i], to);
+            clauses[j++] = clauses[i];
+        }
+    clauses.shrink(i - j);
+}
+
+
+void Solver::garbageCollect()
+{
+    // Initialize the next region to a size corresponding to the estimated utilization degree. This
+    // is not precise but should avoid some unnecessary reallocations for the new region:
+    ClauseAllocator to(ca.size() - ca.wasted()); 
+
+    relocAll(to);
+    if (verbosity >= 2)
+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
+               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+    to.moveTo(ca);
+}

benchmarking/ext_tools/ic3-ref/minisat/minisat/core/Solver.h

+/****************************************************************************************[Solver.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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.
+**************************************************************************************************/
+
+#ifndef Minisat_Solver_h
+#define Minisat_Solver_h
+
+#include "minisat/mtl/Vec.h"
+#include "minisat/mtl/Heap.h"
+#include "minisat/mtl/Alg.h"
+#include "minisat/mtl/IntMap.h"
+#include "minisat/utils/Options.h"
+#include "minisat/core/SolverTypes.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+// Solver -- the main class:
+
+class Solver {
+public:
+
+    // Constructor/Destructor:
+    //
+    Solver();
+    virtual ~Solver();
+
+    // Problem specification:
+    //
+    Var     newVar    (lbool upol = l_Undef, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+    void    releaseVar(Lit l);                                  // Make literal true and promise to never refer to variable again.
+
+    bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. 
+    bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
+    bool    addClause (Lit p);                                  // Add a unit clause to the solver. 
+    bool    addClause (Lit p, Lit q);                           // Add a binary clause to the solver. 
+    bool    addClause (Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver. 
+    bool    addClause (Lit p, Lit q, Lit r, Lit s);             // Add a quaternary clause to the solver. 
+    bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will
+                                                                // change the passed vector 'ps'.
+
+    // Solving:
+    //
+    bool    simplify     ();                        // Removes already satisfied clauses.
+    bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
+    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
+    bool    solve        ();                        // Search without assumptions.
+    bool    solve        (Lit p);                   // Search for a model that respects a single assumption.
+    bool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
+    bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
+    bool    okay         () const;                  // FALSE means solver is in a conflicting state
+
+    bool    implies      (const ve