cprover
qdimacs_cnft::quantifiert Class Reference

#include <qdimacs_cnf.h>

Collaboration diagram for qdimacs_cnft::quantifiert:
[legend]

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 33 of file qdimacs_cnf.h.

Member Enumeration Documentation

§ typet

Enumerator
NONE 
EXISTENTIAL 
UNIVERSAL 

Definition at line 36 of file qdimacs_cnf.h.

Constructor & Destructor Documentation

§ quantifiert() [1/2]

qdimacs_cnft::quantifiert::quantifiert ( )
inline

§ quantifiert() [2/2]

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

Definition at line 44 of file qdimacs_cnf.h.

Member Function Documentation

§ hash()

size_t qdimacs_cnft::quantifiert::hash ( ) const
inline

Definition at line 53 of file qdimacs_cnf.h.

References type.

Referenced by qdimacs_cnft::add_universal_quantifier().

§ operator==()

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

Definition at line 48 of file qdimacs_cnf.h.

References type, and var_no.

Referenced by qdimacs_cnft::add_universal_quantifier().

Member Data Documentation

§ type

§ var_no

unsigned qdimacs_cnft::quantifiert::var_no

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