qdimacs_cnft::quantifiert Class Reference

#include <qdimacs_cnf.h>

Collaboration diagram for qdimacs_cnft::quantifiert:

Public Types
enum	typet { typet::NONE, typet::EXISTENTIAL, typet::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 35 of file qdimacs_cnf.h.

Member Enumeration Documentation

typet

enum qdimacs_cnft::quantifiert::typet

strong

Enumerator
NONE
EXISTENTIAL
UNIVERSAL

Definition at line 38 of file qdimacs_cnf.h.

Constructor & Destructor Documentation

quantifiert() [1/2]

qdimacs_cnft::quantifiert::quantifiert ( )

inline

Definition at line 42 of file qdimacs_cnf.h.

quantifiert() [2/2]

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

inline

Definition at line 46 of file qdimacs_cnf.h.

Member Function Documentation

hash()

size_t qdimacs_cnft::quantifiert::hash ( ) const

inline

Definition at line 55 of file qdimacs_cnf.h.

operator==()

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

inline

Definition at line 50 of file qdimacs_cnf.h.

Member Data Documentation

type

typet qdimacs_cnft::quantifiert::type

Definition at line 39 of file qdimacs_cnf.h.

var_no

unsigned qdimacs_cnft::quantifiert::var_no

Definition at line 40 of file qdimacs_cnf.h.

---

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

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