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) const;
59 
60  static bool is_all(const bvt &bv, literalt l)
61  {
62  for(const auto &literal : bv)
63  {
64  if(literal != l)
65  return false;
66  }
67  return true;
68  }
69 };
70 
71 class cnf_solvert:public cnft
72 {
73 public:
74  explicit cnf_solvert(message_handlert &message_handler)
75  : cnft(message_handler), status(statust::INIT), clause_counter(0)
76  {
77  }
78 
79  virtual size_t no_clauses() const override
80  {
81  return clause_counter;
82  }
83 
84 protected:
85  enum class statust { INIT, SAT, UNSAT, ERROR };
88 };
89 
90 #endif // CPROVER_SOLVERS_SAT_CNF_H
statust status
Definition: cnf.h:86
cnf_solvert(message_handlert &message_handler)
Definition: cnf.h:74
virtual size_t no_clauses() const override
Definition: cnf.h:79
statust
Definition: cnf.h:85
size_t clause_counter
Definition: cnf.h:87
Definition: cnf.h:18
static bool is_all(const bvt &bv, literalt l)
Definition: cnf.h:60
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
Definition: cnf.cpp:145
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
Definition: cnf.cpp:48
virtual ~cnft()
Definition: cnf.h:26
virtual literalt limplies(literalt a, literalt b) override
Definition: cnf.cpp:336
virtual literalt lselect(literalt a, literalt b, literalt c) override
Definition: cnf.cpp:346
virtual void set_no_variables(size_t no)
Definition: cnf.h:42
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
Definition: cnf.cpp:400
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
Definition: cnf.cpp:101
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
Definition: cnf.cpp:387
virtual size_t no_variables() const override
Definition: cnf.h:41
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
Definition: cnf.cpp:70
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
Definition: cnf.cpp:123
size_t _no_variables
Definition: cnf.h:56
cnft(message_handlert &message_handler)
Definition: cnf.h:22
virtual literalt lequal(literalt a, literalt b) override
Definition: cnf.cpp:331
virtual literalt land(literalt a, literalt b) override
Definition: cnf.cpp:265
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
Definition: cnf.cpp:152
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.
Definition: cnf.cpp:246
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
Definition: cnf.cpp:25
virtual literalt lnand(literalt a, literalt b) override
Definition: cnf.cpp:319
virtual size_t no_clauses() const =0
virtual literalt lnor(literalt a, literalt b) override
Definition: cnf.cpp:326
virtual literalt lor(literalt a, literalt b) override
Definition: cnf.cpp:281
TO_BE_DOCUMENTED.
Definition: prop.h:25
std::vector< literalt > bvt
Definition: literal.h:201