cprover
Loading...
Searching...
No Matches
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 229 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 275 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 386 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 321 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 184 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 207 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 138 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 161 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 367 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 252 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 298 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 91 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 115 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 45 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 68 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 344 of file smt_bit_vector_theory.h.


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