Gluco 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	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
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 Gluco::CRef

Definition at line 130 of file SolverTypes.h.

Var

typedef int Gluco::Var

Definition at line 52 of file SolverTypes.h.

Function Documentation

memUsed()

ABC_NAMESPACE_IMPL_START double Gluco::memUsed ( )

extern

Definition at line 110 of file System.cpp.

                      { 
    return 0; }

Here is the caller graph for this function:

memUsedPeak()

double Gluco::memUsedPeak ( )

extern

mkLit()

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

inline

Definition at line 67 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 Gluco::operator^ ( Lit p, bool b )

inline

Definition at line 69 of file SolverTypes.h.

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

operator~()

Lit Gluco::operator~ ( Lit p )

inline

Definition at line 68 of file SolverTypes.h.

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

parseOptions()

void Gluco::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')
                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 Gluco::printUsageAndExit ( int argc, char ** argv, bool verbose = false )

extern

Definition at line 62 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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

selectionSort()

template<class T, class LessThan>

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

extern

Definition at line 61 of file Options.cpp.

{ Option::getHelpPrefixString() = str; }

Here is the call graph for this function:

setUsageHelp()

void Gluco::setUsageHelp ( const char * str )

extern

Definition at line 60 of file Options.cpp.

{ Option::getUsageString() = str; }

Here is the call graph for this function:

sign()

bool Gluco::sign ( Lit p )

inline

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

inline

Definition at line 123 of file SolverTypes.h.

{ return l.value; }

toInt() [2/3]

int Gluco::toInt ( Lit p )

inline

Definition at line 75 of file SolverTypes.h.

{ return p.x; } 

toInt() [3/3]

int Gluco::toInt ( Var v )

inline

Definition at line 74 of file SolverTypes.h.

{ return v; } 

Here is the caller graph for this function:

toLbool()

lbool Gluco::toLbool ( int v )

inline

Definition at line 124 of file SolverTypes.h.

{ return lbool((uint8_t)v);  }

toLit()

Lit Gluco::toLit ( int i )

inline

Definition at line 76 of file SolverTypes.h.

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

Here is the caller graph for this function:

var()

int Gluco::var ( Lit p )

inline

Definition at line 71 of file SolverTypes.h.

{ return p.x >> 1; }

Here is the caller graph for this function:

Variable Documentation

CRef_Undef

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

Definition at line 216 of file SolverTypes.h.

lit_Error

const Lit Gluco::lit_Error = { -1 }

Definition at line 82 of file SolverTypes.h.

{ -1 };  // }

lit_Undef

const Lit Gluco::lit_Undef = { -2 }

Definition at line 81 of file SolverTypes.h.

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