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 "smt2_conv.h"
14 
15 #include <util/message.h>
16 
17 #include <fstream>
18 
20 {
21 protected:
22  std::stringstream stringstream;
23 };
24 
27 class smt2_dect : protected smt2_stringstreamt,
28  public smt2_convt,
29  public messaget
30 {
31 public:
33  const namespacet &_ns,
34  const std::string &_benchmark,
35  const std::string &_notes,
36  const std::string &_logic,
37  solvert _solver):
38  smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream)
39  {
40  }
41 
42  resultt dec_solve() override;
43  std::string decision_procedure_text() const override;
44 
45 protected:
46  resultt read_result(std::istream &in);
47 };
48 
49 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
smt2_conv.h
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
smt2_stringstreamt::stringstream
std::stringstream stringstream
Definition: smt2_dec.h:22
smt2_dect::dec_solve
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_dec.cpp:37
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:32
smt2_convt
Definition: smt2_conv.h:35
smt2_dect::read_result
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:133
smt2_dect::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_dec.cpp:21
smt2_dect
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:30
smt2_convt::solvert
solvert
Definition: smt2_conv.h:38
smt2_stringstreamt
Definition: smt2_dec.h:20
message.h