CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | List of all members
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.
 
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)
 
- 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 ()
 

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.
 
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)
 
- 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
 

Detailed Description

Definition at line 73 of file state_encoding_targets.h.

Constructor & Destructor Documentation

◆ state_encoding_smt2_convt()

state_encoding_smt2_convt::state_encoding_smt2_convt ( const namespacet &  ns,
std::ostream &  _out 
)
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: