cprover
boolbv_map.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_map.h"
10 
11 #include <util/threeval.h>
12 
13 #include <solvers/prop/prop.h>
14 
15 #include "boolbv_width.h"
16 
17 #ifdef DEBUG
18 #include <iostream>
19 #endif
20 
21 std::string boolbv_mapt::map_entryt::get_value(const propt &prop) const
22 {
23  std::string result;
24 
25  result.reserve(literal_map.size());
26 
27  for(std::size_t i=0; i<literal_map.size(); i++)
28  {
29  char ch='*';
30 
31  if(literal_map[i].is_set)
32  {
33  tvt value=prop.l_get(literal_map[i].l);
34 
35  if(value.is_true())
36  ch='1';
37  else if(value.is_false())
38  ch='0';
39  else
40  ch='?';
41  }
42 
43  result=result+ch;
44  }
45 
46  return result;
47 }
48 
50  const irep_idt &identifier,
51  const typet &type)
52 {
53  if(type.id() == ID_symbol_type)
54  return get_map_entry(identifier, ns.follow(type));
55 
56  std::pair<mappingt::iterator, bool> result=
57  mapping.insert(std::pair<irep_idt, map_entryt>(
58  identifier, map_entryt()));
59 
60  map_entryt &map_entry=result.first->second;
61 
62  if(result.second)
63  { // actually inserted
64  map_entry.type=type;
65  map_entry.width=boolbv_width(type);
66  map_entry.bvtype=get_bvtype(type);
67  map_entry.literal_map.resize(map_entry.width);
68  }
69 
70  INVARIANT(
71  map_entry.literal_map.size() == map_entry.width,
72  "number of literals in the literal map shall equal the bitvector width");
73 
74  return map_entry;
75 }
76 
77 void boolbv_mapt::show() const
78 {
79  for(mappingt::const_iterator it=mapping.begin();
80  it!=mapping.end();
81  it++)
82  {
83  }
84 }
85 
87  const irep_idt &identifier,
88  const typet &type,
89  const std::size_t width,
90  bvt &literals)
91 {
92  map_entryt &map_entry=get_map_entry(identifier, type);
93 
94  PRECONDITION(literals.size() == width);
95  INVARIANT(
96  map_entry.literal_map.size() == width,
97  "number of literals in the literal map shall equal the bitvector width");
98 
99  Forall_literals(it, literals)
100  {
101  literalt &l=*it;
102  const std::size_t bit=it-literals.begin();
103 
104  INVARIANT(
105  bit < map_entry.literal_map.size(), "bit index shall be within bounds");
106  map_bitt &mb=map_entry.literal_map[bit];
107 
108  if(mb.is_set)
109  {
110  l=mb.l;
111  continue;
112  }
113 
114  l=prop.new_variable();
115 
116  mb.is_set=true;
117  mb.l=l;
118 
119  #ifdef DEBUG
120  std::cout << "NEW: " << identifier << ":" << bit
121  << "=" << l << '\n';
122  #endif
123  }
124 }
125 
127  const irep_idt &identifier,
128  const typet &type,
129  const bvt &literals)
130 {
131  map_entryt &map_entry=get_map_entry(identifier, type);
132 
133  forall_literals(it, literals)
134  {
135  const literalt &literal=*it;
136 
137  INVARIANT(
138  literal.is_constant() || literal.var_no() < prop.no_variables(),
139  "variable number of non-constant literals shall be within bounds");
140 
141  const std::size_t bit = it - literals.begin();
142 
143  INVARIANT(
144  bit < map_entry.literal_map.size(), "bit index shall be within bounds");
145  map_bitt &mb=map_entry.literal_map[bit];
146 
147  if(mb.is_set)
148  {
149  prop.set_equal(mb.l, literal);
150  continue;
151  }
152 
153  mb.is_set=true;
154  mb.l=literal;
155  }
156 }
157 
159  const irep_idt &identifier,
160  const typet &)
161 {
162  mapping.erase(identifier);
163 }
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression, extends irept.
Definition: type.h:27
bool is_false() const
Definition: threeval.h:26
literal_mapt literal_map
Definition: boolbv_map.h:53
propt & prop
Definition: boolbv_map.h:83
void show() const
Definition: boolbv_map.cpp:77
const namespacet & ns
Definition: boolbv_map.h:84
#define forall_literals(it, bv)
Definition: literal.h:202
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:85
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:206
mappingt mapping
Definition: boolbv_map.h:59
std::string get_value(const propt &) const
Definition: boolbv_map.cpp:21
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:158
virtual size_t no_variables() const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:126
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
TO_BE_DOCUMENTED.
Definition: prop.h:24
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
bool is_true() const
Definition: threeval.h:25
bool is_constant() const
Definition: literal.h:165
var_not l
Definition: literal.h:181
virtual tvt l_get(literalt a) const =0
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:86
std::vector< literalt > bvt
Definition: literal.h:200