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  std::pair<mappingt::iterator, bool> result=
54  mapping.insert(std::pair<irep_idt, map_entryt>(
55  identifier, map_entryt()));
56 
57  map_entryt &map_entry=result.first->second;
58 
59  if(result.second)
60  { // actually inserted
61  map_entry.type=type;
62  map_entry.width=boolbv_width(type);
63  map_entry.bvtype=get_bvtype(type);
64  map_entry.literal_map.resize(map_entry.width);
65  }
66 
67  INVARIANT(
68  map_entry.literal_map.size() == map_entry.width,
69  "number of literals in the literal map shall equal the bitvector width");
70 
71  return map_entry;
72 }
73 
74 void boolbv_mapt::show() const
75 {
76  for(mappingt::const_iterator it=mapping.begin();
77  it!=mapping.end();
78  it++)
79  {
80  }
81 }
82 
84  const irep_idt &identifier,
85  const typet &type,
86  const std::size_t width,
87  bvt &literals)
88 {
89  map_entryt &map_entry=get_map_entry(identifier, type);
90 
91  PRECONDITION(literals.size() == width);
92  INVARIANT(
93  map_entry.literal_map.size() == width,
94  "number of literals in the literal map shall equal the bitvector width");
95 
96  Forall_literals(it, literals)
97  {
98  literalt &l=*it;
99  const std::size_t bit=it-literals.begin();
100 
101  INVARIANT(
102  bit < map_entry.literal_map.size(), "bit index shall be within bounds");
103  map_bitt &mb=map_entry.literal_map[bit];
104 
105  if(mb.is_set)
106  {
107  l=mb.l;
108  continue;
109  }
110 
111  l=prop.new_variable();
112 
113  mb.is_set=true;
114  mb.l=l;
115 
116  #ifdef DEBUG
117  std::cout << "NEW: " << identifier << ":" << bit
118  << "=" << l << '\n';
119  #endif
120  }
121 }
122 
124  const irep_idt &identifier,
125  const typet &type,
126  const bvt &literals)
127 {
128  map_entryt &map_entry=get_map_entry(identifier, type);
129 
130  forall_literals(it, literals)
131  {
132  const literalt &literal=*it;
133 
134  INVARIANT(
135  literal.is_constant() || literal.var_no() < prop.no_variables(),
136  "variable number of non-constant literals shall be within bounds");
137 
138  const std::size_t bit = it - literals.begin();
139 
140  INVARIANT(
141  bit < map_entry.literal_map.size(), "bit index shall be within bounds");
142  map_bitt &mb=map_entry.literal_map[bit];
143 
144  if(mb.is_set)
145  {
146  prop.set_equal(mb.l, literal);
147  continue;
148  }
149 
150  mb.is_set=true;
151  mb.l=literal;
152  }
153 }
154 
156  const irep_idt &identifier,
157  const typet &)
158 {
159  mapping.erase(identifier);
160 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:155
boolbv_mapt::map_entryt::bvtype
bvtypet bvtype
Definition: boolbv_map.h:48
boolbv_mapt::get_map_entry
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
boolbv_mapt::map_entryt::get_value
std::string get_value(const propt &) const
Definition: boolbv_map.cpp:21
typet
The type of an expression, extends irept.
Definition: type.h:29
boolbv_mapt::prop
propt & prop
Definition: boolbv_map.h:80
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
boolbv_mapt::map_bitt
Definition: boolbv_map.h:32
propt::set_equal
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
boolbv_mapt::get_literals
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:83
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
propt::new_variable
virtual literalt new_variable()=0
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:50
boolbv_mapt::show
void show() const
Definition: boolbv_map.cpp:74
literalt::var_no
var_not var_no() const
Definition: literal.h:83
propt::no_variables
virtual size_t no_variables() const =0
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:207
boolbv_mapt::map_entryt::width
std::size_t width
Definition: boolbv_map.h:47
boolbv_mapt::map_entryt
Definition: boolbv_map.h:41
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:56
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
prop.h
boolbv_mapt::boolbv_width
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:81
tvt::is_false
bool is_false() const
Definition: threeval.h:26
tvt
Definition: threeval.h:20
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:49
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
propt::l_get
virtual tvt l_get(literalt a) const =0
boolbv_width.h
literalt
Definition: literal.h:26
boolbv_mapt::map_bitt::is_set
bool is_set
Definition: boolbv_map.h:34
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
boolbv_mapt::map_bitt::l
literalt l
Definition: boolbv_map.h:35
boolbv_map.h
validation_modet::INVARIANT
@ INVARIANT
tvt::is_true
bool is_true() const
Definition: threeval.h:25
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:123