cprover
|
#include <qdimacs_cnf.h>
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 |
Definition at line 33 of file qdimacs_cnf.h.
|
strong |
Enumerator | |
---|---|
NONE | |
EXISTENTIAL | |
UNIVERSAL |
Definition at line 36 of file qdimacs_cnf.h.
|
inline |
Definition at line 40 of file qdimacs_cnf.h.
Referenced by qdimacs_cnft::add_existential_quantifier(), qdimacs_cnft::add_quantifier(), and qdimacs_cnft::add_universal_quantifier().
Definition at line 44 of file qdimacs_cnf.h.
|
inline |
Definition at line 53 of file qdimacs_cnf.h.
References type.
Referenced by qdimacs_cnft::add_universal_quantifier().
|
inline |
Definition at line 48 of file qdimacs_cnf.h.
Referenced by qdimacs_cnft::add_universal_quantifier().
typet qdimacs_cnft::quantifiert::type |
Definition at line 37 of file qdimacs_cnf.h.
Referenced by qbf_squolemt::add_quantifier(), qbf_squolem_coret::add_quantifier(), qdimacs_cnft::add_universal_quantifier(), qbf_bdd_certificatet::f_get(), hash(), operator==(), and qdimacs_cnft::write_prefix().
unsigned qdimacs_cnft::quantifiert::var_no |
Definition at line 38 of file qdimacs_cnf.h.
Referenced by qbf_squolemt::add_quantifier(), qbf_squolem_coret::add_quantifier(), operator==(), and qdimacs_cnft::write_prefix().