cprover
smt2_dec.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_DEC_H
11 #define CPROVER_SOLVERS_SMT2_SMT2_DEC_H
12 
13 #include <fstream>
14 
15 #include "smt2_conv.h"
16 
18 {
19 protected:
20  std::stringstream stringstream;
21 };
22 
25 class smt2_dect:protected smt2_stringstreamt, public smt2_convt
26 {
27 public:
29  const namespacet &_ns,
30  const std::string &_benchmark,
31  const std::string &_notes,
32  const std::string &_logic,
33  solvert _solver):
34  smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream)
35  {
36  }
37 
38  virtual resultt dec_solve();
39  virtual std::string decision_procedure_text() const;
40 
41  // yes, we are incremental!
42  virtual bool has_set_assumptions() const { return true; }
43 
44 protected:
45  resultt read_result(std::istream &in);
46 };
47 
48 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
std::stringstream stringstream
Definition: smt2_dec.h:20
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:131
virtual resultt dec_solve()
Definition: smt2_dec.cpp:37
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:25
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
virtual std::string decision_procedure_text() const
Definition: smt2_dec.cpp:21
virtual bool has_set_assumptions() const
Definition: smt2_dec.h:42
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
Definition: smt2_dec.h:28