CBMC
bv_dimacs.h
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 #ifndef CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
13 #define CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
14 
15 #include "bv_pointers.h"
16 
17 class dimacs_cnft;
18 
19 class bv_dimacst : public bv_pointerst
20 {
21 public:
22  bv_dimacst(
23  const namespacet &_ns,
24  dimacs_cnft &_prop,
26  const std::string &_filename);
27 
28  virtual ~bv_dimacst()
29  {
30  write_dimacs();
31  }
32 
33 protected:
34  const std::string filename;
36 
37  bool write_dimacs();
38  bool write_dimacs(std::ostream &);
39 };
40 
41 #endif // CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
message_handlert & message_handler
Definition: arrays.h:58
const dimacs_cnft & dimacs_cnf_prop
Definition: bv_dimacs.h:35
bool write_dimacs()
Definition: bv_dimacs.cpp:30
const std::string filename
Definition: bv_dimacs.h:34
bv_dimacst(const namespacet &_ns, dimacs_cnft &_prop, message_handlert &message_handler, const std::string &_filename)
Definition: bv_dimacs.cpp:19
virtual ~bv_dimacst()
Definition: bv_dimacs.h:28
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94