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)
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  assert(map_entry.literal_map.size()==map_entry.width);
71 
72  return map_entry;
73 }
74 
75 void boolbv_mapt::show() const
76 {
77  for(mappingt::const_iterator it=mapping.begin();
78  it!=mapping.end();
79  it++)
80  {
81  }
82 }
83 
85  const irep_idt &identifier,
86  const typet &type,
87  const std::size_t width,
88  bvt &literals)
89 {
90  map_entryt &map_entry=get_map_entry(identifier, type);
91 
92  assert(literals.size()==width);
93  assert(map_entry.literal_map.size()==width);
94 
95  Forall_literals(it, literals)
96  {
97  literalt &l=*it;
98  const std::size_t bit=it-literals.begin();
99 
100  assert(bit<map_entry.literal_map.size());
101  map_bitt &mb=map_entry.literal_map[bit];
102 
103  if(mb.is_set)
104  {
105  l=mb.l;
106  continue;
107  }
108 
109  l=prop.new_variable();
110 
111  mb.is_set=true;
112  mb.l=l;
113 
114  #ifdef DEBUG
115  std::cout << "NEW: " << identifier << ":" << bit
116  << "=" << l << '\n';
117  #endif
118  }
119 }
120 
122  const irep_idt &identifier,
123  const typet &type,
124  const bvt &literals)
125 {
126  map_entryt &map_entry=get_map_entry(identifier, type);
127 
128  forall_literals(it, literals)
129  {
130  const literalt &literal=*it;
131  const std::size_t bit=it-literals.begin();
132 
133  assert(literal.is_constant() ||
134  literal.var_no()<prop.no_variables());
135 
136  assert(bit<map_entry.literal_map.size());
137  map_bitt &mb=map_entry.literal_map[bit];
138 
139  if(mb.is_set)
140  {
141  prop.set_equal(mb.l, literal);
142  continue;
143  }
144 
145  mb.is_set=true;
146  mb.l=literal;
147  }
148 }
149 
151  const irep_idt &identifier,
152  const typet &)
153 {
154  mapping.erase(identifier);
155 }
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression.
Definition: type.h:22
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:75
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:150
virtual size_t no_variables() const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:84
std::vector< literalt > bvt
Definition: literal.h:200