cprover
cvc_prop.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_CVC_CVC_PROP_H
11 #define CPROVER_SOLVERS_CVC_CVC_PROP_H
12 
13 #include <iosfwd>
14 
15 #include <util/threeval.h>
16 
17 #include <solvers/prop/prop.h>
18 
19 class cvc_propt:virtual public propt
20 {
21 public:
22  explicit cvc_propt(std::ostream &_out);
23  virtual ~cvc_propt();
24 
25  virtual void land(literalt a, literalt b, literalt o);
26  virtual void lor(literalt a, literalt b, literalt o);
27  virtual void lxor(literalt a, literalt b, literalt o);
28  virtual void lnand(literalt a, literalt b, literalt o);
29  virtual void lnor(literalt a, literalt b, literalt o);
30  virtual void lequal(literalt a, literalt b, literalt o);
31  virtual void limplies(literalt a, literalt b, literalt o);
32 
33  virtual literalt land(literalt a, literalt b);
34  virtual literalt lor(literalt a, literalt b);
35  virtual literalt land(const bvt &bv);
36  virtual literalt lor(const bvt &bv);
37  virtual literalt lxor(const bvt &bv);
38  virtual literalt lxor(literalt a, literalt b);
39  virtual literalt lnand(literalt a, literalt b);
40  virtual literalt lnor(literalt a, literalt b);
41  virtual literalt lequal(literalt a, literalt b);
42  virtual literalt limplies(literalt a, literalt b);
43  virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c
44  virtual literalt new_variable();
45  virtual size_t no_variables() const { return _no_variables; }
46  virtual void set_no_variables(size_t no) { assert(false); }
47 
48  virtual void lcnf(const bvt &bv);
49 
50  virtual const std::string solver_text()
51  { return "CVC"; }
52 
53  virtual tvt l_get(literalt literal) const
54  {
55  unsigned v=literal.var_no();
56  if(v>=assignment.size())
58  tvt r=assignment[v];
59  return literal.sign()?!r:r;
60  }
61 
62  virtual propt::resultt prop_solve();
63 
64  friend class cvc_convt;
65  friend class cvc_dect;
66 
67  virtual void clear()
68  {
69  assignment.clear();
70  }
71 
73  {
74  assignment.clear();
76  }
77 
78 protected:
79  unsigned _no_variables;
80  std::ostream &out;
81 
82  std::string cvc_literal(literalt l);
84 
85  std::vector<tvt> assignment;
86 };
87 
88 #endif // CPROVER_SOLVERS_CVC_CVC_PROP_H
static int8_t r
Definition: irep_hash.h:59
unsigned _no_variables
Definition: cvc_prop.h:79
virtual void limplies(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:71
virtual void lor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:31
virtual void lnor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:55
std::ostream & out
Definition: cvc_prop.h:80
virtual void set_no_variables(size_t no)
Definition: cvc_prop.h:46
void reset_assignment()
Definition: cvc_prop.h:72
virtual void lxor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:39
virtual ~cvc_propt()
Definition: cvc_prop.cpp:19
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::vector< tvt > assignment
Definition: cvc_prop.h:85
virtual void land(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:23
cvc_propt(std::ostream &_out)
Definition: cvc_prop.cpp:14
virtual void lcnf(const bvt &bv)
Definition: cvc_prop.cpp:254
literalt def_cvc_literal()
Definition: cvc_prop.cpp:245
std::string cvc_literal(literalt l)
Definition: cvc_prop.cpp:290
virtual void lequal(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:63
bool sign() const
Definition: literal.h:87
virtual const std::string solver_text()
Definition: cvc_prop.h:50
virtual size_t no_variables() const
Definition: cvc_prop.h:45
virtual literalt new_variable()
Definition: cvc_prop.cpp:236
virtual propt::resultt prop_solve()
Definition: cvc_prop.cpp:303
virtual void lnand(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:47
virtual tvt l_get(literalt literal) const
Definition: cvc_prop.h:53
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: cvc_prop.cpp:216
virtual void clear()
Definition: cvc_prop.h:67
std::vector< literalt > bvt
Definition: literal.h:197