#-fno-inline
CFLAGS_BASE = $(OPTIMIZE)
+CFLAGS_BASE = $(OPTIMIZE)
-# OPTION to compile CRYPTOMiniSAT version 2.x
-ifeq ($(SAT),cryptominisat2)
- CRYPTOMINISAT2 = true
- CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT2 -I$(TOP)/src/
- MTL = $(TOP)/src/sat/cryptominisat2/mtl
- SOLVER_INCLUDE = $(TOP)/src/sat/cryptominisat2
-endif
-
-# OPTION to compile MiniSAT
-ifeq ($(SAT),minisat)
- CORE = true
- CFLAGS_BASE = $(OPTIMIZE) -DCORE
- MTL = $(TOP)/src/sat/mtl
- SOLVER_INCLUDE = $(TOP)/src/sat/core
-endif
ifeq ($(WITHCBITP),yes)
CFLAGS_BASE += -DWITHCBITP
CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) -I../AST
endif
-CFLAGS += -DONLY_MSPACES -DMSPACES
+# Used by Doug Lea's malloc that I added into minisat2.
+#CFLAGS += -DONLY_MSPACES -DMSPACES
+
+#Required my minisat2.2
+CFLAGS += -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
#CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
#CXXFLAGS = $(CFLAGS) -Wextra -DEXT_HASH_MAP -Wno-deprecated
.PHONY: all
all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv extlib-abc
-ifdef CRYPTOMINISAT2
- $(MAKE) -C $(SRC)/sat cryptominisat2
-endif
-ifdef CORE
$(MAKE) -C $(SRC)/sat core
-endif
-ifdef SIMP
- $(MAKE) -C $(SRC)/sat simp
-endif
-
$(MAKE) -C $(SRC)/parser
$(MAKE) -C $(SRC)/main
$(AR) rc libstp.a $(SRC)/AST/*.o \
$(SRC)/to-sat/*.o \
$(SRC)/to-sat/AIG/*.o \
$(SRC)/sat/*.o \
+ $(SRC)/sat/core/*.o? \
+ $(SRC)/sat/simp/*.o? \
+ $(SRC)/sat/utils/*.o \
$(SRC)/simplifier/*.o \
$(SRC)/simplifier/constantBitP/*.o \
$(SRC)/extlib-constbv/*.o \
{
unsigned long long hash = 5381;
long long c;
-
+
while (c = *str++)
hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
//cout << "Hash value computed is: " << hash << endl;
-
+
return (unsigned long long)hash;
}
-
};//end of namespace
#ifndef USEFULDEFS_H
#define USEFULDEFS_H
-#ifndef CRYPTOMINISAT2
-#ifndef CORE
-#ifndef SIMP
-#error "A SAT solver must be specified."
-#endif
-#endif
-#endif
-
-
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
using namespace std;
namespace BEEV {
- using namespace MINISAT;
#ifdef EXT_HASH_MAP
using namespace __gnu_cxx;
#endif
#else
typedef HASHMAP<const char*,
int,
- hash<char *>,
+ BEEV::hash<char *>,
eqstr> function_counters;
#endif
}; //end of namespace
#include "../to-sat/AIG/ToSATAIG.h"
#include "../simplifier/constantBitP/ConstantBitPropagation.h"
#include "../simplifier/constantBitP/NodeToFixedBitsMap.h"
+#include "../sat/SimplifyingMinisat.h"
+#include "../sat/MinisatCore.h"
+#include "../sat/CryptoMinisat.h"
namespace BEEV {
bm->CreateNode(NOT, query));
//solver instantiated here
-#if defined CRYPTOMINISAT2
- MINISAT::Solver NewSolver;
+//#if defined CRYPTOMINISAT2
+ //MINISAT::Solver NewSolver;
- if(bm->UserFlags.print_cnf_flag)
- {
- NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
- }
-#endif
+ //if(bm->UserFlags.print_cnf_flag)
+ //{
+ //NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
+ //}
+//#endif
-#if defined CORE
- MINISAT::Solver *newS;
+
+ SATSolver *newS;
if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER)
- newS = new MINISAT::SimpSolver();
- else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER)
- newS = new MINISAT::Solver();
+ newS = new SimplifyingMinisat();
+ else if (bm->UserFlags.solver_to_use == UserDefinedFlags::CRYPTOMINISAT_SOLVER)
+ newS = new CryptoMinisat();
else
- FatalError("unknown option");
+ newS = new MinisatCore<Minisat::Solver>();
+
+
+
+ SATSolver& NewSolver = *newS;
- MINISAT::Solver& NewSolver = *newS;
-#endif
if(bm->UserFlags.stats_flag)
{
- NewSolver.verbosity = 1;
+ NewSolver.setVerbosity(1);
}
SOLVER_RETURN_TYPE result;
original_input, original_input);
}
-#if defined CORE
delete newS;
-#endif
return result;
//Acceps a query, calls the SAT solver and generates Valid/InValid.
//if returned 0 then input is INVALID if returned 1 then input is
//VALID if returned 2 then UNDECIDED
- SOLVER_RETURN_TYPE STP::TopLevelSTPAux(MINISAT::Solver& NewSolver,
+ SOLVER_RETURN_TYPE STP::TopLevelSTPAux(SATSolver& NewSolver,
const ASTNode& modified_input,
const ASTNode& original_input)
{
//UserGuided abstraction refinement
SOLVER_RETURN_TYPE
STP::
- UserGuided_AbsRefine(MINISAT::Solver& NewSolver,
+ UserGuided_AbsRefine(SATSolver& NewSolver,
const ASTNode& original_input)
{
ASTVec v = bm->GetAsserts_WithKey(0);
// returns VALID, else returns INVALID. Automatically constructs
// counterexample for invalid queries, and prints them upon
// request.
- SOLVER_RETURN_TYPE TopLevelSTPAux(MINISAT::Solver& NewSolver,
+ SOLVER_RETURN_TYPE TopLevelSTPAux(SATSolver& NewSolver,
const ASTNode& modified_input,
const ASTNode& original_input);
SOLVER_RETURN_TYPE
- UserGuided_AbsRefine(MINISAT::Solver& SatSolver,
+ UserGuided_AbsRefine(SATSolver& SatSolver,
const ASTNode& original_input);
void ClearAllTables(void)
********************************************************************/
// to get the PRIu64 macro from inttypes, this needs to be defined.
-#define __STDC_FORMAT_MACROS
+#ifndef __STDC_FORMAT_MACROS
+ #define __STDC_FORMAT_MACROS
+#endif
#include <inttypes.h>
#include <cmath>
-#include "../sat/sat.h"
#include "../STPManager/STPManager.h"
namespace BEEV
return newn;
}
- // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver
- void STPMgr::PrintStats(MINISAT::Solver& s)
- {
- if (!UserFlags.stats_flag)
- return;
- double cpu_time = MINISAT::cpuTime();
- uint64_t mem_used = MINISAT::memUsed();
- printf("restarts : %"PRIu64"\n", s.starts);
- printf("conflicts : %"PRIu64" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time);
- printf("decisions : %"PRIu64" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time);
- printf("propagations : %"PRIu64" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time);
- printf("conflict literals : %"PRIu64" (%4.2f %% deleted)\n", s.tot_literals,
- (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
- if (mem_used != 0)
- printf("Memory used : %.2f MB\n", mem_used / 1048576.0);
- printf("CPU time : %g s\n", cpu_time);
- } //end of PrintStats()
-
-
//Create a new variable of ValueWidth 'n'
ASTNode STPMgr::NewVar(unsigned int n)
{
#include "UserDefinedFlags.h"
#include "../AST/AST.h"
#include "../AST/NodeFactory/HashingNodeFactory.h"
+#include "../sat/SATSolver.h"
namespace BEEV
{
// Print assertions to the input stream
void printAssertsToStream(ostream &os, int simplify);
- // Prints SAT solver statistics
- void PrintStats(MINISAT::Solver& stats);
-
// Create New Variables
ASTNode NewVar(unsigned int n);
enum SATSolvers
{
MINISAT_SOLVER =0,
- SIMPLIFYING_MINISAT_SOLVER
+ SIMPLIFYING_MINISAT_SOLVER,
+ CRYPTOMINISAT_SOLVER
};
enum SATSolvers solver_to_use;
//Converts MINISAT counterexample into an AST memotable (i.e. the
//function populates the datastructure CounterExampleMap)
- void ConstructCounterExample(MINISAT::Solver& newS, ToSATBase::ASTNodeToSATVar& satVarToSymbol);
+ void ConstructCounterExample(SATSolver& newS, ToSATBase::ASTNodeToSATVar& satVarToSymbol);
// Prints MINISAT assigment one bit at a time, for debugging.
- void PrintSATModel(MINISAT::Solver& S, ToSATBase::ASTNodeToSATVar& satVarToSymbol);
+ void PrintSATModel(SATSolver& S, ToSATBase::ASTNodeToSATVar& satVarToSymbol);
public:
* Array Refinement functions *
****************************************************************/
SOLVER_RETURN_TYPE
- CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
+ CallSAT_ResultCheck(SATSolver& SatSolver,
const ASTNode& modified_input,
const ASTNode& original_input,
ToSATBase* tosat);
const ASTNode& array_newname);
SOLVER_RETURN_TYPE
- SATBased_ArrayReadRefinement(MINISAT::Solver& newS,
+ SATBased_ArrayReadRefinement(SATSolver& newS,
const ASTNode& modified_input,
const ASTNode& original_input,
ToSATBase* tosat);
SOLVER_RETURN_TYPE
- SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
+ SATBased_ArrayWriteRefinement(SATSolver& newS,
const ASTNode& orig_input,
ToSATBase *tosat);
// SOLVER_RETURN_TYPE
- // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS,
+ // SATBased_AllFiniteLoops_Refinement(SATSolver& newS,
// const ASTNode& orig_input);
- // ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver&
+ // ASTVec SATBased_FiniteLoop_Refinement(SATSolver&
// SatSolver, const ASTNode& original_input, const ASTNode&
// finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
// absrefine_flag=false);
*****************************************************************/
SOLVER_RETURN_TYPE
AbsRefine_CounterExample::
- SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
+ SATBased_ArrayReadRefinement(SATSolver& SatSolver,
const ASTNode& inputAlreadyInSAT,
const ASTNode& original_input,
ToSATBase* tosat) {
*****************************************************************/
SOLVER_RETURN_TYPE
AbsRefine_CounterExample::
- SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver,
+ SATBased_ArrayWriteRefinement(SATSolver& SatSolver,
const ASTNode& original_input,
ToSATBase *tosat
)
// *****************************************************************/
// SOLVER_RETURN_TYPE
// AbsRefine_CounterExample::
- // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver,
+ // SATBased_AllFiniteLoops_Refinement(SATSolver& SatSolver,
// const ASTNode& original_input)
// {
// cout << "The number of abs-refinement limit is "
// //formulas to the SAT solver
// ASTVec
// AbsRefine_CounterExample::
- // SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver,
+ // SATBased_FiniteLoop_Refinement(SATSolver& SatSolver,
// const ASTNode& original_input,
// const ASTNode& finiteloop,
// ASTNodeMap* ParamToCurrentValMap,
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
-#include "../sat/sat.h"
#include "AbsRefine_CounterExample.h"
#include "../printer/printers.h"
#include "../to-sat/AIG/ToSATAIG.h"
namespace BEEV
{
+
+
/*FUNCTION: constructs counterexample from MINISAT counterexample
* step1 : iterate through MINISAT counterexample and assemble the
* bits for each AST term. Store it in a map from ASTNode to vector
* populate the CounterExampleMap data structure (ASTNode -> BVConst)
*/
void
- AbsRefine_CounterExample::ConstructCounterExample(MINISAT::Solver& newS,
+ AbsRefine_CounterExample::ConstructCounterExample(SATSolver& newS,
ToSATBase::ASTNodeToSATVar& satVarToSymbol)
{
//iterate over MINISAT counterexample and construct a map from AST
if (sat_variable_index == ~((unsigned) 0)) // not sent to the sat solver.
continue;
- if (newS.model[sat_variable_index] == MINISAT::l_Undef)
+ if (newS.modelValue(sat_variable_index) == newS.undef_literal())
continue;
//assemble the counterexample here
//Collect the bits of 'symbol' and store in v. Store
//in reverse order.
- if (newS.model[sat_variable_index] == MINISAT::l_True)
+ if (newS.modelValue(sat_variable_index) == newS.true_literal() )
(*v)[(symbolWidth - 1) - index] = true;
else
(*v)[(symbolWidth - 1) - index] = false;
if (0 != strncmp("cnf", zz, 3) && 0
!= strcmp("*TrueDummy*", zz))
{
- if (newS.model[sat_variable_index] == MINISAT::l_True)
+ if (newS.modelValue(sat_variable_index) == newS.true_literal())
CounterExampleMap[symbol] = ASTTrue;
- else if (newS.model[sat_variable_index] == MINISAT::l_False)
+ else if (newS.modelValue(sat_variable_index) == newS.false_literal())
CounterExampleMap[symbol] = ASTFalse;
else
FatalError("never heres.");
// Prints Satisfying assignment directly, for debugging.
void
- AbsRefine_CounterExample::PrintSATModel(MINISAT::Solver& newS,
+ AbsRefine_CounterExample::PrintSATModel(SATSolver& newS,
ToSATBase::ASTNodeToSATVar& m)
{
if (!newS.okay())
if (v[i] == ~((unsigned)0)) // nb. special value.
continue;
- if (newS.model[v[i]] == MINISAT::l_True)
+
+ if (newS.modelValue(v[i]) == newS.true_literal())
{
it->first.nodeprint(cout);
cout << " {" << i << "}" << endl;
}
- else if (newS.model[v[i]] == MINISAT::l_False)
+ else if (newS.modelValue(v[i]) == newS.false_literal())
{
cout << "NOT ";
it->first.nodeprint(cout);
}
SOLVER_RETURN_TYPE
- AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
+ AbsRefine_CounterExample::CallSAT_ResultCheck(SATSolver& SatSolver,
const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat)
{
SRCS = $(wildcard *.cpp)
OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I$(MTL) -I$(MTRAND) -I$(SOLVER_INCLUDE)
libabstractionrefinement.a: $(OBJS) depend
$(AR) rc $@ $(OBJS)
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
\ No newline at end of file
+-include depend
#include <unistd.h>
#include <vector>
-namespace MINISAT
-{
- class Solver;
-}
-
namespace BEEV
{
class STPMgr;
* step 5. Call SAT to determine if input is SAT or UNSAT
********************************************************************/
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER} OptionType;
int main(int argc, char ** argv) {
char * infile = NULL;
helpstring +=
"-c : construct counterexample\n";
helpstring +=
+ "--cryptominisat : use cryptominisat2 as the solver\n";
+
+ helpstring +=
"-d : check counterexample\n";
#ifdef WITHCBITP
helpstring +=
"-m : use the SMTLIB1 parser\n";
+ helpstring +=
+ "--minisat : use minisat 2.2 as the solver\n";
+
helpstring += "--output-CNF : save the CNF into output.cnf\n";
helpstring += "--output-bench : save in ABC's bench format to output.bench\n";
"-r : switch refinement off (optimizations are ON by default)\n";
helpstring +=
"-s : print function statistics\n";
-#if !defined CRYPTOMINISAT2
helpstring +=
- "--simplifying-minisat : use simplifying-minisat rather than minisat\n";
-#endif
+ "--simplifying-minisat : use simplifying-minisat 2.2 as the solver\n";
helpstring +=
"--SMTLIB1 : use the SMT-LIB1 format parser\n";
helpstring +=
// long options.
map<string,OptionType> lookup;
lookup.insert(make_pair(tolower("--print-back-C"),PRINT_BACK_C));
- lookup.insert(make_pair(tolower("--print-back-CVC"),PRINT_BACK_CVC));
+ lookup.insert(make_pair(tolower("--cryptominisat"),USE_CRYPTOMINISAT_SOLVER));
+ lookup.insert(make_pair(tolower("--minisat"),USE_MINISAT_SOLVER));
+
+ lookup.insert(make_pair(tolower("--print-back-CVC"),PRINT_BACK_CVC));
lookup.insert(make_pair(tolower("--print-back-SMTLIB2"),PRINT_BACK_SMTLIB2));
lookup.insert(make_pair(tolower("--print-back-SMTLIB1"),PRINT_BACK_SMTLIB1));
lookup.insert(make_pair(tolower("--print-back-GDL"),PRINT_BACK_GDL));
if (bm->UserFlags.smtlib2_parser_flag)
FatalError("Can't use both the smtlib and smtlib2 parsers");
break;
-
-
-#if !defined CRYPTOMINISAT2
case USE_SIMPLIFYING_SOLVER:
bm->UserFlags.solver_to_use = UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER;
break;
-#endif
-
-
+ case USE_CRYPTOMINISAT_SOLVER:
+ bm->UserFlags.solver_to_use = UserDefinedFlags::CRYPTOMINISAT_SOLVER;
+ break;
+ case USE_MINISAT_SOLVER:
+ bm->UserFlags.solver_to_use = UserDefinedFlags::MINISAT_SOLVER;
+ break;
default:
fprintf(stderr,usage,prog);
cout << helpstring;
#include "printers.h"
#include "AssortedPrinters.h"
-#include "../sat/sat.h"
// to get the PRIu64 macro from inttypes, this needs to be defined.
-#define __STDC_FORMAT_MACROS
+#ifndef __STDC_FORMAT_MACROS
+ #define __STDC_FORMAT_MACROS
+#endif
#include <inttypes.h>
//#undef __STDC_FORMAT_MACROS
--- /dev/null
+#include "CryptoMinisat.h"
+#include "utils/System.h"
+
+#undef var_Undef
+#undef l_True
+#undef l_False
+#undef l_Undef
+
+
+#include "cryptominisat2/Solver.h"
+#include "cryptominisat2/SolverTypes.h"
+
+namespace BEEV
+{
+
+ CryptoMinisat::CryptoMinisat()
+ {
+ s = new MINISAT::Solver();
+ }
+
+ CryptoMinisat::~CryptoMinisat()
+ {
+ delete s;
+ }
+
+ bool
+ CryptoMinisat::addClause(const vec_literals& ps) // Add a clause to the solver.
+ {
+ // Cryptominisat uses a slightly different vec class.
+ // Cryptominisat uses a slightly different Lit class too.
+
+ // VERY SLOW>
+ MINISAT::vec<MINISAT::Lit> v;
+ for (int i =0; i<ps.size();i++)
+ v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
+
+ s->addClause(v);
+ }
+
+ bool
+ CryptoMinisat::okay() const // FALSE means solver is in a conflicting state
+ {
+ return s->okay();
+ }
+
+ bool
+ CryptoMinisat::solve() // Search without assumptions.
+ {
+ return s->solve().getchar();
+ }
+
+ uint8_t
+ CryptoMinisat::modelValue(Var x) const
+ {
+ return s->model[x].getchar();
+ }
+
+ Minisat::Var
+ CryptoMinisat::newVar()
+ {
+ return s->newVar();
+ }
+
+ int CryptoMinisat::setVerbosity(int v)
+ {
+ s->verbosity = v;
+ }
+
+ int CryptoMinisat::nVars()
+ {return s->nVars();}
+
+ void CryptoMinisat::printStats()
+ {
+ double cpu_time = Minisat::cpuTime();
+ double mem_used = Minisat::memUsedPeak();
+ printf("restarts : %"PRIu64"\n", s->starts);
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+ }
+};
--- /dev/null
+/*
+ * Wraps around CORE minisat.
+ */
+#ifndef MINISATCORE_H_
+#define MINIASTCORE_H_
+
+#include "SATSolver.h"
+
+namespace MINISAT
+{
+ class Solver;
+}
+
+namespace BEEV
+{
+ class CryptoMinisat : public SATSolver
+ {
+ MINISAT::Solver* s;
+
+ public:
+ CryptoMinisat();
+
+ ~CryptoMinisat();
+
+ bool
+ addClause(const vec_literals& ps); // Add a clause to the solver.
+
+ bool
+ okay() const; // FALSE means solver is in a conflicting state
+
+
+ bool
+ solve(); // Search without assumptions.
+
+ virtual uint8_t modelValue(Var x) const;
+
+ virtual Var newVar();
+
+ int setVerbosity(int v);
+
+ int nVars();
+
+ void printStats();
+
+ //nb CMS2 has different literal values to the other minisats.
+ virtual lbool true_literal() {return ((uint8_t)1);}
+ virtual lbool false_literal() {return ((uint8_t)-1);}
+ virtual lbool undef_literal() {return ((uint8_t)0);}
+ };
+}
+;
+
+#endif
-.PHONY: core
-core:
- $(MAKE) -C core all
- $(MAKE) -C simp lib all
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
-.PHONY: cryptominisat2
-cryptominisat2:
+SRCS=$(wildcard *.cpp)
+OBJS=$(SRCS:.cpp=.o)
+SRCS+=utils/System.cc
+OBJS+=utils/System.o
+LIB=libminisat.a
+COPTIMIZE="-O3 -m32"
+
+.PHONY:core
+core: $(OBJS)
+ #Command line variables override those set in the makefile.
+ $(MAKE) -C core libr COPTIMIZE="$(CFLAGS_M32) -O3"
+ $(MAKE) -C simp libr COPTIMIZE="$(CFLAGS_M32) -O3"
$(MAKE) -C cryptominisat2 lib all
+
+ rm -f $(LIB)
+ ar cq $(LIB) ./core/*.or ./simp/*.or *.o utils/*.o *.o
+ ranlib $(LIB)
.PHONY: clean
clean:
- rm -rf *.o *~ libminisat.a
+ rm -rf *.o core/*.o *~ $(LIB)
$(MAKE) -C core clean
$(MAKE) -C simp clean
$(MAKE) -C cryptominisat2 clean
+CryptoMinisat.o: CryptoMinisat.cpp
+ $(CC) $(CFLAGS) -Icryptominisat2/mtl -Imtl CryptoMinisat.cpp -c
--- /dev/null
+#include "core/Solver.h"
+#include "MinisatCore.h"
+#include "utils/System.h"
+
+namespace BEEV
+{
+
+ template <class T>
+ MinisatCore<T>::MinisatCore()
+ {
+ s = new T();
+ };
+
+ template <class T>
+ MinisatCore<T>::~MinisatCore()
+ {
+ delete s;
+ }
+
+
+ template <class T>
+ bool
+ MinisatCore<T>::addClause(const vec_literals& ps) // Add a clause to the solver.
+ {
+ s->addClause(ps);
+ }
+
+ template <class T>
+ bool
+ MinisatCore<T>::okay() const // FALSE means solver is in a conflicting state
+ {
+ return s->okay();
+ }
+
+ template <class T>
+ bool
+ MinisatCore<T>::solve() // Search without assumptions.
+ {
+ if (!s->simplify())
+ return false;
+
+ return s->solve();
+
+ }
+
+ template <class T>
+ uint8_t
+ MinisatCore<T>::modelValue(Var x) const
+ {
+ return Minisat::toInt(s->modelValue(x));
+ }
+
+ template <class T>
+ Minisat::Var
+ MinisatCore<T>::newVar()
+ {
+ return s->newVar();
+ }
+
+ template <class T>
+ int MinisatCore<T>::setVerbosity(int v)
+ {
+ s->verbosity = v;
+ }
+
+ template <class T>
+ int MinisatCore<T>::nVars()
+ {return s->nVars();}
+
+ template <class T>
+ void MinisatCore<T>::printStats()
+ {
+ double cpu_time = Minisat::cpuTime();
+ double mem_used = Minisat::memUsedPeak();
+ printf("restarts : %"PRIu64"\n", s->starts);
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+ }
+
+
+ // I was going to make SimpSolver and Solver instances of this template.
+ // But I'm not so sure now because I don't understand what eliminate() does in the simp solver.
+ template class MinisatCore<Minisat::Solver>;
+};
--- /dev/null
+/*
+ * Wraps around CORE minisat.
+ */
+#ifndef MINISATCORE_H_
+#define MINIASTCORE_H_
+
+#include "SATSolver.h"
+
+namespace Minisat
+{
+ class Solver;
+}
+
+namespace BEEV
+{
+ template <class T>
+ class MinisatCore: public SATSolver
+ {
+ T * s;
+
+ public:
+ MinisatCore();
+
+ ~MinisatCore();
+
+ bool
+ addClause(const vec_literals& ps); // Add a clause to the solver.
+
+ bool
+ okay() const; // FALSE means solver is in a conflicting state
+
+
+ bool
+ solve(); // Search without assumptions.
+
+ bool
+ simplify(); // Removes already satisfied clauses.
+
+ virtual uint8_t modelValue(Var x) const;
+
+ virtual Var newVar();
+
+ int setVerbosity(int v);
+
+ int nVars();
+
+ void printStats();
+
+ virtual lbool true_literal() {return ((uint8_t)0);}
+ virtual lbool false_literal() {return ((uint8_t)1);}
+ virtual lbool undef_literal() {return ((uint8_t)2);}
+
+
+ };
+}
+;
+
+#endif
--- /dev/null
+#ifndef SATSOLVER_H_
+#define SATSOLVER_H_
+
+#include "mtl/Vec.h"
+#include "core/SolverTypes.h"
+
+// Don't let the defines escape outside.
+
+namespace BEEV
+{
+ class SATSolver
+ {
+ private:
+ SATSolver(const SATSolver&); // no copy
+ void operator=(const SATSolver &); // no assign.
+
+
+ public:
+
+ SATSolver(){}
+
+ virtual ~SATSolver(){}
+
+ class vec_literals : public Minisat::vec<Minisat::Lit>
+ {};
+
+ virtual bool
+ addClause(const vec_literals& ps)=0; // Add a clause to the solver.
+
+ virtual bool
+ okay() const=0; // FALSE means solver is in a conflicting state
+
+ virtual bool
+ solve()=0; // Search without assumptions.
+
+ typedef int Var;
+ typedef uint8_t lbool;
+
+ static inline Minisat::Lit mkLit (Var var, bool sign) { Minisat::Lit p; p.x = var + var + (int)sign; return p; }
+
+ virtual uint8_t modelValue (Var x) const = 0;
+
+ virtual Var newVar() =0;
+
+ virtual int nVars() =0;
+
+ virtual void printStats() = 0;
+
+ virtual void setSeed(int i)
+ {}
+
+ virtual int setVerbosity(int v) =0;
+
+ virtual lbool true_literal() =0;
+ virtual lbool false_literal() =0;
+ virtual lbool undef_literal() =0;
+
+ };
+};
+#endif
--- /dev/null
+#include "SimplifyingMinisat.h"
+#include "simp/SimpSolver.h"
+#include "utils/System.h"
+
+namespace BEEV
+{
+ SimplifyingMinisat::SimplifyingMinisat()
+ {
+ s = new Minisat::SimpSolver();
+ }
+
+ SimplifyingMinisat::~SimplifyingMinisat()
+ {
+ delete s;
+ }
+
+ bool
+ SimplifyingMinisat::addClause(const vec_literals& ps) // Add a clause to the solver.
+ {
+ s->addClause(ps);
+ }
+
+ bool
+ SimplifyingMinisat::okay() const // FALSE means solver is in a conflicting state
+ {
+ return s->okay();
+ }
+
+ bool
+ SimplifyingMinisat::solve() // Search without assumptions.
+ {
+ if (!s->simplify())
+ return false;
+
+ return s->solve();
+ }
+
+ bool
+ SimplifyingMinisat::simplify() // Removes already satisfied clauses.
+ {
+ return s->simplify();
+ }
+
+ uint8_t
+ SimplifyingMinisat::modelValue(Var x) const
+ {
+ return Minisat::toInt(s->modelValue(x));
+ }
+
+ int SimplifyingMinisat::setVerbosity(int v)
+ {
+ s->verbosity = v;
+ }
+
+ Minisat::Var
+ SimplifyingMinisat::newVar()
+ {
+ return s->newVar();
+ }
+
+ int SimplifyingMinisat::nVars()
+ {return s->nVars();}
+
+ void SimplifyingMinisat::printStats()
+ {
+#if 0
+ double cpu_time = Minisat::cpuTime();
+ double mem_used = Minisat::memUsedPeak();
+ printf("restarts : %"PRIu64"\n", s->starts);
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+
+#endif
+ }
+};
--- /dev/null
+/*
+ * Wraps around Simplifying minisat.
+ */
+#ifndef CORE_H_
+#define CORE_H_
+
+#include "SATSolver.h"
+
+namespace Minisat
+{
+ class SimpSolver;
+}
+
+namespace BEEV
+{
+ class SimplifyingMinisat : public SATSolver
+ {
+ Minisat::SimpSolver* s;
+
+ public:
+
+ SimplifyingMinisat();
+ ~SimplifyingMinisat();
+
+ bool
+ addClause(const vec_literals& ps); // Add a clause to the solver.
+
+ bool
+ okay() const; // FALSE means solver is in a conflicting state
+
+ bool
+ solve(); // Search without assumptions.
+
+ bool
+ simplify(); // Removes already satisfied clauses.
+
+ int setVerbosity(int v);
+
+ virtual uint8_t modelValue(Var x) const;
+
+ virtual Var newVar();
+
+ int nVars();
+
+ void printStats();
+
+ virtual lbool true_literal() {return ((uint8_t)0);}
+ virtual lbool false_literal() {return ((uint8_t)1);}
+ virtual lbool undef_literal() {return ((uint8_t)2);}
+
+ };
+}
+;
+
+#endif /* CORE_H_ */
--- /dev/null
+/****************************************************************************************[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 "../utils/ParseUtils.h"
+#include "../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) {
+ 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 (vars != S.nVars())
+ fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
+ if (cnt != clauses)
+ fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void parse_DIMACS(gzFile input_stream, Solver& S) {
+ StreamBuffer in(input_stream);
+ parse_DIMACS_main(in, S); }
+
+//=================================================================================================
+}
+
+#endif
--- /dev/null
+/*****************************************************************************************[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 <signal.h>
+#include <zlib.h>
+
+#include "../utils/System.h"
+#include "../utils/ParseUtils.h"
+#include "../utils/Options.h"
+#include "../core/Dimacs.h"
+#include "../core/Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+
+
+void printStats(Solver& solver)
+{
+ double cpu_time = cpuTime();
+ double mem_used = memUsedPeak();
+ printf("restarts : %"PRIu64"\n", solver.starts);
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+}
+
+
+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 signum) { 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 signum) {
+ printf("\n"); printf("*** INTERRUPTED ***\n");
+ if (solver->verbosity > 0){
+ printStats(*solver);
+ 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");
+ // printf("This is MiniSat 2.0 beta\n");
+
+#if defined(__linux__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+ // 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", INT32_MAX, IntRange(0, INT32_MAX));
+ IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
+
+ 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:
+ signal(SIGINT, SIGINT_exit);
+ signal(SIGXCPU,SIGINT_exit);
+
+ // Set limit on CPU-time:
+ if (cpu_lim != INT32_MAX){
+ rlimit rl;
+ getrlimit(RLIMIT_CPU, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
+ rl.rlim_cur = cpu_lim;
+ if (setrlimit(RLIMIT_CPU, &rl) == -1)
+ printf("WARNING! Could not set resource limit: CPU-time.\n");
+ } }
+
+ // Set limit on virtual memory:
+ if (mem_lim != INT32_MAX){
+ rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
+ rlimit rl;
+ getrlimit(RLIMIT_AS, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+ rl.rlim_cur = new_mem_lim;
+ if (setrlimit(RLIMIT_AS, &rl) == -1)
+ printf("WARNING! Could not set resource limit: Virtual memory.\n");
+ } }
+
+ 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);
+ 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:
+ signal(SIGINT, SIGINT_interrupt);
+ signal(SIGXCPU,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");
+ printStats(S);
+ printf("\n"); }
+ printf("UNSATISFIABLE\n");
+ exit(20);
+ }
+
+ vec<Lit> dummy;
+ lbool ret = S.solveLimited(dummy);
+ if (S.verbosity > 0){
+ printStats(S);
+ 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);
+ }
+}
-TOP = ../../..
-include $(TOP)/scripts/Makefile.common
+EXEC = minisat
+DEPDIR = mtl utils
+MROOT=..
-MTL = ../mtl
-SOURCES = Solver.C dlmalloc.c
-OBJECTS = Solver.o dlmalloc.o
-CFLAGS += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
-
-all: $(OBJECTS)
-
-clean:
- rm -f $(OBJECTS) $(LIB)
-
-.C.o:
- $(CC) $(CFLAGS) $< -o $@
+include $(MROOT)/mtl/template.mk
+++ /dev/null
-/****************************************************************************************[Solver.C]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 "Solver.h"
-#include "Sort.h"
-#include <cmath>
-
-namespace MINISAT {
-
-/// This creates a separate "memory space" for the clauses built by minisat. This
-/// stops the clauses being mixed in with the rest of STPs data (like ASTNodes).
-/// The memory spaces are separate heaps. More memory is used, but the SAT solver's
-/// clauses are all lumped together in memory so there are fewer data cache misses.
-#if 1
-mspace tlms =0;
-
-void* tlmalloc(size_t bytes) {
- if (tlms == 0) tlms = create_mspace(0, 0);
- return mspace_malloc(tlms, bytes);
- }
-
-void tlfree(void* mem) { mspace_free(tlms, mem); }
-#else
- void* tlmalloc(size_t bytes) { return malloc(bytes);}
- void tlfree(void* mem) { free(tlms); }
-#endif
-///
-
-
-//=================================================================================================
-// Constructor/Destructor:
-
-
-Solver::Solver() :
-
-// Parameters: (formerly in 'SearchParams')
-var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
-, restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
-
-
- // More parameters:
- //
- , expensive_ccmin (true)
- , polarity_mode (polarity_false)
- , verbosity (0)
-
- // Statistics: (formerly in 'SolverStats')
- //
- , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
- , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
- , ok (true)
- , cla_inc (1)
- , var_inc (1)
- , qhead (0)
- , simpDB_assigns (-1)
- , simpDB_props (0)
- , order_heap (VarOrderLt(activity))
- , random_seed (91648253)
- , progress_estimate(0)
- , remove_satisfied (true)
-{}
-
-
-Solver::~Solver()
-{
- for (int i = 0; i < learnts.size(); i++) tlfree(learnts[i]);
- for (int i = 0; i < clauses.size(); i++) tlfree(clauses[i]);
-}
-
-
-//=================================================================================================
-// Minor methods:
-
-
-// Creates a new SAT variable in the solver. If 'decision_var' 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(bool sign, bool dvar)
-{
- int v = nVars();
- watches .push(); // (list for positive literal)
- watches .push(); // (list for negative literal)
- reason .push(NULL);
- assigns .push(toInt(l_Undef));
- level .push(-1);
- activity .push(0);
- seen .push(0);
-
- polarity .push((char)sign);
- decision_var.push((char)dvar);
-
- insertVarOrder(v);
- return v;
-}
-
-
-bool Solver::addClause(vec<Lit>& ps)
-{
- assert(decisionLevel() == 0);
-
- if (!ok)
- return false;
- else{
- // 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){
- assert(value(ps[0]) == l_Undef);
- uncheckedEnqueue(ps[0]);
- return ok = (propagate() == NULL);
- }else{
- Clause* c = Clause_new(ps, false);
- clauses.push(c);
- attachClause(*c);
- }
-
- return true;
-}
-
-
-void Solver::attachClause(Clause& c) {
- assert(c.size() > 1);
- watches[toInt(~c[0])].push(&c);
- watches[toInt(~c[1])].push(&c);
- if (c.learnt()) learnts_literals += c.size();
- else clauses_literals += c.size(); }
-
-
-void Solver::detachClause(Clause& c) {
- assert(c.size() > 1);
- assert(find(watches[toInt(~c[0])], &c));
- assert(find(watches[toInt(~c[1])], &c));
- remove(watches[toInt(~c[0])], &c);
- remove(watches[toInt(~c[1])], &c);
- if (c.learnt()) learnts_literals -= c.size();
- else clauses_literals -= c.size(); }
-
-
-void Solver::removeClause(Clause& c) {
- detachClause(c);
- tlfree(&c); }
-
-
-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] = toInt(l_Undef);
- 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(int polarity_mode, double random_var_freq)
-{
- 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 (toLbool(assigns[next]) == l_Undef && decision_var[next])
- rnd_decisions++; }
-
- // Activity based decision:
- while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next])
- if (order_heap.empty()){
- next = var_Undef;
- break;
- }else
- next = order_heap.removeMin();
-
- bool sign = false;
- switch (polarity_mode){
- case polarity_true: sign = false; break;
- case polarity_false: sign = true; break;
- case polarity_user: sign = polarity[next]; break;
- case polarity_rnd: sign = irand(random_seed, 2); break;
- default: assert(false); }
-
- return next == var_Undef ? lit_Undef : Lit(next, sign);
-}
-
-/*_________________________________________________________________________________________________
-|
-| 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'.
-|
-| Effect:
-| Will undo part of the trail, upto but not beyond the assumption of the current decision level.
-|________________________________________________________________________________________________@*/
-void Solver::analyze(Clause* 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;
- out_btlevel = 0;
-
- do{
- assert(confl != NULL); // (otherwise should be UIP)
- Clause& c = *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);
- if (level[var(q)] > out_btlevel)
- out_btlevel = level[var(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;
- if (expensive_ccmin){
- uint32_t abstract_level = 0;
- for (i = 1; i < out_learnt.size(); i++)
- abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
-
- out_learnt.copyTo(analyze_toclear);
- for (i = j = 1; i < out_learnt.size(); i++)
- if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level))
- out_learnt[j++] = out_learnt[i];
- }else{
- out_learnt.copyTo(analyze_toclear);
- for (i = j = 1; i < out_learnt.size(); i++){
- Clause& c = *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; }
- }
- }
- 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;
- for (int i = 2; i < out_learnt.size(); i++)
- if (level[var(out_learnt[i])] > level[var(out_learnt[max_i])])
- max_i = i;
- 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. 'abstract_levels' is used to abort early if the algorithm is
-// visiting literals at levels that cannot be removed later.
-bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
-{
- analyze_stack.clear(); analyze_stack.push(p);
- int top = analyze_toclear.size();
- while (analyze_stack.size() > 0){
- assert(reason[var(analyze_stack.last())] != NULL);
- Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
-
- for (int i = 1; i < c.size(); i++){
- Lit p = c[i];
- if (!seen[var(p)] && level[var(p)] > 0){
- if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
- seen[var(p)] = 1;
- analyze_stack.push(p);
- analyze_toclear.push(p);
- }else{
- for (int j = top; j < analyze_toclear.size(); j++)
- seen[var(analyze_toclear[j])] = 0;
- analyze_toclear.shrink(analyze_toclear.size() - top);
- return false;
- }
- }
- }
- }
-
- 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, vec<Lit>& out_conflict)
-{
- out_conflict.clear();
- out_conflict.push(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] == NULL){
- assert(level[x] > 0);
- out_conflict.push(~trail[i]);
- }else{
- Clause& c = *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, Clause* from)
-{
- assert(value(p) == l_Undef);
- assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient
- level [var(p)] = decisionLevel();
- reason [var(p)] = from;
- trail.push(p);
-}
-
-
-/*_________________________________________________________________________________________________
-|
-| propagate : [void] -> [Clause*]
-|
-| Description:
-| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
-| otherwise NULL.
-|
-| Post-conditions:
-| * the propagation queue is empty, even if there was a conflict.
-|________________________________________________________________________________________________@*/
-Clause* Solver::propagate()
-{
- Clause* confl = NULL;
- int num_props = 0;
-
- while (qhead < trail.size()){
- Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
- vec<Clause*>& ws = watches[toInt(p)];
- Clause **i, **j, **end;
- num_props++;
-
- for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){
- Clause& c = **i++;
-
- // Make sure the false literal is data[1]:
- Lit false_lit = ~p;
- if (c[0] == false_lit)
- c[0] = c[1], c[1] = false_lit;
-
- assert(c[1] == false_lit);
-
- // If 0th watch is true, then clause is already satisfied.
- Lit first = c[0];
- if (value(first) == l_True){
- *j++ = &c;
- }else{
- // 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[toInt(~c[1])].push(&c);
- goto FoundWatch; }
-
- // Did not find watch -- clause is unit under assignment:
- *j++ = &c;
- if (value(first) == l_False){
- confl = &c;
- qhead = trail.size();
- // Copy the remaining watches:
- while (i < end)
- *j++ = *i++;
- }else
- uncheckedEnqueue(first, &c);
- }
- FoundWatch:;
- }
- 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 { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < 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());
- for (i = j = 0; i < learnts.size() / 2; i++){
- if (learnts[i]->size() > 2 && !locked(*learnts[i]))
- removeClause(*learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
- for (; i < learnts.size(); i++){
- if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
- removeClause(*learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
- learnts.shrink(i - j);
-}
-
-
-void Solver::removeSatisfied(vec<Clause*>& cs)
-{
- int i,j;
- for (i = j = 0; i < cs.size(); i++){
- if (satisfied(*cs[i]))
- removeClause(*cs[i]);
- else
- cs[j++] = cs[i];
- }
- cs.shrink(i - j);
-}
-
-
-/*_________________________________________________________________________________________________
-|
-| 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() != NULL)
- 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);
-
- // Remove fixed variables from the variable heap:
- order_heap.filter(VarFilter(*this));
-
- 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) (nof_learnts : int) (params : const SearchParams&) -> [lbool]
-|
-| Description:
-| Search for a model the specified number of conflicts, keeping the number of learnt clauses
-| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
-| 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, int nof_learnts)
-{
- assert(ok);
- int backtrack_level;
- int conflictC = 0;
- vec<Lit> learnt_clause;
-
- starts++;
-
- bool first = true;
-
- for (;;){
- Clause* confl = propagate();
- if (confl != NULL){
- // CONFLICT
- conflicts++; conflictC++;
- if (decisionLevel() == 0) return l_False;
-
- first = false;
-
- learnt_clause.clear();
- analyze(confl, learnt_clause, backtrack_level);
- cancelUntil(backtrack_level);
- assert(value(learnt_clause[0]) == l_Undef);
-
- if (learnt_clause.size() == 1){
- uncheckedEnqueue(learnt_clause[0]);
- }else{
- Clause* c = Clause_new(learnt_clause, true);
- learnts.push(c);
- attachClause(*c);
- claBumpActivity(*c);
- uncheckedEnqueue(learnt_clause[0], c);
- }
-
- varDecayActivity();
- claDecayActivity();
-
- }else{
- // NO CONFLICT
-
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
- // 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 (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_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(polarity_mode, random_var_freq);
-
- if (next == lit_Undef){
-
- // Model found:
- return l_True;
- }
-
- }
-
- // Increase decision level and enqueue 'next'
- assert(value(next) == l_Undef);
- 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();
-}
-
-
-bool Solver::solve(const vec<Lit>& assumps)
-{
- model.clear();
- conflict.clear();
-
- if (!ok) return false;
-
- assumps.copyTo(assumptions);
-
- double nof_conflicts = restart_first;
- double nof_learnts = nClauses() * learntsize_factor;
- lbool status = l_Undef;
-
- if (verbosity >= 1){
- reportf("============================[ Search Statistics ]==============================\n");
- reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
- reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
- reportf("===============================================================================\n");
- }
-
- // Search:
- while (status == l_Undef){
- if (verbosity >= 1)
- reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout);
- status = search((int)nof_conflicts, (int)nof_learnts);
- nof_conflicts *= restart_inc;
- nof_learnts *= learntsize_inc;
- }
-
- if (verbosity >= 1)
- reportf("===============================================================================\n");
-
-
- if (status == l_True){
- // Extend & copy model:
- model.growTo(nVars());
- for (int i = 0; i < nVars(); i++) model[i] = value(i);
-#ifndef NDEBUG
- verifyModel();
-#endif
- }else{
- assert(status == l_False);
- if (conflict.size() == 0)
- ok = false;
- }
-
- cancelUntil(0);
- return status == l_True;
-}
-
-
-//=================================================================================================
-// Debug methods:
-
-
-void Solver::verifyModel()
-{
- bool failed = false;
- for (int i = 0; i < clauses.size(); i++){
- assert(clauses[i]->mark() == 0);
- Clause& c = *clauses[i];
- for (int j = 0; j < c.size(); j++)
- if (modelValue(c[j]) == l_True)
- goto next;
-
- reportf("unsatisfied clause: ");
- printClause(*clauses[i]);
- reportf("\n");
- failed = true;
- next:;
- }
-
- assert(!failed);
-
- //reportf("Verified %d original clauses.\n", clauses.size());
-}
-
-
-void Solver::checkLiteralCount()
-{
- // Check that sizes are calculated correctly:
- int cnt = 0;
- for (int i = 0; i < clauses.size(); i++)
- if (clauses[i]->mark() == 0)
- cnt += clauses[i]->size();
-
- if ((int)clauses_literals != cnt){
- fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt);
- assert((int)clauses_literals == cnt);
- }
-}
-
-};
--- /dev/null
+/***************************************************************************************[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 "../mtl/Sort.h"
+#include "../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));
+
+
+//=================================================================================================
+// 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)
+ , 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), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+
+ , ok (true)
+ , cla_inc (1)
+ , var_inc (1)
+ , watches (WatcherDeleted(ca))
+ , qhead (0)
+ , simpDB_assigns (-1)
+ , simpDB_props (0)
+ , order_heap (VarOrderLt(activity))
+ , progress_estimate (0)
+ , remove_satisfied (true)
+
+ // 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(bool sign, bool dvar)
+{
+ int v = nVars();
+ watches .init(mkLit(v, false));
+ watches .init(mkLit(v, true ));
+ assigns .push(l_Undef);
+ vardata .push(mkVarData(CRef_Undef, 0));
+ //activity .push(0);
+ activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
+ seen .push(0);
+ polarity .push(sign);
+ decision .push();
+ trail .capacity(v+1);
+ setDecisionVar(v, dvar);
+ return v;
+}
+
+
+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()) learnts_literals += c.size();
+ else clauses_literals += c.size(); }
+
+
+void Solver::detachClause(CRef cr, bool strict) {
+ const Clause& c = ca[cr];
+ assert(c.size() > 1);
+
+ if (strict){
+ remove(watches[~c[0]], Watcher(cr, c[1]));
+ remove(watches[~c[1]], Watcher(cr, c[0]));
+ }else{
+ // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
+ watches.smudge(~c[0]);
+ watches.smudge(~c[1]);
+ }
+
+ if (c.learnt()) learnts_literals -= c.size();
+ else 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();
+
+ return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : 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){
+ uint32_t abstract_level = 0;
+ for (i = 1; i < out_learnt.size(); i++)
+ abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
+
+ for (i = j = 1; i < out_learnt.size(); i++)
+ if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
+ 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. 'abstract_levels' is used to abort early if the algorithm is
+// visiting literals at levels that cannot be removed later.
+bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
+{
+ analyze_stack.clear(); analyze_stack.push(p);
+ int top = analyze_toclear.size();
+ while (analyze_stack.size() > 0){
+ assert(reason(var(analyze_stack.last())) != CRef_Undef);
+ Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
+
+ for (int i = 1; i < c.size(); i++){
+ Lit p = c[i];
+ if (!seen[var(p)] && level(var(p)) > 0){
+ if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
+ seen[var(p)] = 1;
+ analyze_stack.push(p);
+ analyze_toclear.push(p);
+ }else{
+ for (int j = top; j < analyze_toclear.size(); j++)
+ seen[var(analyze_toclear[j])] = 0;
+ analyze_toclear.shrink(analyze_toclear.size() - top);
+ return false;
+ }
+ }
+ }
+ }
+
+ 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, vec<Lit>& out_conflict)
+{
+ out_conflict.clear();
+ out_conflict.push(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.push(~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;
+ watches.cleanAll();
+
+ while (qhead < trail.size()){
+ Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
+ vec<Watcher>& ws = watches[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
+ 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);
+ 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;
+ 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;
+}
+
+//=================================================================================================
+// 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 += assumptions.size();
+
+ fprintf(f, "p cnf %d %d\n", max, cnt);
+
+ for (int i = 0; i < assumptions.size(); i++){
+ assert(value(assumptions[i]) != l_False);
+ fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
+ }
+
+ for (int i = 0; i < clauses.size(); i++)
+ toDimacs(f, ca[clauses[i]], map, max);
+
+ if (verbosity > 0)
+ printf("Wrote %d clauses with %d variables.\n", cnt, max);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+void Solver::relocAll(ClauseAllocator& to)
+{
+ // All watchers:
+ //
+ // for (int i = 0; i < watches.size(); i++)
+ watches.cleanAll();
+ for (int v = 0; v < nVars(); v++)
+ for (int s = 0; s < 2; s++){
+ Lit p = mkLit(v, s);
+ // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
+ 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]);
+
+ if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
+ ca.reloc(vardata[v].reason, to);
+ }
+
+ // All learnt:
+ //
+ for (int i = 0; i < learnts.size(); i++)
+ ca.reloc(learnts[i], to);
+
+ // All original:
+ //
+ for (int i = 0; i < clauses.size(); i++)
+ ca.reloc(clauses[i], to);
+}
+
+
+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);
+}
/****************************************************************************************[Solver.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Solver_h
-#define Solver_h
+#ifndef Minisat_Solver_h
+#define Minisat_Solver_h
-#include <cstdio>
-
-#include "../mtl/Map.h"
#include "../mtl/Vec.h"
#include "../mtl/Heap.h"
#include "../mtl/Alg.h"
-
-#include "SolverTypes.h"
-
-#ifdef _MSC_VER
- #include <ctime>
-#else
- #include <sys/time.h>
- #include <sys/resource.h>
- #include <unistd.h>
-#endif
-
-namespace MINISAT {
-
-/*************************************************************************************/
-#ifdef _MSC_VER
-
-static inline double cpuTime(void) {
- return (double)clock() / CLOCKS_PER_SEC; }
-#else
-
-static inline double cpuTime(void) {
- struct rusage ru;
- getrusage(RUSAGE_SELF, &ru);
- return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
-#endif
-
-
-#if defined(__linux__)
-static inline int memReadStat(int field)
-{
- char name[256];
- pid_t pid = getpid();
- sprintf(name, "/proc/%d/statm", pid);
- FILE* in = fopen(name, "rb");
- if (in == NULL) return 0;
- int value;
- for (; field >= 0; field--)
- fscanf(in, "%d", &value);
- fclose(in);
- return value;
-}
-static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); }
-
-
-#elif defined(__FreeBSD__)
-static inline uint64_t memUsed(void) {
- struct rusage ru;
- getrusage(RUSAGE_SELF, &ru);
- return ru.ru_maxrss*1024; }
+#include "../utils/Options.h"
+#include "../core/SolverTypes.h"
-#else
-static inline uint64_t memUsed() { return 0; }
-#endif
-
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
+namespace Minisat {
//=================================================================================================
// Solver -- the main class:
-
class Solver {
- friend class DPLLMgr;
public:
// Constructor/Destructor:
// Problem specification:
//
- virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
- virtual bool addClause (vec<Lit>& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+ Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+ 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_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will
+ // change the passed vector 'ps'.
// Solving:
//
- virtual bool simplify (); // Removes already satisfied clauses.
+ bool simplify (); // Removes already satisfied clauses.
bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
- virtual bool solve (); // Search without 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
+ void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
+ void toDimacs (const char *file, const vec<Lit>& assumps);
+ void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
+
+ // Convenience versions of 'toDimacs()':
+ void toDimacs (const char* file);
+ void toDimacs (const char* file, Lit p);
+ void toDimacs (const char* file, Lit p, Lit q);
+ void toDimacs (const char* file, Lit p, Lit q, Lit r);
+
// Variable mode:
//
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
//
lbool value (Var x) const; // The current value of a variable.
lbool value (Lit p) const; // The current value of a literal.
+ lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
int nAssigns () const; // The current number of assigned literals.
int nClauses () const; // The current number of original clauses.
int nLearnts () const; // The current number of learnt clauses.
int nVars () const; // The current number of variables.
+ int nFreeVars () const;
+
+ // Resource contraints:
+ //
+ void setConfBudget(int64_t x);
+ void setPropBudget(int64_t x);
+ void budgetOff();
+ void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
+ void clearInterrupt(); // Clear interrupt indicator flag.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+ void checkGarbage(double gf);
+ void checkGarbage();
// Extra results: (read-only member variable)
//
// Mode of operation:
//
- double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95)
- double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999)
- double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02)
+ int verbosity;
+ double var_decay;
+ double clause_decay;
+ double random_var_freq;
+ double random_seed;
+ bool luby_restart;
+ int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
+ int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
+ bool rnd_pol; // Use random polarities for branching heuristics.
+ bool rnd_init_act; // Initialize variable activities with a small random value.
+ double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
+
int restart_first; // The initial restart limit. (default 100)
double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
- bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE)
- int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false)
- int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0)
- enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
+ int learntsize_adjust_start_confl;
+ double learntsize_adjust_inc;
// Statistics: (read-only member variable)
//
- uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
- uint64_t clauses_literals, learnts_literals, max_literals, tot_literals;
+ uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+ uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
protected:
// Helper structures:
//
+ struct VarData { CRef reason; int level; };
+ static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
+
+ struct Watcher {
+ CRef cref;
+ Lit blocker;
+ Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
+ bool operator==(const Watcher& w) const { return cref == w.cref; }
+ bool operator!=(const Watcher& w) const { return cref != w.cref; }
+ };
+
+ struct WatcherDeleted
+ {
+ const ClauseAllocator& ca;
+ WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+ bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
+ };
+
struct VarOrderLt {
const vec<double>& activity;
bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
VarOrderLt(const vec<double>& act) : activity(act) { }
};
- friend class VarFilter;
- struct VarFilter {
- const Solver& s;
- VarFilter(const Solver& _s) : s(_s) {}
- bool operator()(Var v) const { return toLbool(s.assigns[v]) == l_Undef && s.decision_var[v]; }
- };
-
// Solver state:
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
- vec<Clause*> clauses; // List of problem clauses.
- vec<Clause*> learnts; // List of learnt clauses.
+ vec<CRef> clauses; // List of problem clauses.
+ vec<CRef> learnts; // List of learnt clauses.
double cla_inc; // Amount to bump next clause with.
vec<double> activity; // A heuristic measurement of the activity of a variable.
double var_inc; // Amount to bump next variable with.
- vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
- vec<char> assigns; // The current assignments (lbool:s stored as char:s).
+ OccLists<Lit, vec<Watcher>, WatcherDeleted>
+ watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+ vec<lbool> assigns; // The current assignments.
vec<char> polarity; // The preferred polarity of each variable.
- vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
+ vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
- vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
- vec<int> level; // 'level[var]' contains the level at which the assignment was made.
+ vec<VarData> vardata; // Stores reason and level for each variable.
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
- double random_seed; // Used by the random variable selection.
double progress_estimate;// Set by 'search()'.
bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
+ ClauseAllocator ca;
// Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
// used, exept 'seen' wich is used in several places.
vec<Lit> analyze_toclear;
vec<Lit> add_tmp;
+ double max_learnts;
+ double learntsize_adjust_confl;
+ int learntsize_adjust_cnt;
+
+ // Resource contraints:
+ //
+ int64_t conflict_budget; // -1 means no budget.
+ int64_t propagation_budget; // -1 means no budget.
+ bool asynch_interrupt;
+
// Main internal methods:
//
void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
- Lit pickBranchLit (int polarity_mode, double random_var_freq); // Return the next decision variable.
+ Lit pickBranchLit (); // Return the next decision variable.
void newDecisionLevel (); // Begins a new decision level.
- void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined.
- bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise.
- Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause.
+ void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
+ bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
+ CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
void cancelUntil (int level); // Backtrack until a certain level.
- void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+ void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
- lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts.
+ lbool search (int nof_conflicts); // Search for a given number of conflicts.
+ lbool solve_ (); // Main solve method (assumptions given in 'assumptions').
void reduceDB (); // Reduce the set of learnt clauses.
- void removeSatisfied (vec<Clause*>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
+ void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
+ void rebuildOrderHeap ();
// Maintaining Variable/Clause activity:
//
void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
+ void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
// Operations on clauses:
//
- void attachClause (Clause& c); // Attach a clause to watcher lists.
- void detachClause (Clause& c); // Detach a clause to watcher lists.
- void removeClause (Clause& c); // Detach and free a clause.
+ void attachClause (CRef cr); // Attach a clause to watcher lists.
+ void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
+ void removeClause (CRef cr); // Detach and free a clause.
bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
+ void relocAll (ClauseAllocator& to);
+
// Misc:
//
int decisionLevel () const; // Gives the current decisionlevel.
uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
+ CRef reason (Var x) const;
+ int level (Var x) const;
double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
-
- // Debug:
- void printLit (Lit l);
- template<class C>
- void printClause (const C& c);
- void verifyModel ();
- void checkLiteralCount();
+ bool withinBudget () const;
// Static helpers:
//
//=================================================================================================
// Implementation of inline methods:
+inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
+inline int Solver::level (Var x) const { return vardata[x].level; }
+
inline void Solver::insertVarOrder(Var x) {
- if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
+ if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
-inline void Solver::varDecayActivity() { var_inc *= var_decay; }
-inline void Solver::varBumpActivity(Var v) {
- if ( (activity[v] += var_inc) > 1e100 ) {
+inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
+inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
+inline void Solver::varBumpActivity(Var v, double inc) {
+ if ( (activity[v] += inc) > 1e100 ) {
// Rescale:
for (int i = 0; i < nVars(); i++)
activity[i] *= 1e-100;
if (order_heap.inHeap(v))
order_heap.decrease(v); }
-inline void Solver::claDecayActivity() { cla_inc *= clause_decay; }
+inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
inline void Solver::claBumpActivity (Clause& c) {
if ( (c.activity() += cla_inc) > 1e20 ) {
// Rescale:
for (int i = 0; i < learnts.size(); i++)
- learnts[i]->activity() *= 1e-20;
+ ca[learnts[i]].activity() *= 1e-20;
cla_inc *= 1e-20; } }
-inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
-inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
+inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
+inline void Solver::checkGarbage(double gf){
+ if (ca.wasted() > ca.size() * gf)
+ garbageCollect(); }
+
+// NOTE: enqueue does not set the ok flag! (only public methods do)
+inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
+inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
-inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); }
-inline lbool Solver::value (Var x) const { return toLbool(assigns[x]); }
-inline lbool Solver::value (Lit p) const { return toLbool(assigns[var(p)]) ^ sign(p); }
+inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
+inline lbool Solver::value (Var x) const { return assigns[x]; }
+inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
+inline lbool Solver::modelValue (Var x) const { return model[x]; }
inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
inline int Solver::nAssigns () const { return trail.size(); }
inline int Solver::nClauses () const { return clauses.size(); }
inline int Solver::nLearnts () const { return learnts.size(); }
-inline int Solver::nVars () const { return assigns.size(); }
-inline void Solver::setPolarity (Var v, bool b) { polarity [v] = (char)b; }
-inline void Solver::setDecisionVar(Var v, bool b) { decision_var[v] = (char)b; if (b) { insertVarOrder(v); } }
-inline bool Solver::solve () { vec<Lit> tmp; return solve(tmp); }
+inline int Solver::nVars () const { return vardata.size(); }
+inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
+inline void Solver::setDecisionVar(Var v, bool b)
+{
+ if ( b && !decision[v]) dec_vars++;
+ else if (!b && decision[v]) dec_vars--;
+
+ decision[v] = b;
+ insertVarOrder(v);
+}
+inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
+inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
+inline void Solver::interrupt(){ asynch_interrupt = true; }
+inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
+inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
+inline bool Solver::withinBudget() const {
+ return !asynch_interrupt &&
+ (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+ (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+
+// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
+// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
+// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
+inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
+inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
+inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
+inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
+inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
+inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
inline bool Solver::okay () const { return ok; }
+inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
//=================================================================================================
-// Debug + etc:
+// Debug etc:
-#define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
-
-static inline void logLit(FILE* f, Lit l)
-{
- fprintf(f, "%sx%d", sign(l) ? "~" : "", var(l)+1);
-}
-
-static inline void logLits(FILE* f, const vec<Lit>& ls)
-{
- fprintf(f, "[ ");
- if (ls.size() > 0){
- logLit(f, ls[0]);
- for (int i = 1; i < ls.size(); i++){
- fprintf(f, ", ");
- logLit(f, ls[i]);
- }
- }
- fprintf(f, "] ");
-}
-
-static inline const char* showBool(bool b) { return b ? "true" : "false"; }
-
-
-// Just like 'assert()' but expression will be evaluated in the release version as well.
-static inline void check(bool expr) { assert(expr); }
-
-
-inline void Solver::printLit(Lit l)
-{
- reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
-}
-
-
-template<class C>
-inline void Solver::printClause(const C& c)
-{
- for (int i = 0; i < c.size(); i++){
- printLit(c[i]);
- fprintf(stderr, " ");
- }
+//=================================================================================================
}
-};
-
#endif
/***********************************************************************************[SolverTypes.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+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,
**************************************************************************************************/
-#ifndef SolverTypes_h
-#define SolverTypes_h
+#ifndef Minisat_SolverTypes_h
+#define Minisat_SolverTypes_h
-#include <cassert>
-#include <stdint.h>
-#define ONLY_MSPACES 1
-#include "dlmalloc.h"
+#include <assert.h>
-namespace MINISAT{
+#include "../mtl/IntTypes.h"
+#include "../mtl/Alg.h"
+#include "../mtl/Vec.h"
+#include "../mtl/Map.h"
+#include "../mtl/Alloc.h"
-void* tlmalloc(size_t bytes);
-void tlfree(void* mem);
+namespace Minisat {
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
#define var_Undef (-1)
-class Lit {
+struct Lit {
int x;
- public:
- Lit() : x(2*var_Undef) { } // (lit_Undef)
- explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { }
-
- // Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
- friend int toInt (Lit p); // Guarantees small, positive integers suitable for array indexing.
- friend Lit toLit (int i); // Inverse of 'toInt()'
- friend Lit operator ~(Lit p);
- friend bool sign (Lit p);
- friend int var (Lit p);
- friend Lit unsign (Lit p);
- friend Lit id (Lit p, bool sgn);
+
+ // Use this as a constructor:
+ friend Lit mkLit(Var var, bool sign = false);
bool operator == (Lit p) const { return x == p.x; }
bool operator != (Lit p) const { return x != p.x; }
- bool operator < (Lit p) const { return x < p.x; } // '<' guarantees that p, ~p are adjacent in the ordering.
+ bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
};
-inline int toInt (Lit p) { return p.x; }
-inline Lit toLit (int i) { Lit p; p.x = i; return p; }
-inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
-inline bool sign (Lit p) { return p.x & 1; }
-inline int var (Lit p) { return p.x >> 1; }
-inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; }
-inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
-const Lit lit_Undef(var_Undef, false); // }- Useful special constants.
-const Lit lit_Error(var_Undef, true ); // }
+inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+inline bool sign (Lit p) { return p.x & 1; }
+inline int var (Lit p) { return p.x >> 1; }
+
+// Mapping Literals to and from compact integers suitable for array indexing:
+inline int toInt (Var v) { return v; }
+inline int toInt (Lit p) { return p.x; }
+inline Lit toLit (int i) { Lit p; p.x = i; return p; }
+
+//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
+//const Lit lit_Error = mkLit(var_Undef, true ); // }
+
+const Lit lit_Undef = { -2 }; // }- Useful special constants.
+const Lit lit_Error = { -1 }; // }
//=================================================================================================
// Lifted booleans:
+//
+// NOTE: this implementation is optimized for the case when comparisons between values are mostly
+// between one variable and one constant. Some care had to be taken to make sure that gcc
+// does enough constant propagation to produce sensible code, and this appears to be somewhat
+// fragile unfortunately.
+#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+#define l_False (lbool((uint8_t)1))
+#define l_Undef (lbool((uint8_t)2))
class lbool {
- char value;
- explicit lbool(int v) : value(v) { }
+ uint8_t value;
public:
+ explicit lbool(uint8_t v) : value(v) { }
+
lbool() : value(0) { }
- lbool(bool x) : value((int)x*2-1) { }
- int toInt(void) const { return value; }
+ explicit lbool(bool x) : value(!x) { }
+
+ bool operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
+ bool operator != (lbool b) const { return !(*this == b); }
+ lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
+
+ lbool operator && (lbool b) const {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xF7F755F4 >> sel) & 3;
+ return lbool(v); }
- bool operator == (lbool b) const { return value == b.value; }
- bool operator != (lbool b) const { return value != b.value; }
- lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); }
+ lbool operator || (lbool b) const {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xFCFCF400 >> sel) & 3;
+ return lbool(v); }
friend int toInt (lbool l);
friend lbool toLbool(int v);
};
-inline int toInt (lbool l) { return l.toInt(); }
-inline lbool toLbool(int v) { return lbool(v); }
-
-const lbool l_True = toLbool( 1);
-const lbool l_False = toLbool(-1);
-const lbool l_Undef = toLbool( 0);
+inline int toInt (lbool l) { return l.value; }
+inline lbool toLbool(int v) { return lbool((uint8_t)v); }
//=================================================================================================
// Clause -- a simple class for representing a clause:
+class Clause;
+typedef RegionAllocator<uint32_t>::Ref CRef;
class Clause {
- uint32_t size_etc;
- union { float act; uint32_t abst; } extra;
- Lit data[0];
+ struct {
+ unsigned mark : 2;
+ unsigned learnt : 1;
+ unsigned has_extra : 1;
+ unsigned reloced : 1;
+ unsigned size : 27; } header;
+ union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+
+ friend class ClauseAllocator;
+
+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+ template<class V>
+ Clause(const V& ps, bool use_extra, bool learnt) {
+ header.mark = 0;
+ header.learnt = learnt;
+ header.has_extra = use_extra;
+ header.reloced = 0;
+ header.size = ps.size();
+
+ for (int i = 0; i < ps.size(); i++)
+ data[i].lit = ps[i];
+
+ if (header.has_extra){
+ if (header.learnt)
+ data[header.size].act = 0;
+ else
+ calcAbstraction(); }
+ }
public:
void calcAbstraction() {
+ assert(header.has_extra);
uint32_t abstraction = 0;
for (int i = 0; i < size(); i++)
- abstraction |= 1 << (var(data[i]) & 31);
- extra.abst = abstraction; }
+ abstraction |= 1 << (var(data[i].lit) & 31);
+ data[header.size].abs = abstraction; }
- // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
- template<class V>
- Clause(const V& ps, bool learnt) {
- size_etc = (ps.size() << 3) | (uint32_t)learnt;
- for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
- if (learnt) extra.act = 0; else calcAbstraction(); }
- // -- use this function instead:
- template<class V>
- friend Clause* Clause_new(const V& ps, bool learnt = false) {
- assert(sizeof(Lit) == sizeof(uint32_t));
- assert(sizeof(float) == sizeof(uint32_t));
- void* mem = tlmalloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
- return new (mem) Clause(ps, learnt); }
-
- int size () const { return size_etc >> 3; }
- void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
+ int size () const { return header.size; }
+ void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
void pop () { shrink(1); }
- bool learnt () const { return size_etc & 1; }
- uint32_t mark () const { return (size_etc >> 1) & 3; }
- void mark (uint32_t m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); }
- const Lit& last () const { return data[size()-1]; }
+ bool learnt () const { return header.learnt; }
+ bool has_extra () const { return header.has_extra; }
+ uint32_t mark () const { return header.mark; }
+ void mark (uint32_t m) { header.mark = m; }
+ const Lit& last () const { return data[header.size-1].lit; }
+
+ bool reloced () const { return header.reloced; }
+ CRef relocation () const { return data[0].rel; }
+ void relocate (CRef c) { header.reloced = 1; data[0].rel = c; }
// NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
// subsumption operations to behave correctly.
- Lit& operator [] (int i) { return data[i]; }
- Lit operator [] (int i) const { return data[i]; }
- operator const Lit* (void) const { return data; }
+ Lit& operator [] (int i) { return data[i].lit; }
+ Lit operator [] (int i) const { return data[i].lit; }
+ operator const Lit* (void) const { return (Lit*)data; }
- float& activity () { return extra.act; }
- uint32_t abstraction () const { return extra.abst; }
+ float& activity () { assert(header.has_extra); return data[header.size].act; }
+ uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
Lit subsumes (const Clause& other) const;
void strengthen (Lit p);
};
+//=================================================================================================
+// ClauseAllocator -- a simple class for allocating memory for clauses:
+
+
+const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
+class ClauseAllocator : public RegionAllocator<uint32_t>
+{
+ static int clauseWord32Size(int size, bool has_extra){
+ return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
+ public:
+ bool extra_clause_field;
+
+ ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
+ ClauseAllocator() : extra_clause_field(false){}
+
+ void moveTo(ClauseAllocator& to){
+ to.extra_clause_field = extra_clause_field;
+ RegionAllocator<uint32_t>::moveTo(to); }
+
+ template<class Lits>
+ CRef alloc(const Lits& ps, bool learnt = false)
+ {
+ assert(sizeof(Lit) == sizeof(uint32_t));
+ assert(sizeof(float) == sizeof(uint32_t));
+ bool use_extra = learnt | extra_clause_field;
+
+ CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
+ new (lea(cid)) Clause(ps, use_extra, learnt);
+
+ return cid;
+ }
+
+ // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+ Clause& operator[](Ref r) { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
+ const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
+ Clause* lea (Ref r) { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
+ const Clause* lea (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
+ Ref ael (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
+
+ void free(CRef cid)
+ {
+ Clause& c = operator[](cid);
+ RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
+ }
+
+ void reloc(CRef& cr, ClauseAllocator& to)
+ {
+ Clause& c = operator[](cr);
+
+ if (c.reloced()) { cr = c.relocation(); return; }
+
+ cr = to.alloc(c, c.learnt());
+ c.relocate(cr);
+
+ // Copy extra data-fields:
+ // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
+ to[cr].mark(c.mark());
+ if (to[cr].learnt()) to[cr].activity() = c.activity();
+ else if (to[cr].has_extra()) to[cr].calcAbstraction();
+ }
+};
+
+
+//=================================================================================================
+// OccLists -- a class for maintaining occurence lists with lazy deletion:
+
+template<class Idx, class Vec, class Deleted>
+class OccLists
+{
+ vec<Vec> occs;
+ vec<char> dirty;
+ vec<Idx> dirties;
+ Deleted deleted;
+
+ public:
+ OccLists(const Deleted& d) : deleted(d) {}
+
+ void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
+ // Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
+ Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
+ Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
+
+ void cleanAll ();
+ void clean (const Idx& idx);
+ void smudge (const Idx& idx){
+ if (dirty[toInt(idx)] == 0){
+ dirty[toInt(idx)] = 1;
+ dirties.push(idx);
+ }
+ }
+
+ void clear(bool free = true){
+ occs .clear(free);
+ dirty .clear(free);
+ dirties.clear(free);
+ }
+};
+
+
+template<class Idx, class Vec, class Deleted>
+void OccLists<Idx,Vec,Deleted>::cleanAll()
+{
+ for (int i = 0; i < dirties.size(); i++)
+ // Dirties may contain duplicates so check here if a variable is already cleaned:
+ if (dirty[toInt(dirties[i])])
+ clean(dirties[i]);
+ dirties.clear();
+}
+
+
+template<class Idx, class Vec, class Deleted>
+void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
+{
+ Vec& vec = occs[toInt(idx)];
+ int i, j;
+ for (i = j = 0; i < vec.size(); i++)
+ if (!deleted(vec[i]))
+ vec[j++] = vec[i];
+ vec.shrink(i - j);
+ dirty[toInt(idx)] = 0;
+}
+
+
+//=================================================================================================
+// CMap -- a class for mapping clauses to values:
+
+
+template<class T>
+class CMap
+{
+ struct CRefHash {
+ uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
+
+ typedef Map<CRef, T, CRefHash> HashTable;
+ HashTable map;
+
+ public:
+ // Size-operations:
+ void clear () { map.clear(); }
+ int size () const { return map.elems(); }
+
+
+ // Insert/Remove/Test mapping:
+ void insert (CRef cr, const T& t){ map.insert(cr, t); }
+ void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
+ void remove (CRef cr) { map.remove(cr); }
+ bool has (CRef cr, T& t) { return map.peek(cr, t); }
+
+ // Vector interface (the clause 'c' must already exist):
+ const T& operator [] (CRef cr) const { return map[cr]; }
+ T& operator [] (CRef cr) { return map[cr]; }
+
+ // Iteration (not transparent at all at the moment):
+ int bucket_count() const { return map.bucket_count(); }
+ const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
+
+ // Move contents to other map:
+ void moveTo(CMap& other){ map.moveTo(other.map); }
+
+ // TMP debug:
+ void debug(){
+ printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
+};
+
+
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
|________________________________________________________________________________________________@*/
inline Lit Clause::subsumes(const Clause& other) const
{
- if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
+ //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
+ //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
+ assert(!header.learnt); assert(!other.header.learnt);
+ assert(header.has_extra); assert(other.header.has_extra);
+ if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
return lit_Error;
Lit ret = lit_Undef;
- const Lit* c = (const Lit*)(*this);
- const Lit* d = (const Lit*)other;
+ const Lit* c = (const Lit*)(*this);
+ const Lit* d = (const Lit*)other;
- for (int i = 0; i < size(); i++) {
+ for (unsigned i = 0; i < header.size; i++) {
// search for c[i] or ~c[i]
- for (int j = 0; j < other.size(); j++)
+ for (unsigned j = 0; j < other.header.size; j++)
if (c[i] == d[j])
goto ok;
else if (ret == lit_Undef && c[i] == ~d[j]){
return ret;
}
-
inline void Clause::strengthen(Lit p)
{
remove(*this, p);
calcAbstraction();
}
-};
+//=================================================================================================
+}
#endif
/*******************************************************************************************[Alg.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Alg_h
-#define Alg_h
+#ifndef Minisat_Alg_h
+#define Minisat_Alg_h
-namespace MINISAT {
+#include "../mtl/Vec.h"
+
+namespace Minisat {
//=================================================================================================
-// Useful functions on vectors
+// Useful functions on vector-like types:
+//=================================================================================================
+// Removing and searching for elements:
+//
-#if 1
template<class V, class T>
static inline void remove(V& ts, const T& t)
{
int j = 0;
- for (; j < ts.size() && ts[j] != t; j++) ;
+ for (; j < ts.size() && ts[j] != t; j++);
assert(j < ts.size());
for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
ts.pop();
}
-#else
+
+
template<class V, class T>
-static inline void remove(V& ts, const T& t)
+static inline bool find(V& ts, const T& t)
{
int j = 0;
for (; j < ts.size() && ts[j] != t; j++);
- assert(j < ts.size());
- ts[j] = ts.last();
- ts.pop();
+ return j < ts.size();
}
-#endif
-template<class V, class T>
-static inline bool find(V& ts, const T& t)
+
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
{
- int j = 0;
- for (; j < ts.size() && ts[j] != t; j++) ;
- return j < ts.size();
+ to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+ if (!append)
+ to.clear();
+ for (int i = 0; i < from.size(); i++){
+ to.push();
+ copy(from[i], to.last());
+ }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
}
-};
#endif
--- /dev/null
+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-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_Alloc_h
+#define Minisat_Alloc_h
+
+#include "../mtl/XAlloc.h"
+#include "../mtl/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+ T* memory;
+ uint32_t sz;
+ uint32_t cap;
+ uint32_t wasted_;
+
+ void capacity(uint32_t min_cap);
+
+ public:
+ // TODO: make this a class for better type-checking?
+ typedef uint32_t Ref;
+ enum { Ref_Undef = UINT32_MAX };
+ enum { Unit_Size = sizeof(uint32_t) };
+
+ explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+ ~RegionAllocator()
+ {
+ if (memory != NULL)
+ ::free(memory);
+ }
+
+
+ uint32_t size () const { return sz; }
+ uint32_t wasted () const { return wasted_; }
+
+ Ref alloc (int size);
+ void free (int size) { wasted_ += size; }
+
+ // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+ T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; }
+ const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+
+ T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; }
+ const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
+ Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+ return (Ref)(t - &memory[0]); }
+
+ void moveTo(RegionAllocator& to) {
+ if (to.memory != NULL) ::free(to.memory);
+ to.memory = memory;
+ to.sz = sz;
+ to.cap = cap;
+ to.wasted_ = wasted_;
+
+ memory = NULL;
+ sz = cap = wasted_ = 0;
+ }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+ if (cap >= min_cap) return;
+
+ uint32_t prev_cap = cap;
+ while (cap < min_cap){
+ // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+ // result even by clearing the least significant bit. The resulting sequence of capacities
+ // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+ // using 'uint32_t' as indices so that as much as possible of this space can be used.
+ uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+ cap += delta;
+
+ if (cap <= prev_cap)
+ throw OutOfMemoryException();
+ }
+ // printf(" .. (%p) cap = %u\n", this, cap);
+
+ assert(cap > 0);
+ memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{
+ // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+ assert(size > 0);
+ capacity(sz + size);
+
+ uint32_t prev_sz = sz;
+ sz += size;
+
+ // Handle overflow:
+ if (sz < prev_sz)
+ throw OutOfMemoryException();
+
+ return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif
#ifndef BasicHeap_h
#define BasicHeap_h
-#include "Vec.h"
+#include "../Vec.h"
-namespace MINISAT {
+namespace Minisat {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
#include <cassert>
#include <new>
-namespace MINISAT {
+namespace Minisat {
//=================================================================================================
// Automatically resizable arrays
//
/******************************************************************************************[Heap.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Heap_h
-#define Heap_h
+#ifndef Minisat_Heap_h
+#define Minisat_Heap_h
-#include "Vec.h"
+#include "../mtl/Vec.h"
+
+namespace Minisat {
-namespace MINISAT {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
template<class Comp>
class Heap {
- Comp lt;
- vec<int> heap; // heap of ints
- vec<int> indices; // int -> index in heap
+ Comp lt; // The heap is a minimum-heap with respect to this comparator
+ vec<int> heap; // Heap of integers
+ vec<int> indices; // Each integers position (index) in the Heap
// Index "traversal" functions
static inline int left (int i) { return i*2+1; }
static inline int parent(int i) { return (i-1) >> 1; }
- inline void percolateUp(int i)
+ void percolateUp(int i)
{
- int x = heap[i];
- while (i != 0 && lt(x, heap[parent(i)])){
- heap[i] = heap[parent(i)];
- indices[heap[i]] = i;
- i = parent(i);
+ int x = heap[i];
+ int p = parent(i);
+
+ while (i != 0 && lt(x, heap[p])){
+ heap[i] = heap[p];
+ indices[heap[p]] = i;
+ i = p;
+ p = parent(p);
}
heap [i] = x;
indices[x] = i;
}
- inline void percolateDown(int i)
+ void percolateDown(int i)
{
int x = heap[i];
while (left(i) < heap.size()){
}
- bool heapProperty (int i) const {
- return i >= heap.size()
- || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
-
-
public:
Heap(const Comp& c) : lt(c) { }
bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
- void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); }
- // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED.
- void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+ void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
+ void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+
+
+ // Safe variant of insert/decrease/increase:
+ void update(int n)
+ {
+ if (!inHeap(n))
+ insert(n);
+ else {
+ percolateUp(indices[n]);
+ percolateDown(indices[n]); }
+ }
void insert(int n)
}
- void clear(bool dealloc = false)
- {
+ // Rebuild the heap from scratch, using the elements in 'ns':
+ void build(vec<int>& ns) {
for (int i = 0; i < heap.size(); i++)
indices[heap[i]] = -1;
-#ifdef NDEBUG
- for (int i = 0; i < indices.size(); i++)
- assert(indices[i] == -1);
-#endif
- heap.clear(dealloc);
- }
+ heap.clear();
+ for (int i = 0; i < ns.size(); i++){
+ indices[ns[i]] = i;
+ heap.push(ns[i]); }
- // Fool proof variant of insert/decrease/increase
- void update (int n)
- {
- if (!inHeap(n))
- insert(n);
- else {
- percolateUp(indices[n]);
- percolateDown(indices[n]);
- }
- }
-
-
- // Delete elements from the heap using a given filter function (-object).
- // *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method ***
- template <class F>
- void filter(const F& filt) {
- int i,j;
- for (i = j = 0; i < heap.size(); i++)
- if (filt(heap[i])){
- heap[j] = heap[i];
- indices[heap[i]] = j++;
- }else
- indices[heap[i]] = -1;
-
- heap.shrink(i - j);
for (int i = heap.size() / 2 - 1; i >= 0; i--)
percolateDown(i);
-
- assert(heapProperty());
}
-
- // DEBUG: consistency checking
- bool heapProperty() const {
- return heapProperty(1); }
-
-
- // COMPAT: should be removed
- void setBounds (int n) { }
- void increase (int n) { decrease(n); }
- int getmin () { return removeMin(); }
-
+ void clear(bool dealloc = false)
+ {
+ for (int i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+ heap.clear(dealloc);
+ }
};
//=================================================================================================
-};
+}
+
#endif
--- /dev/null
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-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_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+ // Not sure if there are newer versions that support C99 headers. The
+ // needed features are implemented in the headers below though:
+
+# include <sys/int_types.h>
+# include <sys/int_fmtio.h>
+# include <sys/int_limits.h>
+
+#else
+
+# include <stdint.h>
+# include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
/*******************************************************************************************[Map.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2006-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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Map_h
-#define Map_h
+#ifndef Minisat_Map_h
+#define Minisat_Map_h
-#include <stdint.h>
+#include "../mtl/IntTypes.h"
+#include "../mtl/Vec.h"
-#include "Vec.h"
-
-namespace MINISAT {
+namespace Minisat {
//=================================================================================================
// Default hash/equals functions
//
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
-
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
//=================================================================================================
// Some primes
//
template<class K, class D, class H = Hash<K>, class E = Equal<K> >
class Map {
+ public:
struct Pair { K key; D data; };
+ private:
H hash;
E equals;
int size;
// Don't allow copying (error prone):
- Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); return NULL; }
+ Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
Map (Map<K,D,H,E>& other) { assert(0); }
+ bool checkCap(int new_size) const { return new_size > cap; }
+
int32_t index (const K& k) const { return hash(k) % cap; }
- void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; }
+ void _insert (const K& k, const D& d) {
+ vec<Pair>& ps = table[index(k)];
+ ps.push(); ps.last().key = k; ps.last().data = d; }
+
void rehash () {
const vec<Pair>* old = table;
+ int old_cap = cap;
int newsize = primes[0];
for (int i = 1; newsize <= cap && i < nprimes; i++)
newsize = primes[i];
table = new vec<Pair>[newsize];
+ cap = newsize;
- for (int i = 0; i < cap; i++){
+ for (int i = 0; i < old_cap; i++){
for (int j = 0; j < old[i].size(); j++){
_insert(old[i][j].key, old[i][j].data); }}
delete [] old;
- cap = newsize;
+ // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
}
+
+ public:
- public:
-
- Map () : table(NULL), cap(0), size(0) {}
- Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
+ Map () : table(NULL), cap(0), size(0) {}
+ Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
~Map () { delete [] table; }
- void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; }
+ // PRECONDITION: the key must already exist in the map.
+ const D& operator [] (const K& k) const
+ {
+ assert(size != 0);
+ const D* res = NULL;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
- bool peek (const K& k, D& d) {
+ // PRECONDITION: the key must already exist in the map.
+ D& operator [] (const K& k)
+ {
+ assert(size != 0);
+ D* res = NULL;
+ vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
+
+ // PRECONDITION: the key must *NOT* exist in the map.
+ void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+ bool peek (const K& k, D& d) const {
if (size == 0) return false;
const vec<Pair>& ps = table[index(k)];
for (int i = 0; i < ps.size(); i++)
if (equals(ps[i].key, k)){
d = ps[i].data;
- return true; }
+ return true; }
return false;
}
- void remove (const K& k) {
+ bool has (const K& k) const {
+ if (size == 0) return false;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ return true;
+ return false;
+ }
+
+ // PRECONDITION: the key must exist in the map.
+ void remove(const K& k) {
assert(table != NULL);
vec<Pair>& ps = table[index(k)];
int j = 0;
- for (; j < ps.size() && !equals(ps[j].key, k); j++) ;
+ for (; j < ps.size() && !equals(ps[j].key, k); j++);
assert(j < ps.size());
ps[j] = ps.last();
ps.pop();
+ size--;
}
void clear () {
delete [] table;
table = NULL;
}
-};
+ int elems() const { return size; }
+ int bucket_count() const { return cap; }
+
+ // NOTE: the hash and equality objects are not moved by this method:
+ void moveTo(Map& other){
+ delete [] other.table;
+
+ other.table = table;
+ other.cap = cap;
+ other.size = size;
+
+ table = NULL;
+ size = cap = 0;
+ }
+
+ // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+ const vec<Pair>& bucket(int i) const { return table[i]; }
};
+
+//=================================================================================================
+}
+
#endif
/*****************************************************************************************[Queue.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Queue_h
-#define Queue_h
+#ifndef Minisat_Queue_h
+#define Minisat_Queue_h
-#include "Vec.h"
+#include "../mtl/Vec.h"
-namespace MINISAT {
-//=================================================================================================
+namespace Minisat {
+//=================================================================================================
-template <class T>
+template<class T>
class Queue {
- vec<T> elems;
+ vec<T> buf;
int first;
+ int end;
public:
- Queue(void) : first(0) { }
-
- void insert(T x) { elems.push(x); }
- T peek () const { return elems[first]; }
- void pop () { first++; }
-
- void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; }
- int size(void) { return elems.size() - first; }
-
- //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; }
-
- const T& operator [] (int index) const { return elems[first + index]; }
-
+ typedef T Key;
+
+ Queue() : buf(1), first(0), end(0) {}
+
+ void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+ int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+ const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+ T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+ T peek () const { assert(first != end); return buf[first]; }
+ void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+ void insert(T elem) { // INVARIANT: buf[end] is always unused
+ buf[end++] = elem;
+ if (end == buf.size()) end = 0;
+ if (first == end){ // Resize:
+ vec<T> tmp((buf.size()*3 + 1) >> 1);
+ //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
+ int i = 0;
+ for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
+ for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j];
+ first = 0;
+ end = buf.size();
+ tmp.moveTo(buf);
+ }
+ }
};
-//template<class T>
-//class Queue {
-// vec<T> buf;
-// int first;
-// int end;
-//
-//public:
-// typedef T Key;
-//
-// Queue() : buf(1), first(0), end(0) {}
-//
-// void clear () { buf.shrinkTo(1); first = end = 0; }
-// int size () { return (end >= first) ? end - first : end - first + buf.size(); }
-//
-// T peek () { assert(first != end); return buf[first]; }
-// void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
-// void insert(T elem) { // INVARIANT: buf[end] is always unused
-// buf[end++] = elem;
-// if (end == buf.size()) end = 0;
-// if (first == end){ // Resize:
-// vec<T> tmp((buf.size()*3 + 1) >> 1);
-// //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
-// int i = 0;
-// for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
-// for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j];
-// first = 0;
-// end = buf.size();
-// tmp.moveTo(buf);
-// }
-// }
-//};
//=================================================================================================
-};
+}
+
#endif
/******************************************************************************************[Sort.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2007, 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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Sort_h
-#define Sort_h
+#ifndef Minisat_Sort_h
+#define Minisat_Sort_h
-#include "Vec.h"
-
-namespace MINISAT {
+#include "../mtl/Vec.h"
//=================================================================================================
// Some sorting algorithms for vec's
+namespace Minisat {
+
template<class T>
struct LessThan_default {
bool operator () (T x, T y) { return x < y; }
//=================================================================================================
-};
+}
+
#endif
/*******************************************************************************************[Vec.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2007, 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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef Vec_h
-#define Vec_h
+#ifndef Minisat_Vec_h
+#define Minisat_Vec_h
-#include <cstdlib>
-#include <cassert>
+#include <assert.h>
#include <new>
-namespace MINISAT {
+#include "../mtl/IntTypes.h"
+#include "../mtl/XAlloc.h"
+
+namespace Minisat {
+
//=================================================================================================
// Automatically resizable arrays
//
int sz;
int cap;
- void init(int size, const T& pad);
- void grow(int min_cap);
-
// Don't allow copying (error prone):
vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
vec (vec<T>& other) { assert(0); }
-
- static inline int imin(int x, int y) {
- int mask = (x-y) >> (sizeof(int)*8-1);
- return (x&mask) + (y&(~mask)); }
-
- static inline int imax(int x, int y) {
- int mask = (y-x) >> (sizeof(int)*8-1);
- return (x&mask) + (y&(~mask)); }
+
+ // Helpers for calculating next capacity:
+ static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
+ //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+ static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
public:
- // Types:
- typedef int Key;
- typedef T Datum;
-
// Constructors:
- vec(void) : data(NULL) , sz(0) , cap(0) { }
- vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
+ vec() : data(NULL) , sz(0) , cap(0) { }
+ explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
- vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()')
- ~vec(void) { clear(true); }
+ ~vec() { clear(true); }
- // Ownership of underlying array:
- T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
- operator T* (void) { return data; } // (unsafe but convenient)
- operator const T* (void) const { return data; }
+ // Pointer to first element:
+ operator T* (void) { return data; }
// Size operations:
- int size (void) const { return sz; }
- void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
- void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; }
- void pop (void) { sz--, data[sz].~T(); }
- void growTo (int size);
- void growTo (int size, const T& pad);
- void clear (bool dealloc = false);
- void capacity (int size) { grow(size); }
+ int size (void) const { return sz; }
+ void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+ void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
+ int capacity (void) const { return cap; }
+ void capacity (int min_cap);
+ void growTo (int size);
+ void growTo (int size, const T& pad);
+ void clear (bool dealloc = false);
// Stack interface:
-#if 1
- void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
- //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
- void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
+ void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+ void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
-#else
- void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
- void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
-#endif
+ void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+ // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+ // happen given the way capacities are calculated (below). Essentially, all capacities are
+ // even, but INT_MAX is odd.
const T& last (void) const { return data[sz-1]; }
T& last (void) { return data[sz-1]; }
// Vector interface:
- const T& operator [] (int index) const { return data[index]; }
- T& operator [] (int index) { return data[index]; }
-
+ const T& operator [] (int index) const { return data[index]; }
+ T& operator [] (int index) { return data[index]; }
// Duplicatation (preferred instead):
- void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); }
+ void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
};
+
template<class T>
-void vec<T>::grow(int min_cap) {
- if (min_cap <= cap) return;
- if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
- else do cap = (cap*3+1) >> 1; while (cap < min_cap);
- data = (T*)realloc(data, cap * sizeof(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)
+ throw OutOfMemoryException();
+ }
+
template<class T>
void vec<T>::growTo(int size, const T& pad) {
if (sz >= size) return;
- grow(size);
- for (int i = sz; i < size; i++) new (&data[i]) T(pad);
+ capacity(size);
+ for (int i = sz; i < size; i++) data[i] = pad;
sz = size; }
+
template<class T>
void vec<T>::growTo(int size) {
if (sz >= size) return;
- grow(size);
+ capacity(size);
for (int i = sz; i < size; i++) new (&data[i]) T();
sz = size; }
+
template<class T>
void vec<T>::clear(bool dealloc) {
if (data != NULL){
sz = 0;
if (dealloc) free(data), data = NULL, cap = 0; } }
+//=================================================================================================
+}
-};
#endif
--- /dev/null
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-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_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+ void* mem = realloc(ptr, size);
+ if (mem == NULL && errno == ENOMEM){
+ throw OutOfMemoryException();
+ }else
+ return mem;
+}
+
+//=================================================================================================
+}
+
+#endif
--- /dev/null
+##
+## Template makefile for Standard, Profile, Debug, Release, and Release-static versions
+##
+## eg: "make rs" for a statically linked release version.
+## "make d" for a debug version (no optimizations).
+## "make" for the standard version (optimized, but with debug information and assertions active)
+
+PWD = $(shell pwd)
+EXEC ?= $(notdir $(PWD))
+
+CSRCS = $(wildcard $(PWD)/*.cc)
+DSRCS = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
+CHDRS = $(wildcard $(PWD)/*.h)
+COBJS = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
+
+PCOBJS = $(addsuffix p, $(COBJS))
+DCOBJS = $(addsuffix d, $(COBJS))
+RCOBJS = $(addsuffix r, $(COBJS))
+
+
+CXX ?= g++
+CFLAGS ?= -Wall -Wno-parentheses
+LFLAGS ?= -Wall
+
+COPTIMIZE ?= -O3
+
+CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
+LFLAGS += -lz
+
+.PHONY : s p d r rs clean
+
+s: $(EXEC)
+p: $(EXEC)_profile
+d: $(EXEC)_debug
+r: $(EXEC)_release
+rs: $(EXEC)_static
+
+libs: lib$(LIB)_standard.a
+libp: lib$(LIB)_profile.a
+libd: lib$(LIB)_debug.a
+libr: lib$(LIB)_release.a
+
+## Compile options
+%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
+%.od: CFLAGS +=-O0 -g -D DEBUG
+%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
+
+## Link options
+$(EXEC): LFLAGS += -g
+$(EXEC)_profile: LFLAGS += -g -pg
+$(EXEC)_debug: LFLAGS += -g
+#$(EXEC)_release: LFLAGS += ...
+$(EXEC)_static: LFLAGS += --static
+
+## Dependencies
+$(EXEC): $(COBJS)
+$(EXEC)_profile: $(PCOBJS)
+$(EXEC)_debug: $(DCOBJS)
+$(EXEC)_release: $(RCOBJS)
+$(EXEC)_static: $(RCOBJS)
+
+lib$(LIB)_standard.a: $(filter-out */Main.o, $(COBJS))
+lib$(LIB)_profile.a: $(filter-out */Main.op, $(PCOBJS))
+lib$(LIB)_debug.a: $(filter-out */Main.od, $(DCOBJS))
+lib$(LIB)_release.a: $(filter-out */Main.or, $(RCOBJS))
+
+
+## Build rule
+%.o %.op %.od %.or: %.cc
+ @echo Compiling: $(subst $(MROOT)/,,$@)
+ @$(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+ @echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(CXX) $^ $(LFLAGS) -o $@
+
+## Library rules (standard/profile/debug/release)
+lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
+ @echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(AR) -rcsv $@ $^
+
+## Library Soft Link rule:
+libs libp libd libr:
+ @echo "Making Soft Link: $^ -> lib$(LIB).a"
+ @ln -sf $^ lib$(LIB).a
+
+## Clean rule
+clean:
+ @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk
+
+## Make dependencies
+depend.mk: $(CSRCS) $(CHDRS)
+ @echo Making dependencies
+ @$(CXX) $(CFLAGS) -I$(MROOT) \
+ $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
+ @for dir in $(DEPDIR); do \
+ if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
+ echo Depends on: $${dir}; \
+ cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
+ fi; \
+ done
+
+-include $(MROOT)/mtl/config.mk
+-include depend.mk
+++ /dev/null
-#ifndef SAT_H_
-#define SAT_H_
-
-#ifdef CRYPTOMINISAT2
-#include "cryptominisat2/Solver.h"
-#include "cryptominisat2/SolverTypes.h"
-#endif
-
-#ifdef CORE
-#include "core/Solver.h"
-#include "core/SolverTypes.h"
-#include "simp/SimpSolver.h"
-#endif
-
-#endif
--- /dev/null
+/*****************************************************************************************[Main.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007, 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 <signal.h>
+#include <zlib.h>
+#include <sys/resource.h>
+
+#include "../utils/System.h"
+#include "../utils/ParseUtils.h"
+#include "../utils/Options.h"
+#include "../core/Dimacs.h"
+#include "../simp/SimpSolver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+
+
+void printStats(Solver& solver)
+{
+ double cpu_time = cpuTime();
+ double mem_used = memUsedPeak();
+ printf("restarts : %"PRIu64"\n", solver.starts);
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+}
+
+
+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 signum) { 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 signum) {
+ printf("\n"); printf("*** INTERRUPTED ***\n");
+ if (solver->verbosity > 0){
+ printStats(*solver);
+ 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");
+ // printf("This is MiniSat 2.0 beta\n");
+
+#if defined(__linux__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+ // Extra options:
+ //
+ IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+ BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true);
+ StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
+ IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
+ IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
+
+ parseOptions(argc, argv, true);
+
+ SimpSolver S;
+ double initial_time = cpuTime();
+
+ if (!pre) S.eliminate(true);
+
+ S.verbosity = verb;
+
+ solver = &S;
+ // Use signal handlers that forcibly quit until the solver will be able to respond to
+ // interrupts:
+ signal(SIGINT, SIGINT_exit);
+ signal(SIGXCPU,SIGINT_exit);
+
+ // Set limit on CPU-time:
+ if (cpu_lim != INT32_MAX){
+ rlimit rl;
+ getrlimit(RLIMIT_CPU, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
+ rl.rlim_cur = cpu_lim;
+ if (setrlimit(RLIMIT_CPU, &rl) == -1)
+ printf("WARNING! Could not set resource limit: CPU-time.\n");
+ } }
+
+ // Set limit on virtual memory:
+ if (mem_lim != INT32_MAX){
+ rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
+ rlimit rl;
+ getrlimit(RLIMIT_AS, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+ rl.rlim_cur = new_mem_lim;
+ if (setrlimit(RLIMIT_AS, &rl) == -1)
+ printf("WARNING! Could not set resource limit: Virtual memory.\n");
+ } }
+
+ 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);
+ 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);
+
+ // Change to signal-handlers that will only notify the solver and allow it to terminate
+ // voluntarily:
+ signal(SIGINT, SIGINT_interrupt);
+ signal(SIGXCPU,SIGINT_interrupt);
+
+ S.eliminate(true);
+ double simplified_time = cpuTime();
+ if (S.verbosity > 0){
+ printf("| Simplification time: %12.2f s |\n", simplified_time - parsed_time);
+ printf("| |\n"); }
+
+ if (!S.okay()){
+ if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+ if (S.verbosity > 0){
+ printf("===============================================================================\n");
+ printf("Solved by simplification\n");
+ printStats(S);
+ printf("\n"); }
+ printf("UNSATISFIABLE\n");
+ exit(20);
+ }
+
+ if (dimacs){
+ if (S.verbosity > 0)
+ printf("==============================[ Writing DIMACS ]===============================\n");
+ S.toDimacs((const char*)dimacs);
+ if (S.verbosity > 0)
+ printStats(S);
+ exit(0);
+ }
+
+ vec<Lit> dummy;
+ lbool ret = S.solveLimited(dummy);
+
+ if (S.verbosity > 0){
+ printStats(S);
+ 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);
+ }
+}
-TOP = ../../..
-include $(TOP)/scripts/Makefile.common
-
-MTL = ../mtl
-SOURCES = SimpSolver.C ../core/Solver.C
-OBJECTS = $(SOURCES:.C=.o)
-OBJECTS += ../core/dlmalloc.o
-LIB = libminisat.a
-CFLAGS += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c -DMSPACES
EXEC = minisat
-LFLAGS = -lz
-
-all: $(LIB) #$(EXEC)
-lib: $(LIB)
-
-$(LIB): $(OBJECTS)
- rm -f $@
- ar cq $@ $(OBJECTS)
- ranlib $@
- cp $(LIB) ../
- cp $(OBJECTS) ../
-
-clean:
- rm -f $(OBJECTS) $(LIB)
+DEPDIR = mtl utils core
+MROOT =..
-.C.o:
- $(CC) $(CFLAGS) $< -o $@
+include $(MROOT)/mtl/template.mk
+++ /dev/null
-/************************************************************************************[SimpSolver.C]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 "Sort.h"
-#include "SimpSolver.h"
-
-namespace MINISAT {
-
-//=================================================================================================
-// Constructor/Destructor:
-
-
-SimpSolver::SimpSolver() :
- grow (0)
- , asymm_mode (false)
- , redundancy_check (false)
- , merges (0)
- , asymm_lits (0)
- , remembered_clauses (0)
- , elimorder (1)
- , use_simplification (true)
- , elim_heap (ElimLt(n_occ))
- , bwdsub_assigns (0)
-{
- vec<Lit> dummy(1,lit_Undef);
- bwdsub_tmpunit = Clause_new(dummy);
- remove_satisfied = false;
-}
-
-
-SimpSolver::~SimpSolver()
-{
- tlfree(bwdsub_tmpunit);
-
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int i = 0; i < elimtable.size(); i++)
- for (int j = 0; j < elimtable[i].eliminated.size(); j++)
- tlfree(elimtable[i].eliminated[j]);
-}
-
-
-Var SimpSolver::newVar(bool sign, bool dvar) {
- Var v = Solver::newVar(sign, dvar);
-
- if (use_simplification){
- n_occ .push(0);
- n_occ .push(0);
- occurs .push();
- frozen .push((char)false);
- touched .push(0);
- elim_heap.insert(v);
- elimtable.push();
- }
- return v; }
-
-
-
-bool SimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp) {
- vec<Var> extra_frozen;
- bool result = true;
-
- do_simp &= use_simplification;
-
- if (do_simp){
- // Assumptions must be temporarily frozen to run variable elimination:
- for (int i = 0; i < assumps.size(); i++){
- Var v = var(assumps[i]);
-
- // If an assumption has been eliminated, remember it.
- if (isEliminated(v))
- remember(v);
-
- if (!frozen[v]){
- // Freeze and store.
- setFrozen(v, true);
- extra_frozen.push(v);
- } }
-
- result = eliminate(turn_off_simp);
- }
-
- if (result)
- result = Solver::solve(assumps);
-
- if (result) {
- extendModel();
-#ifndef NDEBUG
- verifyModel();
-#endif
- }
-
- if (do_simp)
- // Unfreeze the assumptions that were frozen:
- for (int i = 0; i < extra_frozen.size(); i++)
- setFrozen(extra_frozen[i], false);
-
- // STP MODIFICATION..
- // If eliminate(bool) finds that the formula is unsatisfiable. ok may not be set.
- // We use okay() to check if the function was satisfiable.
- if (!result)
- ok=false;
- // STP MODIFICATION..
-
- return result;
-}
-
-
-
-bool SimpSolver::addClause(vec<Lit>& ps)
-{
- for (int i = 0; i < ps.size(); i++)
- if (isEliminated(var(ps[i])))
- remember(var(ps[i]));
-
- int nclauses = clauses.size();
-
- if (redundancy_check && implied(ps))
- return true;
-
- if (!Solver::addClause(ps))
- return false;
-
- if (use_simplification && clauses.size() == nclauses + 1){
- Clause& c = *clauses.last();
-
- subsumption_queue.insert(&c);
-
- for (int i = 0; i < c.size(); i++){
- assert(occurs.size() > var(c[i]));
- assert(!find(occurs[var(c[i])], &c));
-
- occurs[var(c[i])].push(&c);
- n_occ[toInt(c[i])]++;
- touched[var(c[i])] = 1;
- assert(elimtable[var(c[i])].order == 0);
- if (elim_heap.inHeap(var(c[i])))
- elim_heap.increase_(var(c[i]));
- }
- }
-
- return true;
-}
-
-
-void SimpSolver::removeClause(Clause& c)
-{
- assert(!c.learnt());
-
- if (use_simplification)
- for (int i = 0; i < c.size(); i++){
- n_occ[toInt(c[i])]--;
- updateElimHeap(var(c[i]));
- }
-
- detachClause(c);
- c.mark(1);
-}
-
-
-bool SimpSolver::strengthenClause(Clause& c, Lit l)
-{
- assert(decisionLevel() == 0);
- assert(c.mark() == 0);
- assert(!c.learnt());
- assert(find(watches[toInt(~c[0])], &c));
- assert(find(watches[toInt(~c[1])], &c));
-
- // FIX: this is too inefficient but would be nice to have (properly implemented)
- // if (!find(subsumption_queue, &c))
- subsumption_queue.insert(&c);
-
- // If l is watched, delete it from watcher list and watch a new literal
- if (c[0] == l || c[1] == l){
- Lit other = c[0] == l ? c[1] : c[0];
- if (c.size() == 2){
- removeClause(c);
- c.strengthen(l);
- }else{
- c.strengthen(l);
- remove(watches[toInt(~l)], &c);
-
- // Add a watch for the correct literal
- watches[toInt(~(c[1] == other ? c[0] : c[1]))].push(&c);
-
- // !! this version assumes that remove does not change the order !!
- //watches[toInt(~c[1])].push(&c);
- clauses_literals -= 1;
- }
- }
- else{
- c.strengthen(l);
- clauses_literals -= 1;
- }
-
- // if subsumption-indexing is active perform the necessary updates
- if (use_simplification){
- remove(occurs[var(l)], &c);
- n_occ[toInt(l)]--;
- updateElimHeap(var(l));
- }
-
- return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true;
-}
-
-
-// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
-bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
-{
- merges++;
- out_clause.clear();
-
- bool ps_smallest = _ps.size() < _qs.size();
- const Clause& ps = ps_smallest ? _qs : _ps;
- const Clause& qs = ps_smallest ? _ps : _qs;
-
- for (int i = 0; i < qs.size(); i++){
- if (var(qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(ps[j]) == var(qs[i]))
- if (ps[j] == ~qs[i])
- return false;
- else
- goto next;
- out_clause.push(qs[i]);
- }
- next:;
- }
-
- for (int i = 0; i < ps.size(); i++)
- if (var(ps[i]) != v)
- out_clause.push(ps[i]);
-
- return true;
-}
-
-
-// Returns FALSE if clause is always satisfied.
-bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
-{
- merges++;
-
- bool ps_smallest = _ps.size() < _qs.size();
- const Clause& ps = ps_smallest ? _qs : _ps;
- const Clause& qs = ps_smallest ? _ps : _qs;
- const Lit* __ps = (const Lit*)ps;
- const Lit* __qs = (const Lit*)qs;
-
- for (int i = 0; i < qs.size(); i++){
- if (var(__qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(__ps[j]) == var(__qs[i]))
- if (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
- }
- next:;
- }
-
- return true;
-}
-
-
-void SimpSolver::gatherTouchedClauses()
-{
- //fprintf(stderr, "Gathering clauses for backwards subsumption\n");
- int ntouched = 0;
- for (int i = 0; i < touched.size(); i++)
- if (touched[i]){
- const vec<Clause*>& cs = getOccurs(i);
- ntouched++;
- for (int j = 0; j < cs.size(); j++)
- if (cs[j]->mark() == 0){
- subsumption_queue.insert(cs[j]);
- cs[j]->mark(2);
- }
- touched[i] = 0;
- }
-
- //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size());
- for (int i = 0; i < subsumption_queue.size(); i++)
- subsumption_queue[i]->mark(0);
-}
-
-
-bool SimpSolver::implied(const vec<Lit>& c)
-{
- assert(decisionLevel() == 0);
-
- trail_lim.push(trail.size());
- for (int i = 0; i < c.size(); i++)
- if (value(c[i]) == l_True){
- cancelUntil(0);
- return false;
- }else if (value(c[i]) != l_False){
- assert(value(c[i]) == l_Undef);
- uncheckedEnqueue(~c[i]);
- }
-
- bool result = propagate() != NULL;
- cancelUntil(0);
- return result;
-}
-
-
-// Backward subsumption + backward subsumption resolution
-bool SimpSolver::backwardSubsumptionCheck(bool verbose)
-{
- int cnt = 0;
- int subsumed = 0;
- int deleted_literals = 0;
- assert(decisionLevel() == 0);
-
- while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
-
- // Check top-level assignments by creating a dummy clause and placing it in the queue:
- if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
- Lit l = trail[bwdsub_assigns++];
- (*bwdsub_tmpunit)[0] = l;
- bwdsub_tmpunit->calcAbstraction();
- assert(bwdsub_tmpunit->mark() == 0);
- subsumption_queue.insert(bwdsub_tmpunit); }
-
- Clause& c = *subsumption_queue.peek(); subsumption_queue.pop();
-
- if (c.mark()) continue;
-
- if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
- reportf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
-
- assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
-
- // Find best variable to scan:
- Var best = var(c[0]);
- for (int i = 1; i < c.size(); i++)
- if (occurs[var(c[i])].size() < occurs[best].size())
- best = var(c[i]);
-
- // Search all candidates:
- vec<Clause*>& _cs = getOccurs(best);
- Clause** cs = (Clause**)_cs;
-
- for (int j = 0; j < _cs.size(); j++)
- if (c.mark())
- break;
- else if (!cs[j]->mark() && cs[j] != &c){
- Lit l = c.subsumes(*cs[j]);
-
- if (l == lit_Undef)
- subsumed++, removeClause(*cs[j]);
- else if (l != lit_Error){
- deleted_literals++;
-
- if (!strengthenClause(*cs[j], ~l))
- return false;
-
- // Did current candidate get deleted from cs? Then check candidate at index j again:
- if (var(l) == best)
- j--;
- }
- }
- }
-
- return true;
-}
-
-
-bool SimpSolver::asymm(Var v, Clause& c)
-{
- assert(decisionLevel() == 0);
-
- if (c.mark() || satisfied(c)) return true;
-
- trail_lim.push(trail.size());
- Lit l = lit_Undef;
- for (int i = 0; i < c.size(); i++)
- if (var(c[i]) != v && value(c[i]) != l_False)
- uncheckedEnqueue(~c[i]);
- else
- l = c[i];
-
- if (propagate() != NULL){
- cancelUntil(0);
- asymm_lits++;
- if (!strengthenClause(c, l))
- return false;
- }else
- cancelUntil(0);
-
- return true;
-}
-
-
-bool SimpSolver::asymmVar(Var v)
-{
- assert(!frozen[v]);
- assert(use_simplification);
-
- vec<Clause*> pos, neg;
- const vec<Clause*>& cls = getOccurs(v);
-
- if (value(v) != l_Undef || cls.size() == 0)
- return true;
-
- for (int i = 0; i < cls.size(); i++)
- if (!asymm(v, *cls[i]))
- return false;
-
- return backwardSubsumptionCheck();
-}
-
-
-void SimpSolver::verifyModel()
-{
- bool failed = false;
- int cnt = 0;
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int i = 0; i < elimtable.size(); i++)
- if (elimtable[i].order > 0)
- for (int j = 0; j < elimtable[i].eliminated.size(); j++){
- cnt++;
- Clause& c = *elimtable[i].eliminated[j];
- for (int k = 0; k < c.size(); k++)
- if (modelValue(c[k]) == l_True)
- goto next;
-
- reportf("unsatisfied clause: ");
- printClause(*elimtable[i].eliminated[j]);
- reportf("\n");
- failed = true;
- next:;
- }
-
- assert(!failed);
- //reportf("Verified %d eliminated clauses.\n", cnt);
-}
-
-
-bool SimpSolver::eliminateVar(Var v, bool fail)
-{
- if (!fail && asymm_mode && !asymmVar(v)) return false;
-
- const vec<Clause*>& cls = getOccurs(v);
-
-// if (value(v) != l_Undef || cls.size() == 0) return true;
- if (value(v) != l_Undef) return true;
-
- // Split the occurrences into positive and negative:
- vec<Clause*> pos, neg;
- for (int i = 0; i < cls.size(); i++)
- (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]);
-
- // Check if number of clauses decreases:
- int cnt = 0;
- for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow)
- return true;
-
- // Delete and store old clauses:
- setDecisionVar(v, false);
- elimtable[v].order = elimorder++;
- assert(elimtable[v].eliminated.size() == 0);
- for (int i = 0; i < cls.size(); i++){
- elimtable[v].eliminated.push(Clause_new(*cls[i]));
- removeClause(*cls[i]); }
-
- // Produce clauses in cross product:
- int top = clauses.size();
- vec<Lit> resolvent;
- for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
- return false;
-
- // DEBUG: For checking that a clause set is saturated with respect to variable elimination.
- // If the clause set is expected to be saturated at this point, this constitutes an
- // error.
- if (fail){
- reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
- reportf("previous clauses:\n");
- for (int i = 0; i < cls.size(); i++){
- printClause(*cls[i]); reportf("\n"); }
- reportf("new clauses:\n");
- for (int i = top; i < clauses.size(); i++){
- printClause(*clauses[i]); reportf("\n"); }
- assert(0); }
-
- return backwardSubsumptionCheck();
-}
-
-
-void SimpSolver::remember(Var v)
-{
- assert(decisionLevel() == 0);
- assert(isEliminated(v));
-
- vec<Lit> clause;
-
- // Re-activate variable:
- elimtable[v].order = 0;
- setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now.
-
- if (use_simplification)
- updateElimHeap(v);
-
- // Reintroduce all old clauses which may implicitly remember other clauses:
- for (int i = 0; i < elimtable[v].eliminated.size(); i++){
- Clause& c = *elimtable[v].eliminated[i];
- clause.clear();
- for (int j = 0; j < c.size(); j++)
- clause.push(c[j]);
-
- remembered_clauses++;
- check(addClause(clause));
- tlfree(&c);
- }
-
- elimtable[v].eliminated.clear();
-}
-
-
-void SimpSolver::extendModel()
-{
- vec<Var> vs;
-
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int v = 0; v < elimtable.size(); v++)
- if (elimtable[v].order > 0)
- vs.push(v);
-
- sort(vs, ElimOrderLt(elimtable));
-
- for (int i = 0; i < vs.size(); i++){
- Var v = vs[i];
- Lit l = lit_Undef;
-
- for (int j = 0; j < elimtable[v].eliminated.size(); j++){
- Clause& c = *elimtable[v].eliminated[j];
-
- for (int k = 0; k < c.size(); k++)
- if (var(c[k]) == v)
- l = c[k];
- else if (modelValue(c[k]) != l_False)
- goto next;
-
- assert(l != lit_Undef);
- model[v] = lbool(!sign(l));
- break;
-
- next:;
- }
-
- if (model[v] == l_Undef)
- model[v] = l_True;
- }
-}
-
-
-bool SimpSolver::eliminate(bool turn_off_elim)
-{
- if (!ok || !use_simplification)
- return ok;
-
- // Main simplification loop:
- //assert(subsumption_queue.size() == 0);
- //gatherTouchedClauses();
- while (subsumption_queue.size() > 0 || elim_heap.size() > 0){
-
- //fprintf(stderr, "subsumption phase: (%d)\n", subsumption_queue.size());
- if (!backwardSubsumptionCheck(true))
- return false;
-
- //fprintf(stderr, "elimination phase:\n (%d)", elim_heap.size());
- for (int cnt = 0; !elim_heap.empty(); cnt++){
- Var elim = elim_heap.removeMin();
-
- if (verbosity >= 2 && cnt % 100 == 0)
- reportf("elimination left: %10d\r", elim_heap.size());
-
- if (!frozen[elim] && !eliminateVar(elim))
- return false;
- }
-
- assert(subsumption_queue.size() == 0);
- gatherTouchedClauses();
- }
-
- // Cleanup:
- cleanUpClauses();
- order_heap.filter(VarFilter(*this));
-
-#ifdef INVARIANTS
- // Check that no more subsumption is possible:
- reportf("Checking that no more subsumption is possible\n");
- for (int i = 0; i < clauses.size(); i++){
- if (i % 1000 == 0)
- reportf("left %10d\r", clauses.size() - i);
-
- assert(clauses[i]->mark() == 0);
- for (int j = 0; j < i; j++)
- assert(clauses[i]->subsumes(*clauses[j]) == lit_Error);
- }
- reportf("done.\n");
-
- // Check that no more elimination is possible:
- reportf("Checking that no more elimination is possible\n");
- for (int i = 0; i < nVars(); i++)
- if (!frozen[i]) eliminateVar(i, true);
- reportf("done.\n");
- checkLiteralCount();
-#endif
-
- // If no more simplification is needed, free all simplification-related data structures:
- if (turn_off_elim){
- use_simplification = false;
- touched.clear(true);
- occurs.clear(true);
- n_occ.clear(true);
- subsumption_queue.clear(true);
- elim_heap.clear(true);
- remove_satisfied = true;
- }
-
-
- return true;
-}
-
-
-void SimpSolver::cleanUpClauses()
-{
- int i , j;
- vec<Var> dirty;
- for (i = 0; i < clauses.size(); i++)
- if (clauses[i]->mark() == 1){
- Clause& c = *clauses[i];
- for (int k = 0; k < c.size(); k++)
- if (!seen[var(c[k])]){
- seen[var(c[k])] = 1;
- dirty.push(var(c[k]));
- } }
-
- for (i = 0; i < dirty.size(); i++){
- cleanOcc(dirty[i]);
- seen[dirty[i]] = 0; }
-
- for (i = j = 0; i < clauses.size(); i++)
- if (clauses[i]->mark() == 1)
- tlfree(clauses[i]);
- else
- clauses[j++] = clauses[i];
- clauses.shrink(i - j);
-}
-
-
-//=================================================================================================
-// Convert to DIMACS:
-
-
-void SimpSolver::toDimacs(FILE* f, Clause& c)
-{
- 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]) ? "-" : "", var(c[i])+1);
- fprintf(f, "0\n");
-}
-
-
-void SimpSolver::toDimacs(const char* file)
-{
- assert(decisionLevel() == 0);
- FILE* f = fopen(file, "wr");
- if (f != NULL){
-
- // 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(*clauses[i]))
- cnt++;
-
- fprintf(f, "p cnf %d %d\n", nVars(), cnt);
-
- for (int i = 0; i < clauses.size(); i++)
- toDimacs(f, *clauses[i]);
-
- fprintf(stderr, "Wrote %d clauses...\n", clauses.size());
- }else
- fprintf(stderr, "could not open file %s\n", file);
-}
-
-};
--- /dev/null
+/***********************************************************************************[SimpSolver.cc]
+Copyright (c) 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 "../mtl/Sort.h"
+#include "../simp/SimpSolver.h"
+#include "../utils/System.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "SIMP";
+
+static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
+static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
+static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
+static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
+static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
+static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
+static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+SimpSolver::SimpSolver() :
+ grow (opt_grow)
+ , clause_lim (opt_clause_lim)
+ , subsumption_lim (opt_subsumption_lim)
+ , simp_garbage_frac (opt_simp_garbage_frac)
+ , use_asymm (opt_use_asymm)
+ , use_rcheck (opt_use_rcheck)
+ , use_elim (opt_use_elim)
+ , merges (0)
+ , asymm_lits (0)
+ , eliminated_vars (0)
+ , elimorder (1)
+ , use_simplification (true)
+ , occurs (ClauseDeleted(ca))
+ , elim_heap (ElimLt(n_occ))
+ , bwdsub_assigns (0)
+ , n_touched (0)
+{
+ vec<Lit> dummy(1,lit_Undef);
+ ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
+ bwdsub_tmpunit = ca.alloc(dummy);
+ remove_satisfied = false;
+}
+
+
+SimpSolver::~SimpSolver()
+{
+}
+
+
+Var SimpSolver::newVar(bool sign, bool dvar) {
+ Var v = Solver::newVar(sign, dvar);
+
+ frozen .push((char)false);
+ eliminated.push((char)false);
+
+ if (use_simplification){
+ n_occ .push(0);
+ n_occ .push(0);
+ occurs .init(v);
+ touched .push(0);
+ elim_heap .insert(v);
+ }
+ return v; }
+
+
+
+lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
+{
+ vec<Var> extra_frozen;
+ lbool result = l_True;
+
+ do_simp &= use_simplification;
+
+ if (do_simp){
+ // Assumptions must be temporarily frozen to run variable elimination:
+ for (int i = 0; i < assumptions.size(); i++){
+ Var v = var(assumptions[i]);
+
+ // If an assumption has been eliminated, remember it.
+ assert(!isEliminated(v));
+
+ if (!frozen[v]){
+ // Freeze and store.
+ setFrozen(v, true);
+ extra_frozen.push(v);
+ } }
+
+ result = lbool(eliminate(turn_off_simp));
+ }
+
+ if (result == l_True)
+ result = Solver::solve_();
+ else if (verbosity >= 1)
+ printf("===============================================================================\n");
+
+ if (result == l_True)
+ extendModel();
+
+ if (do_simp)
+ // Unfreeze the assumptions that were frozen:
+ for (int i = 0; i < extra_frozen.size(); i++)
+ setFrozen(extra_frozen[i], false);
+
+ return result;
+}
+
+
+
+bool SimpSolver::addClause_(vec<Lit>& ps)
+{
+#ifndef NDEBUG
+ for (int i = 0; i < ps.size(); i++)
+ assert(!isEliminated(var(ps[i])));
+#endif
+
+ int nclauses = clauses.size();
+
+ if (use_rcheck && implied(ps))
+ return true;
+
+ if (!Solver::addClause_(ps))
+ return false;
+
+ if (use_simplification && clauses.size() == nclauses + 1){
+ CRef cr = clauses.last();
+ const Clause& c = ca[cr];
+
+ // NOTE: the clause is added to the queue immediately and then
+ // again during 'gatherTouchedClauses()'. If nothing happens
+ // in between, it will only be checked once. Otherwise, it may
+ // be checked twice unnecessarily. This is an unfortunate
+ // consequence of how backward subsumption is used to mimic
+ // forward subsumption.
+ subsumption_queue.insert(cr);
+ for (int i = 0; i < c.size(); i++){
+ occurs[var(c[i])].push(cr);
+ n_occ[toInt(c[i])]++;
+ touched[var(c[i])] = 1;
+ n_touched++;
+ if (elim_heap.inHeap(var(c[i])))
+ elim_heap.increase(var(c[i]));
+ }
+ }
+
+ return true;
+}
+
+
+void SimpSolver::removeClause(CRef cr)
+{
+ const Clause& c = ca[cr];
+
+ if (use_simplification)
+ for (int i = 0; i < c.size(); i++){
+ n_occ[toInt(c[i])]--;
+ updateElimHeap(var(c[i]));
+ occurs.smudge(var(c[i]));
+ }
+
+ Solver::removeClause(cr);
+}
+
+
+bool SimpSolver::strengthenClause(CRef cr, Lit l)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+ assert(use_simplification);
+
+ // FIX: this is too inefficient but would be nice to have (properly implemented)
+ // if (!find(subsumption_queue, &c))
+ subsumption_queue.insert(cr);
+
+ if (c.size() == 2){
+ removeClause(cr);
+ c.strengthen(l);
+ }else{
+ detachClause(cr, true);
+ c.strengthen(l);
+ attachClause(cr);
+ remove(occurs[var(l)], cr);
+ n_occ[toInt(l)]--;
+ updateElimHeap(var(l));
+ }
+
+ return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
+}
+
+
+// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+{
+ merges++;
+ out_clause.clear();
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(ps[j]) == var(qs[i]))
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ out_clause.push(qs[i]);
+ }
+ next:;
+ }
+
+ for (int i = 0; i < ps.size(); i++)
+ if (var(ps[i]) != v)
+ out_clause.push(ps[i]);
+
+ return true;
+}
+
+
+// Returns FALSE if clause is always satisfied.
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
+{
+ merges++;
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+ const Lit* __ps = (const Lit*)ps;
+ const Lit* __qs = (const Lit*)qs;
+
+ size = ps.size()-1;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(__qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(__ps[j]) == var(__qs[i]))
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ size++;
+ }
+ next:;
+ }
+
+ return true;
+}
+
+
+void SimpSolver::gatherTouchedClauses()
+{
+ if (n_touched == 0) return;
+
+ int i,j;
+ for (i = j = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 0)
+ ca[subsumption_queue[i]].mark(2);
+
+ for (i = 0; i < touched.size(); i++)
+ if (touched[i]){
+ const vec<CRef>& cs = occurs.lookup(i);
+ for (j = 0; j < cs.size(); j++)
+ if (ca[cs[j]].mark() == 0){
+ subsumption_queue.insert(cs[j]);
+ ca[cs[j]].mark(2);
+ }
+ touched[i] = 0;
+ }
+
+ for (i = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 2)
+ ca[subsumption_queue[i]].mark(0);
+
+ n_touched = 0;
+}
+
+
+bool SimpSolver::implied(const vec<Lit>& c)
+{
+ assert(decisionLevel() == 0);
+
+ trail_lim.push(trail.size());
+ for (int i = 0; i < c.size(); i++)
+ if (value(c[i]) == l_True){
+ cancelUntil(0);
+ return false;
+ }else if (value(c[i]) != l_False){
+ assert(value(c[i]) == l_Undef);
+ uncheckedEnqueue(~c[i]);
+ }
+
+ bool result = propagate() != CRef_Undef;
+ cancelUntil(0);
+ return result;
+}
+
+
+// Backward subsumption + backward subsumption resolution
+bool SimpSolver::backwardSubsumptionCheck(bool verbose)
+{
+ int cnt = 0;
+ int subsumed = 0;
+ int deleted_literals = 0;
+ assert(decisionLevel() == 0);
+
+ while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
+
+ // Empty subsumption queue and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ subsumption_queue.clear();
+ bwdsub_assigns = trail.size();
+ break; }
+
+ // Check top-level assignments by creating a dummy clause and placing it in the queue:
+ if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
+ Lit l = trail[bwdsub_assigns++];
+ ca[bwdsub_tmpunit][0] = l;
+ ca[bwdsub_tmpunit].calcAbstraction();
+ subsumption_queue.insert(bwdsub_tmpunit); }
+
+ CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
+ Clause& c = ca[cr];
+
+ if (c.mark()) continue;
+
+ if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
+ printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
+
+ assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
+
+ // Find best variable to scan:
+ Var best = var(c[0]);
+ for (int i = 1; i < c.size(); i++)
+ if (occurs[var(c[i])].size() < occurs[best].size())
+ best = var(c[i]);
+
+ // Search all candidates:
+ vec<CRef>& _cs = occurs.lookup(best);
+ CRef* cs = (CRef*)_cs;
+
+ for (int j = 0; j < _cs.size(); j++)
+ if (c.mark())
+ break;
+ else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
+ Lit l = c.subsumes(ca[cs[j]]);
+
+ if (l == lit_Undef)
+ subsumed++, removeClause(cs[j]);
+ else if (l != lit_Error){
+ deleted_literals++;
+
+ if (!strengthenClause(cs[j], ~l))
+ return false;
+
+ // Did current candidate get deleted from cs? Then check candidate at index j again:
+ if (var(l) == best)
+ j--;
+ }
+ }
+ }
+
+ return true;
+}
+
+
+bool SimpSolver::asymm(Var v, CRef cr)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+
+ if (c.mark() || satisfied(c)) return true;
+
+ trail_lim.push(trail.size());
+ Lit l = lit_Undef;
+ for (int i = 0; i < c.size(); i++)
+ if (var(c[i]) != v && value(c[i]) != l_False)
+ uncheckedEnqueue(~c[i]);
+ else
+ l = c[i];
+
+ if (propagate() != CRef_Undef){
+ cancelUntil(0);
+ asymm_lits++;
+ if (!strengthenClause(cr, l))
+ return false;
+ }else
+ cancelUntil(0);
+
+ return true;
+}
+
+
+bool SimpSolver::asymmVar(Var v)
+{
+ assert(use_simplification);
+
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ if (value(v) != l_Undef || cls.size() == 0)
+ return true;
+
+ for (int i = 0; i < cls.size(); i++)
+ if (!asymm(v, cls[i]))
+ return false;
+
+ return backwardSubsumptionCheck();
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
+{
+ elimclauses.push(toInt(x));
+ elimclauses.push(1);
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
+{
+ int first = elimclauses.size();
+ int v_pos = -1;
+
+ // Copy clause to elimclauses-vector. Remember position where the
+ // variable 'v' occurs:
+ for (int i = 0; i < c.size(); i++){
+ elimclauses.push(toInt(c[i]));
+ if (var(c[i]) == v)
+ v_pos = i + first;
+ }
+ assert(v_pos != -1);
+
+ // Swap the first literal with the 'v' literal, so that the literal
+ // containing 'v' will occur first in the clause:
+ uint32_t tmp = elimclauses[v_pos];
+ elimclauses[v_pos] = elimclauses[first];
+ elimclauses[first] = tmp;
+
+ // Store the length of the clause last:
+ elimclauses.push(c.size());
+}
+
+
+
+bool SimpSolver::eliminateVar(Var v)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ // Split the occurrences into positive and negative:
+ //
+ const vec<CRef>& cls = occurs.lookup(v);
+ vec<CRef> pos, neg;
+ for (int i = 0; i < cls.size(); i++)
+ (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+ // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+ // clause must exceed the limit on the maximal clause size (if it is set):
+ //
+ int cnt = 0;
+ int clause_size = 0;
+
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
+ (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
+
+ // Delete and store old clauses:
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ eliminated_vars++;
+
+ if (pos.size() > neg.size()){
+ for (int i = 0; i < neg.size(); i++)
+ mkElimClause(elimclauses, v, ca[neg[i]]);
+ mkElimClause(elimclauses, mkLit(v));
+ }else{
+ for (int i = 0; i < pos.size(); i++)
+ mkElimClause(elimclauses, v, ca[pos[i]]);
+ mkElimClause(elimclauses, ~mkLit(v));
+ }
+
+ for (int i = 0; i < cls.size(); i++)
+ removeClause(cls[i]);
+
+ // Produce clauses in cross product:
+ vec<Lit>& resolvent = add_tmp;
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
+ return false;
+
+ // Free occurs list for this variable:
+ occurs[v].clear(true);
+
+ // Free watchers lists for this variable, if possible:
+ if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
+ if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
+
+ return backwardSubsumptionCheck();
+}
+
+
+bool SimpSolver::substitute(Var v, Lit x)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ if (!ok) return false;
+
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ vec<Lit>& subst_clause = add_tmp;
+ for (int i = 0; i < cls.size(); i++){
+ Clause& c = ca[cls[i]];
+
+ subst_clause.clear();
+ for (int j = 0; j < c.size(); j++){
+ Lit p = c[j];
+ subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+ }
+
+ removeClause(cls[i]);
+
+ if (!addClause_(subst_clause))
+ return ok = false;
+ }
+
+ return true;
+}
+
+
+void SimpSolver::extendModel()
+{
+ int i, j;
+ Lit x;
+
+ for (i = elimclauses.size()-1; i > 0; i -= j){
+ for (j = elimclauses[i--]; j > 1; j--, i--)
+ if (modelValue(toLit(elimclauses[i])) != l_False)
+ goto next;
+
+ x = toLit(elimclauses[i]);
+ model[var(x)] = lbool(!sign(x));
+ next:;
+ }
+}
+
+
+bool SimpSolver::eliminate(bool turn_off_elim)
+{
+ if (!simplify())
+ return false;
+ else if (!use_simplification)
+ return true;
+
+ // Main simplification loop:
+ //
+ while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
+
+ gatherTouchedClauses();
+ // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
+ !backwardSubsumptionCheck(true)){
+ ok = false; goto cleanup; }
+
+ // Empty elim_heap and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ assert(bwdsub_assigns == trail.size());
+ assert(subsumption_queue.size() == 0);
+ assert(n_touched == 0);
+ elim_heap.clear();
+ goto cleanup; }
+
+ // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
+ for (int cnt = 0; !elim_heap.empty(); cnt++){
+ Var elim = elim_heap.removeMin();
+
+ if (asynch_interrupt) break;
+
+ if (isEliminated(elim) || value(elim) != l_Undef) continue;
+
+ if (verbosity >= 2 && cnt % 100 == 0)
+ printf("elimination left: %10d\r", elim_heap.size());
+
+ if (use_asymm){
+ // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
+ bool was_frozen = frozen[elim];
+ frozen[elim] = true;
+ if (!asymmVar(elim)){
+ ok = false; goto cleanup; }
+ frozen[elim] = was_frozen; }
+
+ // At this point, the variable may have been set by assymetric branching, so check it
+ // again. Also, don't eliminate frozen variables:
+ if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
+ ok = false; goto cleanup; }
+
+ checkGarbage(simp_garbage_frac);
+ }
+
+ assert(subsumption_queue.size() == 0);
+ }
+ cleanup:
+
+ // If no more simplification is needed, free all simplification-related data structures:
+ if (turn_off_elim){
+ touched .clear(true);
+ occurs .clear(true);
+ n_occ .clear(true);
+ elim_heap.clear(true);
+ subsumption_queue.clear(true);
+
+ use_simplification = false;
+ remove_satisfied = true;
+ ca.extra_clause_field = false;
+
+ // Force full cleanup (this is safe and desirable since it only happens once):
+ rebuildOrderHeap();
+ garbageCollect();
+ }else{
+ // Cheaper cleanup:
+ cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
+ checkGarbage();
+ }
+
+ if (verbosity >= 1 && elimclauses.size() > 0)
+ printf("| Eliminated clauses: %10.2f Mb |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+
+ return ok;
+}
+
+
+void SimpSolver::cleanUpClauses()
+{
+ occurs.cleanAll();
+ int i,j;
+ for (i = j = 0; i < clauses.size(); i++)
+ if (ca[clauses[i]].mark() == 0)
+ clauses[j++] = clauses[i];
+ clauses.shrink(i - j);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+
+void SimpSolver::relocAll(ClauseAllocator& to)
+{
+ if (!use_simplification) return;
+
+ // All occurs lists:
+ //
+ for (int i = 0; i < nVars(); i++){
+ vec<CRef>& cs = occurs[i];
+ for (int j = 0; j < cs.size(); j++)
+ ca.reloc(cs[j], to);
+ }
+
+ // Subsumption queue:
+ //
+ for (int i = 0; i < subsumption_queue.size(); i++)
+ ca.reloc(subsumption_queue[i], to);
+
+ // Temporary clause:
+ //
+ ca.reloc(bwdsub_tmpunit, to);
+}
+
+
+void SimpSolver::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());
+
+ cleanUpClauses();
+ to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
+ relocAll(to);
+ Solver::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);
+}
/************************************************************************************[SimpSolver.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 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,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef SimpSolver_h
-#define SimpSolver_h
-
-#include <ctime>
-#include <cstdio>
+#ifndef Minisat_SimpSolver_h
+#define Minisat_SimpSolver_h
#include "../mtl/Queue.h"
#include "../core/Solver.h"
-namespace MINISAT {
-
-/*************************************************************************************/
-/* #ifdef _MSC_VER */
-/* #include <ctime> */
-
-/* static inline double cpuTime(void) { */
-/* return (double)clock() / CLOCKS_PER_SEC; } */
-/* #else */
-
-/* #include <sys/time.h> */
-/* #include <sys/resource.h> */
-/* #include <unistd.h> */
-
-/* static inline double cpuTime(void) { */
-/* struct rusage ru; */
-/* getrusage(RUSAGE_SELF, &ru); */
-/* return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } */
-/* #endif */
-
-
-/* #if defined(__linux__) */
-/* static inline int memReadStat(int field) */
-/* { */
-/* char name[256]; */
-/* pid_t pid = getpid(); */
-/* sprintf(name, "/proc/%d/statm", pid); */
-/* FILE* in = fopen(name, "rb"); */
-/* if (in == NULL) return 0; */
-/* int value; */
-/* for (; field >= 0; field--) */
-/* fscanf(in, "%d", &value); */
-/* fclose(in); */
-/* return value; */
-/* } */
-/* static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } */
-
-
-/* #elif defined(__FreeBSD__) */
-/* static inline uint64_t memUsed(void) { */
-/* struct rusage ru; */
-/* getrusage(RUSAGE_SELF, &ru); */
-/* return ru.ru_maxrss*1024; } */
-
-
-/* #else */
-/* static inline uint64_t memUsed() { return 0; } */
-/* #endif */
-
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
+
+namespace Minisat {
+
+//=================================================================================================
+
class SimpSolver : public Solver {
public:
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true);
- bool addClause (vec<Lit>& ps);
+ bool addClause (const vec<Lit>& ps);
+ bool addEmptyClause(); // Add the empty clause to the solver.
+ 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_( vec<Lit>& ps);
+ bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
// Variable mode:
//
void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+ bool isEliminated(Var v) const;
// Solving:
//
- bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
- bool solve ();
- bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
+ bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ bool solve ( bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+ bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+
// Generate a (possibly simplified) DIMACS file:
//
+#if 0
+ void toDimacs (const char* file, const vec<Lit>& assumps);
void toDimacs (const char* file);
+ void toDimacs (const char* file, Lit p);
+ void toDimacs (const char* file, Lit p, Lit q);
+ void toDimacs (const char* file, Lit p, Lit q, Lit r);
+#endif
// Mode of operation:
//
- int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
- bool asymm_mode; // Shrink clauses by asymmetric branching.
- bool redundancy_check; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+ int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
+ int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
+ // -1 means no limit.
+ int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
+ double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+ bool use_asymm; // Shrink clauses by asymmetric branching.
+ bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+ bool use_elim; // Perform variable elimination.
// Statistics:
//
int merges;
int asymm_lits;
- int remembered_clauses;
+ int eliminated_vars;
-// protected:
- public:
+ protected:
// Helper structures:
//
- struct ElimData {
- int order; // 0 means not eliminated, >0 gives an index in the elimination order
- vec<Clause*> eliminated;
- ElimData() : order(0) {} };
-
- struct ElimOrderLt {
- const vec<ElimData>& elimtable;
- ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
- bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
-
struct ElimLt {
const vec<int>& n_occ;
- ElimLt(const vec<int>& no) : n_occ(no) {}
- int cost (Var x) const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
- bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
-
+ explicit ElimLt(const vec<int>& no) : n_occ(no) {}
+
+ // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+ // 32-bit implementation instead then, but this will have to do for now.
+ uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
+ bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+
+ // TODO: investigate this order alternative more.
+ // 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; }
+ };
+
+ struct ClauseDeleted {
+ const ClauseAllocator& ca;
+ explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+ bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
// Solver state:
//
int elimorder;
bool use_simplification;
- vec<ElimData> elimtable;
+ vec<uint32_t> elimclauses;
vec<char> touched;
- vec<vec<Clause*> > occurs;
+ OccLists<Var, vec<CRef>, ClauseDeleted>
+ occurs;
vec<int> n_occ;
Heap<ElimLt> elim_heap;
- Queue<Clause*> subsumption_queue;
+ Queue<CRef> subsumption_queue;
vec<char> frozen;
+ vec<char> eliminated;
int bwdsub_assigns;
+ int n_touched;
// Temporaries:
//
- Clause* bwdsub_tmpunit;
+ CRef bwdsub_tmpunit;
// Main internal methods:
//
- bool asymm (Var v, Clause& c);
+ lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
+ bool asymm (Var v, CRef cr);
bool asymmVar (Var v);
void updateElimHeap (Var v);
- void cleanOcc (Var v);
- vec<Clause*>& getOccurs (Var x);
void gatherTouchedClauses ();
bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
- bool merge (const Clause& _ps, const Clause& _qs, Var v);
+ bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
bool backwardSubsumptionCheck (bool verbose = false);
- bool eliminateVar (Var v, bool fail = false);
- void remember (Var v);
+ bool eliminateVar (Var v);
void extendModel ();
- void verifyModel ();
- void removeClause (Clause& c);
- bool strengthenClause (Clause& c, Lit l);
+ void removeClause (CRef cr);
+ bool strengthenClause (CRef cr, Lit l);
void cleanUpClauses ();
bool implied (const vec<Lit>& c);
- void toDimacs (FILE* f, Clause& c);
- bool isEliminated (Var v) const;
-
+ void relocAll (ClauseAllocator& to);
};
//=================================================================================================
// Implementation of inline methods:
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
inline void SimpSolver::updateElimHeap(Var v) {
- if (elimtable[v].order == 0)
+ assert(use_simplification);
+ // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+ if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
elim_heap.update(v); }
-inline void SimpSolver::cleanOcc(Var v) {
- assert(use_simplification);
- Clause **begin = (Clause**)occurs[v];
- Clause **end = begin + occurs[v].size();
- Clause **i, **j;
- for (i = begin, j = end; i < j; i++)
- if ((*i)->mark() == 1){
- *i = *(--j);
- i--;
- }
- //occurs[v].shrink_(end - j); // This seems slower. Why?!
- occurs[v].shrink(end - j);
-}
-inline vec<Clause*>& SimpSolver::getOccurs(Var x) {
- cleanOcc(x); return occurs[x]; }
+inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
+
+inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
-inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; }
-inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
-inline bool SimpSolver::solve () { vec<Lit> tmp; return solve(tmp, true, false); }
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
//=================================================================================================
-};
+}
+
#endif
#include "ToSATAIG.h"
#include "../../simplifier/constantBitP/ConstantBitPropagation.h"
-#include "../../sat/sat.h"
namespace BEEV
{
// Can not be used with abstraction refinement.
bool
- ToSATAIG::CallSAT(MINISAT::Solver& satSolver, const ASTNode& input)
+ ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input)
{
if (cb != NULL && cb->isUnsatisfiable())
return false;
for (int i = 0; i < cnfData->nVars; i++)
satSolver.newVar();
- MINISAT::vec<MINISAT::Lit> satSolverClause;
+ SATSolver::vec_literals satSolverClause;
for (int i = 0; i < cnfData->nClauses; i++)
{
satSolverClause.clear();
for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i
+ 1]; pLit < pStop; pLit++)
{
- Var var = (*pLit) >> 1;
+ SATSolver::Var var = (*pLit) >> 1;
assert(var < satSolver.nVars());
- MINISAT::Lit l(var, (*pLit) & 1);
+ Minisat::Lit l = SATSolver::mkLit(var, (*pLit) & 1);
satSolverClause.push(l);
}
exit(0);
}
- // cryptominisat treats simplify() as protected.
-#ifndef CRYPTOMINISAT2
- bm->GetRunTimes()->start(RunTimes::SATSimplifying);
- if (!satSolver.simplify())
- {
- bm->GetRunTimes()->stop(RunTimes::SATSimplifying);
- return false;
- }
- bm->GetRunTimes()->stop(RunTimes::SATSimplifying);
-#endif
-
-
-
bm->GetRunTimes()->start(RunTimes::Solving);
satSolver.solve();
bm->GetRunTimes()->stop(RunTimes::Solving);
- if (bm->UserFlags.stats_flag)
- bm->PrintStats(satSolver);
+ if(bm->UserFlags.stats_flag)
+ satSolver.printStats();
return satSolver.okay();
}
}
// Can not be used with abstraction refinement.
- bool CallSAT(MINISAT::Solver& satSolver, const ASTNode& input);
+ bool CallSAT(SATSolver& satSolver, const ASTNode& input);
};
}
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
-#include "../sat/sat.h"
#include "ToCNF.h"
namespace BEEV
* _ASTNode_to_SATVar.
*/
- MINISAT::Var
- ToSAT::LookupOrCreateSATVar(MINISAT::Solver& newSolver, const ASTNode& n)
+ SATSolver::Var
+ ToSAT::LookupOrCreateSATVar(SATSolver& newSolver, const ASTNode& n)
{
ASTtoSATMap::iterator it;
- MINISAT::Var v;
+ SATSolver::Var v;
//look for the symbol in the global map from ASTNodes to ints. if
//not found, create a S.newVar(), else use the existing one.
//ASSUMPTION: I am assuming that the newSolver.newVar() call increments v
//by 1 each time it is called, and the initial value of a
- //MINISAT::Var is 0.
+ //SATSolver::Var is 0.
// Copies the symbol into the map that is used to build the counter example.
// For boolean we create a vector of size 1.
}
// experimental. Don't add Tseitin variables as decision variables.
- if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
- {
- newSolver.setDecisionVar(v,false);
- }
+ //if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
+ //{
+// newSolver.setDecisionVar(v,false);
+ // }
}
else
* and calls solve(). If solve returns unsat, then stop and return
* unsat. else continue.
*/
- bool ToSAT::toSATandSolve(MINISAT::Solver& newSolver,
+ bool ToSAT::toSATandSolve(SATSolver& newSolver,
ClauseList& cll,
bool final,
CNFMgr*& cm,
if(bm->UserFlags.random_seed_flag)
{
-#ifdef CRYPTOMINISAT2
newSolver.setSeed(bm->UserFlags.random_seed);
-#endif
}
ClauseContainer& cc = *cll.asList();
//Clause for the SATSolver
- MINISAT::vec<MINISAT::Lit> satSolverClause;
+ SATSolver::vec_literals satSolverClause;
//iterate through the list (conjunction) of ASTclauses cll
ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
//clauseVec.push_back(node);
bool negate = (NOT == node.GetKind()) ? true : false;
ASTNode n = negate ? node[0] : node;
- MINISAT::Var v = LookupOrCreateSATVar(newSolver, n);
- MINISAT::Lit l(v, negate);
+ SATSolver::Var v = LookupOrCreateSATVar(newSolver, n);
+ Minisat::Lit l = SATSolver::mkLit(v, negate);
satSolverClause.push(l);
}
}
else
{
- bm->PrintStats(newSolver);
+ if(bm->UserFlags.stats_flag)
+ newSolver.printStats();
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
cll.deleteJustVectors();
return false;
// CNF that need to be joined together. Nicer would be to read it out of the solver each time.
if (bm->UserFlags.output_CNF_flag && true)
{
- #if defined CRYPTOMINISAT2
- cerr << "The -j option will give you the xor clauses that this one doesn't" << endl;
- #endif
-
ofstream file;
stringstream fileName;
fileName << "output_" << CNFFileNameCounter++ << ".cnf";
ASTtoSATMap::iterator it = _ASTNode_to_SATVar_Map.find(n);
assert(it != _ASTNode_to_SATVar_Map.end());
- MINISAT::Var v = it->second;
+ SATSolver::Var v = it->second;
if (negate)
file << "-" << (v + 1) << " ";
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
bm->GetRunTimes()->start(RunTimes::Solving);
- #ifdef CORE
- // The call to simplify() was removed. I'm guessing because it didn't work well with cryptominisat.
- // so I'm only enabling it for just minisat.
- newSolver.simplify();
- #endif
newSolver.solve();
bm->GetRunTimes()->stop(RunTimes::Solving);
- bm->PrintStats(newSolver);
+ if(bm->UserFlags.stats_flag)
+ newSolver.printStats();
if (newSolver.okay())
return true;
else
return cb;
} //End of SortClauseList_IntoBuckets()
- bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
+ bool ToSAT::CallSAT_On_ClauseBuckets(SATSolver& SatSolver,
ClauseBuckets * cb, CNFMgr*& cm)
{
ClauseBuckets::iterator it = cb->begin();
//Call the SAT solver, and check the result before returning. This
//can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
//SOLVER_UNDECIDED
- bool ToSAT::CallSAT(MINISAT::Solver& SatSolver,
+ bool ToSAT::CallSAT(SATSolver& SatSolver,
const ASTNode& input)
{
bm->GetRunTimes()->start(RunTimes::BitBlasting);
// Looks up truth value of ASTNode SYMBOL in MINISAT satisfying
// assignment.
- ASTNode ToSAT::SymbolTruthValue(MINISAT::Solver &newSolver, ASTNode form)
+ ASTNode ToSAT::SymbolTruthValue(SATSolver &newSolver, ASTNode form)
{
- MINISAT::Var satvar = _ASTNode_to_SATVar_Map[form];
- if (newSolver.model[satvar] == MINISAT::l_False)
+ SATSolver::Var satvar = _ASTNode_to_SATVar_Map[form];
+ if (newSolver.model[satvar] == SATSolver::l_False)
{
return ASTFalse;
}
// immediately (on the leftmost lowest term). Use CreateSimpForm to
// evaluate, even though it's expensive, so that we can use the
// partial truth assignment.
- ASTNode ToSAT::CheckBBandCNF(MINISAT::Solver& newSolver, ASTNode form)
+ ASTNode ToSAT::CheckBBandCNF(SATSolver& newSolver, ASTNode form)
{
// Clear memo table (in case newSolver has changed).
CheckBBandCNFMemo.clear();
} //End of CheckBBandCNF()
// Recursive body CheckBBandCNF
- ASTNode ToSAT::CheckBBandCNF_int(MINISAT::Solver& newSolver, ASTNode form)
+ ASTNode ToSAT::CheckBBandCNF_int(SATSolver& newSolver, ASTNode form)
{
// cout << "++++++++++++++++"
// << endl
#include "ToCNF.h"
#include "../AST/AST.h"
-#include "../sat/sat.h"
#include "../STPManager/STPManager.h"
#include "ToSATBase.h"
* Private Typedefs and Data *
****************************************************************/
- // MAP: This is a map from ASTNodes to MINISAT::Vars.
+ // MAP: This is a map from ASTNodes to SATSolver::Vars.
//
// The map is populated while ASTclauses are read from the AST
// ClauseList returned by CNF converter. For every new boolean
- // variable in ASTClause a new MINISAT::Var is created (these vars
+ // variable in ASTClause a new SATSolver::Var is created (these vars
// typedefs for ints)
typedef HASHMAP<
ASTNode,
- MINISAT::Var,
+ SATSolver::Var,
ASTNode::ASTNodeHasher,
ASTNode::ASTNodeEqual> ASTtoSATMap;
ASTtoSATMap _ASTNode_to_SATVar_Map;
- // MAP: This is a map from ASTNodes to MINISAT::Vars for SYMBOLS>
+ // MAP: This is a map from ASTNodes to SATSolver::Vars for SYMBOLS>
//
// Reverse map used in building counterexamples. MINISAT returns a
// model in terms of MINISAT Vars, and this map helps us convert
//looksup a MINISAT var from the minisat-var memo-table. if none
//exists, then creates one. Treat the result as const.
- MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S,
+ SATSolver::Var LookupOrCreateSATVar(SATSolver& S,
const ASTNode& n);
//Iteratively goes through the Clause Buckets, and calls
//toSATandSolve()
- bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
+ bool CallSAT_On_ClauseBuckets(SATSolver& SatSolver,
ClauseBuckets * cb
, CNFMgr*& cm);
// Converts the clause to SAT and calls SAT solver
- bool toSATandSolve(MINISAT::Solver& S,
+ bool toSATandSolve(SATSolver& S,
ClauseList& cll,
bool final,
CNFMgr*& cm,
}
// Bitblasts, CNF conversion and calls toSATandSolve()
- bool CallSAT(MINISAT::Solver& SatSolver,
+ bool CallSAT(SATSolver& SatSolver,
const ASTNode& input);
ASTNodeToSATVar& SATVar_to_SymbolIndexMap()
void PrintOutput(SOLVER_RETURN_TYPE ret);
// Bitblasts, CNF conversion and calls toSATandSolve()
- virtual bool CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input) =0;
+ virtual bool CallSAT(SATSolver& SatSolver, const ASTNode& input) =0;
virtual ASTNodeToSATVar& SATVar_to_SymbolIndexMap()= 0;
projects / francis / stp.git / commitdiff