cprover
smt1_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_SMT1_SMT1_PROP_H
11 #define CPROVER_SOLVERS_SMT1_SMT1_PROP_H
12 
13 #include <iosfwd>
14 
15 #include <util/threeval.h>
16 
17 #include <solvers/prop/prop.h>
18 
19 class smt1_propt:public propt
20 {
21 public:
22  smt1_propt(
23  const std::string &_benchmark,
24  const std::string &_source,
25  const std::string &_logic,
26  std::ostream &_out);
27  virtual ~smt1_propt();
28 
29  virtual literalt land(literalt a, literalt b);
30  virtual literalt lor(literalt a, literalt b);
31  virtual literalt land(const bvt &bv);
32  virtual literalt lor(const bvt &bv);
33  virtual literalt lxor(const bvt &bv);
34  virtual literalt lxor(literalt a, literalt b);
35  virtual literalt lnand(literalt a, literalt b);
36  virtual literalt lnor(literalt a, literalt b);
37  virtual literalt lequal(literalt a, literalt b);
38  virtual literalt limplies(literalt a, literalt b);
39  virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c
40 
41  virtual literalt new_variable();
42  virtual size_t no_variables() const { return _no_variables; }
43  virtual void set_no_variables(size_t no) { assert(false); }
44 
45  virtual void lcnf(const bvt &bv);
46 
47  virtual const std::string solver_text()
48  { return "SMT"; }
49 
50  virtual tvt l_get(literalt literal) const;
51  virtual void set_assignment(literalt a, bool value);
52 
53  virtual propt::resultt prop_solve();
54 
55  virtual void clear()
56  {
57  assignment.clear();
58  }
59 
60  virtual void reset_assignment()
61  {
62  assignment.clear();
64  }
65 
66  friend class smt1_convt;
67  friend class smt1_dect;
68 
69  void finalize();
70 
71 protected:
72  size_t _no_variables;
73  std::ostream &out;
74 
75  std::string smt1_literal(literalt l);
77 
78  std::vector<tvt> assignment;
79 };
80 
81 #endif // CPROVER_SOLVERS_SMT1_SMT1_PROP_H
std::vector< tvt > assignment
Definition: smt1_prop.h:78
virtual void reset_assignment()
Definition: smt1_prop.h:60
virtual literalt lnor(literalt a, literalt b)
Definition: smt1_prop.cpp:176
void finalize()
Definition: smt1_prop.cpp:32
virtual void lcnf(const bvt &bv)
Definition: smt1_prop.cpp:232
virtual literalt land(literalt a, literalt b)
Definition: smt1_prop.cpp:95
virtual size_t no_variables() const
Definition: smt1_prop.h:42
virtual literalt lxor(const bvt &bv)
Definition: smt1_prop.cpp:73
virtual literalt new_variable()
Definition: smt1_prop.cpp:221
virtual ~smt1_propt()
Definition: smt1_prop.cpp:28
std::string smt1_literal(literalt l)
Definition: smt1_prop.cpp:255
virtual literalt lor(literalt a, literalt b)
Definition: smt1_prop.cpp:121
virtual literalt limplies(literalt a, literalt b)
Definition: smt1_prop.cpp:186
Definition: threeval.h:19
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: smt1_prop.cpp:191
resultt
Definition: prop.h:94
TO_BE_DOCUMENTED.
Definition: prop.h:22
Decision procedure interface for various SMT 1.x solvers.
Definition: smt1_dec.h:30
virtual void clear()
Definition: smt1_prop.h:55
literalt def_smt1_literal()
virtual void set_assignment(literalt a, bool value)
Definition: smt1_prop.cpp:284
virtual literalt lequal(literalt a, literalt b)
Definition: smt1_prop.cpp:181
virtual literalt lnand(literalt a, literalt b)
Definition: smt1_prop.cpp:171
size_t _no_variables
Definition: smt1_prop.h:72
virtual const std::string solver_text()
Definition: smt1_prop.h:47
virtual propt::resultt prop_solve()
Definition: smt1_prop.cpp:294
virtual void set_no_variables(size_t no)
Definition: smt1_prop.h:43
smt1_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, std::ostream &_out)
Definition: smt1_prop.cpp:15
std::vector< literalt > bvt
Definition: literal.h:197
std::ostream & out
Definition: smt1_prop.h:73
virtual tvt l_get(literalt literal) const
Definition: smt1_prop.cpp:270