cprover
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_thantunsigned_less_than {}
 
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equaltunsigned_less_than_or_equal {}
 
static const smt_function_application_termt::factoryt< unsigned_greater_thantunsigned_greater_than {}
 
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equaltunsigned_greater_than_or_equal {}
 
static const smt_function_application_termt::factoryt< signed_less_thantsigned_less_than {}
 
static const smt_function_application_termt::factoryt< signed_less_than_or_equaltsigned_less_than_or_equal {}
 
static const smt_function_application_termt::factoryt< signed_greater_thantsigned_greater_than {}
 
static const smt_function_application_termt::factoryt< signed_greater_than_or_equaltsigned_greater_than_or_equal {}
 
static const smt_function_application_termt::factoryt< addtadd {}
 
static const smt_function_application_termt::factoryt< subtracttsubtract {}
 
static const smt_function_application_termt::factoryt< multiplytmultiply {}
 
static const smt_function_application_termt::factoryt< unsigned_dividetunsigned_divide {}
 
static const smt_function_application_termt::factoryt< signed_dividetsigned_divide {}
 
static const smt_function_application_termt::factoryt< unsigned_remaindertunsigned_remainder {}
 
static const smt_function_application_termt::factoryt< signed_remaindertsigned_remainder {}
 
static const smt_function_application_termt::factoryt< negatetnegate {}
 

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: