cprover
cnf_clause_list.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CNF Generation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H
13 #define CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H
14 
15 #include <list>
16 
17 #include <util/threeval.h>
18 
19 #include "cnf.h"
20 
21 // CNF given as a list of clauses
22 
23 class cnf_clause_listt:public cnft
24 {
25 public:
27  virtual ~cnf_clause_listt() { }
28 
29  virtual void lcnf(const bvt &bv);
30 
31  virtual const std::string solver_text()
32  { return "CNF clause list"; }
33 
34  virtual tvt l_get(literalt) const
35  {
36  return tvt::unknown();
37  }
38 
39  virtual resultt prop_solve() { return resultt::P_ERROR; }
40 
41  virtual size_t no_clauses() const { return clauses.size(); }
42 
43  typedef std::list<bvt> clausest;
44 
45  clausest &get_clauses() { return clauses; }
46 
47  void copy_to(cnft &cnf) const
48  {
50  for(clausest::const_iterator
51  it=clauses.begin();
52  it!=clauses.end();
53  it++)
54  cnf.lcnf(*it);
55  }
56 
57  static size_t hash_clause(const bvt &bv)
58  {
59  size_t result=0;
60  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
61  result=((result<<2)^it->get())-result;
62 
63  return result;
64  }
65 
66  size_t hash() const
67  {
68  size_t result=0;
69  for(clausest::const_iterator it=clauses.begin(); it!=clauses.end(); it++)
70  result=((result<<2)^hash_clause(*it))-result;
71 
72  return result;
73  }
74 
75 protected:
77 };
78 
79 // CNF given as a list of clauses
80 // PLUS an assignment to the variables
81 
83 {
84 public:
85  typedef std::vector<tvt> assignmentt;
86 
88  {
89  return assignment;
90  }
91 
92  virtual tvt l_get(literalt literal) const
93  {
94  if(literal.is_true())
95  return tvt(true);
96  if(literal.is_false())
97  return tvt(false);
98 
99  unsigned v=literal.var_no();
100 
101  if(v==0 || v>=assignment.size())
102  return tvt::unknown();
103 
104  tvt r=assignment[v];
105  return literal.sign()?!r:r;
106  }
107 
108  virtual void copy_assignment_from(const propt &prop);
109  void print_assignment(std::ostream &out) const;
110 
111 protected:
113 };
114 
115 #endif // CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H
CNF Generation, via Tseitin.
static int8_t r
Definition: irep_hash.h:59
size_t _no_variables
Definition: cnf.h:53
void print_assignment(std::ostream &out) const
void lcnf(literalt l0, literalt l1)
Definition: prop.h:55
assignmentt & get_assignment()
virtual tvt l_get(literalt literal) const
static tvt unknown()
Definition: threeval.h:33
virtual void copy_assignment_from(const propt &prop)
static size_t hash_clause(const bvt &bv)
Definition: cnf.h:17
size_t hash() const
virtual ~cnf_clause_listt()
std::vector< tvt > assignmentt
std::list< bvt > clausest
clausest & get_clauses()
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
resultt
Definition: prop.h:96
virtual resultt prop_solve()
virtual tvt l_get(literalt) const
TO_BE_DOCUMENTED.
Definition: prop.h:24
virtual size_t no_clauses() const
mstreamt & result() const
Definition: message.h:396
bool sign() const
Definition: literal.h:87
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
void copy_to(cnft &cnf) const
std::vector< literalt > bvt
Definition: literal.h:200
bool is_false() const
Definition: literal.h:160