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) | |
| 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... | |
| 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 () |
Protected Member Functions | |
| resultt | dec_solve (const exprt &) override |
| Implementation of the decision procedure. More... | |
| 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 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) |
| 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... | |
| 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'. 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 |
| enum class | solvert { GENERIC , BITWUZLA , BOOLECTOR , CPROVER_SMT2 , CVC3 , CVC4 , CVC5 , MATHSAT , YICES , Z3 } |
| Protected Types inherited from decision_proceduret | |
| enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
| Result of running the decision procedure. More... | |
| Static Protected Member Functions inherited from smt2_convt | |
| static std::string | convert_identifier (const irep_idt &identifier) |
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()
|
overrideprotectedvirtual |
Implementation of the decision procedure.
Reimplemented from smt2_convt.
Definition at line 36 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 160 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 45 of file smt2_dec.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/smt2/smt2_dec.h
- /home/runner/work/cbmc/cbmc/src/solvers/smt2/smt2_dec.cpp
