10 #ifndef CPROVER_SOLVERS_QBF_QDIMACS_CNF_H 11 #define CPROVER_SOLVERS_QBF_QDIMACS_CNF_H 16 #include "../sat/dimacs_cnf.h" 97 #endif // CPROVER_SOLVERS_QBF_QDIMACS_CNF_H The type of an expression.
void write_prefix(std::ostream &out) const
bool is_quantified(const literalt l) const
virtual void add_quantifier(const quantifiert &quantifier)
bool operator==(const qdimacs_cnft &other) const
virtual const std::string solver_text()
quantifiert(typet _type, literalt _l)
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
bool find_quantifier(const literalt l, quantifiert &q) const
void add_existential_quantifier(const literalt l)
std::vector< quantifiert > quantifierst
void add_quantifier(const quantifiert::typet type, const literalt l)
void copy_to(qdimacs_cnft &cnf) const
void add_universal_quantifier(const literalt l)
bool operator==(const quantifiert &other) const
virtual void write_qdimacs_cnf(std::ostream &out)