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 <iostream>
12 
13 #include <util/std_expr.h>
14 #include <util/base_type.h>
15 
16 #include <langapi/language_util.h>
17 
18 #include "flatten_byte_operators.h"
19 
21 {
22  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
23  {
24  std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
25  std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
26  throw "equality without matching types";
27  }
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  exprt tmp=flatten_byte_operators(expr, ns);
38  }
39 
40  return record_array_equality(expr);
41  }
42 
43  const bvt &bv0=convert_bv(expr.lhs());
44  const bvt &bv1=convert_bv(expr.rhs());
45 
46  if(bv0.size()!=bv1.size())
47  {
48  std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
49  std::cerr << "lhs size: " << bv0.size() << '\n';
50  std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
51  std::cerr << "rhs size: " << bv1.size() << '\n';
52  throw "unexpected size mismatch on equality";
53  }
54 
55  if(bv0.empty())
56  {
57  // An empty bit-vector comparison. It's not clear
58  // what this is meant to say.
59  return prop.new_variable();
60  }
61 
62  return bv_utils.equal(bv0, bv1);
63 }
64 
66  const binary_relation_exprt &expr)
67 {
68  // This is 4-valued comparison, i.e., z===z, x===x etc.
69  // The result is always Boolean.
70 
71  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
72  {
73  std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
74  std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
75  throw "verilog_case_equality without matching types";
76  }
77 
78  const bvt &bv0=convert_bv(expr.lhs());
79  const bvt &bv1=convert_bv(expr.rhs());
80 
81  if(bv0.size()!=bv1.size())
82  {
83  std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
84  std::cerr << "lhs size: " << bv0.size() << '\n';
85  std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
86  std::cerr << "rhs size: " << bv1.size() << '\n';
87  throw "unexpected size mismatch on verilog_case_equality";
88  }
89 
90  if(expr.id()==ID_verilog_case_inequality)
91  return !bv_utils.equal(bv0, bv1);
92  else
93  return bv_utils.equal(bv0, bv1);
94 }
bv_utilst bv_utils
Definition: boolbv.h:93
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
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:270
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1105
typet & type()
Definition: expr.h:60
equality
Definition: std_expr.h:1082
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:115
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
API to expression classes.
const namespacet & ns
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
Base class for all expressions.
Definition: expr.h:46
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:197