10 #ifndef CPROVER_SOLVERS_PROP_LITERAL_H 11 #define CPROVER_SOLVERS_PROP_LITERAL_H 197 typedef std::vector<literalt>
bvt;
199 #define forall_literals(it, bv) \ 200 for(bvt::const_iterator it=(bv).begin(), it_end=(bv).end(); \ 203 #define Forall_literals(it, bv) \ 204 for(bvt::iterator it=(bv).begin(); \ 205 it!=(bv).end(); ++it) 207 #endif // CPROVER_SOLVERS_PROP_LITERAL_H literalt operator^=(const bool a)
bool operator<(const literalt other) const
std::ostream & operator<<(std::ostream &out, literalt l)
static var_not unused_var_no()
bool operator==(const literalt other) const
bool operator!=(const literalt other) const
literalt operator^(const bool b) const
literalt operator!() const
literalt const_literal(bool value)
static var_not const_var_no()
literalt(var_not v, bool sign)
std::vector< literalt > bvt