10 #ifndef CPROVER_SOLVERS_PROP_LITERAL_H 11 #define CPROVER_SOLVERS_PROP_LITERAL_H 200 typedef std::vector<literalt>
bvt;
202 #define forall_literals(it, bv) \ 203 for(bvt::const_iterator it=(bv).begin(), it_end=(bv).end(); \ 206 #define Forall_literals(it, bv) \ 207 for(bvt::iterator it=(bv).begin(); \ 208 it!=(bv).end(); ++it) 210 #endif // CPROVER_SOLVERS_PROP_LITERAL_H bool is_true(const literalt &l)
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 is_false(const literalt &l)
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)
void set(var_not v, bool sign)
std::vector< literalt > bvt