CBMC
Macros | Functions
smt2_conv.cpp File Reference

SMT Backend. More...

#include "smt2_conv.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/fixedbv.h>
#include <util/floatbv_expr.h>
#include <util/format_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/mathematical_expr.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <util/string_constant.h>
#include <util/threeval.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/flattening/c_bit_field_replacement_type.h>
#include <solvers/floatbv/float_bv.h>
#include <solvers/prop/literal_expr.h>
#include "smt2_tokenizer.h"
#include <cstdint>
+ 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 883 of file smt2_conv.cpp.

◆ is_smt2_simple_identifier()

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

Definition at line 1000 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.