cprover
boolbv_quantifier.cpp File Reference
#include "boolbv.h"
#include <cassert>
#include <util/arith_tools.h>
#include <util/replace_expr.h>
#include <util/simplify_expr.h>
Include dependency graph for boolbv_quantifier.cpp:

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)
 

Function Documentation

§ expr_eq()

bool expr_eq ( const exprt expr1,
const exprt expr2 
)

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

§ get_quantifier_var_max()

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.

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

§ get_quantifier_var_min()

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.

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

§ instantiate_quantifier()

bool instantiate_quantifier ( exprt expr,
const namespacet ns 
)