cprover
smt2_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_SMT2_SMT2_PROP_H
11 #define CPROVER_SOLVERS_SMT2_SMT2_PROP_H
12 
13 #include <iosfwd>
14 #include <set>
15 
16 #include <util/threeval.h>
17 
18 #include <solvers/prop/prop.h>
19 
20 class smt2_propt:public propt
21 {
22 public:
23  smt2_propt(
24  const std::string &_benchmark,
25  const std::string &_source,
26  const std::string &_logic,
27  bool _core_enabled,
28  std::ostream &_out);
29  virtual ~smt2_propt();
30 
31  virtual literalt land(literalt a, literalt b);
32  virtual literalt lor(literalt a, literalt b);
33  virtual literalt land(const bvt &bv);
34  virtual literalt lor(const bvt &bv);
35  virtual literalt lxor(const bvt &bv);
36  virtual literalt lxor(literalt a, literalt b);
37  virtual literalt lnand(literalt a, literalt b);
38  virtual literalt lnor(literalt a, literalt b);
39  virtual literalt lequal(literalt a, literalt b);
40  virtual literalt limplies(literalt a, literalt b);
41  virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c
42 
43  virtual literalt new_variable();
44  virtual size_t no_variables() const { return _no_variables; }
45  virtual void set_no_variables(size_t no) { assert(false); }
46 
47  virtual void lcnf(const bvt &bv);
48 
49  virtual const std::string solver_text()
50  { return "SMT"; }
51 
52  virtual tvt l_get(literalt literal) const;
53  virtual void set_assignment(literalt a, bool value);
54 
55  virtual propt::resultt prop_solve();
56 
57  virtual void clear()
58  {
59  assignment.clear();
60  }
61 
62  virtual void reset_assignment()
63  {
64  assignment.clear();
66  }
67 
68  friend class smt2_convt;
69  friend class smt2_dect;
70 
71  void finalize();
72 
73 protected:
74  size_t _no_variables;
75  std::ostream &out;
76 
77  std::string smt2_literal(literalt l);
79 
80  std::vector<tvt> assignment;
81 
83 
84  typedef std::set<std::string> smt2_identifierst;
86 
88 };
89 
90 #endif // CPROVER_SOLVERS_SMT2_SMT2_PROP_H
virtual void set_no_variables(size_t no)
Definition: smt2_prop.h:45
virtual ~smt2_propt()
Definition: smt2_prop.cpp:37
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: smt2_prop.cpp:213
virtual literalt lxor(const bvt &bv)
Definition: smt2_prop.cpp:95
literalt def_smt2_literal()
virtual literalt land(literalt a, literalt b)
Definition: smt2_prop.cpp:117
virtual void lcnf(const bvt &bv)
Definition: smt2_prop.cpp:267
virtual literalt limplies(literalt a, literalt b)
Definition: smt2_prop.cpp:208
virtual literalt lequal(literalt a, literalt b)
Definition: smt2_prop.cpp:203
virtual propt::resultt prop_solve()
Definition: smt2_prop.cpp:331
smt2_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out)
Definition: smt2_prop.cpp:13
smt2_identifierst smt2_identifiers
Definition: smt2_prop.h:85
std::string smt2_literal(literalt l)
Definition: smt2_prop.cpp:290
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:35
void finalize()
Definition: smt2_prop.cpp:41
virtual tvt l_get(literalt literal) const
Definition: smt2_prop.cpp:307
virtual void reset_assignment()
Definition: smt2_prop.h:62
virtual literalt lor(literalt a, literalt b)
Definition: smt2_prop.cpp:143
virtual literalt lnand(literalt a, literalt b)
Definition: smt2_prop.cpp:193
Definition: threeval.h:19
std::set< std::string > smt2_identifierst
Definition: smt2_prop.h:84
resultt
Definition: prop.h:94
virtual void clear()
Definition: smt2_prop.h:57
virtual const std::string solver_text()
Definition: smt2_prop.h:49
virtual size_t no_variables() const
Definition: smt2_prop.h:44
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual literalt lnor(literalt a, literalt b)
Definition: smt2_prop.cpp:198
size_t _no_variables
Definition: smt2_prop.h:74
literalt define_new_variable()
Definition: smt2_prop.cpp:254
virtual void set_assignment(literalt a, bool value)
Definition: smt2_prop.cpp:321
bool core_enabled
Definition: smt2_prop.h:87
std::vector< tvt > assignment
Definition: smt2_prop.h:80
virtual literalt new_variable()
Definition: smt2_prop.cpp:243
std::vector< literalt > bvt
Definition: literal.h:197
std::ostream & out
Definition: smt2_prop.h:75