CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt_solver_process.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
5
6class smt_commandt;
7
8#include <util/message.h>
10
12
13#include <memory>
14#include <sstream>
15#include <string>
16
18{
19public:
20 virtual const std::string &description() = 0;
21
24 virtual void send(const smt_commandt &command) = 0;
25
26 virtual smt_responset
27 receive_response(const std::unordered_map<irep_idt, smt_identifier_termt>
28 &identifier_table) = 0;
29
30 virtual ~smt_base_solver_processt() = default;
31};
32
34{
35public:
43 std::string command_line,
44 message_handlert &message_handler,
45 std::unique_ptr<std::ostream> out_stream);
46
47 const std::string &description() override;
48
49 void send(const smt_commandt &smt_command) override;
50
52 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
53 override;
54
55 ~smt_piped_solver_processt() override = default;
56
57protected:
61 std::unique_ptr<std::ostream> out_stream;
65 std::stringstream response_stream;
68};
69
73{
74public:
83 message_handlert &message_handler,
84 std::ostream &out_stream,
85 std::unique_ptr<std::ostream> file_stream);
86
87 const std::string &description() override;
88
89 void send(const smt_commandt &smt_command) override;
90
93 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
94 override;
95
97
98protected:
101 std::unique_ptr<std::ostream> file_stream;
103 std::ostream &out_stream;
106
108 const std::string desc = "SMT2 incremental dry-run";
109};
110
111#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
virtual ~smt_base_solver_processt()=default
virtual smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)=0
virtual const std::string & description()=0
Class for an incremental SMT solver used in combination with --outfile argument where the solver is n...
const std::string & description() override
smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) override
void send(const smt_commandt &smt_command) override
Converts given SMT2 command to SMT2 string and sends it to the solver process.
std::unique_ptr< std::ostream > file_stream
Pointer to the file stream to print the SMT formula.
std::ostream & out_stream
The output stream reference to print the SMT formula to.
messaget log
For debug printing.
const std::string desc
Description of the current solver.
~smt_incremental_dry_run_solvert() override=default
messaget log
For debug printing.
std::string command_line_description
The command line used to start the process.
void send(const smt_commandt &smt_command) override
Converts given SMT2 command to SMT2 string and sends it to the solver process.
~smt_piped_solver_processt() override=default
const std::string & description() override
std::stringstream response_stream
For buffering / combining communications from the solver to cbmc.
smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) override
std::unique_ptr< std::ostream > out_stream
Pointer to the stream to print the SMT formula. nullptr if no output.
piped_processt process
The raw solver sub process.
Subprocess communication with pipes.