smt_core_theoryt::if_then_elset Struct Reference

#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:

• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_core_theory.h
• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_core_theory.cpp