cprover
dimacs_cnf.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "dimacs_cnf.h"
11 
12 #include <iostream>
13 
14 dimacs_cnft::dimacs_cnft():break_lines(false)
15 {
16 }
17 
18 dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
19 {
20 }
21 
23 {
24  write_problem_line(out);
25  write_clauses(out);
26 }
27 
29 {
30  // We start counting at 1, thus there is one variable fewer.
31  out << "p cnf " << (no_variables()-1) << " "
32  << clauses.size() << "\n";
33 }
34 
35 static void write_dimacs_clause(
36  const bvt &clause,
37  std::ostream &out,
38  bool break_lines)
39 {
40  // The DIMACS CNF format allows line breaks in clauses:
41  // "Each clauses is terminated by the value 0. Unlike many formats
42  // that represent the end of a clause by a new-line character,
43  // this format allows clauses to be on multiple lines."
44  // Some historic solvers (zchaff e.g.) have silently swallowed
45  // literals in clauses that exceed some fixed buffer size.
46 
47  // However, the SAT competition format does not allow line
48  // breaks in clauses, so we offer both options.
49 
50  for(size_t j=0; j<clause.size(); j++)
51  {
52  out << clause[j].dimacs() << " ";
53  // newline to avoid overflow in sat checkers
54  if((j&15)==0 && j!=0 && break_lines)
55  out << "\n";
56  }
57 
58  out << "0" << "\n";
59 }
60 
61 void dimacs_cnft::write_clauses(std::ostream &out)
62 {
63  for(clausest::const_iterator it=clauses.begin();
64  it!=clauses.end(); it++)
65  write_dimacs_clause(*it, out, break_lines);
66 }
67 
68 void dimacs_cnf_dumpt::lcnf(const bvt &bv)
69 {
70  write_dimacs_clause(bv, out, true);
71 }
std::ostream & out
Definition: dimacs_cnf.h:68
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:61
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:22
static void write_dimacs_clause(const bvt &clause, std::ostream &out, bool break_lines)
Definition: dimacs_cnf.cpp:35
virtual void lcnf(const bvt &bv)
Definition: dimacs_cnf.cpp:68
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:28
virtual size_t no_variables() const override
Definition: cnf.h:38
dimacs_cnf_dumpt(std::ostream &_out)
Definition: dimacs_cnf.cpp:18
std::vector< literalt > bvt
Definition: literal.h:197