smt_bit_vector_theory.cpp File Reference

#include "smt_bit_vector_theory.h"
#include <util/invariant.h>

Include dependency graph for smt_bit_vector_theory.cpp:

Go to the source code of this file.

Functions
static void	validate_bit_vector_sort (const std::string &descriptor, const smt_termt &operand)
static void	validate_bit_vector_sort (const smt_termt &operand)
static void	validate_bit_vector_sorts (const smt_termt &lhs, const smt_termt &rhs)
static void	validate_matched_bit_vector_sorts (const smt_termt &left, const smt_termt &right)

Function Documentation

validate_bit_vector_sort() [1/2]

static void validate_bit_vector_sort ( const smt_termt &  operand )

static

Definition at line 32 of file smt_bit_vector_theory.cpp.

validate_bit_vector_sort() [2/2]

static void validate_bit_vector_sort ( const std::string &  descriptor, const smt_termt &  operand  )

static

Definition at line 22 of file smt_bit_vector_theory.cpp.

validate_bit_vector_sorts()

static void validate_bit_vector_sorts ( const smt_termt &  lhs, const smt_termt &  rhs  )

static

Definition at line 38 of file smt_bit_vector_theory.cpp.

validate_matched_bit_vector_sorts()

static void validate_matched_bit_vector_sorts ( const smt_termt &  left, const smt_termt &  right  )

static

Definition at line 86 of file smt_bit_vector_theory.cpp.