CBMC
cegis_evaluatort Class Reference

Evaluator for checking if an expression is consistent with a given set of test cases (positive examples and negative examples). More...

#include <cegis_evaluator.h>

+ Collaboration diagram for cegis_evaluatort:

Public Member Functions

 cegis_evaluatort (const exprt &expr, const std::vector< cext > &cexs)
 
bool evaluate ()
 

Protected Member Functions

bool evaluate_rec_bool (const exprt &expr, const cext &cex, const bool is_positive)
 
mp_integer evaluate_rec_int (const exprt &expr, const cext &cex, const bool is_positive)
 

Protected Attributes

const exprtchecked_expr
 The expression being evaluated. More...
 
const std::vector< cext > & cexs
 The set of examples evaluated against. More...
 

Detailed Description

Evaluator for checking if an expression is consistent with a given set of test cases (positive examples and negative examples).

Definition at line 19 of file cegis_evaluator.h.

Constructor & Destructor Documentation

◆ cegis_evaluatort()

cegis_evaluatort::cegis_evaluatort ( const exprt expr,
const std::vector< cext > &  cexs 
)
inline

Definition at line 22 of file cegis_evaluator.h.

Member Function Documentation

◆ evaluate()

bool cegis_evaluatort::evaluate ( )

Definition at line 17 of file cegis_evaluator.cpp.

◆ evaluate_rec_bool()

bool cegis_evaluatort::evaluate_rec_bool ( const exprt expr,
const cext cex,
const bool  is_positive 
)
protected

Definition at line 35 of file cegis_evaluator.cpp.

◆ evaluate_rec_int()

mp_integer cegis_evaluatort::evaluate_rec_int ( const exprt expr,
const cext cex,
const bool  is_positive 
)
protected

Definition at line 149 of file cegis_evaluator.cpp.

Member Data Documentation

◆ cexs

const std::vector<cext>& cegis_evaluatort::cexs
protected

The set of examples evaluated against.

Definition at line 49 of file cegis_evaluator.h.

◆ checked_expr

const exprt& cegis_evaluatort::checked_expr
protected

The expression being evaluated.

Definition at line 47 of file cegis_evaluator.h.


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