cprover
Loading...
Searching...
No Matches
bv_dimacs.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Writing DIMACS Files
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "bv_dimacs.h"
13
14#include <fstream>
15#include <iostream>
16
18
20{
21 if(filename.empty() || filename == "-")
22 return write_dimacs(std::cout);
23
24 std::ofstream out(filename);
25
26 if(!out)
27 {
28 log.error() << "failed to open " << filename << messaget::eom;
29 return false;
30 }
31
32 return write_dimacs(out);
33}
34
35bool 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().get_mapping())
51 {
52 const auto &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 {
61 out << ' ';
62
63 if(lit.is_constant())
64 out << (lit.is_true() ? "TRUE" : "FALSE");
65 else
66 out << lit.dimacs();
67 }
68
69 out << "\n";
70 }
71
72 return false;
73}
Writing DIMACS Files.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
messaget log
Definition arrays.h:57
const mappingt & get_mapping() const
Definition boolbv_map.h:65
const boolbv_mapt & get_map() const
Definition boolbv.h:94
bool write_dimacs()
Definition bv_dimacs.cpp:19
const std::string filename
Definition bv_dimacs.h:35
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
const symbolst & get_symbols() const