Minisat Namespace Reference

Data Structures
class	RegionAllocator
class	Heap
struct	MkIndexDefault
class	IntMap
class	IntSet
struct	Hash
struct	Equal
struct	DeepHash
struct	DeepEqual
class	Map
class	Option
struct	IntRange
struct	Int64Range
struct	DoubleRange
class	DoubleOption
class	IntOption
class	Int64Option
class	StringOption
class	BoolOption
class	StreamBuffer
class	Queue
class	SimpSolver
class	Solver
struct	Lit
struct	MkIndexLit
class	VMap
class	LMap
class	LSet
class	lbool
class	Clause
class	ClauseAllocator
class	ClauseIterator
class	TrailIterator
class	OccLists
class	CMap
struct	LessThan_default
class	vec
class	OutOfMemoryException

Typedefs
typedef int	Var
typedef RegionAllocator < uint32_t >::Ref	CRef

Functions
template<class V , class T >
static void	remove (V &ts, const T &t)
template<class V , class T >
static bool	find (V &ts, const T &t)
template<class T >
static void	copy (const T &from, T &to)
template<class T >
static void	copy (const vec< T > &from, vec< T > &to, bool append=false)
template<class T >
static void	append (const vec< T > &from, vec< T > &to)
template<class B , class Solver >
static void	readClause (B &in, Solver &S, vec< Lit > &lits)
template<class B , class Solver >
static void	parse_DIMACS_main (B &in, Solver &S, bool strictp=false)
template<class Solver >
static void	parse_DIMACS (gzFile input_stream, Solver &S, bool strictp=false)
static uint32_t	hash (uint32_t x)
static uint32_t	hash (uint64_t x)
static uint32_t	hash (int32_t x)
static uint32_t	hash (int64_t x)
void	parseOptions (int &argc, char **argv, bool strict=false)
void	printUsageAndExit (int argc, char **argv, bool verbose=false)
void	setUsageHelp (const char *str)
void	setHelpPrefixStr (const char *str)
static bool	isEof (StreamBuffer &in)
static bool	isEof (const char *in)
template<class B >
static void	skipWhitespace (B &in)
template<class B >
static void	skipLine (B &in)
template<class B >
static int	parseInt (B &in)
template<class B >
static bool	match (B &in, const char *str)
template<class B >
static bool	eagerMatch (B &in, const char *str)
static double	drand (double &seed)
static int	irand (double &seed, int size)
template<class T >
static void	randomShuffle (double &seed, vec< T > &xs)
template<class T >
static void	randomShuffle (double &seed, vec< vec< T > > &xs)
Lit	mkLit (Var var, bool sign=false)
Lit	operator~ (Lit p)
Lit	operator^ (Lit p, bool b)
bool	sign (Lit p)
int	var (Lit p)
int	toInt (Var v)
int	toInt (Lit p)
Lit	toLit (int i)
int	toInt (lbool l)
lbool	toLbool (int v)
const lbool	l_True ((uint8_t) 0)
const lbool	l_False ((uint8_t) 1)
const lbool	l_Undef ((uint8_t) 2)
template<class T , class LessThan >
void	selectionSort (T *array, int size, LessThan lt)
template<class T >
static void	selectionSort (T *array, int size)
template<class T , class LessThan >
void	sort (T *array, int size, LessThan lt)
template<class T >
static void	sort (T *array, int size)
template<class T , class LessThan >
void	sort (vec< T > &v, LessThan lt)
template<class T >
void	sort (vec< T > &v)
static double	cpuTime (void)
double	memUsed ()
double	memUsedPeak (bool strictlyPeak=false)
void	setX86FPUPrecision ()
void	limitMemory (uint64_t max_mem_mb)
void	limitTime (uint32_t max_cpu_time)
void	sigTerm (void handler(int))
static void *	xrealloc (void *ptr, size_t size)

Variables
static const int	nprimes = 25
static const int	primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }
const Var	var_Undef = -1
const Lit	lit_Undef = { -2 }
const Lit	lit_Error = { -1 }
const CRef	CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef

Typedef Documentation

typedef RegionAllocator<uint32_t>::Ref Minisat::CRef

Definition at line 137 of file SolverTypes.h.

typedef int Minisat::Var

Definition at line 43 of file SolverTypes.h.

Function Documentation

template<class T >

static void Minisat::append ( const vec< T > &  from, vec< T > &  to  )

inlinestatic

Definition at line 79 of file Alg.h.

{ copy(from, to, true); }

Here is the call graph for this function:

Here is the caller graph for this function:

template<class T >

static void Minisat::copy ( const T &  from, T &  to  )

inlinestatic

Definition at line 61 of file Alg.h.

{
    to = from;
}

Here is the caller graph for this function:

template<class T >

static void Minisat::copy ( const vec< T > &  from, vec< T > &  to, bool  append = false  )

inlinestatic

Definition at line 68 of file Alg.h.

{
    if (!append)
        to.clear();
    for (int i = 0; i < from.size(); i++){
        to.push();
        copy(from[i], to.last());
    }
}

Here is the call graph for this function:

static double Minisat::cpuTime ( void  )

inlinestatic

Definition at line 65 of file System.h.

                                          {
    struct rusage ru;
    getrusage(RUSAGE_SELF, &ru);
    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }

Here is the caller graph for this function:

static double Minisat::drand ( double &  seed )

inlinestatic

Definition at line 27 of file Rnd.h.

{
    seed *= 1389796;
    int q = (int)(seed / 2147483647);
    seed -= (double)q * 2147483647;
    return seed / 2147483647;
}

Here is the caller graph for this function:

template<class B >

static bool Minisat::eagerMatch ( B &  in, const char *  str  )

static

Definition at line 109 of file ParseUtils.h.

                                               {
    for (; *str != '\0'; ++str, ++in)
        if (*str != *in)
            return false;
    return true; }

Here is the caller graph for this function:

template<class V , class T >

static bool Minisat::find ( V &  ts, const T &  t  )

inlinestatic

Definition at line 47 of file Alg.h.

{
    int j = 0;
    for (; j < (int)ts.size() && ts[j] != t; j++);
    return j < (int)ts.size();
}

Here is the caller graph for this function:

static uint32_t Minisat::hash ( uint32_t  x )

inlinestatic

Definition at line 38 of file Map.h.

{ return x; }

Here is the caller graph for this function:

static uint32_t Minisat::hash ( uint64_t  x )

inlinestatic

Definition at line 39 of file Map.h.

{ return (uint32_t)x; }

static uint32_t Minisat::hash ( int32_t  x )

inlinestatic

Definition at line 40 of file Map.h.

{ return (uint32_t)x; }

static uint32_t Minisat::hash ( int64_t  x )

inlinestatic

Definition at line 41 of file Map.h.

{ return (uint32_t)x; }

static int Minisat::irand ( double &  seed, int  size  )

inlinestatic

Definition at line 37 of file Rnd.h.

{ return (int)(drand(seed) * size); }

Here is the call graph for this function:

Here is the caller graph for this function:

static bool Minisat::isEof ( StreamBuffer &  in )

inlinestatic

Definition at line 58 of file ParseUtils.h.

{ return *in == EOF;  }

Here is the caller graph for this function:

static bool Minisat::isEof ( const char *  in )

inlinestatic

Definition at line 59 of file ParseUtils.h.

{ return *in == '\0'; }

const lbool Minisat::l_False

(

(uint8_t)

1

)

Here is the caller graph for this function:

const lbool Minisat::l_True

(

(uint8_t)

0

)

Here is the caller graph for this function:

const lbool Minisat::l_Undef

(

(uint8_t)

2

)

Here is the caller graph for this function:

void Minisat::limitMemory

(

uint64_t

max_mem_mb

)

Definition at line 112 of file System.cc.

{
// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.
#if defined(__OpenBSD__)
#define RLIMIT_AS RLIMIT_DATA
#endif

    // Set limit on virtual memory:
    if (max_mem_mb != 0){
        rlim_t new_mem_lim = (rlim_t)max_mem_mb * 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 defined(__OpenBSD__)
#undef RLIMIT_AS
#endif
}

void Minisat::limitTime

(

uint32_t

max_cpu_time

)

Definition at line 144 of file System.cc.

{
    if (max_cpu_time != 0){
        rlimit rl;
        getrlimit(RLIMIT_CPU, &rl);
        if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){
            rl.rlim_cur = max_cpu_time;
            if (setrlimit(RLIMIT_CPU, &rl) == -1)
                printf("WARNING! Could not set resource limit: CPU-time.\n");
        }
    }
}

template<class B >

static bool Minisat::match ( B &  in, const char *  str  )

static

Definition at line 96 of file ParseUtils.h.

                                          {
    int i;
    for (i = 0; str[i] != '\0'; i++)
        if (in[i] != str[i])
            return false;

    in += i;

    return true; 
}

Here is the caller graph for this function:

double Minisat::memUsed

(

)

Definition at line 95 of file System.cc.

{ return 0; }

double Minisat::memUsedPeak

(

bool

strictlyPeak = false

)

Definition at line 96 of file System.cc.

{ return 0; }

Here is the caller graph for this function:

Lit Minisat::mkLit ( Var  var, bool  sign = false  )

inline

Definition at line 63 of file SolverTypes.h.

{ Lit p; p.x = var + var + (int)sign; return p; }

Here is the call graph for this function:

Here is the caller graph for this function:

Lit Minisat::operator^ ( Lit  p, bool  b  )

inline

Definition at line 65 of file SolverTypes.h.

{ Lit q; q.x = p.x ^ (unsigned int)b; return q; }

Lit Minisat::operator~ ( Lit  p )

inline

Definition at line 64 of file SolverTypes.h.

{ Lit q; q.x = p.x ^ 1; return q; }

template<class Solver >

static void Minisat::parse_DIMACS ( gzFile  input_stream, Solver &  S, bool  strictp = false  )

static

Definition at line 80 of file Dimacs.h.

                                                                               {
    StreamBuffer in(input_stream);
    parse_DIMACS_main(in, S, strictp); }

Here is the call graph for this function:

template<class B , class Solver >

static void Minisat::parse_DIMACS_main ( B &  in, Solver &  S, bool  strictp = false  )

static

Definition at line 48 of file Dimacs.h.

                                                                      {
    vec<Lit> lits;
    int vars    = 0;
    int clauses = 0;
    int cnt     = 0;
    for (;;){
        skipWhitespace(in);
        if (*in == EOF) break;
        else if (*in == 'p'){
            if (eagerMatch(in, "p cnf")){
                vars    = parseInt(in);
                clauses = parseInt(in);
                // SATRACE'06 hack
                // if (clauses > 4000000)
                //     S.eliminate(true);
            }else{
                printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
            }
        } else if (*in == 'c' || *in == 'p')
            skipLine(in);
        else{
            cnt++;
            readClause(in, S, lits);
            S.addClause_(lits); }
    }
    if (strictp && cnt != clauses)
        printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

template<class B >

static int Minisat::parseInt ( B &  in )

static

Definition at line 80 of file ParseUtils.h.

                           {
    int     val = 0;
    bool    neg = false;
    skipWhitespace(in);
    if      (*in == '-') neg = true, ++in;
    else if (*in == '+') ++in;
    if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
    while (*in >= '0' && *in <= '9')
        val = val*10 + (*in - '0'),
        ++in;
    return neg ? -val : val; }

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::parseOptions	(	int &	argc,
		char **	argv,
		bool	strict = false
	)

Definition at line 28 of file Options.cc.

{
    int i, j;
    for (i = j = 1; i < argc; i++){
        const char* str = argv[i];
        if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
            if (*str == '\0')
                printUsageAndExit(argc, argv);
            else if (match(str, "-verb"))
                printUsageAndExit(argc, argv, true);
        } else {
            bool parsed_ok = false;
        
            for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
                parsed_ok = Option::getOptionList()[k]->parse(argv[i]);

                // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
            }

            if (!parsed_ok){
                if (strict && match(argv[i], "-"))
                    fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
                else
                    argv[j++] = argv[i];
            }
        }
    }

    argc -= (i - j);
}

Here is the call graph for this function:

void Minisat::printUsageAndExit	(	int	argc,
		char **	argv,
		bool	verbose = false
	)

Definition at line 62 of file Options.cc.

{
    const char* usage = Option::getUsageString();
    if (usage != NULL)
        fprintf(stderr, usage, argv[0]);

    sort(Option::getOptionList(), Option::OptionLt());

    const char* prev_cat  = NULL;
    const char* prev_type = NULL;

    for (int i = 0; i < Option::getOptionList().size(); i++){
        const char* cat  = Option::getOptionList()[i]->category;
        const char* type = Option::getOptionList()[i]->type_name;

        if (cat != prev_cat)
            fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
        else if (type != prev_type)
            fprintf(stderr, "\n");

        Option::getOptionList()[i]->help(verbose);

        prev_cat  = Option::getOptionList()[i]->category;
        prev_type = Option::getOptionList()[i]->type_name;
    }

    fprintf(stderr, "\nHELP OPTIONS:\n\n");
    fprintf(stderr, "  --%shelp        Print help message.\n", Option::getHelpPrefixString());
    fprintf(stderr, "  --%shelp-verb   Print verbose help message.\n", Option::getHelpPrefixString());
    fprintf(stderr, "\n");
    exit(0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

template<class T >

static void Minisat::randomShuffle ( double &  seed, vec< T > &  xs  )

static

Definition at line 42 of file Rnd.h.

{
    for (int i = 0; i < xs.size(); i++){
        int pick = i + irand(seed, xs.size() - i);
        T tmp = xs[i];
        xs[i] = xs[pick];
        xs[pick] = tmp;
    }
}

Here is the call graph for this function:

template<class T >

static void Minisat::randomShuffle ( double &  seed, vec< vec< T > > &  xs  )

static

Definition at line 54 of file Rnd.h.

{
    for (int i = 0; i < xs.size(); i++){
        int pick = i + irand(seed, xs.size() - i);
        vec<T> tmp; xs[i].moveTo(tmp);
        xs[pick].moveTo(xs[i]);
        tmp.moveTo(xs[pick]);
    }
}

Here is the call graph for this function:

template<class B , class Solver >

static void Minisat::readClause ( B &  in, Solver &  S, vec< Lit > &  lits  )

static

Definition at line 35 of file Dimacs.h.

                                                         {
    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) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

template<class V , class T >

static void Minisat::remove ( V &  ts, const T &  t  )

inlinestatic

Definition at line 36 of file Alg.h.

{
    int j = 0;
    for (; j < (int)ts.size() && ts[j] != t; j++);
    assert(j < (int)ts.size());
    for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];
    ts.pop();
}

template<class T , class LessThan >

void Minisat::selectionSort	(	T *	array,
		int	size,
		LessThan	lt
	)

Definition at line 39 of file Sort.h.

{
    int     i, j, best_i;
    T       tmp;

    for (i = 0; i < size-1; i++){
        best_i = i;
        for (j = i+1; j < size; j++){
            if (lt(array[j], array[best_i]))
                best_i = j;
        }
        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
    }
}

Here is the caller graph for this function:

template<class T >

static void Minisat::selectionSort ( T *  array, int  size  )

inlinestatic

Definition at line 53 of file Sort.h.

                                                                        {
    selectionSort(array, size, LessThan_default<T>()); }

Here is the call graph for this function:

void Minisat::setHelpPrefixStr

(

const char *

str

)

Definition at line 61 of file Options.cc.

{ Option::getHelpPrefixString() = str; }

Here is the call graph for this function:

void Minisat::setUsageHelp

(

const char *

str

)

Definition at line 60 of file Options.cc.

{ Option::getUsageString() = str; }

Here is the call graph for this function:

void Minisat::setX86FPUPrecision

(

)

Definition at line 100 of file System.cc.

{
#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
    // Only correct FPU precision on Linux architectures that needs and supports it:
    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
}

bool Minisat::sign ( Lit  p )

inline

Definition at line 66 of file SolverTypes.h.

{ return p.x & 1; }

Here is the caller graph for this function:

void Minisat::sigTerm

(

void

handlerint

)

Definition at line 164 of file System.cc.

{
    signal(SIGINT, handler);
    signal(SIGTERM,handler);
#ifdef SIGXCPU
    signal(SIGXCPU,handler);
#endif
}

template<class B >

static void Minisat::skipLine ( B &  in )

static

Definition at line 72 of file ParseUtils.h.

                            {
    for (;;){
        if (isEof(in)) return;
        if (*in == '\n') { ++in; return; }
        ++in; } }

Here is the call graph for this function:

Here is the caller graph for this function:

template<class B >

static void Minisat::skipWhitespace ( B &  in )

static

Definition at line 66 of file ParseUtils.h.

                                  {
    while ((*in >= 9 && *in <= 13) || *in == 32)
        ++in; }

Here is the caller graph for this function:

template<class T , class LessThan >

void Minisat::sort	(	T *	array,
		int	size,
		LessThan	lt
	)

Definition at line 57 of file Sort.h.

{
    if (size <= 15)
        selectionSort(array, size, lt);

    else{
        T           pivot = array[size / 2];
        T           tmp;
        int         i = -1;
        int         j = size;

        for(;;){
            do i++; while(lt(array[i], pivot));
            do j--; while(lt(pivot, array[j]));

            if (i >= j) break;

            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
        }

        sort(array    , i     , lt);
        sort(&array[i], size-i, lt);
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

template<class T >

static void Minisat::sort ( T *  array, int  size  )

inlinestatic

Definition at line 81 of file Sort.h.

                                                               {
    sort(array, size, LessThan_default<T>()); }

Here is the call graph for this function:

template<class T , class LessThan >

void Minisat::sort	(	vec< T > &	v,
		LessThan	lt
	)

Definition at line 89 of file Sort.h.

                                                                     {
    sort((T*)v, v.size(), lt); }

Here is the call graph for this function:

template<class T >

void Minisat::sort

(

vec< T > &

v

)

Definition at line 91 of file Sort.h.

                                        {
    sort(v, LessThan_default<T>()); }

Here is the call graph for this function:

int Minisat::toInt ( Var  v )

inline

Definition at line 70 of file SolverTypes.h.

{ return v; } 

Here is the caller graph for this function:

int Minisat::toInt ( Lit  p )

inline

Definition at line 71 of file SolverTypes.h.

{ return p.x; } 

int Minisat::toInt ( lbool  l )

inline

Definition at line 120 of file SolverTypes.h.

{ return l.value; }

lbool Minisat::toLbool ( int  v )

inline

Definition at line 121 of file SolverTypes.h.

{ return lbool((uint8_t)v);  }

Lit Minisat::toLit ( int  i )

inline

Definition at line 72 of file SolverTypes.h.

{ Lit p; p.x = i; return p; } 

Here is the caller graph for this function:

int Minisat::var ( Lit  p )

inline

Definition at line 67 of file SolverTypes.h.

{ return p.x >> 1; }

Here is the caller graph for this function:

static void* Minisat::xrealloc ( void *  ptr, size_t  size  )

inlinestatic

Definition at line 33 of file XAlloc.h.

{
    void* mem = realloc(ptr, size);
    if (mem == NULL && errno == ENOMEM){
        throw OutOfMemoryException();
    }else
        return mem;
}

Here is the caller graph for this function:

Variable Documentation

const CRef Minisat::CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef

Definition at line 225 of file SolverTypes.h.

const Lit Minisat::lit_Error = { -1 }

Definition at line 78 of file SolverTypes.h.

const Lit Minisat::lit_Undef = { -2 }

Definition at line 77 of file SolverTypes.h.

const int Minisat::nprimes = 25

static

Definition at line 48 of file Map.h.

const int Minisat::primes[nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }

static

Definition at line 49 of file Map.h.

const Var Minisat::var_Undef = -1

Definition at line 47 of file SolverTypes.h.