Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void set_to (const exprt &expr, bool value) override

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

exprt get (const exprt &expr) const override

Return expr with variables replaced by values from satisfying assignment if available.

void print_assignment (std::ostream &out) const override

Print satisfying assignment to out.

void push () override

Unimplemented.

void push (const std::vector< exprt > &_assumptions) override

Currently, only implements a single stack element (no nested contexts)

void pop () override

Currently, only implements a single stack element (no nested contexts)

std::size_t get_number_of_solver_calls () const override

Return the number of incremental solver calls.

void set_converter (irep_idt id, std::function< void(const exprt &)> converter)

- Public Member Functions inherited from stack_decision_proceduret

virtual ~stack_decision_proceduret ()=default

- Public Member Functions inherited from decision_proceduret

void set_to_true (const exprt &)

For a Boolean expression expr, add the constraint 'expr'.

void set_to_false (const exprt &)

For a Boolean expression expr, add the constraint 'not expr'.

resultt operator() ()

Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt operator() (const exprt &assumption)

Run the decision procedure to solve the problem under the given assumption.

virtual ~decision_proceduret ()

Protected Member Functions

resultt dec_solve (const exprt &) override

Implementation of the decision procedure.

resultt read_result (std::istream &in)

- Protected Member Functions inherited from smt2_convt

void write_header ()

void write_footer ()

Writes the end of the SMT file to the smt_convt::out stream.

bool use_array_theory (const exprt &)

void flatten_array (const exprt &)

produce a flat bit-vector for a given array of fixed size

void convert_typecast (const typecast_exprt &expr)

void convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

void convert_struct (const struct_exprt &expr)

void convert_union (const union_exprt &expr)

void convert_constant (const constant_exprt &expr)

void convert_relation (const binary_relation_exprt &)

void convert_is_dynamic_object (const unary_exprt &)

void convert_plus (const plus_exprt &expr)

void convert_minus (const minus_exprt &expr)

void convert_div (const div_exprt &expr)

void convert_mult (const mult_exprt &expr)

void convert_rounding_mode_FPA (const exprt &expr)

Converting a constant or symbolic rounding mode to SMT-LIB.

void convert_floatbv_plus (const ieee_float_op_exprt &expr)

void convert_floatbv_minus (const ieee_float_op_exprt &expr)

void convert_floatbv_div (const ieee_float_op_exprt &expr)

void convert_floatbv_mult (const ieee_float_op_exprt &expr)

void convert_floatbv_rem (const binary_exprt &expr)

void convert_floatbv_fma (const floatbv_fma_exprt &expr)

void convert_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)

void convert_mod (const mod_exprt &expr)

void convert_euclidean_mod (const euclidean_mod_exprt &expr)

void convert_index (const index_exprt &expr)

void convert_member (const member_exprt &expr)

void convert_with (const with_exprt &expr)

void convert_update (const update_exprt &)

void convert_update_bit (const update_bit_exprt &)

void convert_update_bits (const update_bits_exprt &)

void convert_expr (const exprt &)

void convert_type (const typet &)

void convert_literal (const literalt)

void convert_string_literal (const std::string &)

literalt convert (const exprt &expr)

tvt l_get (literalt l) const

exprt prepare_for_convert_expr (const exprt &expr)

Perform steps necessary before an expression is passed to convert_expr.

exprt lower_byte_operators (const exprt &expr)

Lower byte_update and byte_extract operations within expr.

void find_symbols (const exprt &expr)

Find and declare symbols used in an expression This function traverses the expression tree and creates SMT2 declarations for all symbols (variables) found.

void find_symbols (const typet &type)

void find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)

constant_exprt parse_literal (const irept &, const typet &type)

struct_exprt parse_struct (const irept &s, const struct_typet &type)

exprt parse_union (const irept &s, const union_typet &type)

exprt parse_array (const irept &s, const array_typet &type)

This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array object.

exprt parse_rec (const irept &s, const typet &type)

void walk_array_tree (std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)

This function walks the SMT output and populates a map with index/value pairs for the array.

void convert_floatbv (const exprt &expr)

std::string type2id (const typet &) const

std::string floatbv_suffix (const exprt &) const

const smt2_symbolt & to_smt2_symbol (const exprt &expr)

void flatten2bv (const exprt &)

void unflatten (wheret, const typet &, unsigned nesting=0)

void convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)

void define_object_size (const irep_idt &id, const object_size_exprt &expr)

smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)

~smt2_convt () override=default

exprt handle (const exprt &expr) override

Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void set_to (const exprt &expr, bool value) override

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

exprt get (const exprt &expr) const override

Return expr with variables replaced by values from satisfying assignment if available.

void print_assignment (std::ostream &out) const override

Print satisfying assignment to out.

void push () override

Unimplemented.

void push (const std::vector< exprt > &_assumptions) override

Currently, only implements a single stack element (no nested contexts)

void pop () override

Currently, only implements a single stack element (no nested contexts)

std::size_t get_number_of_solver_calls () const override

Return the number of incremental solver calls.

void set_converter (irep_idt id, std::function< void(const exprt &)> converter)

- Protected Member Functions inherited from stack_decision_proceduret

virtual ~stack_decision_proceduret ()=default

void set_to_true (const exprt &)

For a Boolean expression expr, add the constraint 'expr'.

void set_to_false (const exprt &)

For a Boolean expression expr, add the constraint 'not expr'.

resultt operator() ()

Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt operator() (const exprt &assumption)

Run the decision procedure to solve the problem under the given assumption.

virtual ~decision_proceduret ()

Protected Attributes

std::string solver_binary_or_empty

message_handlert & message_handler

std::stringstream cached_output

Everything except the footer is cached, so that output files can be rewritten with varying footers.

- Protected Attributes inherited from smt2_stringstreamt

std::stringstream stringstream

- Protected Attributes inherited from smt2_convt

const namespacet & ns

std::ostream & out

std::string benchmark

std::string notes

std::string logic

solvert solver

converterst converters

std::vector< literalt > assumptions

boolbv_widtht boolbv_width

std::size_t number_of_solver_calls = 0

letifyt letify

std::unordered_map< irep_idt, irept > current_bindings

std::set< irep_idt > bvfp_set

std::set< irep_idt > state_fkt_declared

pointer_logict pointer_logic

identifier_mapt identifier_map

datatype_mapt datatype_map

defined_expressionst defined_expressions

std::unordered_map< irep_idt, bool > set_values

The values which boolean identifiers have been smt2_convt::set_to or in other words those which are asserted as true / false in the output smt2 formula.

std::map< object_size_exprt, irep_idt > object_sizes

smt2_identifierst smt2_identifiers

std::size_t no_boolean_variables

std::vector< bool > boolean_assignment

bool use_FPA_theory = false

bool use_array_of_bool = false

bool use_as_const = false

bool use_check_sat_assuming = false

bool use_datatypes = false

bool use_lambda_for_array = false

bool emit_set_logic = true