cprover
|
#include "boolbv.h"
#include <util/arith_tools.h>
#include <util/invariant.h>
#include <util/optional.h>
#include <util/replace_expr.h>
#include <util/simplify_expr.h>
Go to the source code of this file.
Functions | |
bool | expr_eq (const exprt &expr1, const exprt &expr2) |
A method to detect equivalence between experts that can contain typecast. More... | |
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... | |
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... | |
optionalt< exprt > | instantiate_quantifier (const quantifier_exprt &expr, const namespacet &ns) |
A method to detect equivalence between experts that can contain typecast.
Definition at line 18 of file boolbv_quantifier.cpp.
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.
The max variable is in the form of "!(var_expr >= constant)".
Definition at line 78 of file boolbv_quantifier.cpp.
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)".
The min variable is in the form of "var_expr >= constant".
Definition at line 31 of file boolbv_quantifier.cpp.
optionalt<exprt> instantiate_quantifier | ( | const quantifier_exprt & | expr, |
const namespacet & | ns | ||
) |
We need to rewrite the forall/exists quantifier into an OR/AND expr.
Definition at line 136 of file boolbv_quantifier.cpp.