ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
SolverTypes.h File Reference
#include <assert.h>
#include "sat/glucose/IntTypes.h"
#include "sat/glucose/Alg.h"
#include "sat/glucose/Vec.h"
#include "sat/glucose/Map.h"
#include "sat/glucose/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.

Classes

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

Namespaces

namespace  Gluco
 

Macros

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

Typedefs

typedef int Gluco::Var
 
typedef RegionAllocator< uint32_t >::Ref Gluco::CRef
 

Functions

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

Variables

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

Macro Definition Documentation

◆ l_False

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

Definition at line 94 of file SolverTypes.h.

◆ l_True

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

Definition at line 93 of file SolverTypes.h.

◆ l_Undef

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

Definition at line 95 of file SolverTypes.h.

◆ var_Undef

#define var_Undef   (-1)

Definition at line 53 of file SolverTypes.h.