Gluco2 Namespace Reference

Classes
class	BoolOption
class	bqueue
class	Clause
class	ClauseAllocator
class	CMap
struct	DeepEqual
struct	DeepHash
class	DoubleOption
struct	DoubleRange
struct	Equal
struct	Hash
class	Heap
class	Heap2
class	Int64Option
struct	Int64Range
class	IntOption
struct	IntRange
class	lbool
struct	LessThan_default
struct	Lit
class	Map
class	OccLists
class	Option
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
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)
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
BoolOption	opt_certified_ (_certified, "certified", "Certified UNSAT using DRUP format", false)
StringOption	opt_certified_file_ (_certified, "certified-output", "Certified UNSAT output file", "NULL")
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 Gluco2::CRef

Definition at line 132 of file SolverTypes.h.

Var

typedef int Gluco2::Var

Definition at line 54 of file SolverTypes.h.

Function Documentation

memUsed()

ABC_NAMESPACE_IMPL_START double Gluco2::memUsed ( )

extern

Definition at line 110 of file System2.cpp.

                       { 
    return 0; }

Here is the caller graph for this function:

memUsedPeak()

double Gluco2::memUsedPeak ( )

extern

mkLit()

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

inline

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

operator^()

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

inline

Definition at line 71 of file SolverTypes.h.

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

operator~()

Lit Gluco2::operator~ ( Lit p )

inline

Definition at line 70 of file SolverTypes.h.

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

parseOptions()

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

extern

Definition at line 28 of file Options2.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')
                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:

printUsageAndExit()

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

extern

Definition at line 62 of file Options2.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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

selectionSort()

template<class T, class LessThan>

void Gluco2::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 Gluco2::setHelpPrefixStr ( const char * str )

extern

Definition at line 61 of file Options2.cpp.

{ Option::getHelpPrefixString() = str; }

Here is the call graph for this function:

setUsageHelp()

void Gluco2::setUsageHelp ( const char * str )

extern

Definition at line 60 of file Options2.cpp.

{ Option::getUsageString() = str; }

Here is the call graph for this function:

sign()

bool Gluco2::sign ( Lit p )

inline

Definition at line 72 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 Gluco2::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 Gluco2::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 Gluco2::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 Gluco2::toInt ( lbool l )

inline

Definition at line 125 of file SolverTypes.h.

{ return l.value; }

toInt() [2/3]

int Gluco2::toInt ( Lit p )

inline

Definition at line 77 of file SolverTypes.h.

{ return p.x; } 

toInt() [3/3]

int Gluco2::toInt ( Var v )

inline

Definition at line 76 of file SolverTypes.h.

{ return v; } 

Here is the caller graph for this function:

toLbool()

lbool Gluco2::toLbool ( int v )

inline

Definition at line 126 of file SolverTypes.h.

{ return lbool((uint8_t)v);  }

toLit()

Lit Gluco2::toLit ( int i )

inline

Definition at line 78 of file SolverTypes.h.

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

Here is the caller graph for this function:

var()

int Gluco2::var ( Lit p )

inline

Definition at line 73 of file SolverTypes.h.

{ return p.x >> 1; }

Here is the caller graph for this function:

Variable Documentation

CRef_Undef

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

Definition at line 222 of file SolverTypes.h.

lit_Error

const Lit Gluco2::lit_Error = { -1 }

Definition at line 84 of file SolverTypes.h.

{ -1 };  // }

lit_Undef

const Lit Gluco2::lit_Undef = { -2 }

Definition at line 83 of file SolverTypes.h.

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

opt_certified_

BoolOption Gluco2::opt_certified_(_certified, "certified", "Certified UNSAT using DRUP format", false)	(	_certified	,
		"certified"	,
		"Certified UNSAT using DRUP format"	,
		false	)

opt_certified_file_

StringOption Gluco2::opt_certified_file_(_certified, "certified-output", "Certified UNSAT output file", "NULL")	(	_certified	,
		"certified-output"	,
		"Certified UNSAT output file"	,
		"NULL"	)