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  explicit dimacs_cnft(message_handlert &);
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  dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
46  virtual ~dimacs_cnf_dumpt() { }
47 
48  const std::string solver_text() override
49  {
50  return "DIMACS CNF Dumper";
51  }
52 
53  void lcnf(const bvt &bv) override;
54 
55  tvt l_get(literalt) const override
56  {
57  return tvt::unknown();
58  }
59 
60  size_t no_clauses() const override
61  {
62  return 0;
63  }
64 
65 protected:
67  {
68  return resultt::P_ERROR;
69  }
70 
71  std::ostream &out;
72 };
73 
74 #endif // CPROVER_SOLVERS_SAT_DIMACS_CNF_H
dimacs_cnf_dumpt::no_clauses
size_t no_clauses() const override
Definition: dimacs_cnf.h:60
dimacs_cnft::write_clauses
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:80
dimacs_cnft::write_problem_line
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:47
dimacs_cnft::write_dimacs_cnf
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:41
dimacs_cnft::~dimacs_cnft
virtual ~dimacs_cnft()
Definition: dimacs_cnf.h:21
bvt
std::vector< literalt > bvt
Definition: literal.h:201
cnf_clause_listt
Definition: cnf_clause_list.h:24
cnf_clause_list.h
cnft
Definition: cnf.h:18
dimacs_cnf_dumpt::out
std::ostream & out
Definition: dimacs_cnf.h:71
dimacs_cnf_dumpt::do_prop_solve
resultt do_prop_solve() override
Definition: dimacs_cnf.h:66
dimacs_cnf_dumpt::dimacs_cnf_dumpt
dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler)
Definition: dimacs_cnf.cpp:34
dimacs_cnf_dumpt::lcnf
void lcnf(const bvt &bv) override
Definition: dimacs_cnf.cpp:101
dimacs_cnf_dumpt::l_get
tvt l_get(literalt) const override
Definition: dimacs_cnf.h:55
dimacs_cnft::dimacs_cnft
dimacs_cnft(message_handlert &)
Definition: dimacs_cnf.cpp:18
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:28
dimacs_cnf_dumpt::solver_text
const std::string solver_text() override
Definition: dimacs_cnf.h:48
propt::resultt::P_ERROR
@ P_ERROR
message_handlert
Definition: message.h:27
dimacs_cnf_dumpt
Definition: dimacs_cnf.h:43
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:99
tvt
Definition: threeval.h:20
dimacs_cnft::set_assignment
void set_assignment(literalt a, bool value) override
Definition: dimacs_cnf.cpp:23
literalt
Definition: literal.h:26
dimacs_cnft::solver_text
const std::string solver_text() override
Definition: dimacs_cnf.h:27
dimacs_cnft
Definition: dimacs_cnf.h:18
dimacs_cnf_dumpt::~dimacs_cnf_dumpt
virtual ~dimacs_cnf_dumpt()
Definition: dimacs_cnf.h:46