Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Loading...
Searching...
No Matches
SolverTypes.h File Reference

Go to the source code of this file.

Classes

class  Minisat::Internal::Clause
 
class  Minisat::Internal::ClauseAllocator
 
class  Minisat::Internal::CMap< T >
 
struct  Minisat::Internal::CMap< T >::CRefHash
 
class  Minisat::Internal::lbool
 
struct  Minisat::Internal::Lit
 
class  Minisat::Internal::OccLists< Idx, Vec, Deleted >
 

Namespaces

namespace  Minisat
 
namespace  Minisat::Internal
 

Macros

#define l_False   (lbool((uint8_t)1))
 
#define l_Timeout   (lbool((uint8_t)9))
 
#define l_True   (lbool((uint8_t)0))
 
#define l_Undef   (lbool((uint8_t)2))
 
#define var_Undef   (-1)
 

Typedefs

using Minisat::Internal::CRef = RegionAllocator< uint32_t >::Ref
 
using Minisat::Internal::Var = int
 

Functions

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

Variables

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

Macro Definition Documentation

◆ l_False

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

Definition at line 86 of file SolverTypes.h.

◆ l_Timeout

#define l_Timeout   (lbool((uint8_t)9))

Definition at line 88 of file SolverTypes.h.

◆ l_True

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

Definition at line 85 of file SolverTypes.h.

◆ l_Undef

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

Definition at line 87 of file SolverTypes.h.

◆ var_Undef

#define var_Undef   (-1)

Definition at line 42 of file SolverTypes.h.