cprover
Loading...
Searching...
No Matches
incremental_goto_checkert::resultt Struct Reference

#include <incremental_goto_checker.h>

Collaboration diagram for incremental_goto_checkert::resultt:

Public Types

enum class  progresst { FOUND_FAIL , DONE }

Public Member Functions

 resultt ()=delete
 resultt (progresst)

Public Attributes

progresst progress
std::unordered_set< irep_idt > updated_properties
 Changed properties since the last call to incremental_goto_checkert::operator().

Detailed Description

Definition at line 42 of file incremental_goto_checker.h.

Member Enumeration Documentation

◆ progresst

enum class incremental_goto_checkert::resultt::progresst
strong
Enumerator
FOUND_FAIL 

The goto checker may be able to find another FAILed property if operator() is called again.

DONE 

The goto checker has returned all results for the given set of properties.

Definition at line 44 of file incremental_goto_checker.h.

Constructor & Destructor Documentation

◆ resultt() [1/2]

incremental_goto_checkert::resultt::resultt ( )
delete

◆ resultt() [2/2]

incremental_goto_checkert::resultt::resultt ( resultt::progresst progress)
explicit

Definition at line 25 of file incremental_goto_checker.cpp.

Member Data Documentation

◆ progress

progresst incremental_goto_checkert::resultt::progress

Definition at line 54 of file incremental_goto_checker.h.

◆ updated_properties

std::unordered_set<irep_idt> incremental_goto_checkert::resultt::updated_properties

Changed properties since the last call to incremental_goto_checkert::operator().

Definition at line 61 of file incremental_goto_checker.h.

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