cprover
cnf.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CNF Generation, via Tseitin
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_SAT_CNF_H
13 #define CPROVER_SOLVERS_SAT_CNF_H
14 
15 #include <solvers/prop/prop.h>
16 
17 class cnft:public propt
18 {
19 public:
20  // For CNF, we don't use index 0 as a matter of principle,
21  // so we'll start counting variables at 1.
22  explicit cnft(message_handlert &message_handler)
23  : propt(message_handler), _no_variables(1)
24  {
25  }
26  virtual ~cnft() { }
27 
28  virtual literalt land(literalt a, literalt b) override;
29  virtual literalt lor(literalt a, literalt b) override;
30  virtual literalt land(const bvt &bv) override;
31  virtual literalt lor(const bvt &bv) override;
32  virtual literalt lxor(const bvt &bv) override;
33  virtual literalt lxor(literalt a, literalt b) override;
34  virtual literalt lnand(literalt a, literalt b) override;
35  virtual literalt lnor(literalt a, literalt b) override;
36  virtual literalt lequal(literalt a, literalt b) override;
37  virtual literalt limplies(literalt a, literalt b) override;
38  // a?b:c
39  virtual literalt lselect(literalt a, literalt b, literalt c) override;
40  virtual literalt new_variable() override;
41  virtual size_t no_variables() const override { return _no_variables; }
42  virtual void set_no_variables(size_t no) { _no_variables=no; }
43  virtual size_t no_clauses() const=0;
44 
45 protected:
46  void gate_and(literalt a, literalt b, literalt o);
47  void gate_or(literalt a, literalt b, literalt o);
48  void gate_xor(literalt a, literalt b, literalt o);
49  void gate_nand(literalt a, literalt b, literalt o);
50  void gate_nor(literalt a, literalt b, literalt o);
51  void gate_equal(literalt a, literalt b, literalt o);
52  void gate_implies(literalt a, literalt b, literalt o);
53 
54  static bvt eliminate_duplicates(const bvt &);
55 
56  size_t _no_variables;
57 
58  bool process_clause(const bvt &bv, bvt &dest);
59 
60  static bool is_all(const bvt &bv, literalt l)
61  {
62  forall_literals(it, bv)
63  if(*it!=l)
64  return false;
65  return true;
66  }
67 };
68 
69 class cnf_solvert:public cnft
70 {
71 public:
72  explicit cnf_solvert(message_handlert &message_handler)
73  : cnft(message_handler), status(statust::INIT), clause_counter(0)
74  {
75  }
76 
77  virtual size_t no_clauses() const override
78  {
79  return clause_counter;
80  }
81 
82 protected:
83  enum class statust { INIT, SAT, UNSAT, ERROR };
86 };
87 
88 #endif // CPROVER_SOLVERS_SAT_CNF_H
cnft::lnand
virtual literalt lnand(literalt a, literalt b) override
Definition: cnf.cpp:319
cnf_solvert::statust::SAT
@ SAT
cnft::gate_xor
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
Definition: cnf.cpp:70
cnft::process_clause
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
bvt
std::vector< literalt > bvt
Definition: literal.h:201
cnft::lnor
virtual literalt lnor(literalt a, literalt b) override
Definition: cnf.cpp:326
cnft::cnft
cnft(message_handlert &message_handler)
Definition: cnf.h:22
cnft
Definition: cnf.h:18
cnft::~cnft
virtual ~cnft()
Definition: cnf.h:26
cnf_solvert::statust::INIT
@ INIT
cnft::gate_equal
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
Definition: cnf.cpp:145
cnft::lxor
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.
Definition: cnf.cpp:246
cnft::gate_nor
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
Definition: cnf.cpp:123
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
cnft::land
virtual literalt land(literalt a, literalt b) override
Definition: cnf.cpp:265
cnf_solvert
Definition: cnf.h:70
cnf_solvert::statust::ERROR
@ ERROR
cnft::gate_or
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
Definition: cnf.cpp:48
cnft::is_all
static bool is_all(const bvt &bv, literalt l)
Definition: cnf.h:60
cnft::lor
virtual literalt lor(literalt a, literalt b) override
Definition: cnf.cpp:281
cnft::set_no_variables
virtual void set_no_variables(size_t no)
Definition: cnf.h:42
cnft::new_variable
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
Definition: cnf.cpp:387
cnft::limplies
virtual literalt limplies(literalt a, literalt b) override
Definition: cnf.cpp:336
cnft::gate_implies
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
Definition: cnf.cpp:152
cnf_solvert::statust::UNSAT
@ UNSAT
cnft::eliminate_duplicates
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
Definition: cnf.cpp:400
cnf_solvert::status
statust status
Definition: cnf.h:84
prop.h
cnf_solvert::clause_counter
size_t clause_counter
Definition: cnf.h:85
message_handlert
Definition: message.h:28
cnf_solvert::cnf_solvert
cnf_solvert(message_handlert &message_handler)
Definition: cnf.h:72
cnft::lselect
virtual literalt lselect(literalt a, literalt b, literalt c) override
Definition: cnf.cpp:346
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
cnft::gate_and
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
Definition: cnf.cpp:25
cnft::gate_nand
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
Definition: cnf.cpp:101
literalt
Definition: literal.h:26
cnft::_no_variables
size_t _no_variables
Definition: cnf.h:56
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:41
cnf_solvert::no_clauses
virtual size_t no_clauses() const override
Definition: cnf.h:77
cnft::no_clauses
virtual size_t no_clauses() const =0
cnft::lequal
virtual literalt lequal(literalt a, literalt b) override
Definition: cnf.cpp:331
cnf_solvert::statust
statust
Definition: cnf.h:83