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