cprover
bv_dimacs.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Writing DIMACS Files
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
bv_dimacs.h
"
13
14
#include <fstream>
15
#include <iostream>
16
17
#include <
solvers/sat/dimacs_cnf.h
>
18
19
bool
bv_dimacst::write_dimacs
(
const
std::string &filename)
20
{
21
if
(
filename
.empty() ||
filename
==
"-"
)
22
return
write_dimacs
(std::cout);
23
24
std::ofstream out(
filename
);
25
26
if
(!out)
27
{
28
error
() <<
"failed to open "
<<
filename
<<
eom
;
29
return
false
;
30
}
31
32
return
write_dimacs
(out);
33
}
34
35
bool
bv_dimacst::write_dimacs
(std::ostream &out)
36
{
37
dynamic_cast<dimacs_cnft &>(
prop
).write_dimacs_cnf(out);
38
39
// we dump the mapping variable<->literals
40
for
(
const
auto
&s :
get_symbols
())
41
{
42
if
(s.second.is_constant())
43
out <<
"c "
<< s.first <<
" "
<< (s.second.is_true() ?
"TRUE"
:
"FALSE"
)
44
<<
"\n"
;
45
else
46
out <<
"c "
<< s.first <<
" "
<< s.second.dimacs() <<
"\n"
;
47
}
48
49
// dump mapping for selected bit-vectors
50
for
(
const
auto
&m :
get_map
().mapping)
51
{
52
const
boolbv_mapt::literal_mapt
&literal_map = m.second.literal_map;
53
54
if
(literal_map.empty())
55
continue
;
56
57
out <<
"c "
<< m.first;
58
59
for
(
const
auto
&lit : literal_map)
60
if
(!lit.is_set)
61
out <<
" "
62
<<
"?"
;
63
else
if
(lit.l.is_constant())
64
out <<
" "
<< (lit.l.is_true() ?
"TRUE"
:
"FALSE"
);
65
else
66
out <<
" "
<< lit.l.dimacs();
67
68
out <<
"\n"
;
69
}
70
71
return
false
;
72
}
boolbv_mapt::literal_mapt
std::vector< map_bitt > literal_mapt
Definition:
boolbv_map.h:41
messaget::eom
static eomt eom
Definition:
message.h:284
bv_dimacst::write_dimacs
bool write_dimacs(const std::string &filename)
Definition:
bv_dimacs.cpp:19
messaget::error
mstreamt & error() const
Definition:
message.h:386
bv_dimacst::filename
std::string filename
Definition:
bv_dimacs.h:31
dimacs_cnf.h
boolbvt::get_map
const boolbv_mapt & get_map() const
Definition:
boolbv.h:87
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition:
prop_conv.h:121
bv_dimacs.h
prop_conv_solvert::prop
propt & prop
Definition:
prop_conv.h:152
solvers
flattening
bv_dimacs.cpp
Generated by
1.8.16