SolverTypes.h File Reference

#include <assert.h>
#include "IntTypes.h"
#include "Alg.h"
#include "Vec.h"
#include "Map.h"
#include "Alloc.h"

Include dependency graph for SolverTypes.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	Minisat::Lit
class	Minisat::lbool
class	Minisat::Clause
class	Minisat::ClauseAllocator
class	Minisat::OccLists< Idx, Vec, Deleted >
class	Minisat::CMap< T >
struct	Minisat::CMap< T >::CRefHash
struct	Minisat::Watcher
	[Minisat related code] More...

Namespaces
	Minisat

Macros
#define	var_Undef   (-1)
#define	l_True   (Minisat::lbool((uint8_t)0))
#define	l_False   (Minisat::lbool((uint8_t)1))
#define	l_Undef   (Minisat::lbool((uint8_t)2))
#define	BITMASK_MARK   0x03
#define	BITMASK_TYPE   0x03
#define	BITMASK_HASEXTRA   0x01
#define	BITMASK_RELOCED   0x01
#define	BITMASK_SIZE   0x3fff

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

Functions
Lit	Minisat::mkLit (Var var, bool sign=false)
Lit	Minisat::operator~ (Lit p)
Lit	Minisat::operator^ (Lit p, bool b)
bool	Minisat::sign (Lit p)
int	Minisat::var (Lit p)
Lit	Minisat::neg (Lit p)
int	Minisat::toInt (Var v)
int	Minisat::toInt (Lit p)
Lit	Minisat::toLit (int i)
std::ostream &	Minisat::operator<< (std::ostream &os, const Lit &l)
int	Minisat::toInt (lbool l)
lbool	Minisat::toLbool (int v)
std::ostream &	Minisat::operator<< (std::ostream &os, Minisat::lbool b)
std::ostream &	Minisat::operator<< (std::ostream &os, const Minisat::Clause &c)

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

Macro Definition Documentation

BITMASK_HASEXTRA

#define BITMASK_HASEXTRA   0x01

Definition at line 152 of file SolverTypes.h.

BITMASK_MARK

#define BITMASK_MARK   0x03

Definition at line 150 of file SolverTypes.h.

BITMASK_RELOCED

#define BITMASK_RELOCED   0x01

Definition at line 153 of file SolverTypes.h.

BITMASK_SIZE

#define BITMASK_SIZE   0x3fff

Definition at line 154 of file SolverTypes.h.

BITMASK_TYPE

#define BITMASK_TYPE   0x03

Definition at line 151 of file SolverTypes.h.

l_False

#define l_False   (Minisat::lbool((uint8_t)1))

Definition at line 98 of file SolverTypes.h.

l_True

#define l_True   (Minisat::lbool((uint8_t)0))

Definition at line 97 of file SolverTypes.h.

l_Undef

#define l_Undef   (Minisat::lbool((uint8_t)2))

Definition at line 99 of file SolverTypes.h.

var_Undef

#define var_Undef   (-1)

Definition at line 43 of file SolverTypes.h.