cprover
literal.h File Reference
#include <iosfwd>
#include <util/narrow.h>
#include <vector>
+ Include dependency graph for literal.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  literalt
 

Macros

#define forall_literals(it, bv)
 
#define Forall_literals(it, bv)
 

Typedefs

typedef std::vector< literaltbvt
 

Functions

std::ostream & operator<< (std::ostream &out, literalt l)
 
literalt const_literal (bool value)
 
literalt neg (literalt a)
 
literalt pos (literalt a)
 
bool is_false (const literalt &l)
 
bool is_true (const literalt &l)
 

Macro Definition Documentation

◆ forall_literals

#define forall_literals (   it,
  bv 
)
Value:
for(bvt::const_iterator it=(bv).begin(), it_end=(bv).end(); \
it!=it_end; ++it)

Definition at line 203 of file literal.h.

◆ Forall_literals

#define Forall_literals (   it,
  bv 
)
Value:
for(bvt::iterator it=(bv).begin(); \
it!=(bv).end(); ++it)

Definition at line 207 of file literal.h.

Typedef Documentation

◆ bvt

typedef std::vector<literalt> bvt

Definition at line 201 of file literal.h.

Function Documentation

◆ const_literal()

literalt const_literal ( bool  value)
inline

Definition at line 188 of file literal.h.

◆ is_false()

bool is_false ( const literalt l)
inline

Definition at line 197 of file literal.h.

◆ is_true()

bool is_true ( const literalt l)
inline

Definition at line 198 of file literal.h.

◆ neg()

literalt neg ( literalt  a)
inline

Definition at line 193 of file literal.h.

◆ operator<<()

std::ostream& operator<< ( std::ostream &  out,
literalt  l 
)

Definition at line 16 of file literal.cpp.

◆ pos()

literalt pos ( literalt  a)
inline

Definition at line 194 of file literal.h.