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",
49  irep_pretty_diagnosticst{expr.lhs()},
50  "lhs size: " + std::to_string(lhs_bv.size()),
51  irep_pretty_diagnosticst{expr.rhs()},
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",
84  irep_pretty_diagnosticst{expr.lhs()},
85  "lhs size: " + std::to_string(lhs_bv.size()),
86  irep_pretty_diagnosticst{expr.rhs()},
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 }
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
bvt
std::vector< literalt > bvt
Definition: literal.h:200
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:630
binary_relation_exprt::rhs
exprt & rhs()
Definition: std_expr.h:931
propt::new_variable
virtual literalt new_variable()=0
binary_relation_exprt::lhs
exprt & lhs()
Definition: std_expr.h:921
invariant.h
bv_conversion_exceptions.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
equal_exprt
Equality.
Definition: std_expr.h:1484
expr_lowering.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
base_type.h
base_type_eq
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
boolbvt::convert_verilog_case_equality
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Definition: boolbv_equality.cpp:64
lower_byte_operators
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Definition: byte_operators.cpp:645
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
irept::id
const irep_idt & id() const
Definition: irep.h:259
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
irep_pretty_diagnosticst
Definition: irep.h:466
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:486
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
literalt
Definition: literal.h:24
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
boolbvt::convert_equality
virtual literalt convert_equality(const equal_exprt &expr)
Definition: boolbv_equality.cpp:19
boolbv.h
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1116
std_expr.h
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152