#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/lowering/expr_lowering.h>
#include <solvers/prop/literal_expr.h>
#include "smt2_tokenizer.h"

Include dependency graph for smt2_conv.cpp:

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

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

Functions
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 53 of file smt2_conv.cpp.

◆ UNEXPECTEDCASE

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

Definition at line 50 of file smt2_conv.cpp.

Function Documentation

◆ has_quantifier()

static bool has_quantifier ( const exprt & expr )

static

Definition at line 794 of file smt2_conv.cpp.

◆ is_smt2_simple_identifier()

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