smt2_conv.cpp File Reference

SMT Backend. More...

#include "smt2_conv.h"
#include <util/algebraic_number.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/rational.h>
#include <util/rational_tools.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.
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 57 of file smt2_conv.cpp.

UNEXPECTEDCASE

#define UNEXPECTEDCASE

(

S

)

PRECONDITION_WITH_DIAGNOSTICS(false, S);

Definition at line 54 of file smt2_conv.cpp.

Function Documentation

has_quantifier()

static bool has_quantifier ( const exprt &  expr )

static

Definition at line 972 of file smt2_conv.cpp.

is_smt2_simple_identifier()

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

static

Definition at line 1089 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 260 of file smt2_conv.cpp.