Skip to content

Commit c6314a7

Browse files
tautschnigtautschnig
authored
Merge pull request #1099 from diffblue/netlist_boolbv_h
extract `instantiate_var_mapt` into a separate header file
2 parents f885b0d + a2d17ec commit c6314a7

File tree

4 files changed

+178
-139
lines changed

4 files changed

+178
-139
lines changed

‎src/trans-netlist/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ SRC = aig.cpp \
99
ldg.cpp \
1010
map_aigs.cpp \
1111
netlist.cpp \
12+
netlist_boolbv.cpp \
1213
smv_netlist.cpp \
1314
trans_to_netlist.cpp \
1415
trans_trace.cpp \

‎src/trans-netlist/instantiate_netlist.cpp

+5-139
Original file line numberDiff line numberDiff line change
@@ -13,48 +13,15 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/std_expr.h>
1414

1515
#include <ebmc/ebmc_error.h>
16-
#include <solvers/flattening/boolbv.h>
1716
#include <solvers/prop/literal_expr.h>
1817
#include <temporal-logic/temporal_logic.h>
1918
#include <verilog/sva_expr.h>
2019

20+
#include "netlist_boolbv.h"
21+
2122
#include <cassert>
2223
#include <cstdlib>
2324

24-
/*******************************************************************\
25-
26-
Class: instantiate_var_mapt
27-
28-
Purpose:
29-
30-
\*******************************************************************/
31-
32-
class instantiate_var_mapt:public boolbvt
33-
{
34-
public:
35-
instantiate_var_mapt(const namespacet &_ns, propt &solver,
36-
message_handlert &message_handler,
37-
const var_mapt &_var_map)
38-
: boolbvt(_ns, solver, message_handler), var_map(_var_map) {}
39-
40-
typedef boolbvt SUB;
41-
42-
// overloading
43-
using boolbvt::get_literal;
44-
45-
virtual literalt convert_bool(const exprt &expr);
46-
virtual literalt get_literal(const std::string &symbol, const unsigned bit);
47-
virtual bvt convert_bitvector(const exprt &expr);
48-
49-
protected:
50-
// disable smart variable allocation,
51-
// we already have literals for all variables
52-
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr) { return true; }
53-
virtual bool set_equality_to_true(const equal_exprt &expr) { return true; }
54-
55-
const var_mapt &var_map;
56-
};
57-
5825
/*******************************************************************\
5926
6027
Function: instantiate_constraint
@@ -74,7 +41,7 @@ void instantiate_constraint(
7441
const namespacet &ns,
7542
message_handlert &message_handler)
7643
{
77-
instantiate_var_mapt i(ns, solver, message_handler, var_map);
44+
netlist_boolbvt i(ns, solver, message_handler, var_map);
7845

7946
try
8047
{
@@ -113,7 +80,7 @@ literalt instantiate_convert(
11380
const namespacet &ns,
11481
message_handlert &message_handler)
11582
{
116-
instantiate_var_mapt i(ns, solver, message_handler, var_map);
83+
netlist_boolbvt i(ns, solver, message_handler, var_map);
11784

11885
try
11986
{
@@ -153,7 +120,7 @@ void instantiate_convert(
153120
message_handlert &message_handler,
154121
bvt &bv)
155122
{
156-
instantiate_var_mapt i(ns, solver, message_handler, var_map);
123+
netlist_boolbvt i(ns, solver, message_handler, var_map);
157124

158125
try
159126
{
@@ -175,107 +142,6 @@ void instantiate_convert(
175142

176143
/*******************************************************************\
177144
178-
Function: instantiate_var_mapt::convert_bool
179-
180-
Inputs:
181-
182-
Outputs:
183-
184-
Purpose:
185-
186-
\*******************************************************************/
187-
188-
literalt instantiate_var_mapt::convert_bool(const exprt &expr)
189-
{
190-
if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
191-
{
192-
bvt result=convert_bitvector(expr);
193-
194-
if(result.size()!=1)
195-
throw "expected one-bit result";
196-
197-
return result[0];
198-
}
199-
else if(expr.id()==ID_sva_overlapped_implication)
200-
{
201-
// same as regular implication
202-
auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr);
203-
return prop.limplies(
204-
convert_bool(sva_overlapped_implication.lhs()),
205-
convert_bool(sva_overlapped_implication.rhs()));
206-
}
207-
else if(expr.id() == ID_verilog_past)
208-
{
209-
throw ebmc_errort().with_location(expr.source_location())
210-
<< "no support for $past when using AIG backends";
211-
}
212-
213-
return SUB::convert_bool(expr);
214-
}
215-
216-
/*******************************************************************\
217-
218-
Function: instantiate_var_mapt::convert_bitvector
219-
220-
Inputs:
221-
222-
Outputs:
223-
224-
Purpose:
225-
226-
\*******************************************************************/
227-
228-
bvt instantiate_var_mapt::convert_bitvector(const exprt &expr)
229-
{
230-
if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
231-
{
232-
bool next=(expr.id()==ID_next_symbol);
233-
const irep_idt &identifier=expr.get(ID_identifier);
234-
235-
std::size_t width=boolbv_width(expr.type());
236-
237-
if(width!=0)
238-
{
239-
bvt bv;
240-
bv.resize(width);
241-
242-
for(std::size_t i=0; i<width; i++)
243-
bv[i]=next?var_map.get_next(identifier, i)
244-
:var_map.get_current(identifier, i);
245-
246-
return bv;
247-
}
248-
}
249-
else if(expr.id() == ID_verilog_past)
250-
{
251-
throw ebmc_errort().with_location(expr.source_location())
252-
<< "no support for $past when using AIG backends";
253-
}
254-
255-
return SUB::convert_bitvector(expr);
256-
}
257-
258-
/*******************************************************************\
259-
260-
Function: instantiate_var_mapt::get_literal
261-
262-
Inputs:
263-
264-
Outputs:
265-
266-
Purpose:
267-
268-
\*******************************************************************/
269-
270-
literalt instantiate_var_mapt::get_literal(
271-
const std::string &symbol,
272-
const unsigned bit)
273-
{
274-
return var_map.get_current(symbol, bit);
275-
}
276-
277-
/*******************************************************************\
278-
279145
Function: netlist_property
280146
281147
Inputs:

‎src/trans-netlist/netlist_boolbv.cpp

+112
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
/*******************************************************************\
2+
3+
Module: boolbvt for Netlists
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "netlist_boolbv.h"
10+
11+
#include <ebmc/ebmc_error.h>
12+
#include <verilog/sva_expr.h>
13+
14+
/*******************************************************************\
15+
16+
Function: netlist_boolbvt::convert_bool
17+
18+
Inputs:
19+
20+
Outputs:
21+
22+
Purpose:
23+
24+
\*******************************************************************/
25+
26+
literalt netlist_boolbvt::convert_bool(const exprt &expr)
27+
{
28+
if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
29+
{
30+
bvt result = convert_bitvector(expr);
31+
32+
if(result.size() != 1)
33+
throw "expected one-bit result";
34+
35+
return result[0];
36+
}
37+
else if(expr.id() == ID_sva_overlapped_implication)
38+
{
39+
// same as regular implication
40+
auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr);
41+
return prop.limplies(
42+
convert_bool(sva_overlapped_implication.lhs()),
43+
convert_bool(sva_overlapped_implication.rhs()));
44+
}
45+
else if(expr.id() == ID_verilog_past)
46+
{
47+
throw ebmc_errort().with_location(expr.source_location())
48+
<< "no support for $past when using AIG backends";
49+
}
50+
51+
return SUB::convert_bool(expr);
52+
}
53+
54+
/*******************************************************************\
55+
56+
Function: netlist_boolbvt::convert_bitvector
57+
58+
Inputs:
59+
60+
Outputs:
61+
62+
Purpose:
63+
64+
\*******************************************************************/
65+
66+
bvt netlist_boolbvt::convert_bitvector(const exprt &expr)
67+
{
68+
if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
69+
{
70+
bool next = (expr.id() == ID_next_symbol);
71+
const irep_idt &identifier = expr.get(ID_identifier);
72+
73+
std::size_t width = boolbv_width(expr.type());
74+
75+
if(width != 0)
76+
{
77+
bvt bv;
78+
bv.resize(width);
79+
80+
for(std::size_t i = 0; i < width; i++)
81+
bv[i] = next ? var_map.get_next(identifier, i)
82+
: var_map.get_current(identifier, i);
83+
84+
return bv;
85+
}
86+
}
87+
else if(expr.id() == ID_verilog_past)
88+
{
89+
throw ebmc_errort().with_location(expr.source_location())
90+
<< "no support for $past when using AIG backends";
91+
}
92+
93+
return SUB::convert_bitvector(expr);
94+
}
95+
96+
/*******************************************************************\
97+
98+
Function: netlist_boolbvt::get_literal
99+
100+
Inputs:
101+
102+
Outputs:
103+
104+
Purpose:
105+
106+
\*******************************************************************/
107+
108+
literalt
109+
netlist_boolbvt::get_literal(const std::string &symbol, const unsigned bit)
110+
{
111+
return var_map.get_current(symbol, bit);
112+
}

‎src/trans-netlist/netlist_boolbv.h

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/*******************************************************************\
2+
3+
Module: boolbvt for Netlists
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H
10+
#define CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H
11+
12+
#include <solvers/flattening/boolbv.h>
13+
14+
#include "var_map.h"
15+
16+
/*******************************************************************\
17+
18+
Class: netlist_boolbvt
19+
20+
Purpose:
21+
22+
\*******************************************************************/
23+
24+
class netlist_boolbvt : public boolbvt
25+
{
26+
public:
27+
netlist_boolbvt(
28+
const namespacet &_ns,
29+
propt &solver,
30+
message_handlert &message_handler,
31+
const var_mapt &_var_map)
32+
: boolbvt(_ns, solver, message_handler), var_map(_var_map)
33+
{
34+
}
35+
36+
typedef boolbvt SUB;
37+
38+
// overloading
39+
literalt convert_bool(const exprt &) override;
40+
bvt convert_bitvector(const exprt &expr) override;
41+
42+
using boolbvt::get_literal;
43+
literalt get_literal(const std::string &symbol, const unsigned bit);
44+
45+
protected:
46+
// disable smart variable allocation,
47+
// we already have literals for all variables
48+
bool boolbv_set_equality_to_true(const equal_exprt &) override
49+
{
50+
return true;
51+
}
52+
bool set_equality_to_true(const equal_exprt &expr) override
53+
{
54+
return true;
55+
}
56+
57+
const var_mapt &var_map;
58+
};
59+
60+
#endif // CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H

0 commit comments

Comments
 (0)