Minisat Namespace Reference

Classes
class	BoolOption
class	Clause
class	ClauseAllocator
class	CMap
struct	DeepEqual
struct	DeepHash
class	DoubleOption
struct	DoubleRange
struct	Equal
struct	Hash
class	Heap
struct	Int64Range
class	IntOption
struct	IntRange
class	lbool
struct	LessThan_default
struct	Lit
class	Map
class	OccLists
class	Option
class	OutOfMemoryException
class	Queue
class	RegionAllocator
class	SimpSolver
class	Solver
class	StreamBuffer
class	StringOption
class	vec

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

Functions
int	parseOptions (int &argc, char **argv, bool strict=false)
int	printUsageAndExit (int argc, char **argv, bool verbose=false)
void	setUsageHelp (const char *str)
void	setHelpPrefixStr (const char *str)
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)
template<class T, class LessThan>
void	selectionSort (T *array, int size, LessThan lt)
template<class T, class LessThan>
void	sort (T *array, int size, LessThan lt)
template<class T, class LessThan>
void	sort (vec< T > &v, LessThan lt)
template<class T>
void	sort (vec< T > &v)
double	memUsed ()
double	memUsedPeak ()

Variables
const Lit	lit_Undef = { -2 }
const Lit	lit_Error = { -1 }
const CRef	CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef

Typedef Documentation

CRef

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

Definition at line 123 of file SolverTypes.h.

Var

typedef int Minisat::Var

Definition at line 44 of file SolverTypes.h.

Function Documentation

memUsed()

ABC_NAMESPACE_IMPL_START double Minisat::memUsed ( )

extern

Definition at line 107 of file System.cpp.

{ return 0; }

memUsedPeak()

double Minisat::memUsedPeak ( )

extern

Definition at line 108 of file System.cpp.

{ return 0; }

Here is the caller graph for this function:

mkLit()

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

inline

Definition at line 60 of file SolverTypes.h.

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

Here is the caller graph for this function:

operator^()

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

inline

Definition at line 62 of file SolverTypes.h.

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

operator~()

Lit Minisat::operator~ ( Lit p )

inline

Definition at line 61 of file SolverTypes.h.

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

parseOptions()

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

extern

Definition at line 28 of file Options.cpp.

{
    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')
                return printUsageAndExit(argc, argv);
            else if (match(str, "-verb"))
                return 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()); return 0; } //  exit(0);
                else
                    argv[j++] = argv[i];
            }
        }
    }
 
    argc -= (i - j);
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

printUsageAndExit()

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

extern

Definition at line 64 of file Options.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

selectionSort()

template<class T, class LessThan>

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

Definition at line 40 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:

setHelpPrefixStr()

void Minisat::setHelpPrefixStr ( const char * str )

extern

Definition at line 63 of file Options.cpp.

{ Option::getHelpPrefixString() = str; }

Here is the call graph for this function:

setUsageHelp()

void Minisat::setUsageHelp ( const char * str )

extern

Definition at line 62 of file Options.cpp.

{ Option::getUsageString() = str; }

Here is the call graph for this function:

Here is the caller graph for this function:

sign()

bool Minisat::sign ( Lit p )

inline

Definition at line 63 of file SolverTypes.h.

{ return p.x & 1; }

Here is the caller graph for this function:

sort() [1/3]

template<class T, class LessThan>

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

Definition at line 58 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:

sort() [2/3]

template<class T>

void Minisat::sort

(

vec< T > &

v

)

Definition at line 92 of file Sort.h.

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

Here is the call graph for this function:

sort() [3/3]

template<class T, class LessThan>

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

Definition at line 90 of file Sort.h.

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

Here is the call graph for this function:

toInt() [1/3]

int Minisat::toInt ( lbool l )

inline

Definition at line 116 of file SolverTypes.h.

{ return l.value; }

toInt() [2/3]

int Minisat::toInt ( Lit p )

inline

Definition at line 68 of file SolverTypes.h.

{ return p.x; } 

toInt() [3/3]

int Minisat::toInt ( Var v )

inline

Definition at line 67 of file SolverTypes.h.

{ return v; } 

Here is the caller graph for this function:

toLbool()

lbool Minisat::toLbool ( int v )

inline

Definition at line 117 of file SolverTypes.h.

{ return lbool((uint8_t)v);  }

toLit()

Lit Minisat::toLit ( int i )

inline

Definition at line 69 of file SolverTypes.h.

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

Here is the caller graph for this function:

var()

int Minisat::var ( Lit p )

inline

Definition at line 64 of file SolverTypes.h.

{ return p.x >> 1; }

Here is the caller graph for this function:

Variable Documentation

CRef_Undef

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

Definition at line 195 of file SolverTypes.h.

lit_Error

const Lit Minisat::lit_Error = { -1 }

Definition at line 75 of file SolverTypes.h.

{ -1 };  // }

lit_Undef

const Lit Minisat::lit_Undef = { -2 }

Definition at line 74 of file SolverTypes.h.

{ -2 };  // }- Useful special constants.