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
dimacs_cnf_dumpt::dimacs_cnf_dumpt
dimacs_cnf_dumpt(std::ostream &_out)
Definition: dimacs_cnf.cpp:33
dimacs_cnft::write_clauses
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:76
dimacs_cnft::write_problem_line
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:43
dimacs_cnft::write_dimacs_cnf
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:37
dimacs_cnft::~dimacs_cnft
virtual ~dimacs_cnft()
Definition: dimacs_cnf.h:21
bvt
std::vector< literalt > bvt
Definition: literal.h:200
cnf_clause_listt
Definition: cnf_clause_list.h:23
dimacs_cnf_dumpt::no_clauses
virtual size_t no_clauses() const
Definition: dimacs_cnf.h:65
cnf_clause_list.h
cnft
Definition: cnf.h:17
dimacs_cnf_dumpt::out
std::ostream & out
Definition: dimacs_cnf.h:71
dimacs_cnf_dumpt::lcnf
virtual void lcnf(const bvt &bv)
Definition: dimacs_cnf.cpp:97
dimacs_cnft::break_lines
bool break_lines
Definition: dimacs_cnf.h:39
dimacs_cnft::is_in_conflict
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::prop_solve
virtual resultt prop_solve()
Definition: dimacs_cnf.h:55
propt::resultt::P_ERROR
dimacs_cnf_dumpt
Definition: dimacs_cnf.h:42
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:96
tvt
Definition: threeval.h:19
dimacs_cnft::dimacs_cnft
dimacs_cnft()
Definition: dimacs_cnf.cpp:18
dimacs_cnf_dumpt::l_get
virtual tvt l_get(literalt) const
Definition: dimacs_cnf.h:60
dimacs_cnf_dumpt::solver_text
virtual const std::string solver_text()
Definition: dimacs_cnf.h:48
dimacs_cnft::set_assignment
void set_assignment(literalt a, bool value) override
Definition: dimacs_cnf.cpp:22
literalt
Definition: literal.h:24
dimacs_cnft::solver_text
const std::string solver_text() override
Definition: dimacs_cnf.h:27
dimacs_cnft
Definition: dimacs_cnf.h:17
dimacs_cnf_dumpt::~dimacs_cnf_dumpt
virtual ~dimacs_cnf_dumpt()
Definition: dimacs_cnf.h:46