CBMC: /home/runner/work/cbmc/cbmc/src/solvers/qbf/qbf_squolem.cpp Source File

14 qbf_squolemt::qbf_squolemt():

15 early_decision(false)

16{

17}

19 qbf_squolemt::~qbf_squolemt()

20{

21 squolem.reset();

22}

24 tvt qbf_squolemt::l_get(literalt a) const

25{

26 UNREACHABLE;

27}

29 std::string qbf_squolemt::solver_text() const

30{

31 return "Squolem";

32}

34 propt::resultt qbf_squolemt::prop_solve()

35{

36 {

37 std::string msg=

38 "Squolem: "+

39 std::to_string(no_variables())+" variables, "+

40 std::to_string(no_clauses())+" clauses";

41 messaget::status() << msg << messaget::eom;

42 }

43

44 if(early_decision)

45 return P_UNSATISFIABLE;

46

47// squolem.options.set_showStatus(true);

48 squolem.options.set_freeOnExit(true);

49// squolem.options.set_useExpansion(true);

50// squolem.options.set_predictOnLiteralBound(true);

51 squolem.options.set_debugFilename("debug.qdimacs");

52 squolem.options.set_saveDebugFile(true);

53

54 squolem.endOfOriginals();

55 bool result=squolem.decide();

56

57 if(result)

58 {

59 messaget::status() << "Squolem: VALID" << messaget::eom;

60 return P_SATISFIABLE;

61 }

62 else

63 {

64 messaget::status() << "Squolem: INVALID" << messaget::eom;

65 return P_UNSATISFIABLE;

66 }

67

68 return P_ERROR;

69}

71 void qbf_squolemt::lcnf(const bvt &bv)

72{

73 if(early_decision)

74 return; // we don't need no more...

75

76 bvt new_bv;

77

78 if(process_clause(bv, new_bv))

79 return;

80

81 if(new_bv.empty())

82 {

83 early_decision=true;

84 return;

85 }

86

87 std::vector<Literal> buffer(new_bv.size());

88 unsigned long i=0;

89 do

90 {

91 buffer[i]=new_bv[i].dimacs();

92 i++;

93 }

94 while(i<new_bv.size());

95

96 if(!squolem.addClause(buffer))

97 early_decision=true;

98}

100 void qbf_squolemt::add_quantifier(const quantifiert &quantifier)

101{

102 squolem.quantifyVariableInner(

103 quantifier.var_no,

104 quantifier.type==quantifiert::UNIVERSAL);

105

106 qdimacs_cnft::add_quantifier(quantifier); // necessary?

107}

109 void qbf_squolemt::set_no_variables(unsigned no)

110{

111 squolem.setLastVariable(no+1);

112 cnft::set_no_variables(no);

113}

115 void qbf_squolemt::set_quantifier(

116 const quantifiert::typet type,

117 const literalt l)

118{

119 qdimacs_cnft::set_quantifier(type, l);

120 squolem.requantifyVariable(l.var_no(), type==quantifiert::UNIVERSAL);

121}

widen_modet::no

@ no

ait

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

Definition ai.h:566

cnft::process_clause

bool process_clause(const bvt &bv, bvt &dest) const

filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses

Definition cnf.cpp:424

cnft::set_no_variables

virtual void set_no_variables(size_t no)

Definition cnf.h:43

cnft::no_variables

virtual size_t no_variables() const override

Definition cnf.h:42

literalt

Definition literal.h:26

literalt::var_no

var_not var_no() const

Definition literal.h:83

messaget::eom

static eomt eom

Definition message.h:289

messaget::status

mstreamt & status() const

Definition message.h:416

propt::resultt

resultt

Definition prop.h:101

propt::resultt::P_UNSATISFIABLE

@ P_UNSATISFIABLE

propt::resultt::P_SATISFIABLE

@ P_SATISFIABLE

propt::resultt::P_ERROR

@ P_ERROR

qbf_squolemt::prop_solve

resultt prop_solve() override

Definition qbf_squolem.cpp:34

qbf_squolemt::solver_text

std::string solver_text() const override

Definition qbf_squolem.cpp:29

qbf_squolemt::squolem

Squolem2 squolem

Definition qbf_squolem.h:22

qbf_squolemt::qbf_squolemt

qbf_squolemt()

Definition qbf_squolem.cpp:14

qbf_squolemt::early_decision

bool early_decision

Definition qbf_squolem.h:23

qbf_squolemt::~qbf_squolemt

~qbf_squolemt() override

Definition qbf_squolem.cpp:19

qbf_squolemt::l_get

tvt l_get(literalt a) const override

Definition qbf_squolem.cpp:24

qbf_squolemt::set_no_variables

void set_no_variables(size_t no) override

Definition qbf_squolem.cpp:109

qbf_squolemt::set_quantifier

void set_quantifier(const quantifiert::typet type, const literalt l) override

Definition qbf_squolem.cpp:115

qbf_squolemt::no_clauses

virtual size_t no_clauses() const

Definition qbf_squolem.h:37

qbf_squolemt::add_quantifier

void add_quantifier(const quantifiert &quantifier) override

Definition qbf_squolem.cpp:100

qbf_squolemt::lcnf

void lcnf(const bvt &bv) override

Definition qbf_squolem.cpp:71

qdimacs_cnft::quantifiert

Definition qdimacs_cnf.h:35

qdimacs_cnft::add_quantifier

virtual void add_quantifier(const quantifiert &quantifier)

Definition qdimacs_cnf.h:64

qdimacs_cnft::set_quantifier

virtual void set_quantifier(const quantifiert::typet type, const literalt l)

Definition qdimacs_cnf.cpp:73

tvt

Definition threeval.h:20

bvt

std::vector< literalt > bvt

Definition literal.h:201

qbf_squolem.h

Squolem Backend.

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525