CBMC
smt2_conv.cpp File Reference

SMT Backend. More...

+ Include dependency graph for smt2_conv.cpp:

Go to the source code of this file.

Macros

#define UNEXPECTEDCASE(S)   PRECONDITION_WITH_DIAGNOSTICS(false, S);
 
#define SMT2_TODO(S)   PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
 

Functions

static bool is_zero_width (const typet &type, const namespacet &ns)
 Returns true iff type has effective width of zero bits. More...
 
static bool has_quantifier (const exprt &expr)
 
static bool is_smt2_simple_identifier (const std::string &identifier)
 

Detailed Description

SMT Backend.

Definition in file smt2_conv.cpp.

Macro Definition Documentation

◆ SMT2_TODO

#define SMT2_TODO (   S)    PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)

Definition at line 54 of file smt2_conv.cpp.

◆ UNEXPECTEDCASE

#define UNEXPECTEDCASE (   S)    PRECONDITION_WITH_DIAGNOSTICS(false, S);

Definition at line 51 of file smt2_conv.cpp.

Function Documentation

◆ has_quantifier()

static bool has_quantifier ( const exprt expr)
static

Definition at line 886 of file smt2_conv.cpp.

◆ is_smt2_simple_identifier()

static bool is_smt2_simple_identifier ( const std::string &  identifier)
static

Definition at line 1003 of file smt2_conv.cpp.

◆ is_zero_width()

static bool is_zero_width ( const typet type,
const namespacet ns 
)
static

Returns true iff type has effective width of zero bits.

Definition at line 257 of file smt2_conv.cpp.