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 public:
22 
23  std::ofstream temp_out;
25 };
26 
28 {
29 protected:
30  std::stringstream stringstream;
31 };
32 
35 class smt2_dect:protected smt2_stringstreamt, public smt2_convt
36 {
37 public:
39  const namespacet &_ns,
40  const std::string &_benchmark,
41  const std::string &_notes,
42  const std::string &_logic,
43  solvert _solver):
44  smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream)
45  {
46  }
47 
48  virtual resultt dec_solve();
49  virtual std::string decision_procedure_text() const;
50 
51  // yes, we are incremental!
52  virtual bool has_set_assumptions() const { return true; }
53 
54 protected:
55  resultt read_result(std::istream &in);
56 };
57 
58 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
std::stringstream stringstream
Definition: smt2_dec.h:30
std::string temp_result_filename
Definition: smt2_dec.h:24
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:35
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::string temp_out_filename
Definition: smt2_dec.h:24
std::ofstream temp_out
Definition: smt2_dec.h:23
virtual bool has_set_assumptions() const
Definition: smt2_dec.h:52
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
Definition: smt2_dec.h:38