CBMC
Loading...
Searching...
No Matches
Classes | Static Public Attributes | List of all members
smt_core_theoryt Class Reference

#include <smt_core_theory.h>

+ Collaboration diagram for smt_core_theoryt:

Classes

struct  andt
 
struct  distinctt
 
struct  equalt
 
struct  if_then_elset
 
struct  impliest
 
struct  nott
 
struct  ort
 
struct  xort
 

Static Public Attributes

static const smt_function_application_termt::factoryt< nott > make_not {}
 
static const smt_function_application_termt::factoryt< impliest > implies {}
 
static const smt_function_application_termt::factoryt< andt > make_and {}
 
static const smt_function_application_termt::factoryt< ort > make_or {}
 
static const smt_function_application_termt::factoryt< xort > make_xor {}
 
static const smt_function_application_termt::factoryt< equalt > equal {}
 
static const smt_function_application_termt::factoryt< distinctt > distinct {}
 Makes applications of the function which returns true iff its two arguments are not identical.
 
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
 

Detailed Description

Definition at line 8 of file smt_core_theory.h.

Member Data Documentation

◆ distinct

const smt_function_application_termt::factoryt< smt_core_theoryt::distinctt > smt_core_theoryt::distinct {}
static

Makes applications of the function which returns true iff its two arguments are not identical.

Definition at line 171 of file smt_core_theory.h.

◆ equal

const smt_function_application_termt::factoryt< smt_core_theoryt::equalt > smt_core_theoryt::equal {}
static

Definition at line 148 of file smt_core_theory.h.

◆ if_then_else

const smt_function_application_termt::factoryt< smt_core_theoryt::if_then_elset > smt_core_theoryt::if_then_else
static

Definition at line 82 of file smt_core_theory.h.

◆ implies

const smt_function_application_termt::factoryt< smt_core_theoryt::impliest > smt_core_theoryt::implies {}
static

Definition at line 49 of file smt_core_theory.h.

◆ make_and

const smt_function_application_termt::factoryt< smt_core_theoryt::andt > smt_core_theoryt::make_and {}
static

Definition at line 75 of file smt_core_theory.h.

◆ make_not

const smt_function_application_termt::factoryt< smt_core_theoryt::nott > smt_core_theoryt::make_not {}
static

Definition at line 23 of file smt_core_theory.h.

◆ make_or

const smt_function_application_termt::factoryt< smt_core_theoryt::ort > smt_core_theoryt::make_or {}
static

Definition at line 99 of file smt_core_theory.h.

◆ make_xor

const smt_function_application_termt::factoryt< smt_core_theoryt::xort > smt_core_theoryt::make_xor {}
static

Definition at line 125 of file smt_core_theory.h.

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