3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
39 "The response_or_errort class must be in the valid state or error state, "
41 return smt.has_value() ? &
smt.value() :
nullptr;
50 "The response_or_errort class must be in the valid state or error state, "
Holds either a valid parsed response or response sub-tree of type.
const std::vector< std::string > * get_if_error() const
Gets the error messages if the response is invalid, or returns nullptr otherwise.
response_or_errort(std::string message)
response_or_errort(smtt smt)
std::vector< std::string > messages
const smtt * get_if_valid() const
Gets the smt response if the response is valid, or returns nullptr otherwise.
response_or_errort(std::vector< std::string > messages)
nonstd::optional< T > optionalt
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.