cprover
Classes | Static Public Attributes | List of all members
smt_bit_vector_theoryt Class Reference

#include <smt_bit_vector_theory.h>

+ Collaboration diagram for smt_bit_vector_theoryt:

Classes

struct  addt
 
struct  multiplyt
 
struct  negatet
 
struct  signed_dividet
 
struct  signed_greater_than_or_equalt
 
struct  signed_greater_thant
 
struct  signed_less_than_or_equalt
 
struct  signed_less_thant
 
struct  signed_remaindert
 
struct  subtractt
 
struct  unsigned_dividet
 
struct  unsigned_greater_than_or_equalt
 
struct  unsigned_greater_thant
 
struct  unsigned_less_than_or_equalt
 
struct  unsigned_less_thant
 
struct  unsigned_remaindert
 

Static Public Attributes

static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than {}
 
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal {}
 
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than {}
 
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal {}
 
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than {}
 
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal {}
 
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than {}
 
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal {}
 
static const smt_function_application_termt::factoryt< addt > add {}
 
static const smt_function_application_termt::factoryt< subtractt > subtract {}
 
static const smt_function_application_termt::factoryt< multiplyt > multiply {}
 
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide {}
 
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide {}
 
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder {}
 
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder {}
 
static const smt_function_application_termt::factoryt< negatet > negate {}
 

Detailed Description

Definition at line 8 of file smt_bit_vector_theory.h.

Member Data Documentation

◆ add

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::addt > smt_bit_vector_theoryt::add {}
static

Definition at line 94 of file smt_bit_vector_theory.h.

◆ multiply

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::multiplyt > smt_bit_vector_theoryt::multiply {}
static

Definition at line 110 of file smt_bit_vector_theory.h.

◆ negate

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::negatet > smt_bit_vector_theoryt::negate {}
static

Definition at line 154 of file smt_bit_vector_theory.h.

◆ signed_divide

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_dividet > smt_bit_vector_theoryt::signed_divide {}
static

Definition at line 128 of file smt_bit_vector_theory.h.

◆ signed_greater_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_thant > smt_bit_vector_theoryt::signed_greater_than {}
static

Definition at line 76 of file smt_bit_vector_theory.h.

◆ signed_greater_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_than_or_equalt > smt_bit_vector_theoryt::signed_greater_than_or_equal {}
static

Definition at line 86 of file smt_bit_vector_theory.h.

◆ signed_less_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_thant > smt_bit_vector_theoryt::signed_less_than {}
static

Definition at line 57 of file smt_bit_vector_theory.h.

◆ signed_less_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_than_or_equalt > smt_bit_vector_theoryt::signed_less_than_or_equal {}
static

Definition at line 67 of file smt_bit_vector_theory.h.

◆ signed_remainder

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_remaindert > smt_bit_vector_theoryt::signed_remainder {}
static

Definition at line 146 of file smt_bit_vector_theory.h.

◆ subtract

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::subtractt > smt_bit_vector_theoryt::subtract {}
static

Definition at line 102 of file smt_bit_vector_theory.h.

◆ unsigned_divide

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_dividet > smt_bit_vector_theoryt::unsigned_divide {}
static

Definition at line 119 of file smt_bit_vector_theory.h.

◆ unsigned_greater_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_thant > smt_bit_vector_theoryt::unsigned_greater_than {}
static

Definition at line 38 of file smt_bit_vector_theory.h.

◆ unsigned_greater_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_than_or_equalt > smt_bit_vector_theoryt::unsigned_greater_than_or_equal {}
static

Definition at line 48 of file smt_bit_vector_theory.h.

◆ unsigned_less_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_thant > smt_bit_vector_theoryt::unsigned_less_than {}
static

Definition at line 19 of file smt_bit_vector_theory.h.

◆ unsigned_less_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_than_or_equalt > smt_bit_vector_theoryt::unsigned_less_than_or_equal {}
static

Definition at line 29 of file smt_bit_vector_theory.h.

◆ unsigned_remainder

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_remaindert > smt_bit_vector_theoryt::unsigned_remainder {}
static

Definition at line 137 of file smt_bit_vector_theory.h.

The documentation for this class was generated from the following files: