cprover
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_exprtget_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_exprtget_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< exprteager_quantifier_instantiation (const quantifier_exprt &expr, const namespacet &ns)

Function Documentation

◆ eager_quantifier_instantiation()

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()

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()

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()

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.