Struct PropositionAnnotation

Struct Documentation

struct PropositionAnnotation

Public Functions

inline PropositionAnnotation(const bool polarity = true)
inline PropositionAnnotation(const StepAndBeforeOrAfter &propositionIsAvailableFrom, const map<StepAndBeforeOrAfter, bool> &propositionCanBeToggledFrom, const bool &polarity)

Full Constructor for a Proposition Annotation

@propositionIsAvailableFrom: which step the proposition is available from @availableBeforeOrAfter: PropositionAnnotation::AFTER if available from epsilon after that onwards, PropositionAnnotation::BEFORE otherwise @propositionCanBeToggledFrom: which step the proposition can be deleted from @deletableBeforeOrAfter: PropositionAnnotation::BEFORE if available from the moment the step starts onwards (e.g. an invariant finishes), PropositionAnnotation::AFTER otherwise (e.g. start/end precondition)

inline PropositionAnnotation(const unsigned int &stepID)

Lazy Constructor for a Proposition Annotation. Use for when a proposition has just been added. The resulting Proposition Annotation denotes that it is available from after the end of the specified step ID onwards, and can be deleted from the end of the specified stepID onwards.

@stepID uint denoting the step at which the proposition is added.

inline PropositionAnnotation(const StepAndBeforeOrAfter &sba)

Lazy Constructor for a Proposition Annotation. Use for when a proposition has just been added. The resulting Proposition Annotation denotes that it is available from after the end of the specified step ID onwards, and can be deleted from the end of the specified stepID onwards.

@stepID uint denoting the step at which the proposition is added.

inline void markAsDeleted(const StepAndBeforeOrAfter &step)
inline void markAsAdded(const StepAndBeforeOrAfter &step)
inline bool operator==(const PropositionAnnotation &other) const

Public Members

StepAndBeforeOrAfter negativeAvailableFrom
StepAndBeforeOrAfter availableFrom
map<StepAndBeforeOrAfter, bool> deletableFrom
map<StepAndBeforeOrAfter, bool> addableFrom
set<int> promisedDelete
set<int> promisedAdd