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 
18 
20 {
21  const bool is_base_type_eq =
22  base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
24  is_base_type_eq,
25  "types of expressions on each side of equality should match",
28 
29  // see if it is an unbounded array
30  if(is_unbounded_array(expr.lhs().type()))
31  {
32  // flatten byte_update/byte_extract operators if needed
33 
34  if(has_byte_operator(expr))
35  {
36  return record_array_equality(
38  }
39 
40  return record_array_equality(expr);
41  }
42 
43  const bvt &lhs_bv = convert_bv(expr.lhs());
44  const bvt &rhs_bv = convert_bv(expr.rhs());
45 
47  lhs_bv.size() == rhs_bv.size(),
48  "sizes of lhs and rhs bitvectors should match",
50  "lhs size: " + std::to_string(lhs_bv.size()),
52  "rhs size: " + std::to_string(rhs_bv.size()));
53 
54  if(lhs_bv.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(lhs_bv, rhs_bv);
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  "lhs and rhs types should match in verilog_case_equality",
77 
78  const bvt &lhs_bv = convert_bv(expr.lhs());
79  const bvt &rhs_bv = convert_bv(expr.rhs());
80 
82  lhs_bv.size() == rhs_bv.size(),
83  "bitvector arguments to verilog_case_equality should have the same size",
85  "lhs size: " + std::to_string(lhs_bv.size()),
87  "rhs size: " + std::to_string(rhs_bv.size()));
88 
89  if(expr.id()==ID_verilog_case_inequality)
90  return !bv_utils.equal(lhs_bv, rhs_bv);
91  else
92  return bv_utils.equal(lhs_bv, rhs_bv);
93 }
bv_utilst bv_utils
Definition: boolbv.h:95
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1116
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:486
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 an exprt to an equal_exprt.
Definition: std_expr.h:1519
bool has_byte_operator(const exprt &src)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Base Type Computation.
std::vector< literalt > bvt
Definition: literal.h:200