qdimacs_cnft::quantifiert Class Reference

#include <qdimacs_cnf.h>

Collaboration diagram for qdimacs_cnft::quantifiert:

Public Types
enum class	typet { NONE , EXISTENTIAL , UNIVERSAL }

Public Member Functions
	quantifiert ()
	quantifiert (typet _type, literalt _l)
bool	operator== (const quantifiert &other) const
size_t	hash () const

Public Attributes
typet	type
unsigned	var_no

Detailed Description

Definition at line 34 of file qdimacs_cnf.h.

Member Enumeration Documentation

typet

enum class qdimacs_cnft::quantifiert::typet

strong

Enumerator
NONE
EXISTENTIAL
UNIVERSAL

Definition at line 37 of file qdimacs_cnf.h.

Constructor & Destructor Documentation

quantifiert() [1/2]

qdimacs_cnft::quantifiert::quantifiert ( )

inline

Definition at line 41 of file qdimacs_cnf.h.

quantifiert() [2/2]

qdimacs_cnft::quantifiert::quantifiert ( typet  _type, literalt  _l  )

inline

Definition at line 45 of file qdimacs_cnf.h.

Member Function Documentation

hash()

size_t qdimacs_cnft::quantifiert::hash ( ) const

inline

Definition at line 54 of file qdimacs_cnf.h.

operator==()

bool qdimacs_cnft::quantifiert::operator== ( const quantifiert &  other ) const

inline

Definition at line 49 of file qdimacs_cnf.h.

Member Data Documentation

type

typet qdimacs_cnft::quantifiert::type

Definition at line 38 of file qdimacs_cnf.h.

var_no

unsigned qdimacs_cnft::quantifiert::var_no

Definition at line 39 of file qdimacs_cnf.h.

---

The documentation for this class was generated from the following file:

• /home/runner/work/cbmc/cbmc/src/solvers/qbf/qdimacs_cnf.h