inductiveness_resultt Class Reference

#include <inductiveness.h>

Public Types
enum	outcomet { INDUCTIVE , BASE_CASE_FAIL , STEP_CASE_FAIL }

Static Public Member Functions
static inductiveness_resultt	inductive ()
static inductiveness_resultt	base_case_fail (workt refuted)
static inductiveness_resultt	step_case_fail (workt dropped)

Public Attributes
enum inductiveness_resultt::outcomet	outcome
std::optional< workt >	work

Private Member Functions
	inductiveness_resultt (outcomet __outcome)

Detailed Description

Definition at line 19 of file inductiveness.h.

Member Enumeration Documentation

outcomet

enum inductiveness_resultt::outcomet

Enumerator
INDUCTIVE
BASE_CASE_FAIL
STEP_CASE_FAIL

Definition at line 22 of file inductiveness.h.

Constructor & Destructor Documentation

inductiveness_resultt()

inductiveness_resultt::inductiveness_resultt ( outcomet  __outcome )

inlineexplicitprivate

Definition at line 51 of file inductiveness.h.

Member Function Documentation

base_case_fail()

static inductiveness_resultt inductiveness_resultt::base_case_fail ( workt  refuted )

inlinestatic

Definition at line 34 of file inductiveness.h.

inductive()

static inductiveness_resultt inductiveness_resultt::inductive ( )

inlinestatic

Definition at line 29 of file inductiveness.h.

step_case_fail()

static inductiveness_resultt inductiveness_resultt::step_case_fail ( workt  dropped )

inlinestatic

Definition at line 41 of file inductiveness.h.

Member Data Documentation

outcome

enum inductiveness_resultt::outcomet inductiveness_resultt::outcome

work

std::optional<workt> inductiveness_resultt::work

Definition at line 48 of file inductiveness.h.

---

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

• /home/runner/work/cbmc/cbmc/src/cprover/inductiveness.h