cprover
|
#include "boolbv.h"
#include <cassert>
#include <util/arith_tools.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... | |
bool | instantiate_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.
References irept::id(), and exprt::op0().
Referenced by get_quantifier_var_max(), and get_quantifier_var_min().
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 79 of file boolbv_quantifier.cpp.
References expr_eq(), from_integer(), irept::id(), exprt::make_false(), exprt::op0(), exprt::op1(), exprt::operands(), to_integer(), and exprt::type().
Referenced by instantiate_quantifier().
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.
References expr_eq(), irept::id(), exprt::make_false(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by instantiate_quantifier().
bool instantiate_quantifier | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
We need to rewrite the forall/exists quantifier into an OR/AND expr.
Definition at line 140 of file boolbv_quantifier.cpp.
References conjunction(), disjunction(), from_integer(), get_quantifier_var_max(), get_quantifier_var_min(), irept::id(), exprt::is_false(), exprt::is_true(), exprt::op0(), exprt::op1(), exprt::operands(), replace_expr(), simplify_expr(), irept::swap(), and to_integer().
Referenced by boolbvt::convert_quantifier().