Go to the documentation of this file.
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 operator<(const literalt other) const
literalt(var_not v, bool sign)
bool operator==(const literalt other) const
std::ostream & operator<<(std::ostream &out, literalt l)
std::vector< literalt > bvt
static var_not const_var_no()
static var_not unused_var_no()
bool is_false(const literalt &l)
literalt const_literal(bool value)
literalt operator^(const bool b) const
void set(var_not v, bool sign)
bool operator!=(const literalt other) const
literalt operator!() const
bool is_true(const literalt &l)
literalt operator^=(const bool a)