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
smt2_conv.h
smt2_dect::decision_procedure_text
virtual std::string decision_procedure_text() const
Definition: smt2_dec.cpp:21
smt2_dect::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: smt2_dec.h:42
smt2_stringstreamt::stringstream
std::stringstream stringstream
Definition: smt2_dec.h:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
smt2_dect::smt2_dect
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
Definition: smt2_dec.h:28
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
smt2_convt
Definition: smt2_conv.h:32
smt2_dect::read_result
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:131
smt2_dect
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:25
smt2_dect::dec_solve
virtual resultt dec_solve()
Definition: smt2_dec.cpp:37
smt2_convt::solvert
solvert
Definition: smt2_conv.h:35
smt2_stringstreamt
Definition: smt2_dec.h:17