CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
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
}
16
std::ostream &
operator <<
(std::ostream &out,
literalt
l) {
…
}
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
}
24
std::ostream &
operator<<
(std::ostream &out,
const
bvt
&bv) {
…
}
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.8