Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

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.