CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
literal.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Literals
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "literal.h"
13
14#include <ostream>
15
16std::ostream &operator << (std::ostream &out, literalt l)
17{
18 if(l.is_constant())
19 return out << (l.is_true()?"true":"false");
20 else
21 return out << (l.sign()?"-":"") << l.var_no();
22}
23
24std::ostream &operator<<(std::ostream &out, const bvt &bv)
25{
26 for(auto it = bv.begin(); it != bv.end(); ++it)
27 {
28 out << *it;
29 if(std::next(it) != bv.end())
30 out << ' ';
31 }
32 return out;
33}
bool is_true() const
Definition literal.h:156
bool sign() const
Definition literal.h:88
bool is_constant() const
Definition literal.h:166
var_not var_no() const
Definition literal.h:83
std::ostream & operator<<(std::ostream &out, literalt l)
Definition literal.cpp:16
std::vector< literalt > bvt
Definition literal.h:201