cprover
boolbv_equality.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/std_expr.h>
12 #include <util/base_type.h>
13 #include <util/invariant.h>
14 
16 #include "flatten_byte_operators.h"
17 
19 {
20  const bool is_base_type_eq =
21  base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
22  if(!is_base_type_eq)
23  {
24  const std::string error_msg =
25  std::string("equality without matching types:\n") + "######### lhs: " +
26  expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty();
27  throw bitvector_conversion_exceptiont(error_msg, expr);
28  }
29 
30  // see if it is an unbounded array
31  if(is_unbounded_array(expr.lhs().type()))
32  {
33  // flatten byte_update/byte_extract operators if needed
34 
35  if(has_byte_operator(expr))
36  {
37  exprt tmp=flatten_byte_operators(expr, ns);
39  }
40 
41  return record_array_equality(expr);
42  }
43 
44  const bvt &bv0=convert_bv(expr.lhs());
45  const bvt &bv1=convert_bv(expr.rhs());
46 
48  bv0.size() == bv1.size(),
49  std::string("unexpected size mismatch on equality:\n") + "lhs: " +
50  expr.lhs().pretty() + '\n' + "lhs size: " + std::to_string(bv0.size()) +
51  '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
52  "rhs size: " + std::to_string(bv1.size()));
53 
54  if(bv0.empty())
55  {
56  // An empty bit-vector comparison. It's not clear
57  // what this is meant to say.
58  return prop.new_variable();
59  }
60 
61  return bv_utils.equal(bv0, bv1);
62 }
63 
65  const binary_relation_exprt &expr)
66 {
67  // This is 4-valued comparison, i.e., z===z, x===x etc.
68  // The result is always Boolean.
69 
70  const bool is_base_type_eq =
71  base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
73  is_base_type_eq,
74  std::string("verilog_case_equality without matching types:\n") +
75  "######### lhs: " + expr.lhs().pretty() + '\n' +
76  "######### rhs: " + expr.rhs().pretty());
77 
78  const bvt &bv0=convert_bv(expr.lhs());
79  const bvt &bv1=convert_bv(expr.rhs());
80 
82  bv0.size() == bv1.size(),
83  std::string("unexpected size mismatch on verilog_case_equality:\n") +
84  "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
85  std::to_string(bv0.size()) + '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
86  "rhs size: " + std::to_string(bv1.size()));
87 
88  if(expr.id()==ID_verilog_case_inequality)
89  return !bv_utils.equal(bv0, bv1);
90  else
91  return bv_utils.equal(bv0, bv1);
92 }
bv_utilst bv_utils
Definition: boolbv.h:93
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
typet & type()
Definition: expr.h:56
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
Exceptions that can be raised in bv_conversion.
API to expression classes.
const namespacet & ns
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool has_byte_operator(const exprt &src)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
std::vector< literalt > bvt
Definition: literal.h:200