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 
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 
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:38
bv_dimacst::write_dimacs
bool write_dimacs()
Definition: bv_dimacs.cpp:19
messaget::eom
static eomt eom
Definition: message.h:297
bv_dimacst::filename
const std::string filename
Definition: bv_dimacs.h:35
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:56
messaget::error
mstreamt & error() const
Definition: message.h:399
dimacs_cnf.h
boolbvt::get_map
const boolbv_mapt & get_map() const
Definition: boolbv.h:90
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition: prop_conv_solver.h:91
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:133
bv_dimacs.h
Writing DIMACS Files.
dimacs_cnft
Definition: dimacs_cnf.h:18
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131