#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"

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 |
| #define l_False (Gluco::lbool((uint8_t)1)) |
Definition at line 94 of file SolverTypes.h.
| #define l_True (Gluco::lbool((uint8_t)0)) |
Definition at line 93 of file SolverTypes.h.
| #define l_Undef (Gluco::lbool((uint8_t)2)) |
Definition at line 95 of file SolverTypes.h.
| #define var_Undef (-1) |
Definition at line 53 of file SolverTypes.h.