cprover
smt2_convt Class Reference

#include <smt2_conv.h>

+ Inheritance diagram for smt2_convt:
+ Collaboration diagram for smt2_convt:

Classes

struct  identifiert
 
class  smt2_symbolt
 

Public Types

enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3,
  solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3
}
 
- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 Result of running the decision procedure. More...
 

Public Member Functions

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

Public Attributes

bool use_FPA_theory
 
bool use_datatypes
 
bool use_array_of_bool
 
bool emit_set_logic
 

Protected Types

enum  wheret { wheret::BEGIN, wheret::END }
 
typedef std::unordered_map< irep_idt, identifiertidentifier_mapt
 
typedef std::map< typet, std::string > datatype_mapt
 
typedef std::map< exprt, irep_idtdefined_expressionst
 
typedef std::set< std::string > smt2_identifierst
 

Protected Member Functions

resultt dec_solve () override
 Run the decision procedure to solve the problem. More...
 
void write_header ()
 
void write_footer (std::ostream &)
 
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_mod (const 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)
 
std::string convert_identifier (const irep_idt &identifier)
 
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)
 
exprt parse_rec (const irept &s, const typet &type)
 
void convert_floatbv (const exprt &expr)
 
std::string type2id (const typet &) const
 
std::string floatbv_suffix (const exprt &) const
 
const smt2_symboltto_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 exprt &expr)
 

Protected Attributes

const namespacetns
 
std::ostream & out
 
std::string benchmark
 
std::string notes
 
std::string logic
 
solvert solver
 
std::vector< exprtassumptions
 
boolbv_widtht boolbv_width
 
std::size_t number_of_solver_calls = 0
 
letifyt letify
 
std::set< irep_idtbvfp_set
 
pointer_logict pointer_logic
 
identifier_mapt identifier_map
 
datatype_mapt datatype_map
 
defined_expressionst defined_expressions
 
defined_expressionst object_sizes
 
smt2_identifierst smt2_identifiers
 
std::size_t no_boolean_variables
 
std::vector< bool > boolean_assignment
 

Detailed Description

Definition at line 34 of file smt2_conv.h.

Member Typedef Documentation

◆ datatype_mapt

typedef std::map<typet, std::string> smt2_convt::datatype_mapt
protected

Definition at line 211 of file smt2_conv.h.

◆ defined_expressionst

typedef std::map<exprt, irep_idt> smt2_convt::defined_expressionst
protected

Definition at line 220 of file smt2_conv.h.

◆ identifier_mapt

typedef std::unordered_map<irep_idt, identifiert> smt2_convt::identifier_mapt
protected

Definition at line 205 of file smt2_conv.h.

◆ smt2_identifierst

typedef std::set<std::string> smt2_convt::smt2_identifierst
protected

Definition at line 225 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

enum smt2_convt::solvert
strong
Enumerator
GENERIC 
BOOLECTOR 
CPROVER_SMT2 
CVC3 
CVC4 
MATHSAT 
YICES 
Z3 

Definition at line 37 of file smt2_conv.h.

◆ wheret

enum smt2_convt::wheret
strongprotected
Enumerator
BEGIN 
END 

Definition at line 180 of file smt2_conv.h.

Constructor & Destructor Documentation

◆ smt2_convt()

smt2_convt::smt2_convt ( const namespacet _ns,
const std::string &  _benchmark,
const std::string &  _notes,
const std::string &  _logic,
solvert  _solver,
std::ostream &  _out 
)

Definition at line 46 of file smt2_conv.cpp.

◆ ~smt2_convt()

smt2_convt::~smt2_convt ( )
overridedefault

Member Function Documentation

◆ convert()

literalt smt2_convt::convert ( const exprt expr)
protected

Definition at line 698 of file smt2_conv.cpp.

◆ convert_address_of_rec()

void smt2_convt::convert_address_of_rec ( const exprt expr,
const pointer_typet result_type 
)
protected

Definition at line 606 of file smt2_conv.cpp.

◆ convert_constant()

void smt2_convt::convert_constant ( const constant_exprt expr)
protected

Definition at line 2762 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt expr)
protected

Definition at line 3367 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt expr)
protected

Definition at line 885 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt expr)
protected

Definition at line 851 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt expr)
protected

Definition at line 3411 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt expr)
protected

Definition at line 3347 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt expr)
protected

Definition at line 3506 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt expr)
protected

Definition at line 3211 of file smt2_conv.cpp.

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt expr)
protected

Definition at line 2488 of file smt2_conv.cpp.

◆ convert_identifier()

std::string smt2_convt::convert_identifier ( const irep_idt identifier)
protected

Definition at line 776 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt expr)
protected

Definition at line 3780 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const unary_exprt expr)
protected

Definition at line 2912 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt  l)
protected

Definition at line 739 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt expr)
protected

Definition at line 3878 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt expr)
protected

Definition at line 3250 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt expr)
protected

Definition at line 2893 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt expr)
protected

Definition at line 3431 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt expr)
protected

Definition at line 3032 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const binary_relation_exprt expr)
protected

Definition at line 2949 of file smt2_conv.cpp.

◆ convert_rounding_mode_FPA()

void smt2_convt::convert_rounding_mode_FPA ( const exprt expr)
protected

Converting a constant or symbolic rounding mode to SMT-LIB.

Only called when use_FPA_theory is enabled

parameters: The expression representing the rounding mode.
Returns
SMT-LIB output to out.

Definition at line 3154 of file smt2_conv.cpp.

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt expr)
protected

Definition at line 2634 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet type)
protected

Definition at line 4502 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt expr)
protected

Definition at line 1955 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt expr)
protected

Definition at line 2729 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const exprt expr)
protected

Definition at line 3773 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt expr)
protected

Definition at line 3526 of file smt2_conv.cpp.

◆ dec_solve()

decision_proceduret::resultt smt2_convt::dec_solve ( )
overrideprotectedvirtual

Run the decision procedure to solve the problem.

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 242 of file smt2_conv.cpp.

◆ decision_procedure_text()

std::string smt2_convt::decision_procedure_text ( ) const
overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 105 of file smt2_conv.cpp.

◆ define_object_size()

void smt2_convt::define_object_size ( const irep_idt id,
const exprt expr 
)
protected

Definition at line 204 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt expr)
protected

Definition at line 4271 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet type)
protected

Definition at line 4637 of file smt2_conv.cpp.

◆ find_symbols_rec()

void smt2_convt::find_symbols_rec ( const typet type,
std::set< irep_idt > &  recstack 
)
protected

Definition at line 4643 of file smt2_conv.cpp.

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt expr)
protected

Definition at line 3939 of file smt2_conv.cpp.

◆ flatten_array()

void smt2_convt::flatten_array ( const exprt expr)
protected

produce a flat bit-vector for a given array of fixed size

Definition at line 2698 of file smt2_conv.cpp.

◆ floatbv_suffix()

std::string smt2_convt::floatbv_suffix ( const exprt expr) const
protected

Definition at line 844 of file smt2_conv.cpp.

◆ get()

exprt smt2_convt::get ( const exprt expr) const
overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Definition at line 249 of file smt2_conv.cpp.

◆ get_number_of_solver_calls()

std::size_t smt2_convt::get_number_of_solver_calls ( ) const
overridevirtual

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 4847 of file smt2_conv.cpp.

◆ handle()

exprt smt2_convt::handle ( const exprt expr)
overridevirtual

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.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 730 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt  l) const
protected

Definition at line 120 of file smt2_conv.cpp.

◆ lower_byte_operators()

exprt smt2_convt::lower_byte_operators ( const exprt expr)
protected

Lower byte_update and byte_extract operations within expr.

Return an equivalent expression that doesn't use byte operators. Note this replaces operators post-order (compare lower_byte_operators, which uses a pre-order walk, replacing in child expressions before the parent). Pre-order replacement currently fails regression tests: see https://github.com/diffblue/cbmc/issues/4380

Definition at line 4224 of file smt2_conv.cpp.

◆ parse_array()

exprt smt2_convt::parse_array ( const irept s,
const array_typet type 
)
protected

Definition at line 437 of file smt2_conv.cpp.

◆ parse_literal()

constant_exprt smt2_convt::parse_literal ( const irept src,
const typet type 
)
protected

Definition at line 299 of file smt2_conv.cpp.

◆ parse_rec()

exprt smt2_convt::parse_rec ( const irept s,
const typet type 
)
protected

Definition at line 542 of file smt2_conv.cpp.

◆ parse_struct()

struct_exprt smt2_convt::parse_struct ( const irept s,
const struct_typet type 
)
protected

Definition at line 483 of file smt2_conv.cpp.

◆ parse_union()

exprt smt2_convt::parse_union ( const irept s,
const union_typet type 
)
protected

Definition at line 467 of file smt2_conv.cpp.

◆ pop()

void smt2_convt::pop ( )
overridevirtual

Currently, only implements a single stack element (no nested contexts)

Implements stack_decision_proceduret.

Definition at line 771 of file smt2_conv.cpp.

◆ prepare_for_convert_expr()

exprt smt2_convt::prepare_for_convert_expr ( const exprt expr)
protected

Perform steps necessary before an expression is passed to convert_expr.

  1. Replace byte operators (byte_extract, _update) with equivalent expressions
  2. Call find_symbols to create auxiliary symbols, e.g. for array expressions.
    Parameters
    exprexpression to prepare
    Returns
    equivalent expression suitable for convert_expr.

Definition at line 4256 of file smt2_conv.cpp.

◆ print_assignment()

void smt2_convt::print_assignment ( std::ostream &  out) const
overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 110 of file smt2_conv.cpp.

◆ push() [1/2]

void smt2_convt::push ( )
overridevirtual

Unimplemented.

Implements stack_decision_proceduret.

Definition at line 759 of file smt2_conv.cpp.

◆ push() [2/2]

void smt2_convt::push ( const std::vector< exprt > &  _assumptions)
overridevirtual

Currently, only implements a single stack element (no nested contexts)

Implements stack_decision_proceduret.

Definition at line 764 of file smt2_conv.cpp.

◆ set_to()

void smt2_convt::set_to ( const exprt expr,
bool  value 
)
overridevirtual

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

Implements decision_proceduret.

Definition at line 4132 of file smt2_conv.cpp.

◆ to_smt2_symbol()

const smt2_symbolt& smt2_convt::to_smt2_symbol ( const exprt expr)
inlineprotected

Definition at line 170 of file smt2_conv.h.

◆ type2id()

std::string smt2_convt::type2id ( const typet type) const
protected

Definition at line 807 of file smt2_conv.cpp.

◆ unflatten()

void smt2_convt::unflatten ( wheret  where,
const typet type,
unsigned  nesting = 0 
)
protected

Definition at line 4028 of file smt2_conv.cpp.

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt expr)
protected

Definition at line 4481 of file smt2_conv.cpp.

◆ write_footer()

void smt2_convt::write_footer ( std::ostream &  os)
protected

Definition at line 163 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )
protected

Definition at line 133 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

std::vector<exprt> smt2_convt::assumptions
protected

Definition at line 87 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark
protected

Definition at line 84 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width
protected

Definition at line 88 of file smt2_conv.h.

◆ boolean_assignment

std::vector<bool> smt2_convt::boolean_assignment
protected

Definition at line 230 of file smt2_conv.h.

◆ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set
protected

Definition at line 155 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map
protected

Definition at line 212 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions
protected

Definition at line 221 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 62 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map
protected

Definition at line 207 of file smt2_conv.h.

◆ letify

letifyt smt2_convt::letify
protected

Definition at line 142 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic
protected

Definition at line 84 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables
protected

Definition at line 229 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes
protected

Definition at line 84 of file smt2_conv.h.

◆ ns

const namespacet& smt2_convt::ns
protected

Definition at line 82 of file smt2_conv.h.

◆ number_of_solver_calls

std::size_t smt2_convt::number_of_solver_calls = 0
protected

Definition at line 90 of file smt2_conv.h.

◆ object_sizes

defined_expressionst smt2_convt::object_sizes
protected

Definition at line 223 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out
protected

Definition at line 83 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic
protected

Definition at line 185 of file smt2_conv.h.

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers
protected

Definition at line 226 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver
protected

Definition at line 85 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 61 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 60 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 59 of file smt2_conv.h.


The documentation for this class was generated from the following files: