3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
22 template <
typename sub_
classt>
23 const sub_classt *
cast() const &;
47 template <
typename sub_
classt>
48 const sub_classt *
cast() const &;
56 template <typename derivedt>
121 std::vector<std::reference_wrapper<const valuation_pairt>>
pairs()
const;
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
irept(const irep_idt &_id)
Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept.
static irept upcast(smt_check_sat_response_kindt check_sat_response_kind)
static const smt_check_sat_response_kindt & downcast(const irept &)
irept(const irep_idt &_id)
smt_check_sat_response_kindt()=delete
const sub_classt * cast() const &
smt_check_sat_responset(smt_check_sat_response_kindt kind)
const smt_check_sat_response_kindt & kind() const
const irep_idt & message() const
smt_error_responset(irep_idt message)
const smt_termt & descriptor() const
const smt_termt & value() const
friend smt_get_value_responset
smt_get_value_responset(std::vector< valuation_pairt > pairs)
std::vector< std::reference_wrapper< const valuation_pairt > > pairs() const
irept(const irep_idt &_id)
bool operator!=(const smt_responset &) const
bool operator==(const smt_responset &) const
const sub_classt * cast() const &
Class for adding the ability to up and down cast smt_termt to and from irept.
smt_unsupported_responset()
bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)