cprover
cbmc_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 "cbmc_dimacs.h"
13 
14 #include <fstream>
15 #include <iostream>
16 
17 #include <solvers/sat/dimacs_cnf.h>
18 
19 bool cbmc_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 cbmc_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 << " "
44  << (s.second.is_true()?"TRUE":"FALSE") << "\n";
45  else
46  out << "c " << s.first << " "
47  << s.second.dimacs() << "\n";
48  }
49 
50  // dump mapping for selected bit-vectors
51  for(const auto &m : get_map().mapping)
52  {
53  const boolbv_mapt::literal_mapt &literal_map=m.second.literal_map;
54 
55  if(literal_map.empty())
56  continue;
57 
58  out << "c " << m.first;
59 
60  for(const auto &lit : literal_map)
61  if(!lit.is_set)
62  out << " " << "?";
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 }
Writing DIMACS Files.
const symbolst & get_symbols() const
Definition: prop_conv.h:116
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool write_dimacs(const std::string &filename)
Definition: cbmc_dimacs.cpp:19
std::vector< map_bitt > literal_mapt
Definition: boolbv_map.h:41
const boolbv_mapt & get_map() const
Definition: boolbv.h:85
mstreamt & error()
Definition: message.h:223