cprover
dplib_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_DPLIB_DPLIB_PROP_H
11 #define CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H
12 
13 #include <iosfwd>
14 
15 #include <util/threeval.h>
16 
17 #include <solvers/prop/prop.h>
18 
19 class dplib_propt:virtual public propt
20 {
21 public:
22  explicit dplib_propt(std::ostream &_out);
23  virtual ~dplib_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  // virtual unsigned no_clauses()=0;
48 
49  virtual void lcnf(const bvt &bv);
50 
51  virtual const std::string solver_text()
52  { return "DPLIB"; }
53 
54  virtual tvt l_get(literalt literal) const
55  {
56  unsigned v=literal.var_no();
57  if(v>=assignment.size())
58  return tvt::unknown();
59  tvt r=assignment[v];
60  return literal.sign()?!r:r;
61  }
62 
63  virtual propt::resultt prop_solve();
64 
65  friend class dplib_convt;
66  friend class dplib_dect;
67 
68  virtual void clear()
69  {
70  assignment.clear();
71  }
72 
74  {
75  assignment.clear();
77  }
78 
79 protected:
80  unsigned _no_variables;
81  std::ostream &out;
82 
83  std::string dplib_literal(literalt l);
85 
86  std::vector<tvt> assignment;
87 
88  void finish();
89 };
90 
91 #endif // CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H
virtual void lnand(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:45
virtual const std::string solver_text()
Definition: dplib_prop.h:51
static int8_t r
Definition: irep_hash.h:59
virtual tvt l_get(literalt literal) const
Definition: dplib_prop.h:54
virtual propt::resultt prop_solve()
Definition: dplib_prop.cpp:301
static tvt unknown()
Definition: threeval.h:33
std::string dplib_literal(literalt l)
Definition: dplib_prop.cpp:282
virtual void set_no_variables(size_t no)
Definition: dplib_prop.h:46
virtual size_t no_variables() const
Definition: dplib_prop.h:45
virtual void lcnf(const bvt &bv)
Definition: dplib_prop.cpp:246
virtual literalt new_variable()
Definition: dplib_prop.cpp:228
Definition: threeval.h:19
virtual void clear()
Definition: dplib_prop.h:68
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
void reset_assignment()
Definition: dplib_prop.h:73
virtual ~dplib_propt()
Definition: dplib_prop.h:23
std::vector< tvt > assignment
Definition: dplib_prop.h:86
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::ostream & out
Definition: dplib_prop.h:81
virtual void land(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:21
virtual void limplies(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:69
dplib_propt(std::ostream &_out)
Definition: dplib_prop.cpp:15
literalt def_dplib_literal()
Definition: dplib_prop.cpp:237
unsigned _no_variables
Definition: dplib_prop.h:80
virtual void lnor(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:53
virtual void lequal(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:61
bool sign() const
Definition: literal.h:87
void finish()
Definition: dplib_prop.cpp:295
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: dplib_prop.cpp:208
virtual void lor(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:29
std::vector< literalt > bvt
Definition: literal.h:197
virtual void lxor(literalt a, literalt b, literalt o)
Definition: dplib_prop.cpp:37