CBMC: /home/runner/work/cbmc/cbmc/src/solvers/sat/dimacs_cnf.cpp Source File

15 dimacs_cnft::dimacs_cnft(message_handlert &message_handler)

16 : cnf_clause_listt(message_handler), break_lines(false)

17{

18}

20 void dimacs_cnft::set_assignment(literalt, bool)

21{

22 UNIMPLEMENTED;

23}

25 bool dimacs_cnft::is_in_conflict(literalt) const

26{

27 UNREACHABLE;

28 return false;

29}

31 dimacs_cnf_dumpt::dimacs_cnf_dumpt(

32 std::ostream &_out,

33 message_handlert &message_handler)

34 : cnft(message_handler), out(_out)

35{

36}

38 void dimacs_cnft::write_dimacs_cnf(std::ostream &out) const

39{

40 write_problem_line(out);

41 write_clauses(out);

42}

44 void dimacs_cnft::write_problem_line(std::ostream &out) const

45{

46 // We start counting at 1, thus there is one variable fewer.

47 out << "p cnf " << (no_variables()-1) << " "

48 << clauses.size() << "\n";

49}

51 void dimacs_cnft::write_dimacs_clause(

52 const bvt &clause,

53 std::ostream &out,

54 bool break_lines)

55{

56 // The DIMACS CNF format allows line breaks in clauses:

57 // "Each clauses is terminated by the value 0. Unlike many formats

58 // that represent the end of a clause by a new-line character,

59 // this format allows clauses to be on multiple lines."

60 // Some historic solvers (zchaff e.g.) have silently swallowed

61 // literals in clauses that exceed some fixed buffer size.

62

63 // However, the SAT competition format does not allow line

64 // breaks in clauses, so we offer both options.

65

66 for(size_t j=0; j<clause.size(); j++)

67 {

68 out << clause[j].dimacs() << " ";

69 // newline to avoid overflow in sat checkers

70 if((j&15)==0 && j!=0 && break_lines)

71 out << "\n";

72 }

73

74 out << "0" << "\n";

75}

77 void dimacs_cnft::write_clauses(std::ostream &out) const

78{

79 std::size_t count = 0;

80 std::stringstream output_block;

81 for(clausest::const_iterator it=clauses.begin();

82 it!=clauses.end(); it++)

83 {

84 write_dimacs_clause(*it, output_block, break_lines);

85

86 // print the block once in a while

87 if(++count % CNF_DUMP_BLOCK_SIZE == 0)

88 {

89 out << output_block.str();

90 output_block.str("");

91 }

92 }

93

94 // make sure the final block is printed as well

95 out << output_block.str();

96}

98 void dimacs_cnf_dumpt::lcnf(const bvt &bv)

99{

100 dimacs_cnft::write_dimacs_clause(bv, out, true);

101}

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

cnf_clause_listt

Definition cnf_clause_list.h:24

cnf_clause_listt::clauses

clausest clauses

Definition cnf_clause_list.h:85

cnft

Definition cnf.h:18

cnft::no_variables

virtual size_t no_variables() const override

Definition cnf.h:42

dimacs_cnf_dumpt::out

std::ostream & out

Definition dimacs_cnf.h:74

dimacs_cnf_dumpt::dimacs_cnf_dumpt

dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler)

Definition dimacs_cnf.cpp:31

dimacs_cnf_dumpt::lcnf

void lcnf(const bvt &bv) override

Definition dimacs_cnf.cpp:98

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:25

dimacs_cnft::dimacs_cnft

dimacs_cnft(message_handlert &)

Definition dimacs_cnf.cpp:15

dimacs_cnft::write_clauses

void write_clauses(std::ostream &out) const

Definition dimacs_cnf.cpp:77

dimacs_cnft::write_dimacs_clause

static void write_dimacs_clause(const bvt &, std::ostream &, bool break_lines)

Definition dimacs_cnf.cpp:51

dimacs_cnft::break_lines

bool break_lines

Definition dimacs_cnf.h:42

dimacs_cnft::set_assignment

void set_assignment(literalt a, bool value) override

Definition dimacs_cnf.cpp:20

dimacs_cnft::write_dimacs_cnf

virtual void write_dimacs_cnf(std::ostream &out) const

Definition dimacs_cnf.cpp:38

dimacs_cnft::write_problem_line

void write_problem_line(std::ostream &out) const

Definition dimacs_cnf.cpp:44

literalt

Definition literal.h:26

message_handlert

Definition message.h:27

dimacs_cnf.h

bvt

std::vector< literalt > bvt

Definition literal.h:201

magic.h

Magic numbers used throughout the codebase.

CNF_DUMP_BLOCK_SIZE

const std::size_t CNF_DUMP_BLOCK_SIZE

Definition magic.h:10

invariant.h

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525

UNIMPLEMENTED

#define UNIMPLEMENTED

Definition invariant.h:558