cprover
Loading...
Searching...
No Matches
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)
 
#define SMT2_TODO(S)
 

Functions

static bool is_zero_width (const typet &type, const namespacet &ns)
 Returns true iff type has effective width of zero bits.
 
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)
Value:
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464

Definition at line 54 of file smt2_conv.cpp.

◆ UNEXPECTEDCASE

#define UNEXPECTEDCASE ( S)
Value:

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.