cprover
dimacs_cnf.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_DIMACS_CNF_H
11 #define CPROVER_SOLVERS_SAT_DIMACS_CNF_H
12 
13 #include <iosfwd>
14 
15 #include "cnf_clause_list.h"
16 
18 {
19 public:
20  dimacs_cnft();
21  virtual ~dimacs_cnft() { }
22 
23  virtual void write_dimacs_cnf(std::ostream &out);
24 
25  // dummy functions
26 
27  virtual const std::string solver_text()
28  {
29  return "DIMACS CNF";
30  }
31 
32 protected:
33  void write_problem_line(std::ostream &out);
34  void write_clauses(std::ostream &out);
35 
37 };
38 
39 class dimacs_cnf_dumpt:public cnft
40 {
41 public:
42  explicit dimacs_cnf_dumpt(std::ostream &_out);
43  virtual ~dimacs_cnf_dumpt() { }
44 
45  virtual const std::string solver_text()
46  {
47  return "DIMACS CNF Dumper";
48  }
49 
50  virtual void lcnf(const bvt &bv);
51 
52  virtual resultt prop_solve()
53  {
54  return resultt::P_ERROR;
55  }
56 
57  virtual tvt l_get(literalt) const
58  {
59  return tvt::unknown();
60  }
61 
62  virtual size_t no_clauses() const
63  {
64  return 0;
65  }
66 
67 protected:
68  std::ostream &out;
69 };
70 
71 #endif // CPROVER_SOLVERS_SAT_DIMACS_CNF_H
virtual tvt l_get(literalt) const
Definition: dimacs_cnf.h:57
virtual const std::string solver_text()
Definition: dimacs_cnf.h:45
virtual const std::string solver_text()
Definition: dimacs_cnf.h:27
std::ostream & out
Definition: dimacs_cnf.h:68
static tvt unknown()
Definition: threeval.h:33
CNF Generation.
bool break_lines
Definition: dimacs_cnf.h:36
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:61
virtual size_t no_clauses() const
Definition: dimacs_cnf.h:62
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:22
Definition: cnf.h:17
virtual resultt prop_solve()
Definition: dimacs_cnf.h:52
Definition: threeval.h:19
virtual void lcnf(const bvt &bv)
virtual ~dimacs_cnf_dumpt()
Definition: dimacs_cnf.h:43
resultt
Definition: prop.h:94
virtual ~dimacs_cnft()
Definition: dimacs_cnf.h:21
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:28
std::vector< literalt > bvt
Definition: literal.h:197