Skip to content

Commit d0f270e

Browse files
committed
Use std::forward_list instead of std::map in irept by default
This reduces the size of an irept by 5 pointers (i.e., 40 bytes on 64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with the std::map configuration. The performance improvements are spread across various `irept`-related operations.
1 parent ae99660 commit d0f270e

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed

.travis.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -177,7 +177,7 @@ jobs:
177177
- CCACHE_CPP2=yes
178178
script: echo "Not running any tests for a debug build."
179179

180-
# cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST
180+
# cmake build using g++-7, disable NAMED_SUB_IS_FORWARD_LIST
181181
- stage: Test different OS/CXX/Flags
182182
os: linux
183183
sudo: false
@@ -200,7 +200,7 @@ jobs:
200200
install:
201201
- ccache -z
202202
- ccache --max-size=1G
203-
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST'
203+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST=0'
204204
- git submodule update --init --recursive
205205
- cmake --build build -- -j4
206206
script: (cd build; bin/unit "[core][irept]")

src/util/irep.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ Author: Daniel Kroening, [email protected]
1818

1919
#define SHARING
2020
// #define HASH_CODE
21-
// #define NAMED_SUB_IS_FORWARD_LIST
21+
#ifndef NAMED_SUB_IS_FORWARD_LIST
22+
# define NAMED_SUB_IS_FORWARD_LIST
23+
#endif
2224

2325
#ifdef NAMED_SUB_IS_FORWARD_LIST
2426
#include <forward_list>

0 commit comments

Comments
 (0)