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 } |
using Minisat::Internal::CRef = typedef RegionAllocator<uint32_t>::Ref |
Definition at line 129 of file SolverTypes.h.
using Minisat::Internal::Var = typedef int |
Definition at line 41 of file SolverTypes.h.
|
inlinestatic |
|
static |
Definition at line 114 of file ParseUtils.h.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
static |
Definition at line 101 of file ParseUtils.h.
Definition at line 57 of file SolverTypes.h.
Definition at line 59 of file SolverTypes.h.
Definition at line 58 of file SolverTypes.h.
|
static |
Definition at line 85 of file ParseUtils.h.
|
inlinestatic |
|
inlinestatic |
void Minisat::Internal::selectionSort | ( | T * | array, |
int | size, | ||
LessThan | lt | ||
) |
|
inline |
Definition at line 60 of file SolverTypes.h.
|
static |
Definition at line 77 of file ParseUtils.h.
|
static |
Definition at line 71 of file ParseUtils.h.
|
inlinestatic |
void Minisat::Internal::sort | ( | T * | array, |
int | size, | ||
LessThan | lt | ||
) |
void Minisat::Internal::sort | ( | vec< T > & | v | ) |
void Minisat::Internal::sort | ( | vec< T > & | v, |
LessThan | lt | ||
) |
|
inline |
Definition at line 122 of file SolverTypes.h.
|
inline |
Definition at line 65 of file SolverTypes.h.
|
inline |
Definition at line 64 of file SolverTypes.h.
|
inline |
Definition at line 123 of file SolverTypes.h.
|
inline |
Definition at line 66 of file SolverTypes.h.
|
inline |
Definition at line 61 of file SolverTypes.h.
|
inlinestatic |
|
static |
Definition at line 34 of file ParseUtils.h.
const CRef Minisat::Internal::CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef |
Definition at line 210 of file SolverTypes.h.
const Lit Minisat::Internal::lit_Error = { -1 } |
Definition at line 74 of file SolverTypes.h.
const Lit Minisat::Internal::lit_Undef = { -2 } |
Definition at line 73 of file SolverTypes.h.