Loading...

Searching...

No Matches

boolbv_quantifier.cpp File Reference

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/simplify_expr.h>
#include "boolbv.h"

+ Include dependency graph for boolbv_quantifier.cpp:

[フレーム]

Go to the source code of this file.

Functions

static bool expr_eq (const exprt &expr1, const exprt &expr2)

A method to detect equivalence between experts that can contain typecast.

static std::optional< constant_exprt > get_quantifier_var_min (const exprt &var_expr, const exprt &quantifier_expr)

To obtain the min value for the quantifier variable of the specified forall/exists operator.

static std::optional< constant_exprt > get_quantifier_var_max (const exprt &var_expr, const exprt &quantifier_expr)

To obtain the max value for the quantifier variable of the specified forall/exists operator.

static std::optional< exprt > eager_quantifier_instantiation (const quantifier_exprt &expr, const namespacet &ns)

Function Documentation

◆ eager_quantifier_instantiation()

static std::optional< exprt > eager_quantifier_instantiation ( const quantifier_exprt & expr,

const namespacet & ns

)

static

We need to rewrite the forall/exists quantifier into an OR/AND expr.

Definition at line 153 of file boolbv_quantifier.cpp.

◆ expr_eq()

static bool expr_eq ( const exprt & expr1,

const exprt & expr2

)

static

A method to detect equivalence between experts that can contain typecast.

Definition at line 18 of file boolbv_quantifier.cpp.

◆ get_quantifier_var_max()

static std::optional< constant_exprt > get_quantifier_var_max ( const exprt & var_expr,

const exprt & quantifier_expr

)

static

To obtain the max value for the quantifier variable of the specified forall/exists operator.

The max variable is in the form of "var_expr >= constant".

Due to the ''simplify'', the ''over_i'' value we obtain here is not the exact maximum index as specified in the original code.

Definition at line 79 of file boolbv_quantifier.cpp.

◆ get_quantifier_var_min()

static std::optional< constant_exprt > get_quantifier_var_min ( const exprt & var_expr,

const exprt & quantifier_expr

)

static

To obtain the min value for the quantifier variable of the specified forall/exists operator.

The min variable is in the form of "!(var_expr > constant)".

The min variable is in the form of "!(var_expr >= constant)".

Definition at line 27 of file boolbv_quantifier.cpp.