cprover
prop_wrapper.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_PROP_PROP_WRAPPER_H
11 #define CPROVER_SOLVERS_PROP_PROP_WRAPPER_H
12 
13 #include "prop.h"
14 
15 class prop_wrappert:public virtual propt
16 {
17  public:
18  explicit prop_wrappert(propt &_prop):propt(_prop), p(_prop) { }
19  virtual ~prop_wrappert() { }
20 
21  virtual literalt constant(bool value)
22  { return p.constant(value); }
23 
24  // boolean operators
26  { return p.land(a, b); }
27 
28  virtual literalt lor(literalt a, literalt b)
29  { return p.lor(a, b); }
30 
31  virtual literalt land(const bvt &bv)
32  { return p.land(bv); }
33 
34  virtual literalt lor(const bvt &bv)
35  { return p.lor(bv); }
36 
38  { return p.lxor(a, b); }
39 
40  virtual literalt lxor(const bvt &bv)
41  { return p.lxor(bv); }
42 
44  { return p.lnand(a, b); }
45 
47  { return p.lnor(a, b); }
48 
50  { return p.lequal(a, b); }
51 
53  { return p.limplies(a, b); }
54 
55  virtual literalt lselect(literalt a, literalt b, literalt c) // a?b:c
56  { return p.lselect(a, b, c); }
57 
58  // constraints
59  virtual void lcnf(const bvt &bv)
60  { p.lcnf(bv); }
61 
62  virtual void l_set_to(literalt a, bool value)
63  { p.l_set_to(a, value); }
64 
65  // literals
67  { return p.new_variable(); }
68 
69  virtual std::size_t no_variables() const
70  { return p.no_variables(); }
71 
72  // solving
73  virtual const std::string solver_text()
74  { return p.solver_text(); }
75 
76  virtual tvt l_get(literalt a) const
77  { return p.l_get(a); }
78 
79  virtual resultt prop_solve()
80  { return p.prop_solve(); }
81 
82  protected:
83  propt &p;
84 };
85 
86 #endif // CPROVER_SOLVERS_PROP_PROP_WRAPPER_H
virtual literalt new_variable()
Definition: prop_wrapper.h:66
virtual resultt prop_solve()
Definition: prop_wrapper.h:79
virtual literalt land(literalt a, literalt b)
Definition: prop_wrapper.h:25
virtual literalt lxor(literalt a, literalt b)
Definition: prop_wrapper.h:37
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
virtual const std::string solver_text()=0
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: prop_wrapper.h:55
virtual const std::string solver_text()
Definition: prop_wrapper.h:73
virtual literalt lor(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)
Definition: prop_wrapper.h:28
virtual std::size_t no_variables() const
Definition: prop_wrapper.h:69
virtual literalt limplies(literalt a, literalt b)
Definition: prop_wrapper.h:52
virtual literalt limplies(literalt a, literalt b)=0
prop_wrappert(propt &_prop)
Definition: prop_wrapper.h:18
virtual literalt lor(const bvt &bv)
Definition: prop_wrapper.h:34
virtual literalt land(literalt a, literalt b)=0
virtual literalt constant(bool value)
Definition: prop_wrapper.h:21
virtual ~prop_wrappert()
Definition: prop_wrapper.h:19
virtual tvt l_get(literalt a) const
Definition: prop_wrapper.h:76
virtual literalt new_variable()=0
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:42
virtual void l_set_to(literalt a, bool value)
Definition: prop_wrapper.h:62
virtual literalt lxor(literalt a, literalt b)=0
virtual size_t no_variables() const =0
Definition: threeval.h:19
resultt
Definition: prop.h:94
virtual literalt lxor(const bvt &bv)
Definition: prop_wrapper.h:40
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual void lcnf(const bvt &bv)
Definition: prop_wrapper.h:59
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lnand(literalt a, literalt b)
Definition: prop_wrapper.h:43
virtual literalt lnor(literalt a, literalt b)
Definition: prop_wrapper.h:46
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
virtual literalt lequal(literalt a, literalt b)
Definition: prop_wrapper.h:49
virtual literalt land(const bvt &bv)
Definition: prop_wrapper.h:31
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt
Definition: literal.h:197