cprover
Loading...
Searching...
No Matches
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< nottmake_not {}
static const smt_function_application_termt::factoryt< impliestimplies {}
static const smt_function_application_termt::factoryt< andtmake_and {}
static const smt_function_application_termt::factoryt< ortmake_or {}
static const smt_function_application_termt::factoryt< xortmake_xor {}
static const smt_function_application_termt::factoryt< equaltequal {}
static const smt_function_application_termt::factoryt< distincttdistinct {}
 Makes applications of the function which returns true iff its two arguments are not identical.
static const smt_function_application_termt::factoryt< if_then_elsetif_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: