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_clause_listt::~cnf_clause_listt
virtual ~cnf_clause_listt()
Definition: cnf_clause_list.h:27
cnf_clause_listt::no_clauses
virtual size_t no_clauses() const
Definition: cnf_clause_list.h:41
cnf_clause_listt::clauses
clausest clauses
Definition: cnf_clause_list.h:76
cnf_clause_list_assignmentt::copy_assignment_from
virtual void copy_assignment_from(const propt &prop)
Definition: cnf_clause_list.cpp:32
bvt
std::vector< literalt > bvt
Definition: literal.h:200
cnf_clause_listt
Definition: cnf_clause_list.h:23
threeval.h
cnf_clause_listt::l_get
virtual tvt l_get(literalt) const
Definition: cnf_clause_list.h:34
cnf_clause_list_assignmentt
Definition: cnf_clause_list.h:82
cnft
Definition: cnf.h:17
literalt::var_no
var_not var_no() const
Definition: literal.h:82
cnf_clause_listt::cnf_clause_listt
cnf_clause_listt()
Definition: cnf_clause_list.h:26
cnf_clause_listt::prop_solve
virtual resultt prop_solve()
Definition: cnf_clause_list.h:39
literalt::is_true
bool is_true() const
Definition: literal.h:155
cnft::set_no_variables
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
cnf_clause_listt::clausest
std::list< bvt > clausest
Definition: cnf_clause_list.h:43
messaget::result
mstreamt & result() const
Definition: message.h:396
cnf_clause_list_assignmentt::l_get
virtual tvt l_get(literalt literal) const
Definition: cnf_clause_list.h:92
propt::resultt::P_ERROR
literalt::is_false
bool is_false() const
Definition: literal.h:160
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:96
cnf_clause_list_assignmentt::print_assignment
void print_assignment(std::ostream &out) const
Definition: cnf_clause_list.cpp:26
cnf_clause_listt::hash_clause
static size_t hash_clause(const bvt &bv)
Definition: cnf_clause_list.h:57
cnf_clause_listt::get_clauses
clausest & get_clauses()
Definition: cnf_clause_list.h:45
tvt
Definition: threeval.h:19
literalt::sign
bool sign() const
Definition: literal.h:87
cnf_clause_list_assignmentt::get_assignment
assignmentt & get_assignment()
Definition: cnf_clause_list.h:87
cnf_clause_listt::lcnf
virtual void lcnf(const bvt &bv)
Definition: cnf_clause_list.cpp:16
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
cnf_clause_list_assignmentt::assignmentt
std::vector< tvt > assignmentt
Definition: cnf_clause_list.h:85
literalt
Definition: literal.h:24
cnft::_no_variables
size_t _no_variables
Definition: cnf.h:53
r
static int8_t r
Definition: irep_hash.h:59
cnf_clause_listt::copy_to
void copy_to(cnft &cnf) const
Definition: cnf_clause_list.h:47
cnf.h
cnf_clause_listt::solver_text
virtual const std::string solver_text()
Definition: cnf_clause_list.h:31
cnf_clause_list_assignmentt::assignment
assignmentt assignment
Definition: cnf_clause_list.h:112
cnf_clause_listt::hash
size_t hash() const
Definition: cnf_clause_list.h:66
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:55