#include "boolbv.h"#include <util/arith_tools.h>#include <util/expr_util.h>#include <util/invariant.h>#include <util/simplify_expr.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. More... | |
| 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. More... | |
| 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. More... | |
| static std::optional< exprt > | eager_quantifier_instantiation (const quantifier_exprt &expr, const namespacet &ns) |
Function Documentation
◆ eager_quantifier_instantiation()
|
static |
We need to rewrite the forall/exists quantifier into an OR/AND expr.
Definition at line 152 of file boolbv_quantifier.cpp.
◆ expr_eq()
A method to detect equivalence between experts that can contain typecast.
Definition at line 17 of file boolbv_quantifier.cpp.
◆ get_quantifier_var_max()
|
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 78 of file boolbv_quantifier.cpp.
◆ get_quantifier_var_min()
|
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 26 of file boolbv_quantifier.cpp.
