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 <util/magic.h>
13 
14 #include <iostream>
15 #include <sstream>
16 
17 dimacs_cnft::dimacs_cnft():break_lines(false)
18 {
19 }
20 
21 dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
22 {
23 }
24 
25 void dimacs_cnft::write_dimacs_cnf(std::ostream &out)
26 {
27  write_problem_line(out);
28  write_clauses(out);
29 }
30 
31 void dimacs_cnft::write_problem_line(std::ostream &out)
32 {
33  // We start counting at 1, thus there is one variable fewer.
34  out << "p cnf " << (no_variables()-1) << " "
35  << clauses.size() << "\n";
36 }
37 
38 static void write_dimacs_clause(
39  const bvt &clause,
40  std::ostream &out,
41  bool break_lines)
42 {
43  // The DIMACS CNF format allows line breaks in clauses:
44  // "Each clauses is terminated by the value 0. Unlike many formats
45  // that represent the end of a clause by a new-line character,
46  // this format allows clauses to be on multiple lines."
47  // Some historic solvers (zchaff e.g.) have silently swallowed
48  // literals in clauses that exceed some fixed buffer size.
49 
50  // However, the SAT competition format does not allow line
51  // breaks in clauses, so we offer both options.
52 
53  for(size_t j=0; j<clause.size(); j++)
54  {
55  out << clause[j].dimacs() << " ";
56  // newline to avoid overflow in sat checkers
57  if((j&15)==0 && j!=0 && break_lines)
58  out << "\n";
59  }
60 
61  out << "0" << "\n";
62 }
63 
64 void dimacs_cnft::write_clauses(std::ostream &out)
65 {
66  std::size_t count = 0;
67  std::stringstream output_block;
68  for(clausest::const_iterator it=clauses.begin();
69  it!=clauses.end(); it++)
70  {
71  write_dimacs_clause(*it, output_block, break_lines);
72 
73  // print the block once in a while
74  if(++count % CNF_DUMP_BLOCK_SIZE == 0)
75  {
76  out << output_block.str();
77  output_block.str("");
78  }
79  }
80 
81  // make sure the final block is printed as well
82  out << output_block.str();
83 }
84 
85 void dimacs_cnf_dumpt::lcnf(const bvt &bv)
86 {
87  write_dimacs_clause(bv, out, true);
88 }
std::ostream & out
Definition: dimacs_cnf.h:68
bool break_lines
Definition: dimacs_cnf.h:36
Magic numbers used throughout the codebase.
void write_clauses(std::ostream &out)
Definition: dimacs_cnf.cpp:64
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:25
const std::size_t CNF_DUMP_BLOCK_SIZE
Definition: magic.h:10
static void write_dimacs_clause(const bvt &clause, std::ostream &out, bool break_lines)
Definition: dimacs_cnf.cpp:38
virtual void lcnf(const bvt &bv)
Definition: dimacs_cnf.cpp:85
void write_problem_line(std::ostream &out)
Definition: dimacs_cnf.cpp:31
virtual size_t no_variables() const override
Definition: cnf.h:38
dimacs_cnf_dumpt(std::ostream &_out)
Definition: dimacs_cnf.cpp:21
std::vector< literalt > bvt
Definition: literal.h:200