CBMC
Static Public Member Functions | List of all members
smt_core_theoryt::if_then_elset Struct Referencefinal

#include <smt_core_theory.h>

Static Public Member Functions

static const char * identifier ()
 
static smt_sortt return_sort (const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
 
static void validate (const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
 

Detailed Description

Definition at line 69 of file smt_core_theory.h.

Member Function Documentation

◆ identifier()

const char * smt_core_theoryt::if_then_elset::identifier ( )
static

Definition at line 173 of file smt_core_theory.cpp.

◆ return_sort()

smt_sortt smt_core_theoryt::if_then_elset::return_sort ( const smt_termt &  condition,
const smt_termt &  then_term,
const smt_termt &  else_term 
)
static

Definition at line 178 of file smt_core_theory.cpp.

◆ validate()

void smt_core_theoryt::if_then_elset::validate ( const smt_termt &  condition,
const smt_termt &  then_term,
const smt_termt &  else_term 
)
static

Definition at line 186 of file smt_core_theory.cpp.

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