SolverTypes.h File Reference

#include <assert.h>
#include "sat/glucose2/IntTypes.h"
#include "sat/glucose2/Alg.h"
#include "sat/glucose2/Vec.h"
#include "sat/glucose2/Map.h"
#include "sat/glucose2/Alloc.h"
#include "sat/glucose2/CGlucose.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.

Classes
struct	Gluco2::Lit
class	Gluco2::lbool
class	Gluco2::Clause
class	Gluco2::ClauseAllocator
class	Gluco2::OccLists< Idx, Vec, Deleted >
class	Gluco2::CMap< T >

Namespaces
namespace	Gluco2

Macros
#define	var_Undef   (-1)
#define	l_True   (Gluco2::lbool((uint8_t)0))
#define	l_False   (Gluco2::lbool((uint8_t)1))
#define	l_Undef   (Gluco2::lbool((uint8_t)2))

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

Functions
Lit	Gluco2::mkLit (Var var, bool sign=false)
Lit	Gluco2::operator~ (Lit p)
Lit	Gluco2::operator^ (Lit p, bool b)
bool	Gluco2::sign (Lit p)
int	Gluco2::var (Lit p)
int	Gluco2::toInt (Var v)
int	Gluco2::toInt (Lit p)
Lit	Gluco2::toLit (int i)
int	Gluco2::toInt (lbool l)
lbool	Gluco2::toLbool (int v)

Variables
const Lit	Gluco2::lit_Undef = { -2 }
const Lit	Gluco2::lit_Error = { -1 }
const CRef	Gluco2::CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef

Macro Definition Documentation

l_False

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

Definition at line 96 of file SolverTypes.h.

l_True

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

Definition at line 95 of file SolverTypes.h.

l_Undef

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

Definition at line 97 of file SolverTypes.h.

var_Undef

#define var_Undef   (-1)

Definition at line 55 of file SolverTypes.h.