10 #ifndef CPROVER_SOLVERS_QBF_QDIMACS_CNF_H 11 #define CPROVER_SOLVERS_QBF_QDIMACS_CNF_H 16 #include "../sat/dimacs_cnf.h" 50 return type==other.
type && var_no==other.
var_no;
55 return var_no^(
static_cast<int>(
type)<<24);
65 quantifiers.push_back(quantifier);
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)
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)