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