smt2_dect Class Reference
Decision procedure interface for various SMT 2.x solvers. More...
#include <smt2_dec.h>
Inheritance diagram for smt2_dect: Collaboration diagram for smt2_dect:Public Member Functions | |
| smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, message_handlert &_message_handler) | |
| resultt | dec_solve () override |
| Run the decision procedure to solve the problem. More... | |
| std::string | decision_procedure_text () const override |
| Return a textual description of the decision procedure. More... | |
| 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... | |
| 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... | |
| 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 &expr) |
For a Boolean expression expr, add the constraint 'expr'. More... | |
| void | set_to_false (const exprt &expr) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem. More... | |
| virtual | ~decision_proceduret () |
Protected Member Functions | |
| 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. 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 exprt &expr) |
| void | convert_expr (const exprt &) |
| void | convert_type (const typet &) |
| void | convert_literal (const literalt) |
| 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) |
| 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... | |
| 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... | |
| Protected Member Functions inherited from stack_decision_proceduret | |
| virtual | ~stack_decision_proceduret ()=default |
| void | set_to_true (const exprt &expr) |
For a Boolean expression expr, add the constraint 'expr'. More... | |
| void | set_to_false (const exprt &expr) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem. More... | |
| virtual | ~decision_proceduret () |
Protected Attributes | |
| message_handlert & | message_handler |
| std::stringstream | cached_output |
| Everything except the footer is cached, so that output files can be rewritten with varying footers. More... | |
| 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 |
| std::vector< exprt > | assumptions |
| boolbv_widtht | boolbv_width |
| std::size_t | number_of_solver_calls = 0 |
| letifyt | letify |
| std::set< irep_idt > | bvfp_set |
| 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 |
| 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 |
Detailed Description
Decision procedure interface for various SMT 2.x solvers.
Definition at line 27 of file smt2_dec.h.
Constructor & Destructor Documentation
◆ smt2_dect()
|
inline |
Definition at line 30 of file smt2_dec.h.
Member Function Documentation
◆ dec_solve()
|
overridevirtual |
Run the decision procedure to solve the problem.
Reimplemented from smt2_convt.
Definition at line 34 of file smt2_dec.cpp.
◆ decision_procedure_text()
|
overridevirtual |
Return a textual description of the decision procedure.
Reimplemented from smt2_convt.
Definition at line 18 of file smt2_dec.cpp.
◆ read_result()
|
protected |
Definition at line 141 of file smt2_dec.cpp.
Member Data Documentation
◆ cached_output
|
protected |
Everything except the footer is cached, so that output files can be rewritten with varying footers.
Definition at line 50 of file smt2_dec.h.
◆ message_handler
|
protected |
Definition at line 46 of file smt2_dec.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2/smt2_dec.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2/smt2_dec.cpp
