CBMC
literal.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Literals
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
literal.h
"
13
14
#include <ostream>
15
16
std::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
24
std::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
}
literalt
Definition:
literal.h:26
literalt::is_true
bool is_true() const
Definition:
literal.h:156
literalt::sign
bool sign() const
Definition:
literal.h:88
literalt::is_constant
bool is_constant() const
Definition:
literal.h:166
literalt::var_no
var_not var_no() const
Definition:
literal.h:83
operator<<
std::ostream & operator<<(std::ostream &out, literalt l)
Definition:
literal.cpp:16
literal.h
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
src
solvers
prop
literal.cpp
Generated by
1.9.1