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

Include dependency graph for SolverTypes.h:

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

Data Structures
struct	Minisat::Lit

struct	Minisat::MkIndexLit

class	Minisat::VMap< T >

class	Minisat::LMap< T >

class	Minisat::LSet

class	Minisat::lbool

class	Minisat::Clause

class	Minisat::ClauseAllocator

class	Minisat::ClauseIterator

class	Minisat::TrailIterator

class	Minisat::OccLists< K, Vec, Deleted, MkIndex >

class	Minisat::CMap< T >

struct	Minisat::CMap< T >::CRefHash

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)

int	Minisat::toInt (Var v)

int	Minisat::toInt (Lit p)

Lit	Minisat::toLit (int i)

int	Minisat::toInt (lbool l)

lbool	Minisat::toLbool (int v)

const lbool	Minisat::l_True ((uint8_t) 0)

const lbool	Minisat::l_False ((uint8_t) 1)

const lbool	Minisat::l_Undef ((uint8_t) 2)

Variables
const Var	Minisat::var_Undef = -1

const Lit	Minisat::lit_Undef = { -2 }

const Lit	Minisat::lit_Error = { -1 }

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

Data Structures

Namespaces