|
| | state_encoding_smt2_convt (const namespacet &ns, std::ostream &_out) |
| |
| void | add_converters () |
| |
| | 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.
|
| |
| std::string | decision_procedure_text () const override |
| | Return a textual description of the decision procedure.
|
| |
| 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) |
| |
| 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 () |
| |
|
| enum class | solvert {
GENERIC
, BITWUZLA
, BOOLECTOR
, CPROVER_SMT2
,
CVC3
, CVC4
, CVC5
, MATHSAT
,
YICES
, Z3
} |
| |
| enum class | resultt { D_SATISFIABLE
, D_UNSATISFIABLE
, D_ERROR
} |
| | Result of running the decision procedure. More...
|
| |
| static std::string | convert_identifier (const irep_idt &identifier) |
| |
| 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 |
| |
| 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 |
| |
| resultt | dec_solve (const exprt &) override |
| | Implementation of the decision procedure.
|
| |
| 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_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) |
| |
| 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) |
| |
| 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 |
| |
Definition at line 73 of file state_encoding_targets.h.
Inheritance diagram for state_encoding_smt2_convt: