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.
23  virtual ~cnft() { }
24 
25  virtual literalt land(literalt a, literalt b) override;
26  virtual literalt lor(literalt a, literalt b) override;
27  virtual literalt land(const bvt &bv) override;
28  virtual literalt lor(const bvt &bv) override;
29  virtual literalt lxor(const bvt &bv) override;
30  virtual literalt lxor(literalt a, literalt b) override;
31  virtual literalt lnand(literalt a, literalt b) override;
32  virtual literalt lnor(literalt a, literalt b) override;
33  virtual literalt lequal(literalt a, literalt b) override;
34  virtual literalt limplies(literalt a, literalt b) override;
35  // a?b:c
36  virtual literalt lselect(literalt a, literalt b, literalt c) override;
37  virtual literalt new_variable() override;
38  virtual size_t no_variables() const override { return _no_variables; }
39  virtual void set_no_variables(size_t no) { _no_variables=no; }
40  virtual size_t no_clauses() const=0;
41 
42  void gate_and(literalt a, literalt b, literalt o);
43  void gate_or(literalt a, literalt b, literalt o);
44  void gate_xor(literalt a, literalt b, literalt o);
45  void gate_nand(literalt a, literalt b, literalt o);
46  void gate_nor(literalt a, literalt b, literalt o);
47  void gate_equal(literalt a, literalt b, literalt o);
48  void gate_implies(literalt a, literalt b, literalt o);
49 
50  static bvt eliminate_duplicates(const bvt &);
51 
52 protected:
53  size_t _no_variables;
54 
55  bool process_clause(const bvt &bv, bvt &dest);
56 
57  static bool is_all(const bvt &bv, literalt l)
58  {
59  forall_literals(it, bv)
60  if(*it!=l)
61  return false;
62  return true;
63  }
64 };
65 
66 class cnf_solvert:public cnft
67 {
68 public:
70  {
71  }
72 
73  virtual size_t no_clauses() const override
74  {
75  return clause_counter;
76  }
77 
78 protected:
79  enum class statust { INIT, SAT, UNSAT, ERROR };
82 };
83 
84 #endif // CPROVER_SOLVERS_SAT_CNF_H
size_t _no_variables
Definition: cnf.h:53
size_t clause_counter
Definition: cnf.h:81
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
Definition: cnf.cpp:152
virtual literalt lequal(literalt a, literalt b) override
Definition: cnf.cpp:331
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
Definition: cnf.cpp:101
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
virtual literalt lnor(literalt a, literalt b) override
Definition: cnf.cpp:326
statust status
Definition: cnf.h:80
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
Definition: cnf.cpp:400
virtual size_t no_clauses() const =0
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
Definition: cnf.cpp:48
virtual literalt lselect(literalt a, literalt b, literalt c) override
Definition: cnf.cpp:346
virtual size_t no_clauses() const override
Definition: cnf.h:73
virtual literalt land(literalt a, literalt b) override
Definition: cnf.cpp:265
#define forall_literals(it, bv)
Definition: literal.h:202
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
Definition: cnf.cpp:70
Definition: cnf.h:17
cnf_solvert()
Definition: cnf.h:69
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
Definition: cnf.cpp:387
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
Definition: cnf.cpp:123
virtual literalt limplies(literalt a, literalt b) override
Definition: cnf.cpp:336
virtual ~cnft()
Definition: cnf.h:23
TO_BE_DOCUMENTED.
Definition: prop.h:24
cnft()
Definition: cnf.h:22
virtual literalt lor(literalt a, literalt b) override
Definition: cnf.cpp:281
statust
Definition: cnf.h:79
mstreamt & status() const
Definition: message.h:401
static bool is_all(const bvt &bv, literalt l)
Definition: cnf.h:57
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
Definition: cnf.cpp:25
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
Definition: cnf.cpp:145
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual literalt lnand(literalt a, literalt b) override
Definition: cnf.cpp:319
std::vector< literalt > bvt
Definition: literal.h:200
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.
Definition: cnf.cpp:246