CBMC
Loading...
Searching...
No Matches
bv_dimacs.h
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#ifndef CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
13#define CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
14
15#include "bv_pointers.h"
16
17#include <iosfwd>
18
19class dimacs_cnft;
20
22{
23public:
25 const namespacet &_ns,
28 std::ostream &_out);
29
30 virtual ~bv_dimacst()
31 {
33 }
34
35protected:
36 std::ostream &out;
38
39 void write_dimacs();
40};
41
42#endif // CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
message_handlert & message_handler
Definition arrays.h:58
const dimacs_cnft & dimacs_cnf_prop
Definition bv_dimacs.h:37
void write_dimacs()
Definition bv_dimacs.cpp:25
std::ostream & out
Definition bv_dimacs.h:36
virtual ~bv_dimacst()
Definition bv_dimacs.h:30
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91