Minisat::Internal 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
class	IntOption
struct	IntRange
class	lbool
struct	LessThan_default
struct	Lit
class	Map
class	OccLists
class	OutOfMemoryException
class	Queue
class	RegionAllocator
class	SimpSolver
class	Solver
class	vec

Typedefs
using	CRef = RegionAllocator< uint32_t >::Ref
using	Var = int

Functions
template<class T >
static void	append (const vec< T > &from, vec< T > &to)
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 B >
static bool	eagerMatch (B &in, const char *str)
template<class V , class T >
static bool	find (V &ts, const T &t)
static uint32_t	hash (int32_t x)
static uint32_t	hash (int64_t x)
static uint32_t	hash (uint32_t x)
static uint32_t	hash (uint64_t x)
template<class B >
static bool	match (B &in, const char *str)
Lit	mkLit (Var var, bool sign=false)
Lit	operator^ (Lit p, bool b)
Lit	operator~ (Lit p)
template<class B >
static int	parseInt (B &in)
template<class V , class T >
static void	remove (V &ts, const T &t)
template<class T >
static void	selectionSort (T *array, int size)
template<class T , class LessThan >
void	selectionSort (T *array, int size, LessThan lt)
bool	sign (Lit p)
template<class B >
static void	skipLine (B &in)
template<class B >
static void	skipWhitespace (B &in)
template<class T >
static void	sort (T *array, int size)
template<class T , class LessThan >
void	sort (T *array, int size, LessThan lt)
template<class T >
void	sort (vec< T > &v)
template<class T , class LessThan >
void	sort (vec< T > &v, LessThan lt)
int	toInt (lbool l)
int	toInt (Lit p)
int	toInt (Var v)
lbool	toLbool (int v)
Lit	toLit (int i)
int	var (Lit p)
static void *	xrealloc (void *ptr, size_t size)

Variables
static const int	buffer_size = 1048576
const CRef	CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef
const Lit	lit_Error = { -1 }
const Lit	lit_Undef = { -2 }
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 }

Typedef Documentation

CRef

using Minisat::Internal::CRef = typedef RegionAllocator<uint32_t>::Ref

Definition at line 129 of file SolverTypes.h.

Var

using Minisat::Internal::Var = typedef int

Definition at line 41 of file SolverTypes.h.

Function Documentation

append()

template<class T >

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

inlinestatic

Definition at line 79 of file Alg.h.

copy() [1/2]

template<class T >

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

inlinestatic

Definition at line 61 of file Alg.h.

copy() [2/2]

template<class T >

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

inlinestatic

Definition at line 68 of file Alg.h.

eagerMatch()

template<class B >

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

static

Definition at line 114 of file ParseUtils.h.

find()

template<class V , class T >

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

inlinestatic

Definition at line 47 of file Alg.h.

hash() [1/4]

static uint32_t Minisat::Internal::hash ( int32_t  x )

inlinestatic

Definition at line 40 of file Map.h.

hash() [2/4]

static uint32_t Minisat::Internal::hash ( int64_t  x )

inlinestatic

Definition at line 41 of file Map.h.

hash() [3/4]

static uint32_t Minisat::Internal::hash ( uint32_t  x )

inlinestatic

Definition at line 38 of file Map.h.

hash() [4/4]

static uint32_t Minisat::Internal::hash ( uint64_t  x )

inlinestatic

Definition at line 39 of file Map.h.

match()

template<class B >

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

static

Definition at line 101 of file ParseUtils.h.

mkLit()

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

inline

Definition at line 57 of file SolverTypes.h.

operator^()

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

inline

Definition at line 59 of file SolverTypes.h.

operator~()

Lit Minisat::Internal::operator~ ( Lit  p )

inline

Definition at line 58 of file SolverTypes.h.

parseInt()

template<class B >

static int Minisat::Internal::parseInt ( B &  in )

static

Definition at line 85 of file ParseUtils.h.

remove()

template<class V , class T >

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

inlinestatic

Definition at line 36 of file Alg.h.

selectionSort() [1/2]

template<class T >

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

inlinestatic

Definition at line 53 of file Sort.h.

selectionSort() [2/2]

template<class T , class LessThan >

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

Definition at line 39 of file Sort.h.

sign()

bool Minisat::Internal::sign ( Lit  p )

inline

Definition at line 60 of file SolverTypes.h.

skipLine()

template<class B >

static void Minisat::Internal::skipLine ( B &  in )

static

Definition at line 77 of file ParseUtils.h.

skipWhitespace()

template<class B >

static void Minisat::Internal::skipWhitespace ( B &  in )

static

Definition at line 71 of file ParseUtils.h.

sort() [1/4]

template<class T >

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

inlinestatic

Definition at line 81 of file Sort.h.

sort() [2/4]

template<class T , class LessThan >

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

Definition at line 57 of file Sort.h.

sort() [3/4]

template<class T >

void Minisat::Internal::sort

(

vec< T > &

v

)

Definition at line 91 of file Sort.h.

sort() [4/4]

template<class T , class LessThan >

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

Definition at line 89 of file Sort.h.

toInt() [1/3]

int Minisat::Internal::toInt ( lbool  l )

inline

Definition at line 122 of file SolverTypes.h.

toInt() [2/3]

int Minisat::Internal::toInt ( Lit  p )

inline

Definition at line 65 of file SolverTypes.h.

toInt() [3/3]

int Minisat::Internal::toInt ( Var  v )

inline

Definition at line 64 of file SolverTypes.h.

toLbool()

lbool Minisat::Internal::toLbool ( int  v )

inline

Definition at line 123 of file SolverTypes.h.

toLit()

Lit Minisat::Internal::toLit ( int  i )

inline

Definition at line 66 of file SolverTypes.h.

var()

int Minisat::Internal::var ( Lit  p )

inline

Definition at line 61 of file SolverTypes.h.

xrealloc()

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

inlinestatic

Definition at line 32 of file XAlloc.h.

Variable Documentation

buffer_size

const int Minisat::Internal::buffer_size = 1048576

static

Definition at line 34 of file ParseUtils.h.

CRef_Undef

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

Definition at line 210 of file SolverTypes.h.

lit_Error

const Lit Minisat::Internal::lit_Error = { -1 }

Definition at line 74 of file SolverTypes.h.

lit_Undef

const Lit Minisat::Internal::lit_Undef = { -2 }

Definition at line 73 of file SolverTypes.h.

nprimes

const int Minisat::Internal::nprimes = 25

static

Definition at line 48 of file Map.h.

primes

const int Minisat::Internal::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.