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  const std::string solver_text() override
28  {
29  return "DIMACS CNF";
30  }
31 
32  void set_assignment(literalt a, bool value) override;
33  bool is_in_conflict(literalt l) const override;
34 
35 protected:
36  void write_problem_line(std::ostream &out);
37  void write_clauses(std::ostream &out);
38 
40 };
41 
42 class dimacs_cnf_dumpt:public cnft
43 {
44 public:
45  explicit dimacs_cnf_dumpt(std::ostream &_out);
46  virtual ~dimacs_cnf_dumpt() { }
47 
48  virtual const std::string solver_text()
49  {
50  return "DIMACS CNF Dumper";
51  }
52 
53  virtual void lcnf(const bvt &bv);
54 
55  virtual resultt prop_solve()
56  {
57  return resultt::P_ERROR;
58  }
59 
60  virtual tvt l_get(literalt) const
61  {
62  return tvt::unknown();
63  }
64 
65  virtual size_t no_clauses() const
66  {
67  return 0;
68  }
69 
70 protected:
71  std::ostream &out;
72 };
73 
74 #endif // CPROVER_SOLVERS_SAT_DIMACS_CNF_H
const std::string solver_text() override
Definition: dimacs_cnf.h:27
virtual tvt l_get(literalt) const
Definition: dimacs_cnf.h:60
virtual const std::string solver_text()
Definition: dimacs_cnf.h:48
std::ostream & out
Definition: dimacs_cnf.h:71
static tvt unknown()
Definition: threeval.h:33
CNF Generation.
bool break_lines
Definition: dimacs_cnf.h:39
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:76
virtual size_t no_clauses() const
Definition: dimacs_cnf.h:65
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:37
Definition: cnf.h:17
virtual resultt prop_solve()
Definition: dimacs_cnf.h:55
Definition: threeval.h:19
virtual ~dimacs_cnf_dumpt()
Definition: dimacs_cnf.h:46
resultt
Definition: prop.h:96
virtual ~dimacs_cnft()
Definition: dimacs_cnf.h:21
virtual void lcnf(const bvt &bv)
Definition: dimacs_cnf.cpp:97
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:43
bool is_in_conflict(literalt l) const override
Returns true if an assumption is in the final conflict.
Definition: dimacs_cnf.cpp:27
dimacs_cnf_dumpt(std::ostream &_out)
Definition: dimacs_cnf.cpp:33
std::vector< literalt > bvt
Definition: literal.h:200
void set_assignment(literalt a, bool value) override
Definition: dimacs_cnf.cpp:22