cprover
Loading...
Searching...
No Matches
smt2_dec.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <fstream>
16
18
20{
21protected:
22 std::stringstream stringstream;
23};
24
27class smt2_dect : protected smt2_stringstreamt, public smt2_convt
28{
29public:
31 const namespacet &_ns,
32 const std::string &_benchmark,
33 const std::string &_notes,
34 const std::string &_logic,
39 {
40 }
41
42 resultt dec_solve() override;
43 std::string decision_procedure_text() const override;
44
45protected:
47
50 std::stringstream cached_output;
51
52 resultt read_result(std::istream &in);
53};
54
55#endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
resultt
Result of running the decision procedure.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Decision procedure interface for various SMT 2.x solvers.
Definition smt2_dec.h:28
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, message_handlert &_message_handler)
Definition smt2_dec.h:30
message_handlert & message_handler
Definition smt2_dec.h:46
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition smt2_dec.cpp:18
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition smt2_dec.cpp:34
resultt read_result(std::istream &in)
Definition smt2_dec.cpp:133
std::stringstream cached_output
Everything except the footer is cached, so that output files can be rewritten with varying footers.
Definition smt2_dec.h:50
std::stringstream stringstream
Definition smt2_dec.h:22
resultt
The result of goto verifying.
Definition properties.h:45