state_encoding_smt2_convt Class Reference
#include <state_encoding_targets.h>
Inheritance diagram for state_encoding_smt2_convt: Collaboration diagram for state_encoding_smt2_convt:Public Member Functions | |
| state_encoding_smt2_convt (const namespacet &ns, std::ostream &_out) | |
| void | add_converters () |
| Public Member Functions inherited from smt2_convt | |
| 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. More... | |
| 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'. More... | |
| exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
| std::string | decision_procedure_text () const override |
| Return a textual description of the decision procedure. More... | |
| void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out. More... | |
| void | push () override |
| Unimplemented. More... | |
| void | push (const std::vector< exprt > &_assumptions) override |
| Currently, only implements a single stack element (no nested contexts) More... | |
| void | pop () override |
| Currently, only implements a single stack element (no nested contexts) More... | |
| std::size_t | get_number_of_solver_calls () const override |
| Return the number of incremental solver calls. More... | |
| 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'. More... | |
| void | set_to_false (const exprt &) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More... | |
| resultt | operator() (const exprt &assumption) |
| Run the decision procedure to solve the problem under the given assumption. More... | |
| virtual | ~decision_proceduret () |
Additional Inherited Members | |
| Public Types inherited from smt2_convt | |
| enum class | solvert { GENERIC , BITWUZLA , BOOLECTOR , CPROVER_SMT2 , CVC3 , CVC4 , CVC5 , MATHSAT , YICES , Z3 } |
| Public Types inherited from decision_proceduret | |
| enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
| Result of running the decision procedure. More... | |
| Static Public Member Functions inherited from smt2_convt | |
| static std::string | convert_identifier (const irep_idt &identifier) |
| Public Attributes inherited from smt2_convt | |
| bool | use_FPA_theory |
| bool | use_array_of_bool |
| bool | use_as_const |
| bool | use_check_sat_assuming |
| bool | use_datatypes |
| bool | use_lambda_for_array |
| bool | emit_set_logic |
| Protected Types inherited from smt2_convt | |
| enum class | wheret { BEGIN , END } |
| using | converterst = std::unordered_map< irep_idt, std::function< void(const exprt &)>, irep_id_hash > |
| typedef std::unordered_map< irep_idt, identifiert > | identifier_mapt |
| typedef std::map< typet, std::string > | datatype_mapt |
| typedef std::map< exprt, irep_idt > | defined_expressionst |
| typedef std::set< std::string > | smt2_identifierst |
| Protected Member Functions inherited from smt2_convt | |
| resultt | dec_solve (const exprt &) override |
| Implementation of the decision procedure. More... | |
| void | write_header () |
| void | write_footer () |
Writes the end of the SMT file to the smt_convt::out stream. More... | |
| bool | use_array_theory (const exprt &) |
| void | flatten_array (const exprt &) |
| produce a flat bit-vector for a given array of fixed size More... | |
| 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. More... | |
| 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_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. More... | |
| exprt | lower_byte_operators (const exprt &expr) |
Lower byte_update and byte_extract operations within expr. More... | |
| void | find_symbols (const exprt &expr) |
| 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. More... | |
| 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. More... | |
| 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) |
| 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. More... | |
| std::map< object_size_exprt, irep_idt > | object_sizes |
| smt2_identifierst | smt2_identifiers |
| std::size_t | no_boolean_variables |
| std::vector< bool > | boolean_assignment |
Detailed Description
Definition at line 73 of file state_encoding_targets.h.
Constructor & Destructor Documentation
◆ state_encoding_smt2_convt()
|
inline |
Definition at line 76 of file state_encoding_targets.h.
Member Function Documentation
◆ add_converters()
| void state_encoding_smt2_convt::add_converters | ( | ) |
Definition at line 25 of file state_encoding_targets.cpp.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/cprover/state_encoding_targets.h
- /home/runner/work/cbmc/cbmc/src/cprover/state_encoding_targets.cpp
