3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
21 template <
typename sub_
classt>
22 const sub_classt *
cast() const &;
46 template <
typename sub_
classt>
47 const sub_classt *
cast() const &;
55 template <typename derivedt>
120 std::vector<std::reference_wrapper<const valuation_pairt>> pairs()
const;
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept.
smt_check_sat_response_kindt()=delete
const sub_classt * cast() const &
friend smt_get_value_responset
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.
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)