smt_solver_process.h

Go to the documentation of this file.

// Author: Diffblue Ltd.
 
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
 
class smt_commandt;
 
#include <util/message.h>
#include <util/piped_process.h>
 
#include <solvers/smt2_incremental/ast/smt_responses.h>
 
#include <memory>
#include <sstream>
#include <string>
 
class smt_base_solver_processt
{
public:
  virtual const std::string &description() = 0;

  virtual void send(const smt_commandt &command) = 0;
 
  virtual smt_responset
  receive_response(const std::unordered_map<irep_idt, smt_identifier_termt>
                     &identifier_table) = 0;
 
  virtual ~smt_base_solver_processt() = default;
};
 
class smt_piped_solver_processt : public smt_base_solver_processt
{
public:
  smt_piped_solver_processt(
    std::string command_line,
    message_handlert &message_handler,
    std::unique_ptr<std::ostream> out_stream);
 
  const std::string &description() override;
 
  void send(const smt_commandt &smt_command) override;
 
  smt_responset receive_response(
    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
    override;
 
  ~smt_piped_solver_processt() override = default;
 
protected:
  std::string command_line_description;
  std::unique_ptr<std::ostream> out_stream;
  piped_processt process;
  std::stringstream response_stream;
  messaget log;
};

class smt_incremental_dry_run_solvert : public smt_base_solver_processt
{
public:
  smt_incremental_dry_run_solvert(
    message_handlert &message_handler,
    std::ostream &out_stream,
    std::unique_ptr<std::ostream> file_stream);
 
  const std::string &description() override;
 
  void send(const smt_commandt &smt_command) override;

  smt_responset receive_response(
    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
    override;
 
  ~smt_incremental_dry_run_solvert() override = default;
 
protected:
  std::unique_ptr<std::ostream> file_stream;
  std::ostream &out_stream;
  messaget log;

  const std::string desc = "SMT2 incremental dry-run";
};
 
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H