SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Typedefs | Functions | Variables
Minisat Namespace Reference

Data Structures

class  RegionAllocator
 
class  Heap
 
struct  Hash
 
struct  Equal
 
struct  DeepHash
 
struct  DeepEqual
 
class  Map
 
class  Option
 
struct  IntRange
 
struct  Int64Range
 
struct  DoubleRange
 
class  DoubleOption
 
class  IntOption
 
class  StringOption
 
class  BoolOption
 
class  Queue
 
struct  Lit
 
class  lbool
 
class  Clause
 
class  ClauseAllocator
 
class  OccLists
 
class  CMap
 
struct  Watcher
 [Minisat related code] More...
 
struct  LessThan_default
 
class  vec
 
class  OutOfMemoryException
 

Typedefs

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

Functions

template<class V , class T >
static void remove (V &ts, const T &t)
 
template<class V , class T >
static bool find (V &ts, const T &t)
 
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 T >
static void append (const vec< T > &from, vec< T > &to)
 
static uint32_t hash (uint32_t x)
 
static uint32_t hash (uint64_t x)
 
static uint32_t hash (int32_t x)
 
static uint32_t hash (int64_t x)
 
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)
 
Lit neg (Lit p)
 
int toInt (Var v)
 
int toInt (Lit p)
 
Lit toLit (int i)
 
std::ostream & operator<< (std::ostream &os, const Lit &l)
 
int toInt (lbool l)
 
lbool toLbool (int v)
 
std::ostream & operator<< (std::ostream &os, Minisat::lbool b)
 
std::ostream & operator<< (std::ostream &os, const Minisat::Clause &c)
 
template<class T , class LessThan >
void selectionSort (T *array, int size, LessThan lt)
 
template<class T >
static void selectionSort (T *array, int size)
 
template<class T , class LessThan >
void sort (T *array, int size, LessThan lt)
 
template<class T >
static void sort (T *array, int size)
 
template<class T , class LessThan >
void sort (vec< T > &v, LessThan lt)
 
template<class T >
void sort (vec< T > &v)
 
template<typename T >
std::ostream & operator<< (std::ostream &os, const vec< T > &v)
 
template<>
std::ostream & operator<< (std::ostream &os, const vec< char > &v)
 
static void * xrealloc (void *ptr, size_t size)
 

Variables

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 }
 
const Lit lit_Undef = { -2 }
 
const Lit lit_Error = { -1 }
 
static const unsigned NORMAL_CLAUSE = 0
 
static const unsigned LEMMA_CLAUSE = 1
 
static const unsigned CONFLICT_CLAUSE = 2
 
static const unsigned PERMANENT_CLAUSE = 3
 
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef
 
const CRef CRef_Lazy = RegionAllocator<uint32_t>::Ref_Undef - 1
 
const CRef CRef_TPropagation = RegionAllocator<uint32_t>::Ref_Undef - 2
 

Typedef Documentation

◆ CRef

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

Definition at line 143 of file SolverTypes.h.

◆ Var

typedef int Minisat::Var

Definition at line 42 of file SolverTypes.h.

Function Documentation

◆ append()

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

Definition at line 79 of file Alg.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ copy() [1/2]

template<class T >
static void Minisat::copy ( const T &  from,
T &  to 
)
inlinestatic

Definition at line 60 of file Alg.h.

Here is the caller graph for this function:

◆ copy() [2/2]

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

Definition at line 67 of file Alg.h.

Here is the call graph for this function:

◆ find()

template<class V , class T >
static bool Minisat::find ( V &  ts,
const T &  t 
)
inlinestatic

Definition at line 47 of file Alg.h.

Here is the caller graph for this function:

◆ hash() [1/4]

static uint32_t Minisat::hash ( int32_t  x)
inlinestatic

Definition at line 34 of file Map.h.

◆ hash() [2/4]

static uint32_t Minisat::hash ( int64_t  x)
inlinestatic

Definition at line 35 of file Map.h.

◆ hash() [3/4]

static uint32_t Minisat::hash ( uint32_t  x)
inlinestatic

Definition at line 32 of file Map.h.

Here is the caller graph for this function:

◆ hash() [4/4]

static uint32_t Minisat::hash ( uint64_t  x)
inlinestatic

Definition at line 33 of file Map.h.

◆ mkLit()

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

Definition at line 60 of file SolverTypes.h.

Here is the caller graph for this function:

◆ neg()

Lit Minisat::neg ( Lit  p)
inline

Definition at line 65 of file SolverTypes.h.

Here is the call graph for this function:

◆ operator<<() [1/5]

std::ostream& Minisat::operator<< ( std::ostream &  os,
const Lit &  l 
)
inline

Definition at line 75 of file SolverTypes.h.

Here is the call graph for this function:

◆ operator<<() [2/5]

std::ostream& Minisat::operator<< ( std::ostream &  os,
const Minisat::Clause &  c 
)
inline

Definition at line 232 of file SolverTypes.h.

◆ operator<<() [3/5]

template<>
std::ostream& Minisat::operator<< ( std::ostream &  os,
const vec< char > &  v 
)
inline

Definition at line 231 of file Vec.h.

Here is the call graph for this function:

◆ operator<<() [4/5]

template<typename T >
std::ostream& Minisat::operator<< ( std::ostream &  os,
const vec< T > &  v 
)
inline

Definition at line 221 of file Vec.h.

Here is the call graph for this function:

◆ operator<<() [5/5]

std::ostream& Minisat::operator<< ( std::ostream &  os,
Minisat::lbool  b 
)
inline

Definition at line 130 of file SolverTypes.h.

Here is the call graph for this function:

◆ operator^()

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

Definition at line 62 of file SolverTypes.h.

◆ operator~()

Lit Minisat::operator~ ( Lit  p)
inline

Definition at line 61 of file SolverTypes.h.

◆ printUsageAndExit()

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

Definition at line 35 of file Options.cpp.

Here is the call graph for this function:

◆ remove()

template<class V , class T >
static void Minisat::remove ( V &  ts,
const T &  t 
)
inlinestatic

Definition at line 36 of file Alg.h.

Here is the caller graph for this function:

◆ selectionSort() [1/2]

template<class T >
static void Minisat::selectionSort ( T *  array,
int  size 
)
inlinestatic

Definition at line 61 of file Sort.h.

Here is the call graph for this function:

◆ selectionSort() [2/2]

template<class T , class LessThan >
void Minisat::selectionSort ( T *  array,
int  size,
LessThan  lt 
)

Definition at line 41 of file Sort.h.

Here is the caller graph for this function:

◆ setHelpPrefixStr()

void Minisat::setHelpPrefixStr ( const char *  str)

Definition at line 30 of file Options.cpp.

Here is the call graph for this function:

◆ setUsageHelp()

void Minisat::setUsageHelp ( const char *  str)

Definition at line 25 of file Options.cpp.

Here is the call graph for this function:

◆ sign()

bool Minisat::sign ( Lit  p)
inline

Definition at line 63 of file SolverTypes.h.

Here is the caller graph for this function:

◆ sort() [1/4]

template<class T >
static void Minisat::sort ( T *  array,
int  size 
)
inlinestatic

Definition at line 102 of file Sort.h.

Here is the call graph for this function:

◆ sort() [2/4]

template<class T , class LessThan >
void Minisat::sort ( T *  array,
int  size,
LessThan  lt 
)

Definition at line 67 of file Sort.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ sort() [3/4]

template<class T >
void Minisat::sort ( vec< T > &  v)

Definition at line 117 of file Sort.h.

Here is the call graph for this function:

◆ sort() [4/4]

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

Definition at line 111 of file Sort.h.

Here is the call graph for this function:

◆ toInt() [1/3]

int Minisat::toInt ( lbool  l)
inline

Definition at line 127 of file SolverTypes.h.

◆ toInt() [2/3]

int Minisat::toInt ( Lit  p)
inline

Definition at line 69 of file SolverTypes.h.

◆ toInt() [3/3]

int Minisat::toInt ( Var  v)
inline

Definition at line 68 of file SolverTypes.h.

Here is the caller graph for this function:

◆ toLbool()

lbool Minisat::toLbool ( int  v)
inline

Definition at line 128 of file SolverTypes.h.

◆ toLit()

Lit Minisat::toLit ( int  i)
inline

Definition at line 70 of file SolverTypes.h.

◆ var()

int Minisat::var ( Lit  p)
inline

Definition at line 64 of file SolverTypes.h.

◆ xrealloc()

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

Definition at line 32 of file XAlloc.h.

Here is the caller graph for this function:

Variable Documentation

◆ CONFLICT_CLAUSE

const unsigned Minisat::CONFLICT_CLAUSE = 2
static

Definition at line 147 of file SolverTypes.h.

◆ CRef_Lazy

const CRef Minisat::CRef_Lazy = RegionAllocator<uint32_t>::Ref_Undef - 1

Definition at line 247 of file SolverTypes.h.

◆ CRef_TPropagation

const CRef Minisat::CRef_TPropagation = RegionAllocator<uint32_t>::Ref_Undef - 2

Definition at line 248 of file SolverTypes.h.

◆ CRef_Undef

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

Definition at line 246 of file SolverTypes.h.

◆ LEMMA_CLAUSE

const unsigned Minisat::LEMMA_CLAUSE = 1
static

Definition at line 146 of file SolverTypes.h.

◆ lit_Error

const Lit Minisat::lit_Error = { -1 }

Definition at line 73 of file SolverTypes.h.

◆ lit_Undef

const Lit Minisat::lit_Undef = { -2 }

Definition at line 72 of file SolverTypes.h.

◆ NORMAL_CLAUSE

const unsigned Minisat::NORMAL_CLAUSE = 0
static

Definition at line 145 of file SolverTypes.h.

◆ nprimes

const int Minisat::nprimes = 25
static

Definition at line 49 of file Map.h.

◆ PERMANENT_CLAUSE

const unsigned Minisat::PERMANENT_CLAUSE = 3
static

Definition at line 148 of file SolverTypes.h.

◆ primes

const int Minisat::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 50 of file Map.h.