diff --git a/resources/3rdparty/sylvan/.gitignore b/resources/3rdparty/sylvan/.gitignore index 4c6b4e09b..d45dee77e 100644 --- a/resources/3rdparty/sylvan/.gitignore +++ b/resources/3rdparty/sylvan/.gitignore @@ -33,3 +33,11 @@ src/libsylvan.a # MacOS file .DS_Store + +# eclipse files +.cproject +.project +.settings + +# coverage output +coverage diff --git a/resources/3rdparty/sylvan/.travis.yml b/resources/3rdparty/sylvan/.travis.yml new file mode 100644 index 000000000..ac0da9fb9 --- /dev/null +++ b/resources/3rdparty/sylvan/.travis.yml @@ -0,0 +1,100 @@ +sudo: false + +matrix: + include: + - os: linux + env: TOOLSET=gcc CC=gcc-4.7 CXX=g++-4.7 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["gcc-4.7", "g++-4.7", "libstd++-4.7-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-4.8 CXX=g++-4.8 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["gcc-4.8", "g++-4.8", "libstd++-4.8-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-4.9 CXX=g++-4.9 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["gcc-4.9", "g++-4.9", "libstd++-4.9-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Debug" HWLOC="OFF" SYLVAN_STATS="OFF" + addons: + apt: + packages: ["gcc-5", "g++-5", "libstd++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Debug" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["gcc-5", "g++-5", "libstd++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["gcc-5", "g++-5", "libstd++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="OFF" + addons: + apt: + packages: ["gcc-5", "g++-5", "libstd++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" VARIANT="coverage" + addons: + apt: + packages: ["gcc-5", "g++-5", "libstd++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test"] + - os: linux + env: TOOLSET=clang CC=/usr/local/clang-3.4/bin/clang CXX=/usr/local/clang-3.4/bin/clang++ BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["clang-3.4", "libstdc++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test", "llvm-toolchain-precise-3.4"] + - os: linux + env: TOOLSET=clang CC=clang-3.6 CXX=clang++-3.6 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["clang-3.6", "libstdc++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test", "llvm-toolchain-precise-3.6"] + - os: linux + env: TOOLSET=clang CC=clang-3.7 CXX=clang++-3.7 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="ON" + addons: + apt: + packages: ["clang-3.7", "libstdc++-5-dev", "libgmp-dev", "cmake", "libhwloc-dev"] + sources: ["ubuntu-toolchain-r-test", "llvm-toolchain-precise-3.7"] + - os: osx + env: TOOLSET=clang CC=clang CXX=clang++ BUILD_TYPE="Debug" HWLOC="ON" SYLVAN_STATS="ON" + - os: osx + env: TOOLSET=clang CC=clang CXX=clang++ BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="OFF" + - os: osx + env: TOOLSET=gcc CC=gcc-4.9 CXX=g++-4.9 BUILD_TYPE="Debug" HWLOC="ON" SYLVAN_STATS="OFF" + - os: osx + env: TOOLSET=gcc CC=gcc-4.9 CXX=g++-4.9 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="OFF" + - os: osx + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Debug" HWLOC="ON" SYLVAN_STATS="OFF" + - os: osx + env: TOOLSET=gcc CC=gcc-5 CXX=g++-5 BUILD_TYPE="Release" HWLOC="ON" SYLVAN_STATS="OFF" + +install: +- if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update; brew install argp-standalone homebrew/science/hwloc; fi +- if [[ "$TRAVIS_OS_NAME" == "osx" && "$CC" == "gcc-5" ]]; then brew install homebrew/versions/gcc5; fi + +script: +- ${CC} --version +- ${CXX} --version +- cmake . -DCMAKE_BUILD_TYPE=${BUILD_TYPE} -DUSE_HWLOC=${HWLOC} -DSYLVAN_STATS=${SYLVAN_STATS} -DWITH_COVERAGE=${COVERAGE} +- make -j 2 +- make test +- examples/simple +- examples/mc models/schedule_world.2.8-rgs.bdd -w 2 | tee /dev/fd/2 | grep -q "1,570,340" +- examples/lddmc models/blocks.2.ldd -w 2 | tee /dev/fd/2 | grep -q "7057 states" + +notifications: + email: false + diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt index 7cfa8b636..27762655b 100644 --- a/resources/3rdparty/sylvan/CMakeLists.txt +++ b/resources/3rdparty/sylvan/CMakeLists.txt @@ -1,10 +1,38 @@ cmake_minimum_required(VERSION 2.6) project(sylvan C CXX) +enable_testing() + +set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11") +set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11") + +option(WITH_COVERAGE "Add generation of test coverage" OFF) +if(WITH_COVERAGE) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0 -g -coverage") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0 -g -coverage") + + find_program(GCOV_PATH gcov) + find_program(LCOV_PATH lcov) + find_program(GENHTML_PATH genhtml) + + add_custom_target(coverage + # Cleanup lcov + ${LCOV_PATH} --directory . --zerocounters + # Run tests + COMMAND make test + # Capture counters + COMMAND ${LCOV_PATH} --gcov-tool ${GCOV_PATH} --directory . --capture --output-file coverage.info + COMMAND ${LCOV_PATH} --remove coverage.info 'test/*' '/usr/*' 'examples/*' 'src/sylvan_mtbdd*' 'src/lace*' 'src/sylvan_ldd*' 'src/avl.h' 'src/sha2.c' --output-file coverage.info.cleaned + COMMAND ${GENHTML_PATH} -o coverage coverage.info.cleaned + COMMAND ${CMAKE_COMMAND} -E remove coverage.info coverage.info.cleaned + WORKING_DIRECTORY ${CMAKE_BINARY_DIR} + ) +endif() set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) find_package(GMP REQUIRED) include_directories(${GMP_INCLUDE_DIR}) -#message(STATUS "Include directory ${GMP_INCLUDE_DIR}") +include_directories(src) + include_directories(src) add_subdirectory(src) @@ -15,7 +43,7 @@ if(SYLVAN_BUILD_TEST) add_subdirectory(test) endif() -option(SYLVAN_BUILD_EXAMPLES "Build example tools" ON) +option(SYLVAN_BUILD_EXAMPLES "Build example tools" OFF) if(SYLVAN_BUILD_EXAMPLES) add_subdirectory(examples) diff --git a/resources/3rdparty/sylvan/README.md b/resources/3rdparty/sylvan/README.md index 421e9e659..f0f88b851 100644 --- a/resources/3rdparty/sylvan/README.md +++ b/resources/3rdparty/sylvan/README.md @@ -1,8 +1,8 @@ -Sylvan +Sylvan [![Build Status](https://travis-ci.org/trolando/sylvan.svg?branch=master)](https://travis-ci.org/trolando/sylvan) ====== Sylvan is a parallel (multi-core) BDD library in C. Sylvan allows both sequential and parallel BDD-based algorithms to benefit from parallelism. Sylvan uses the work-stealing framework Lace and a scalable lockless hashtable to implement scalable multi-core BDD operations. -Sylvan is developed (© 2011-2014) by the [Formal Methods and Tools](http://fmt.ewi.utwente.nl/) group at the University of Twente as part of the MaDriD project, which is funded by NWO. Sylvan is licensed with the Apache 2.0 license. +Sylvan is developed (© 2011-2016) by the [Formal Methods and Tools](http://fmt.ewi.utwente.nl/) group at the University of Twente as part of the MaDriD project, which is funded by NWO. Sylvan is licensed with the Apache 2.0 license. You can contact the main author of Sylvan at . Please let us know if you use Sylvan in your projects. @@ -12,47 +12,28 @@ Haskell bindings: https://github.com/adamwalker/sylvan-haskell Publications ------------ -Dijk, T. van (2012) [The parallelization of binary decision diagram operations for model checking](http://essay.utwente.nl/61650/). Master’s Thesis, University of Twente, 27 April 2012. +T. van Dijk and J. van de Pol (2015) [Sylvan: Multi-core Decision Diagrams](http://dx.doi.org/10.1007/978-3-662-46681-0_60). In: TACAS 2015, LNCS 9035. Springer. -Dijk, T. van and Laarman, A.W. and Pol, J.C. van de (2012) [Multi-Core BDD Operations for Symbolic Reachability](http://eprints.eemcs.utwente.nl/22166/). In: 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, 17 Sept. 2012, London, UK. Electronic Notes in Theoretical Computer Science. Elsevier. +T. van Dijk and A.W. Laarman and J. van de Pol (2012) [Multi-Core BDD Operations for Symbolic Reachability](http://eprints.eemcs.utwente.nl/22166/). In: PDMC 2012, ENTCS. Elsevier. Usage ----- -For a quick demo, you can find an example of a simple BDD-based reachability algorithm in `test/mc.c`. This demo features both a sequential (bfs) and a parallel (par) symbolic reachability algorithm, demonstrating how both sequential programs and parallel programs can benefit from parallized BDD operations. +Simple examples can be found in the `examples` subdirectory. The file `simple.cpp` contains a toy program that +uses the C++ objects to perform basic BDD manipulation. +The `mc.c` and `lddmc.c` programs are more advanced examples of symbolic model checking (with example models in the `models` subdirectory). -To use Sylvan, include header file `sylvan.h`. - -Sylvan depends on the [work-stealing framework Lace](http://fmt.ewi.utwente.nl/tools/lace) for its implementation. Currently, Lace is embedded in the Sylvan distribution, but this may change in the future. To use the BDD operations of Sylvan, you must first start Lace and run all workers. - -Sylvan must be initialized after `lace_init` with a call to `sylvan_init`. This function takes three parameters: the log2 size of the BDD nodes table, the log2 size of the operation cache and the caching granularity. For example, `sylvan_init(16, 15, 4)` will initialize Sylvan with a BDD nodes table of size 65536, an operation cache of size 32768 and granularity 4. See below for detailed information about caching granularity. - -Example C code for initialization: -``` -#include - -// initialize with queue size of 1000000 -// autodetect number of workers -lace_init(0, 1000000); -// startup with defaults (create N-1 workers) -lace_startup(0, NULL, NULL); -// initialize with unique table size = 2^25 -// cache table size = 2^24 -// cache granularity = 4 -sylvan_init(25, 24, 4); -``` - -Sylvan may require a larger than normal program stack. You may need to increase the program stack size on your system using `ulimit -s`. Segmentation faults on large computations typically indicate a program stack overflow. +Sylvan depends on the [work-stealing framework Lace](http://fmt.ewi.utwente.nl/tools/lace) for its implementation. Lace is embedded in the Sylvan distribution. +To use Sylvan, Lace must be initialized first. +For more details, see the comments in `src/sylvan.h`. ### Basic functionality To create new BDDs, you can use: - `sylvan_true`: representation of constant `true`. - `sylvan_false`: representation of constant `false`. -- `sylvan_ithvar(var)`: representation of literal <var>. -- `sylvan_nithvar(var)`: representation of literal <var> negated. -- `sylvan_cube(variables, count, vector)`: create conjunction of variables in <variables> according to the corresponding value in <vector>. +- `sylvan_ithvar(var)`: representation of literal <var> (negated: `sylvan_nithvar(var)`) -To walk the BDD edges and obtain the variable at the root of a BDD, you can use: +To follow the BDD edges and obtain the variable at the root of a BDD, you can use: - `sylvan_var(bdd)`: obtain variable of the root node of <bdd> - requires that <bdd> is not constant `true` or `false`. - `sylvan_high(bdd)`: follow high edge of <bdd>. - `sylvan_low(bdd)`: follow low edge of <bdd>. @@ -60,68 +41,57 @@ To walk the BDD edges and obtain the variable at the root of a BDD, you can use: You need to manually reference BDDs that you want to keep during garbage collection: - `sylvan_ref(bdd)`: add reference to <bdd>. - `sylvan_deref(bdd)`: remove reference to <bdd>. +- `sylvan_protect(bddptr)`: add a pointer reference to the BDD variable <bddptr> +- `sylvan_unprotect(bddptr)`: remove a pointer reference to the BDD variable <bddptr> -See below for more detailed information about garbage collection. Note that garbage collection does not proceed outside BDD operations, e.g., you can safely call `sylvan_ref` on the result of a BDD operation. +It is recommended to use `sylvan_protect` and `sylvan_unprotect`. +The C++ objects handle this automatically. The following 'primitives' are implemented: - `sylvan_not(bdd)`: negation of <bdd>. - `sylvan_ite(a,b,c)`: calculate 'if <a> then <b> else <c>'. -- `sylvan_exists(bdd, vars)`: existential quantification of <bdd> with respect to variables <vars>. Here, <vars> is a disjunction of literals. - -Sylvan uses complement edges to implement negation, therefore negation is performed in constant time. - -These primitives are used to implement the following operations: -- `sylvan_and(a, b)` -- `sylvan_or(a, b)` -- `sylvan_nand(a, b)` -- `sylvan_nor(a, b)` -- `sylvan_imp(a, b)` (a implies b) -- `sylvan_invimp(a, b)` (b implies a) -- `sylvan_xor(a, b)` -- `sylvan_equiv(a, b)` (alias: `sylvan_biimp`) -- `sylvan_diff(a, b)` (a and not b) -- `sylvan_less(a, b)` (b and not a) -- `sylvan_forall(bdd, vars)` +- `sylvan_and(a, b)`: calculate a and b +- `sylvan_or(a, b)`: calculate a or b +- `sylvan_nand(a, b)`: calculate not (a and b) +- `sylvan_nor(a, b)`: calculate not (a or b) +- `sylvan_imp(a, b)`: calculate a implies b +- `sylvan_invimp(a, b)`: calculate implies a +- `sylvan_xor(a, b)`: calculate a xor b +- `sylvan_equiv(a, b)`: calculate a = b +- `sylvan_diff(a, b)`: calculate a and not b +- `sylvan_less(a, b)`: calculate b and not a +- `sylvan_exists(bdd, vars)`: existential quantification of <bdd> with respect to variables <vars>. Here, <vars> is a conjunction of literals. +- `sylvan_forall(bdd, vars)`: universal quantification of <bdd> with respect to variables <vars>. Here, <vars> is a conjunction of literals. ### Other BDD operations -We also implemented the following BDD operations: -- `sylvan_restrict(f, c)`: calculate the restrict algorithm on f,c. -- `sylvan_constrain(f, c)`: calculate the constrain f@c, also called generalized co-factor (gcf). -- `sylvan_relprod_paired(a, t, vars)`: calculate the relational product by applying transition relation <t> on <a>. Assumes variables in <a> are even and primed variables (only in <t>) are odd and paired (i.e., x' = x+1). Assumes <t> is defined on variables in <vars>, which is a disjunction of literals, including non-primed and primed variables. -- `sylvan_relprod_paired_prev(a, t, vars)`: calculate the relational product backwards, i.e., calculate previous states instead of next states. -- `sylvan_support(bdd)`: calculate the support of <bdd>, i.e., all variables that occur in the BDD; returns a disjunction of literals. -- `sylvan_satcount(bdd, vars)`: calculate the number of assignments that satisfy <bdd> with respect to the variables in <vars>, which is a disjunction of literals. -- `sylvan_pathcount(bdd)`: calculate the number of distinct paths from the root node of <bdd> to constant 'true'. -- `sylvan_nodecount(bdd)`: calculate the number of nodes in <bdd> (not thread-safe). -- `sylvan_sat_one_bdd(bdd)`: calculate a cube that satisfies <bdd>. -- `sylvan_sat_one(bdd, vars, count, vector)`: reverse of `sylvan_cube` on the result of `sylvan_sat_one_bdd`. Alias: `sylvan_pick_cube`. +See `src/sylvan_bdd.h`, `src/sylvan_mtbdd.h` and `src/sylvan_ldd.h` for other implemented operations. +See `src/sylvan_obj.hpp` for the C++ interface. ### Garbage collection -Garbage collection is triggered when trying to insert a new node and no new bucket can be found within a reasonable upper bound. This upper bound is typically 8*(4+tablesize) buckets, where tablesize is the log2 size of the table. In practice, garbage collection occurs when the table is about 90% full. Garbage collection occurs by rehashing all BDD nodes that must stay in the table. It is designed such that all workers must cooperate on garbage collection. This condition is checked in `sylvan_gc_test()` which is called from every BDD operation and from a callback in the Lace framework that is called when there is no work. - +Garbage collection is triggered when trying to insert a new node and no new bucket can be found within a reasonable upper bound. +Garbage collection is stop-the-world and all workers must cooperate on garbage collection. (Beware of deadlocks if you use Sylvan operations in critical sections!) - `sylvan_gc()`: manually trigger garbage collection. - `sylvan_gc_enable()`: enable garbage collection. - `sylvan_gc_disable()`: disable garbage collection. -### Caching granularity - -Caching granularity works as follows: with granularity G, each variable x is in a variable group x/G, e.g. the first G variables are in variable group 0, the next G variables are in variable group 1, etc. -BDD operations only consult the operation cache when they change variable groups. +### Table resizing -Higher granularity values result in less cache use. In practice, values between 4 and 8 tend to work well, but this depends on many factors, such as the structure and size of the BDDs and the characteristics of the computer architecture. +During garbage collection, it is possible to resize the nodes table and the cache. +Sylvan provides two default implementations: an agressive version that resizes every time garbage collection is performed, +and a less agressive version that only resizes when at least half the table is full. +This can be configured in `src/sylvan_config.h` +It is not possible to decrease the size of the nodes table and the cache. ### Dynamic reordering Dynamic reordening is currently not supported. -We are interested in examples where this is necessary for good performance and would like to perform research into parallel dynamic reordering in future work. - For now, we suggest users find a good static variable ordering. -### Resizing tables - -Resizing of nodes table and operation cache is currently not supported. In theory stop-the-world resizing can be implemented to grow the nodes table, but not to shrink the nodes table, since shrinking requires recreating all BDDs. Operation cache resizing is trivial to implement. - -Please let us know if you need this functionality. +Troubleshooting +--------------- +Sylvan may require a larger than normal program stack. You may need to increase the program stack size on your system using `ulimit -s`. Segmentation faults on large computations typically indicate a program stack overflow. +### I am getting the error "unable to allocate memory: ...!" +Sylvan allocates virtual memory using mmap. If you specify a combined size for the cache and node table larger than your actual available memory you may need to set `vm.overcommit_memory` to `1`. E.g. `echo 1 > /proc/sys/vm/overcommit_memory`. You can make this setting permanent with `echo "vm.overcommit_memory = 1" > /etc/sysctl.d/99-sylvan.conf`. You can verify the setting with `cat /proc/sys/vm/overcommit_memory`. It should report `1`. diff --git a/resources/3rdparty/sylvan/configure.ac b/resources/3rdparty/sylvan/configure.ac index 4a9102b9d..5363e6daa 100644 --- a/resources/3rdparty/sylvan/configure.ac +++ b/resources/3rdparty/sylvan/configure.ac @@ -1,10 +1,11 @@ -AC_PREREQ([2.69]) +AC_PREREQ([2.60]) AC_INIT([sylvan], [1.0]) AC_CONFIG_MACRO_DIR([m4]) AC_CONFIG_AUX_DIR([tools]) AM_INIT_AUTOMAKE([foreign]) AC_PROG_CC +AX_CHECK_COMPILE_FLAG([-std=c11],,[AC_MSG_FAILURE([no acceptable C11 compiler found.])]) AC_PROG_CXX LT_INIT diff --git a/resources/3rdparty/sylvan/examples/CMakeLists.txt b/resources/3rdparty/sylvan/examples/CMakeLists.txt index 1029e0288..bb335935d 100644 --- a/resources/3rdparty/sylvan/examples/CMakeLists.txt +++ b/resources/3rdparty/sylvan/examples/CMakeLists.txt @@ -1,7 +1,5 @@ cmake_minimum_required(VERSION 2.6) -project(sylvan C) - -set(CMAKE_C_FLAGS "-g -O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11") +project(sylvan C CXX) include_directories(.) @@ -11,6 +9,9 @@ target_link_libraries(mc sylvan) add_executable(lddmc lddmc.c getrss.h getrss.c) target_link_libraries(lddmc sylvan) +add_executable(simple simple.cpp) +target_link_libraries(simple sylvan stdc++) + include(CheckIncludeFiles) check_include_files("gperftools/profiler.h" HAVE_PROFILER) diff --git a/resources/3rdparty/sylvan/examples/mc.c b/resources/3rdparty/sylvan/examples/mc.c index 4dd8b3554..2e7938fd9 100644 --- a/resources/3rdparty/sylvan/examples/mc.c +++ b/resources/3rdparty/sylvan/examples/mc.c @@ -274,7 +274,7 @@ VOID_TASK_1(par, set_t, set) size_t filled, total; sylvan_table_usage(&filled, &total); INFO("Level %d done, %'0.0f states explored, table: %0.1f%% full (%'zu nodes)\n", - iteration, sylvan_satcount_cached(visited, set->variables), + iteration, sylvan_satcount(visited, set->variables), 100.0*(double)filled/total, filled); } else if (report_table) { size_t filled, total; @@ -385,7 +385,7 @@ VOID_TASK_1(bfs, set_t, set) size_t filled, total; sylvan_table_usage(&filled, &total); INFO("Level %d done, %'0.0f states explored, table: %0.1f%% full (%'zu nodes)\n", - iteration, sylvan_satcount_cached(visited, set->variables), + iteration, sylvan_satcount(visited, set->variables), 100.0*(double)filled/total, filled); } else if (report_table) { size_t filled, total; @@ -605,7 +605,7 @@ main(int argc, char **argv) #endif // Now we just have states - INFO("Final states: %'0.0f states\n", sylvan_satcount_cached(states->bdd, states->variables)); + INFO("Final states: %'0.0f states\n", sylvan_satcount(states->bdd, states->variables)); if (report_nodes) { INFO("Final states: %'zu BDD nodes\n", sylvan_nodecount(states->bdd)); } diff --git a/resources/3rdparty/sylvan/examples/simple.cpp b/resources/3rdparty/sylvan/examples/simple.cpp new file mode 100644 index 000000000..22bd9eb8b --- /dev/null +++ b/resources/3rdparty/sylvan/examples/simple.cpp @@ -0,0 +1,121 @@ +#include +#include +#include + +#include +#include + +using namespace sylvan; + +VOID_TASK_0(simple_cxx) +{ + Bdd one = Bdd::bddOne(); // the True terminal + Bdd zero = Bdd::bddZero(); // the False terminal + + // check if they really are the True/False terminal + assert(one.GetBDD() == sylvan_true); + assert(zero.GetBDD() == sylvan_false); + + Bdd a = Bdd::bddVar(0); // create a BDD variable x_0 + Bdd b = Bdd::bddVar(1); // create a BDD variable x_1 + + // check if a really is the Boolean formula "x_0" + assert(!a.isConstant()); + assert(a.TopVar() == 0); + assert(a.Then() == one); + assert(a.Else() == zero); + + // check if b really is the Boolean formula "x_1" + assert(!b.isConstant()); + assert(b.TopVar() == 1); + assert(b.Then() == one); + assert(b.Else() == zero); + + // compute !a + Bdd not_a = !a; + + // check if !!a is really a + assert((!not_a) == a); + + // compute a * b and !(!a + !b) and check if they are equivalent + Bdd a_and_b = a * b; + Bdd not_not_a_or_not_b = !(!a + !b); + assert(a_and_b == not_not_a_or_not_b); + + // perform some simple quantification and check the results + Bdd ex = a_and_b.ExistAbstract(a); // \exists a . a * b + assert(ex == b); + Bdd andabs = a.AndAbstract(b, a); // \exists a . a * b using AndAbstract + assert(ex == andabs); + Bdd univ = a_and_b.UnivAbstract(a); // \forall a . a * b + assert(univ == zero); + + // alternative method to get the cube "ab" using bddCube + BddSet variables = a * b; + std::vector vec = {1, 1}; + assert(a_and_b == Bdd::bddCube(variables, vec)); + + // test the bddCube method for all combinations + assert((!a * !b) == Bdd::bddCube(variables, std::vector({0, 0}))); + assert((!a * b) == Bdd::bddCube(variables, std::vector({0, 1}))); + assert((!a) == Bdd::bddCube(variables, std::vector({0, 2}))); + assert((a * !b) == Bdd::bddCube(variables, std::vector({1, 0}))); + assert((a * b) == Bdd::bddCube(variables, std::vector({1, 1}))); + assert((a) == Bdd::bddCube(variables, std::vector({1, 2}))); + assert((!b) == Bdd::bddCube(variables, std::vector({2, 0}))); + assert((b) == Bdd::bddCube(variables, std::vector({2, 1}))); + assert(one == Bdd::bddCube(variables, std::vector({2, 2}))); +} + +VOID_TASK_1(_main, void*, arg) +{ + // Initialize Sylvan + // With starting size of the nodes table 1 << 21, and maximum size 1 << 27. + // With starting size of the cache table 1 << 20, and maximum size 1 << 20. + // Memory usage: 24 bytes per node, and 36 bytes per cache bucket + // - 1<<24 nodes: 384 MB + // - 1<<25 nodes: 768 MB + // - 1<<26 nodes: 1536 MB + // - 1<<27 nodes: 3072 MB + // - 1<<24 cache: 576 MB + // - 1<<25 cache: 1152 MB + // - 1<<26 cache: 2304 MB + // - 1<<27 cache: 4608 MB + sylvan_init_package(1LL<<22, 1LL<<26, 1LL<<22, 1LL<<26); + + // Initialize the BDD module with granularity 1 (cache every operation) + // A higher granularity (e.g. 6) often results in better performance in practice + sylvan_init_bdd(1); + + // Now we can do some simple stuff using the C++ objects. + CALL(simple_cxx); + + // Report statistics (if SYLVAN_STATS is 1 in the configuration) + sylvan_stats_report(stdout, 1); + + // And quit, freeing memory + sylvan_quit(); + + // We didn't use arg + (void)arg; +} + +int +main (int argc, char *argv[]) +{ + int n_workers = 0; // automatically detect number of workers + size_t deque_size = 0; // default value for the size of task deques for the workers + size_t program_stack_size = 0; // default value for the program stack of each pthread + + // Initialize the Lace framework for workers. + lace_init(n_workers, deque_size); + + // Spawn and start all worker pthreads; suspends current thread until done. + lace_startup(program_stack_size, TASK(_main), NULL); + + // The lace_startup command also exits Lace after _main is completed. + + return 0; + (void)argc; // unused variable + (void)argv; // unused variable +} diff --git a/resources/3rdparty/sylvan/m4/.gitignore b/resources/3rdparty/sylvan/m4/.gitignore index 5e7d2734c..5590b8bc5 100644 --- a/resources/3rdparty/sylvan/m4/.gitignore +++ b/resources/3rdparty/sylvan/m4/.gitignore @@ -1,4 +1,5 @@ # Ignore everything in this directory * -# Except this file +# Except: !.gitignore +!m4_ax_check_compile_flag.m4 diff --git a/resources/3rdparty/sylvan/m4/m4_ax_check_compile_flag.m4 b/resources/3rdparty/sylvan/m4/m4_ax_check_compile_flag.m4 new file mode 100644 index 000000000..c3a8d695a --- /dev/null +++ b/resources/3rdparty/sylvan/m4/m4_ax_check_compile_flag.m4 @@ -0,0 +1,72 @@ +# =========================================================================== +# http://www.gnu.org/software/autoconf-archive/ax_check_compile_flag.html +# =========================================================================== +# +# SYNOPSIS +# +# AX_CHECK_COMPILE_FLAG(FLAG, [ACTION-SUCCESS], [ACTION-FAILURE], [EXTRA-FLAGS]) +# +# DESCRIPTION +# +# Check whether the given FLAG works with the current language's compiler +# or gives an error. (Warnings, however, are ignored) +# +# ACTION-SUCCESS/ACTION-FAILURE are shell commands to execute on +# success/failure. +# +# If EXTRA-FLAGS is defined, it is added to the current language's default +# flags (e.g. CFLAGS) when the check is done. The check is thus made with +# the flags: "CFLAGS EXTRA-FLAGS FLAG". This can for example be used to +# force the compiler to issue an error when a bad flag is given. +# +# NOTE: Implementation based on AX_CFLAGS_GCC_OPTION. Please keep this +# macro in sync with AX_CHECK_{PREPROC,LINK}_FLAG. +# +# LICENSE +# +# Copyright (c) 2008 Guido U. Draheim +# Copyright (c) 2011 Maarten Bosmans +# +# This program is free software: you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by the +# Free Software Foundation, either version 3 of the License, or (at your +# option) any later version. +# +# This program is distributed in the hope that it will be useful, but +# WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General +# Public License for more details. +# +# You should have received a copy of the GNU General Public License along +# with this program. If not, see . +# +# As a special exception, the respective Autoconf Macro's copyright owner +# gives unlimited permission to copy, distribute and modify the configure +# scripts that are the output of Autoconf when processing the Macro. You +# need not follow the terms of the GNU General Public License when using +# or distributing such scripts, even though portions of the text of the +# Macro appear in them. The GNU General Public License (GPL) does govern +# all other use of the material that constitutes the Autoconf Macro. +# +# This special exception to the GPL applies to versions of the Autoconf +# Macro released by the Autoconf Archive. When you make and distribute a +# modified version of the Autoconf Macro, you may extend this special +# exception to the GPL to apply to your modified version as well. + +#serial 2 + +AC_DEFUN([AX_CHECK_COMPILE_FLAG], +[AC_PREREQ(2.59)dnl for _AC_LANG_PREFIX +AS_VAR_PUSHDEF([CACHEVAR],[ax_cv_check_[]_AC_LANG_ABBREV[]flags_$4_$1])dnl +AC_CACHE_CHECK([whether _AC_LANG compiler accepts $1], CACHEVAR, [ + ax_check_save_flags=$[]_AC_LANG_PREFIX[]FLAGS + _AC_LANG_PREFIX[]FLAGS="$[]_AC_LANG_PREFIX[]FLAGS $4 $1" + AC_COMPILE_IFELSE([AC_LANG_PROGRAM()], + [AS_VAR_SET(CACHEVAR,[yes])], + [AS_VAR_SET(CACHEVAR,[no])]) + _AC_LANG_PREFIX[]FLAGS=$ax_check_save_flags]) +AS_IF([test x"AS_VAR_GET(CACHEVAR)" = xyes], + [m4_default([$2], :)], + [m4_default([$3], :)]) +AS_VAR_POPDEF([CACHEVAR])dnl +])dnl AX_CHECK_COMPILE_FLAGS diff --git a/resources/3rdparty/sylvan/src/CMakeLists.txt b/resources/3rdparty/sylvan/src/CMakeLists.txt index f5105f9d3..50a645f22 100644 --- a/resources/3rdparty/sylvan/src/CMakeLists.txt +++ b/resources/3rdparty/sylvan/src/CMakeLists.txt @@ -1,8 +1,6 @@ cmake_minimum_required(VERSION 2.6) project(sylvan C CXX) -set(CMAKE_C_FLAGS "-g -O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11") - add_library(sylvan avl.h lace.h @@ -44,12 +42,24 @@ set_target_properties(sylvan PROPERTIES target_link_libraries(sylvan m pthread) -include(CheckIncludeFiles) -check_include_files(hwloc.h HAVE_HWLOC) +if(UNIX AND NOT APPLE) + target_link_libraries(sylvan rt) +endif() + +option(USE_HWLOC "Use HWLOC library if available" ON) + +if(USE_HWLOC) + include(CheckIncludeFiles) + check_include_files(hwloc.h HAVE_HWLOC) + if(HAVE_HWLOC) + set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "USE_HWLOC=1") + target_link_libraries(sylvan hwloc) + endif() +endif() -if(HAVE_HWLOC) - set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "USE_HWLOC=1") - target_link_libraries(sylvan hwloc) +option(SYLVAN_STATS "Collect statistics" OFF) +if(SYLVAN_STATS) + set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "SYLVAN_STATS") endif() install(TARGETS diff --git a/resources/3rdparty/sylvan/src/Makefile.am b/resources/3rdparty/sylvan/src/Makefile.am index 33a674dc7..5894c000f 100644 --- a/resources/3rdparty/sylvan/src/Makefile.am +++ b/resources/3rdparty/sylvan/src/Makefile.am @@ -26,6 +26,7 @@ libsylvan_la_SOURCES = \ sylvan_common.h \ sylvan_mtbdd.h \ sylvan_mtbdd.c \ + sylvan_mtbdd_int.h \ sylvan_obj.hpp \ sylvan_obj.cpp \ tls.h diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c index a49db4f8a..9a0b3cb82 100644 --- a/resources/3rdparty/sylvan/src/lace.c +++ b/resources/3rdparty/sylvan/src/lace.c @@ -14,7 +14,7 @@ * limitations under the License. */ -#include +#include // for errno #include // for sched_getaffinity #include // for fprintf #include // for memalign, malloc @@ -276,6 +276,11 @@ lace_init_worker(int worker, size_t dq_size) w->split = w->dq; w->allstolen = 0; w->worker = worker; +#if USE_HWLOC + w->pu = worker % n_pus; +#else + w->pu = -1; +#endif w->enabled = 1; if (workers_init[worker].stack != 0) { w->stack_trigger = ((size_t)workers_init[worker].stack) + workers_init[worker].stacksize/20; @@ -584,9 +589,9 @@ lace_spawn_worker(int worker, size_t stacksize, void* (*fun)(void*), void* arg) exit(1); } #else - void *stack_location = mmap(NULL, stacksize + pagesize, PROT_READ | PROT_WRITE, MAP_ANON | MAP_PRIVATE, 0, 0); + void *stack_location = mmap(NULL, stacksize + pagesize, PROT_READ | PROT_WRITE, MAP_ANON | MAP_PRIVATE, -1, 0); if (stack_location == MAP_FAILED) { - fprintf(stderr, "Lace error: Cannot allocate program stack, errno=%d!\n", errno); + fprintf(stderr, "Lace error: Cannot allocate program stack: %s!\n", strerror(errno)); exit(1); } #endif diff --git a/resources/3rdparty/sylvan/src/lace.h b/resources/3rdparty/sylvan/src/lace.h index a4f343ca8..8d6d1b645 100644 --- a/resources/3rdparty/sylvan/src/lace.h +++ b/resources/3rdparty/sylvan/src/lace.h @@ -182,7 +182,7 @@ struct __lace_common_fields_only { TASK_COMMON_FIELDS(_Task) }; #define LACE_COMMON_FIELD_SIZE sizeof(struct __lace_common_fields_only) typedef struct _Task { - TASK_COMMON_FIELDS(_Task) + TASK_COMMON_FIELDS(_Task); char p1[PAD(LACE_COMMON_FIELD_SIZE, P_SZ)]; char d[LACE_TASKSIZE]; char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)]; @@ -207,22 +207,23 @@ typedef struct _Worker { } Worker; typedef struct _WorkerP { - Task *dq; // same as dq - Task *split; // same as dq+ts.ts.split - Task *end; // dq+dq_size - Worker *_public; - size_t stack_trigger; // for stack overflow detection - int16_t worker; // what is my worker id? - uint8_t allstolen; // my allstolen - volatile int enabled; // if this worker is enabled + Task *dq; // same as dq + Task *split; // same as dq+ts.ts.split + Task *end; // dq+dq_size + Worker *_public; // pointer to public Worker struct + size_t stack_trigger; // for stack overflow detection + int16_t worker; // what is my worker id? + int16_t pu; // my pu (for HWLOC) + uint8_t allstolen; // my allstolen + volatile int8_t enabled; // if this worker is enabled #if LACE_COUNT_EVENTS - uint64_t ctr[CTR_MAX]; // counters + uint64_t ctr[CTR_MAX]; // counters volatile uint64_t time; volatile int level; #endif - uint32_t seed; // my random seed (for lace_steal_random) + uint32_t seed; // my random seed (for lace_steal_random) } WorkerP; #define LACE_TYPEDEF_CB(t, f, ...) typedef t (*f)(WorkerP *, Task *, ##__VA_ARGS__); @@ -338,6 +339,7 @@ void lace_exit(); #define NEWFRAME(f, ...) ( WRAP(f##_NEWFRAME, ##__VA_ARGS__) ) #define STEAL_RANDOM() ( CALL(lace_steal_random) ) #define LACE_WORKER_ID ( __lace_worker->worker ) +#define LACE_WORKER_PU ( __lace_worker->pu ) /* Use LACE_ME to initialize Lace variables, in case you want to call multiple Lace tasks */ #define LACE_ME WorkerP * __attribute__((unused)) __lace_worker = lace_get_worker(); Task * __attribute__((unused)) __lace_dq_head = lace_get_head(__lace_worker); diff --git a/resources/3rdparty/sylvan/src/llmsset.c b/resources/3rdparty/sylvan/src/llmsset.c index 3e1e54b6a..9c21f2e94 100644 --- a/resources/3rdparty/sylvan/src/llmsset.c +++ b/resources/3rdparty/sylvan/src/llmsset.c @@ -16,6 +16,7 @@ #include +#include // for errno #include // for uint64_t etc #include // for printf #include @@ -340,20 +341,20 @@ llmsset_create(size_t initial_size, size_t max_size) /* This implementation of "resizable hash table" allocates the max_size table in virtual memory, but only uses the "actual size" part in real memory */ - dbs->table = (uint64_t*)mmap(0, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); - dbs->data = (uint8_t*)mmap(0, dbs->max_size * 16, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); + dbs->table = (uint64_t*)mmap(0, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + dbs->data = (uint8_t*)mmap(0, dbs->max_size * 16, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); /* Also allocate bitmaps. Each region is 64*8 = 512 buckets. Overhead of bitmap1: 1 bit per 4096 bucket. Overhead of bitmap2: 1 bit per bucket. Overhead of bitmapc: 1 bit per bucket. */ - dbs->bitmap1 = (uint64_t*)mmap(0, dbs->max_size / (512*8), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); - dbs->bitmap2 = (uint64_t*)mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); - dbs->bitmapc = (uint64_t*)mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); + dbs->bitmap1 = (uint64_t*)mmap(0, dbs->max_size / (512*8), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + dbs->bitmap2 = (uint64_t*)mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + dbs->bitmapc = (uint64_t*)mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); if (dbs->table == (uint64_t*)-1 || dbs->data == (uint8_t*)-1 || dbs->bitmap1 == (uint64_t*)-1 || dbs->bitmap2 == (uint64_t*)-1 || dbs->bitmapc == (uint64_t*)-1) { - fprintf(stderr, "llmsset_create: Unable to allocate memory!\n"); + fprintf(stderr, "llmsset_create: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } diff --git a/resources/3rdparty/sylvan/src/llmsset.h b/resources/3rdparty/sylvan/src/llmsset.h index 34feefaf0..84c55e23b 100644 --- a/resources/3rdparty/sylvan/src/llmsset.h +++ b/resources/3rdparty/sylvan/src/llmsset.h @@ -14,13 +14,11 @@ * limitations under the License. */ -#include "sylvan_config.h" +#include #include #include -#include "lace.h" - -#include +#include #ifndef LLMSSET_H #define LLMSSET_H @@ -77,7 +75,6 @@ typedef struct llmsset /** * Retrieve a pointer to the data associated with the 42-bit value. */ - static inline void* llmsset_index_to_ptr(const llmsset_t dbs, size_t index) { diff --git a/resources/3rdparty/sylvan/src/refs.c b/resources/3rdparty/sylvan/src/refs.c index e13e6d5e6..0d6963bfe 100644 --- a/resources/3rdparty/sylvan/src/refs.c +++ b/resources/3rdparty/sylvan/src/refs.c @@ -17,9 +17,11 @@ #include #include // for assert +#include // for errno #include // for fprintf #include // for uint32_t etc #include // for exit +#include // for strerror #include // for mmap #include @@ -134,9 +136,9 @@ refs_resize(refs_table_t *tbl) if (count*4 > tbl->refs_size) new_size *= 2; // allocate new table - uint64_t *new_table = (uint64_t*)mmap(0, new_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, 0, 0); + uint64_t *new_table = (uint64_t*)mmap(0, new_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, -1, 0); if (new_table == (uint64_t*)-1) { - fprintf(stderr, "refs: Unable to allocate memory!\n"); + fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } @@ -312,9 +314,9 @@ refs_create(refs_table_t *tbl, size_t _refs_size) } tbl->refs_size = _refs_size; - tbl->refs_table = (uint64_t*)mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, 0, 0); + tbl->refs_table = (uint64_t*)mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, -1, 0); if (tbl->refs_table == (uint64_t*)-1) { - fprintf(stderr, "refs: Unable to allocate memory!\n"); + fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } } @@ -413,9 +415,9 @@ protect_resize(refs_table_t *tbl) if (count*4 > tbl->refs_size) new_size *= 2; // allocate new table - uint64_t *new_table = (uint64_t*)mmap(0, new_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, 0, 0); + uint64_t *new_table = (uint64_t*)mmap(0, new_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, -1, 0); if (new_table == (uint64_t*)-1) { - fprintf(stderr, "refs: Unable to allocate memory!\n"); + fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } @@ -581,9 +583,9 @@ protect_create(refs_table_t *tbl, size_t _refs_size) } tbl->refs_size = _refs_size; - tbl->refs_table = (uint64_t*)mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, 0, 0); + tbl->refs_table = (uint64_t*)mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, -1, 0); if (tbl->refs_table == (uint64_t*)-1) { - fprintf(stderr, "refs: Unable to allocate memory!\n"); + fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } } @@ -592,4 +594,5 @@ void protect_free(refs_table_t *tbl) { munmap(tbl->refs_table, tbl->refs_size * sizeof(uint64_t)); + tbl->refs_table = 0; } diff --git a/resources/3rdparty/sylvan/src/stats.c b/resources/3rdparty/sylvan/src/stats.c index 0f5394dbd..18ad5c088 100644 --- a/resources/3rdparty/sylvan/src/stats.c +++ b/resources/3rdparty/sylvan/src/stats.c @@ -14,18 +14,30 @@ * limitations under the License. */ +#include // for errno #include // memset #include #include #include #include // for nodes table +#if SYLVAN_STATS + #ifdef __ELF__ __thread sylvan_stats_t sylvan_stats; #else pthread_key_t sylvan_stats_key; #endif +#ifndef USE_HWLOC +#define USE_HWLOC 0 +#endif + +#if USE_HWLOC +#include +static hwloc_topology_t topo; +#endif + VOID_TASK_0(sylvan_stats_reset_perthread) { #ifdef __ELF__ @@ -38,8 +50,16 @@ VOID_TASK_0(sylvan_stats_reset_perthread) #else sylvan_stats_t *sylvan_stats = pthread_getspecific(sylvan_stats_key); if (sylvan_stats == NULL) { - sylvan_stats = mmap(0, sizeof(sylvan_stats_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, 0, 0); - // TODO: hwloc + sylvan_stats = mmap(0, sizeof(sylvan_stats_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANON, -1, 0); + if (sylvan_stats == (sylvan_stats_t *)-1) { + fprintf(stderr, "sylvan_stats: Unable to allocate memory: %s!\n", strerror(errno)); + exit(1); + } +#if USE_HWLOC + // Ensure the stats object is on our pu + hwloc_obj_t pu = hwloc_get_obj_by_type(topo, HWLOC_OBJ_PU, LACE_WORKER_PU); + hwloc_set_area_membind(topo, sylvan_stats, sizeof(sylvan_stats_t), pu->cpuset, HWLOC_MEMBIND_BIND, 0); +#endif pthread_setspecific(sylvan_stats_key, sylvan_stats); } for (int i=0; i +#include #ifndef SYLVAN_STATS_H #define SYLVAN_STATS_H @@ -127,6 +127,9 @@ typedef enum SYLVAN_TIMER_COUNTER } Sylvan_Timers; +/** + * Initialize stats system (done by sylvan_init_package) + */ #define sylvan_stats_init() CALL(sylvan_stats_init) VOID_TASK_DECL_0(sylvan_stats_init) @@ -141,6 +144,8 @@ VOID_TASK_DECL_0(sylvan_stats_reset) */ void sylvan_stats_report(FILE* target, int color); +#if SYLVAN_STATS + /* Infrastructure for internal markings */ typedef struct { @@ -149,8 +154,6 @@ typedef struct uint64_t timers_startstop[SYLVAN_TIMER_COUNTER]; } sylvan_stats_t; -#if SYLVAN_STATS - #ifdef __MACH__ #include #define getabstime() mach_absolute_time() diff --git a/resources/3rdparty/sylvan/src/sylvan.h b/resources/3rdparty/sylvan/src/sylvan.h index 3b490993a..6fe09f9d6 100644 --- a/resources/3rdparty/sylvan/src/sylvan.h +++ b/resources/3rdparty/sylvan/src/sylvan.h @@ -35,16 +35,16 @@ * To temporarily disable garbage collection, use sylvan_gc_disable() and sylvan_gc_enable(). */ -#include "sylvan_config.h" +#include #include #include // for FILE #include -#include "lace.h" // for definitions +#include // for definitions -#include "sylvan_cache.h" -#include "llmsset.h" -#include "stats.h" +#include +#include +#include #ifndef SYLVAN_H #define SYLVAN_H @@ -175,8 +175,8 @@ extern llmsset_t nodes; } #endif /* __cplusplus */ -#include "sylvan_bdd.h" -#include "sylvan_ldd.h" -#include "sylvan_mtbdd.h" +#include +#include +#include #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.c b/resources/3rdparty/sylvan/src/sylvan_bdd.c index 37b154534..74936a62d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.c @@ -148,7 +148,7 @@ sylvan_protect(BDD *a) void sylvan_unprotect(BDD *a) { - protect_down(&bdd_protected, (size_t)a); + if (bdd_protected.refs_table != NULL) protect_down(&bdd_protected, (size_t)a); } size_t @@ -2446,7 +2446,7 @@ sylvan_fprintdot(FILE *out, BDD bdd) fprintf(out, "graph [dpi = 300];\n"); fprintf(out, "center = true;\n"); fprintf(out, "edge [dir = forward];\n"); - fprintf(out, "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n"); + fprintf(out, "0 [label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n"); fprintf(out, "root [style=invis];\n"); fprintf(out, "root -> \"%" PRIx64 "\" [style=solid dir=both arrowtail=%s];\n", BDD_STRIPMARK(bdd), BDD_HASMARK(bdd) ? "dot" : "none"); @@ -2487,7 +2487,7 @@ sylvan_fprintdot_nc_rec(FILE *out, BDD bdd, avl_node_t **levels) BDD low = sylvan_low(bdd); BDD high = sylvan_high(bdd); - fprintf(out, "\"%" PRIx64 " [label=\"%d\"];\n", bdd, sylvan_var(bdd)); + fprintf(out, "\"%" PRIx64 "\" [label=\"%d\"];\n", bdd, sylvan_var(bdd)); fprintf(out, "\"%" PRIx64 "\" -> \"%" PRIx64 "\" [style=dashed];\n", bdd, low); fprintf(out, "\"%" PRIx64 "\" -> \"%" PRIx64 "\" [style=solid];\n", bdd, high); sylvan_fprintdot_nc_rec(out, low, levels); diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.h b/resources/3rdparty/sylvan/src/sylvan_bdd.h index 96566e63e..6cd4ef584 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.h @@ -414,7 +414,7 @@ bdd_refs_sync(BDD result) return result; } -#include "sylvan_bdd_storm.h" +#include "sylvan_bdd_storm.h" #ifdef __cplusplus } diff --git a/resources/3rdparty/sylvan/src/sylvan_cache.c b/resources/3rdparty/sylvan/src/sylvan_cache.c index 55f29f555..7bfb72afd 100644 --- a/resources/3rdparty/sylvan/src/sylvan_cache.c +++ b/resources/3rdparty/sylvan/src/sylvan_cache.c @@ -14,9 +14,11 @@ * limitations under the License. */ +#include // for errno #include // for fprintf #include // for uint32_t etc #include // for exit +#include // for strerror #include // for mmap #include @@ -159,11 +161,11 @@ cache_create(size_t _cache_size, size_t _max_size) exit(1); } - cache_table = (cache_entry_t)mmap(0, cache_max * sizeof(struct cache_entry), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); - cache_status = (uint32_t*)mmap(0, cache_max * sizeof(uint32_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, 0, 0); + cache_table = (cache_entry_t)mmap(0, cache_max * sizeof(struct cache_entry), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + cache_status = (uint32_t*)mmap(0, cache_max * sizeof(uint32_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); if (cache_table == (cache_entry_t)-1 || cache_status == (uint32_t*)-1) { - fprintf(stderr, "cache_create: Unable to allocate memory!\n"); + fprintf(stderr, "cache_create: Unable to allocate memory: %s!\n", strerror(errno)); exit(1); } diff --git a/resources/3rdparty/sylvan/src/sylvan_cache.h b/resources/3rdparty/sylvan/src/sylvan_cache.h index 9555c3e58..babc74f65 100644 --- a/resources/3rdparty/sylvan/src/sylvan_cache.h +++ b/resources/3rdparty/sylvan/src/sylvan_cache.h @@ -1,6 +1,6 @@ #include // for uint32_t etc -#include "sylvan_config.h" +#include #ifndef CACHE_H #define CACHE_H diff --git a/resources/3rdparty/sylvan/src/sylvan_gmp.h b/resources/3rdparty/sylvan/src/sylvan_gmp.h index 9650c56d3..fbf6bc2ad 100644 --- a/resources/3rdparty/sylvan/src/sylvan_gmp.h +++ b/resources/3rdparty/sylvan/src/sylvan_gmp.h @@ -21,7 +21,7 @@ #ifndef SYLVAN_GMP_H #define SYLVAN_GMP_H -#include "sylvan.h" +#include #include #ifdef __cplusplus diff --git a/resources/3rdparty/sylvan/src/sylvan_ldd.c b/resources/3rdparty/sylvan/src/sylvan_ldd.c index 2bd10c5ba..814b7e61c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_ldd.c +++ b/resources/3rdparty/sylvan/src/sylvan_ldd.c @@ -44,61 +44,61 @@ typedef struct __attribute__((packed)) mddnode { // Ensure our mddnode is 16 bytes typedef char __lddmc_check_mddnode_t_is_16_bytes[(sizeof(struct mddnode)==16) ? 1 : -1]; -inline uint32_t +static inline uint32_t __attribute__((unused)) mddnode_getvalue(mddnode_t n) { return *(uint32_t*)((uint8_t*)n+6); } -inline uint8_t +static inline uint8_t __attribute__((unused)) mddnode_getmark(mddnode_t n) { return n->a & 1; } -inline uint8_t +static inline uint8_t __attribute__((unused)) mddnode_getcopy(mddnode_t n) { return n->b & 0x10000 ? 1 : 0; } -inline uint64_t +static inline uint64_t __attribute__((unused)) mddnode_getright(mddnode_t n) { return (n->a & 0x0000ffffffffffff) >> 1; } -inline uint64_t +static inline uint64_t __attribute__((unused)) mddnode_getdown(mddnode_t n) { return n->b >> 17; } -inline void +static inline void __attribute__((unused)) mddnode_setvalue(mddnode_t n, uint32_t value) { *(uint32_t*)((uint8_t*)n+6) = value; } -inline void +static inline void __attribute__((unused)) mddnode_setmark(mddnode_t n, uint8_t mark) { n->a = (n->a & 0xfffffffffffffffe) | (mark ? 1 : 0); } -inline void +static inline void __attribute__((unused)) mddnode_setright(mddnode_t n, uint64_t right) { n->a = (n->a & 0xffff000000000001) | (right << 1); } -inline void +static inline void __attribute__((unused)) mddnode_setdown(mddnode_t n, uint64_t down) { n->b = (n->b & 0x000000000001ffff) | (down << 16); } -inline void +static inline void __attribute__((unused)) mddnode_make(mddnode_t n, uint32_t value, uint64_t right, uint64_t down) { n->a = right << 1; @@ -106,7 +106,7 @@ mddnode_make(mddnode_t n, uint32_t value, uint64_t right, uint64_t down) *(uint32_t*)((uint8_t*)n+6) = value; } -inline void +static inline void __attribute__((unused)) mddnode_makecopy(mddnode_t n, uint64_t right, uint64_t down) { n->a = right << 1; @@ -1461,6 +1461,8 @@ TASK_IMPL_4(MDD, lddmc_join, MDD, a, MDD, b, MDD, a_proj, MDD, b_proj) uint32_t val; MDD down; + // Make copies (for cache) + MDD _a_proj = a_proj, _b_proj = b_proj; if (keep_a) { if (keep_b) { val = mddnode_getvalue(nb); @@ -1489,7 +1491,7 @@ TASK_IMPL_4(MDD, lddmc_join, MDD, a, MDD, b, MDD, a_proj, MDD, b_proj) result = lddmc_makenode(val, down, right); /* Write to cache */ - if (cache_put4(CACHE_MDD_JOIN, a, b, a_proj, b_proj, result)) sylvan_stats_count(LDD_JOIN_CACHEDPUT); + if (cache_put4(CACHE_MDD_JOIN, a, b, _a_proj, _b_proj, result)) sylvan_stats_count(LDD_JOIN_CACHEDPUT); return result; } diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 87db4c84b..a4eb1bd62 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -150,7 +150,7 @@ mtbdd_protect(MTBDD *a) void mtbdd_unprotect(MTBDD *a) { - protect_down(&mtbdd_protected, (size_t)a); + if (mtbdd_protected.refs_table != NULL) protect_down(&mtbdd_protected, (size_t)a); } size_t @@ -1434,8 +1434,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho if (result != SYNC(mtbdd_equal_norm_d2)) result = mtbdd_false; if (result == mtbdd_false) *shortcircuit = 1; - /* Store in cache (only if we are not short circuiting) */ - if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result); + /* Store in cache */ + cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result); return result; } @@ -1470,7 +1470,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, // assume Double MTBDD double va = mtbdd_getdouble(a); double vb = mtbdd_getdouble(b); - if (va == 0.0 || va == -0.0) return mtbdd_false; + if (va == 0) return mtbdd_false; va = (va - vb) / va; if (va < 0) va = -va; return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false; @@ -1501,8 +1501,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, if (result != SYNC(mtbdd_equal_norm_rel_d2)) result = mtbdd_false; if (result == mtbdd_false) *shortcircuit = 1; - /* Store in cache (only if we are not short circuiting) */ - if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result); + /* Store in cache */ + cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result); return result; } @@ -2540,4 +2540,3 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables) } #include "sylvan_mtbdd_storm.c" - diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 07a232626..a573c7a49 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -1037,4 +1037,3 @@ Sylvan::quitPackage() } #include "sylvan_obj_storm.cpp" - diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 4ae849dad..e7f77f6ca 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -28,7 +28,7 @@ namespace sylvan { class BddSet; class BddMap; class Mtbdd; - + class Bdd { friend class Sylvan; friend class BddSet; @@ -326,7 +326,7 @@ public: size_t NodeCount() const; #include "sylvan_obj_bdd_storm.hpp" - + private: BDD bdd; }; @@ -776,7 +776,7 @@ public: size_t NodeCount() const; #include "sylvan_obj_mtbdd_storm.hpp" - + private: MTBDD mtbdd; }; diff --git a/resources/3rdparty/sylvan/test/CMakeLists.txt b/resources/3rdparty/sylvan/test/CMakeLists.txt index 50fc616dc..a331904e8 100644 --- a/resources/3rdparty/sylvan/test/CMakeLists.txt +++ b/resources/3rdparty/sylvan/test/CMakeLists.txt @@ -1,8 +1,15 @@ cmake_minimum_required(VERSION 2.6) project(sylvan C CXX) +enable_testing() add_executable(sylvan_test main.c) target_link_libraries(sylvan_test sylvan) +add_executable(test_basic test_basic.c) +target_link_libraries(test_basic sylvan) + add_executable(test_cxx test_cxx.cpp) target_link_libraries(test_cxx sylvan stdc++) + +add_test(test_cxx test_cxx) +add_test(test_basic test_basic) diff --git a/resources/3rdparty/sylvan/test/main.c b/resources/3rdparty/sylvan/test/main.c index 37bdee989..941f60d2c 100644 --- a/resources/3rdparty/sylvan/test/main.c +++ b/resources/3rdparty/sylvan/test/main.c @@ -10,6 +10,7 @@ #include #include +#include "test_assert.h" #include "llmsset.h" #include "sylvan.h" @@ -94,271 +95,6 @@ make_random(int i, int j) return result; } - -void testFun(BDD p1, BDD p2, BDD r1, BDD r2) -{ - if (r1 == r2) return; - - printf("Parameter 1:\n"); - fflush(stdout); - sylvan_printdot(p1); - sylvan_print(p1);printf("\n"); - - printf("Parameter 2:\n"); - fflush(stdout); - sylvan_printdot(p2); - sylvan_print(p2);printf("\n"); - - printf("Result 1:\n"); - fflush(stdout); - sylvan_printdot(r1); - - printf("Result 2:\n"); - fflush(stdout); - sylvan_printdot(r2); - - assert(0); -} - -int testEqual(BDD a, BDD b) -{ - if (a == b) return 1; - - if (a == sylvan_invalid) { - printf("a is invalid!\n"); - return 0; - } - - if (b == sylvan_invalid) { - printf("b is invalid!\n"); - return 0; - } - - printf("Not Equal!\n"); - fflush(stdout); - - sylvan_print(a);printf("\n"); - sylvan_print(b);printf("\n"); - - return 0; -} - -void -test_bdd() -{ - sylvan_gc_disable(); - - assert(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_true) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_false))); - assert(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_true) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_false))); - assert(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_false) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_true))); - assert(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_false) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_true))); - - sylvan_gc_enable(); -} - -void -test_cube() -{ - LACE_ME; - BDDSET vars = sylvan_set_fromarray(((BDDVAR[]){1,2,3,4,6,8}), 6); - - uint8_t cube[6], check[6]; - int i, j; - for (i=0;i<6;i++) cube[i] = rng(0,3); - BDD bdd = sylvan_cube(vars, cube); - - sylvan_sat_one(bdd, vars, check); - for (i=0; i<6;i++) assert(cube[i] == check[i] || cube[i] == 2 && check[i] == 0); - - BDD picked = sylvan_pick_cube(bdd); - assert(testEqual(sylvan_and(picked, bdd), picked)); - - BDD t1 = sylvan_cube(vars, ((uint8_t[]){1,1,2,2,0,0})); - BDD t2 = sylvan_cube(vars, ((uint8_t[]){1,1,1,0,0,2})); - assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){1,1,1,0,0,2})), sylvan_or(t1, t2))); - t2 = sylvan_cube(vars, ((uint8_t[]){2,2,2,1,1,0})); - assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){2,2,2,1,1,0})), sylvan_or(t1, t2))); - t2 = sylvan_cube(vars, ((uint8_t[]){1,1,1,0,0,0})); - assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){1,1,1,0,0,0})), sylvan_or(t1, t2))); - - sylvan_gc_disable(); - bdd = make_random(1, 16); - for (j=0;j<10;j++) { - for (i=0;i<6;i++) cube[i] = rng(0,3); - BDD c = sylvan_cube(vars, cube); - assert(sylvan_union_cube(bdd, vars, cube) == sylvan_or(bdd, c)); - } - - for (i=0;i<10;i++) { - picked = sylvan_pick_cube(bdd); - assert(testEqual(sylvan_and(picked, bdd), picked)); - } - sylvan_gc_enable(); -} - -static void -test_operators() -{ - // We need to test: xor, and, or, nand, nor, imp, biimp, invimp, diff, less - sylvan_gc_disable(); - - LACE_ME; - - //int i; - BDD a = sylvan_ithvar(1); - BDD b = sylvan_ithvar(2); - BDD one = make_random(1, 12); - BDD two = make_random(6, 24); - - // Test or - assert(testEqual(sylvan_or(a, b), sylvan_makenode(1, b, sylvan_true))); - assert(testEqual(sylvan_or(a, b), sylvan_or(b, a))); - assert(testEqual(sylvan_or(one, two), sylvan_or(two, one))); - - // Test and - assert(testEqual(sylvan_and(a, b), sylvan_makenode(1, sylvan_false, b))); - assert(testEqual(sylvan_and(a, b), sylvan_and(b, a))); - assert(testEqual(sylvan_and(one, two), sylvan_and(two, one))); - - // Test xor - assert(testEqual(sylvan_xor(a, b), sylvan_makenode(1, b, sylvan_not(b)))); - assert(testEqual(sylvan_xor(a, b), sylvan_xor(a, b))); - assert(testEqual(sylvan_xor(a, b), sylvan_xor(b, a))); - assert(testEqual(sylvan_xor(one, two), sylvan_xor(two, one))); - assert(testEqual(sylvan_xor(a, b), sylvan_ite(a, sylvan_not(b), b))); - - // Test diff - assert(testEqual(sylvan_diff(a, b), sylvan_diff(a, b))); - assert(testEqual(sylvan_diff(a, b), sylvan_diff(a, sylvan_and(a, b)))); - assert(testEqual(sylvan_diff(a, b), sylvan_and(a, sylvan_not(b)))); - assert(testEqual(sylvan_diff(a, b), sylvan_ite(b, sylvan_false, a))); - assert(testEqual(sylvan_diff(one, two), sylvan_diff(one, two))); - assert(testEqual(sylvan_diff(one, two), sylvan_diff(one, sylvan_and(one, two)))); - assert(testEqual(sylvan_diff(one, two), sylvan_and(one, sylvan_not(two)))); - assert(testEqual(sylvan_diff(one, two), sylvan_ite(two, sylvan_false, one))); - - // Test biimp - assert(testEqual(sylvan_biimp(a, b), sylvan_makenode(1, sylvan_not(b), b))); - assert(testEqual(sylvan_biimp(a, b), sylvan_biimp(b, a))); - assert(testEqual(sylvan_biimp(one, two), sylvan_biimp(two, one))); - - // Test nand / and - assert(testEqual(sylvan_not(sylvan_and(a, b)), sylvan_nand(b, a))); - assert(testEqual(sylvan_not(sylvan_and(one, two)), sylvan_nand(two, one))); - - // Test nor / or - assert(testEqual(sylvan_not(sylvan_or(a, b)), sylvan_nor(b, a))); - assert(testEqual(sylvan_not(sylvan_or(one, two)), sylvan_nor(two, one))); - - // Test xor / biimp - assert(testEqual(sylvan_xor(a, b), sylvan_not(sylvan_biimp(b, a)))); - assert(testEqual(sylvan_xor(one, two), sylvan_not(sylvan_biimp(two, one)))); - - // Test imp - assert(testEqual(sylvan_imp(a, b), sylvan_ite(a, b, sylvan_true))); - assert(testEqual(sylvan_imp(one, two), sylvan_ite(one, two, sylvan_true))); - assert(testEqual(sylvan_imp(one, two), sylvan_not(sylvan_diff(one, two)))); - assert(testEqual(sylvan_invimp(one, two), sylvan_not(sylvan_less(one, two)))); - assert(testEqual(sylvan_imp(a, b), sylvan_invimp(b, a))); - assert(testEqual(sylvan_imp(one, two), sylvan_invimp(two, one))); - - // Test constrain, exists and forall - - sylvan_gc_enable(); -} - -static void -test_relprod() -{ - LACE_ME; - - sylvan_gc_disable(); - - BDDVAR vars[] = {0,2,4}; - BDDVAR all_vars[] = {0,1,2,3,4,5}; - - BDDSET vars_set = sylvan_set_fromarray(vars, 3); - BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6); - - BDD s, t, next, prev; - BDD zeroes, ones; - - // transition relation: 000 --> 111 and !000 --> 000 - t = sylvan_false; - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1})); - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0})); - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,2,0,1,0})); - - s = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); - zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - ones = sylvan_cube(vars_set, (uint8_t[]){1,1,1}); - - next = sylvan_relnext(s, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - assert(next == zeroes); - assert(prev == sylvan_not(zeroes)); - - next = sylvan_relnext(next, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - assert(next == ones); - assert(prev == zeroes); - - t = sylvan_cube(all_vars_set, (uint8_t[]){0,0,0,0,0,1}); - assert(sylvan_relprev(t, s, all_vars_set) == zeroes); - assert(sylvan_relprev(t, sylvan_not(s), all_vars_set) == sylvan_false); - assert(sylvan_relnext(s, t, all_vars_set) == sylvan_false); - assert(sylvan_relnext(zeroes, t, all_vars_set) == s); - - t = sylvan_cube(all_vars_set, (uint8_t[]){0,0,0,0,0,2}); - assert(sylvan_relprev(t, s, all_vars_set) == zeroes); - assert(sylvan_relprev(t, zeroes, all_vars_set) == zeroes); - assert(sylvan_relnext(sylvan_not(zeroes), t, all_vars_set) == sylvan_false); - - sylvan_gc_enable(); -} - -static void -test_compose() -{ - sylvan_gc_disable(); - - LACE_ME; - - BDD a = sylvan_ithvar(1); - BDD b = sylvan_ithvar(2); - - BDD a_or_b = sylvan_or(a, b); - - BDD one = make_random(3, 16); - BDD two = make_random(8, 24); - - BDDMAP map = sylvan_map_empty(); - - map = sylvan_map_add(map, 1, one); - map = sylvan_map_add(map, 2, two); - - assert(sylvan_map_key(map) == 1); - assert(sylvan_map_value(map) == one); - assert(sylvan_map_key(sylvan_map_next(map)) == 2); - assert(sylvan_map_value(sylvan_map_next(map)) == two); - - assert(testEqual(one, sylvan_compose(a, map))); - assert(testEqual(two, sylvan_compose(b, map))); - - assert(testEqual(sylvan_or(one, two), sylvan_compose(a_or_b, map))); - - map = sylvan_map_add(map, 2, one); - assert(testEqual(sylvan_compose(a_or_b, map), one)); - - map = sylvan_map_add(map, 1, two); - assert(testEqual(sylvan_or(one, two), sylvan_compose(a_or_b, map))); - - assert(testEqual(sylvan_and(one, two), sylvan_compose(sylvan_and(a, b), map))); - - sylvan_gc_enable(); -} - /** GC testing */ VOID_TASK_2(gctest_fill, int, levels, int, width) { @@ -381,7 +117,7 @@ void report_table() printf("done, table: %0.1f%% full (%zu nodes).\n", 100.0*(double)filled/total, filled); } -void test_gc(int threads) +int test_gc(int threads) { LACE_ME; int N_canaries = 16; @@ -396,16 +132,17 @@ void test_gc(int threads) sylvan_getsha(canaries[i], hashes[i]); sylvan_test_isbdd(canaries[i]); } - assert(sylvan_count_refs() == (size_t)N_canaries); + test_assert(sylvan_count_refs() == (size_t)N_canaries); for (j=0;j<10*threads;j++) { CALL(gctest_fill, 6, 5); for (i=0;i 1) sscanf(argv[1], "%d", &threads); - runtests(threads); + if (runtests(threads)) exit(1); printf(NC); exit(0); } diff --git a/resources/3rdparty/sylvan/test/test_assert.h b/resources/3rdparty/sylvan/test/test_assert.h new file mode 100644 index 000000000..8cd18501a --- /dev/null +++ b/resources/3rdparty/sylvan/test/test_assert.h @@ -0,0 +1,13 @@ +#ifndef test_assert +#define test_assert(expr) do { \ + if (!(expr)) \ + { \ + fprintf(stderr, \ + "file %s: line %d (%s): precondition `%s' failed.\n", \ + __FILE__, \ + __LINE__, \ + __PRETTY_FUNCTION__, \ + #expr); \ + return 1; \ + } } while(0) +#endif diff --git a/resources/3rdparty/sylvan/test/test_basic.c b/resources/3rdparty/sylvan/test/test_basic.c new file mode 100644 index 000000000..f6cffcc15 --- /dev/null +++ b/resources/3rdparty/sylvan/test/test_basic.c @@ -0,0 +1,331 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "llmsset.h" +#include "sylvan.h" +#include "test_assert.h" + +__thread uint64_t seed = 1; + +uint64_t +xorshift_rand(void) +{ + uint64_t x = seed; + if (seed == 0) seed = rand(); + x ^= x >> 12; + x ^= x << 25; + x ^= x >> 27; + seed = x; + return x * 2685821657736338717LL; +} + +double +uniform_deviate(uint64_t seed) +{ + return seed * (1.0 / (0xffffffffffffffffL + 1.0)); +} + +int +rng(int low, int high) +{ + return low + uniform_deviate(xorshift_rand()) * (high-low); +} + +static inline BDD +make_random(int i, int j) +{ + if (i == j) return rng(0, 2) ? sylvan_true : sylvan_false; + + BDD yes = make_random(i+1, j); + BDD no = make_random(i+1, j); + BDD result = sylvan_invalid; + + switch(rng(0, 4)) { + case 0: + result = no; + sylvan_deref(yes); + break; + case 1: + result = yes; + sylvan_deref(no); + break; + case 2: + result = sylvan_ref(sylvan_makenode(i, yes, no)); + sylvan_deref(no); + sylvan_deref(yes); + break; + case 3: + default: + result = sylvan_ref(sylvan_makenode(i, no, yes)); + sylvan_deref(no); + sylvan_deref(yes); + break; + } + + return result; +} + +int testEqual(BDD a, BDD b) +{ + if (a == b) return 1; + + if (a == sylvan_invalid) { + fprintf(stderr, "a is invalid!\n"); + return 0; + } + + if (b == sylvan_invalid) { + fprintf(stderr, "b is invalid!\n"); + return 0; + } + + fprintf(stderr, "a and b are not equal!\n"); + + sylvan_fprint(stderr, a);fprintf(stderr, "\n"); + sylvan_fprint(stderr, b);fprintf(stderr, "\n"); + + return 0; +} + +int +test_bdd() +{ + test_assert(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_true) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_false))); + test_assert(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_true) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_false))); + test_assert(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_false) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_true))); + test_assert(sylvan_makenode(sylvan_ithvar(1), sylvan_false, sylvan_false) == sylvan_not(sylvan_makenode(sylvan_ithvar(1), sylvan_true, sylvan_true))); + + return 0; +} + +int +test_cube() +{ + LACE_ME; + BDDSET vars = sylvan_set_fromarray(((BDDVAR[]){1,2,3,4,6,8}), 6); + + uint8_t cube[6], check[6]; + int i, j; + for (i=0;i<6;i++) cube[i] = rng(0,3); + BDD bdd = sylvan_cube(vars, cube); + + sylvan_sat_one(bdd, vars, check); + for (i=0; i<6;i++) test_assert(cube[i] == check[i] || (cube[i] == 2 && check[i] == 0)); + + BDD picked = sylvan_pick_cube(bdd); + test_assert(testEqual(sylvan_and(picked, bdd), picked)); + + BDD t1 = sylvan_cube(vars, ((uint8_t[]){1,1,2,2,0,0})); + BDD t2 = sylvan_cube(vars, ((uint8_t[]){1,1,1,0,0,2})); + test_assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){1,1,1,0,0,2})), sylvan_or(t1, t2))); + t2 = sylvan_cube(vars, ((uint8_t[]){2,2,2,1,1,0})); + test_assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){2,2,2,1,1,0})), sylvan_or(t1, t2))); + t2 = sylvan_cube(vars, ((uint8_t[]){1,1,1,0,0,0})); + test_assert(testEqual(sylvan_union_cube(t1, vars, ((uint8_t[]){1,1,1,0,0,0})), sylvan_or(t1, t2))); + + bdd = make_random(1, 16); + for (j=0;j<10;j++) { + for (i=0;i<6;i++) cube[i] = rng(0,3); + BDD c = sylvan_cube(vars, cube); + test_assert(sylvan_union_cube(bdd, vars, cube) == sylvan_or(bdd, c)); + } + + for (i=0;i<10;i++) { + picked = sylvan_pick_cube(bdd); + test_assert(testEqual(sylvan_and(picked, bdd), picked)); + } + return 0; +} + +static int +test_operators() +{ + // We need to test: xor, and, or, nand, nor, imp, biimp, invimp, diff, less + LACE_ME; + + //int i; + BDD a = sylvan_ithvar(1); + BDD b = sylvan_ithvar(2); + BDD one = make_random(1, 12); + BDD two = make_random(6, 24); + + // Test or + test_assert(testEqual(sylvan_or(a, b), sylvan_makenode(1, b, sylvan_true))); + test_assert(testEqual(sylvan_or(a, b), sylvan_or(b, a))); + test_assert(testEqual(sylvan_or(one, two), sylvan_or(two, one))); + + // Test and + test_assert(testEqual(sylvan_and(a, b), sylvan_makenode(1, sylvan_false, b))); + test_assert(testEqual(sylvan_and(a, b), sylvan_and(b, a))); + test_assert(testEqual(sylvan_and(one, two), sylvan_and(two, one))); + + // Test xor + test_assert(testEqual(sylvan_xor(a, b), sylvan_makenode(1, b, sylvan_not(b)))); + test_assert(testEqual(sylvan_xor(a, b), sylvan_xor(a, b))); + test_assert(testEqual(sylvan_xor(a, b), sylvan_xor(b, a))); + test_assert(testEqual(sylvan_xor(one, two), sylvan_xor(two, one))); + test_assert(testEqual(sylvan_xor(a, b), sylvan_ite(a, sylvan_not(b), b))); + + // Test diff + test_assert(testEqual(sylvan_diff(a, b), sylvan_diff(a, b))); + test_assert(testEqual(sylvan_diff(a, b), sylvan_diff(a, sylvan_and(a, b)))); + test_assert(testEqual(sylvan_diff(a, b), sylvan_and(a, sylvan_not(b)))); + test_assert(testEqual(sylvan_diff(a, b), sylvan_ite(b, sylvan_false, a))); + test_assert(testEqual(sylvan_diff(one, two), sylvan_diff(one, two))); + test_assert(testEqual(sylvan_diff(one, two), sylvan_diff(one, sylvan_and(one, two)))); + test_assert(testEqual(sylvan_diff(one, two), sylvan_and(one, sylvan_not(two)))); + test_assert(testEqual(sylvan_diff(one, two), sylvan_ite(two, sylvan_false, one))); + + // Test biimp + test_assert(testEqual(sylvan_biimp(a, b), sylvan_makenode(1, sylvan_not(b), b))); + test_assert(testEqual(sylvan_biimp(a, b), sylvan_biimp(b, a))); + test_assert(testEqual(sylvan_biimp(one, two), sylvan_biimp(two, one))); + + // Test nand / and + test_assert(testEqual(sylvan_not(sylvan_and(a, b)), sylvan_nand(b, a))); + test_assert(testEqual(sylvan_not(sylvan_and(one, two)), sylvan_nand(two, one))); + + // Test nor / or + test_assert(testEqual(sylvan_not(sylvan_or(a, b)), sylvan_nor(b, a))); + test_assert(testEqual(sylvan_not(sylvan_or(one, two)), sylvan_nor(two, one))); + + // Test xor / biimp + test_assert(testEqual(sylvan_xor(a, b), sylvan_not(sylvan_biimp(b, a)))); + test_assert(testEqual(sylvan_xor(one, two), sylvan_not(sylvan_biimp(two, one)))); + + // Test imp + test_assert(testEqual(sylvan_imp(a, b), sylvan_ite(a, b, sylvan_true))); + test_assert(testEqual(sylvan_imp(one, two), sylvan_ite(one, two, sylvan_true))); + test_assert(testEqual(sylvan_imp(one, two), sylvan_not(sylvan_diff(one, two)))); + test_assert(testEqual(sylvan_invimp(one, two), sylvan_not(sylvan_less(one, two)))); + test_assert(testEqual(sylvan_imp(a, b), sylvan_invimp(b, a))); + test_assert(testEqual(sylvan_imp(one, two), sylvan_invimp(two, one))); + + return 0; +} + +int +test_relprod() +{ + LACE_ME; + + BDDVAR vars[] = {0,2,4}; + BDDVAR all_vars[] = {0,1,2,3,4,5}; + + BDDSET vars_set = sylvan_set_fromarray(vars, 3); + BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6); + + BDD s, t, next, prev; + BDD zeroes, ones; + + // transition relation: 000 --> 111 and !000 --> 000 + t = sylvan_false; + t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1})); + t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); + t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0})); + t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,2,0,1,0})); + + s = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); + zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); + ones = sylvan_cube(vars_set, (uint8_t[]){1,1,1}); + + next = sylvan_relnext(s, t, all_vars_set); + prev = sylvan_relprev(t, next, all_vars_set); + test_assert(next == zeroes); + test_assert(prev == sylvan_not(zeroes)); + + next = sylvan_relnext(next, t, all_vars_set); + prev = sylvan_relprev(t, next, all_vars_set); + test_assert(next == ones); + test_assert(prev == zeroes); + + t = sylvan_cube(all_vars_set, (uint8_t[]){0,0,0,0,0,1}); + test_assert(sylvan_relprev(t, s, all_vars_set) == zeroes); + test_assert(sylvan_relprev(t, sylvan_not(s), all_vars_set) == sylvan_false); + test_assert(sylvan_relnext(s, t, all_vars_set) == sylvan_false); + test_assert(sylvan_relnext(zeroes, t, all_vars_set) == s); + + t = sylvan_cube(all_vars_set, (uint8_t[]){0,0,0,0,0,2}); + test_assert(sylvan_relprev(t, s, all_vars_set) == zeroes); + test_assert(sylvan_relprev(t, zeroes, all_vars_set) == zeroes); + test_assert(sylvan_relnext(sylvan_not(zeroes), t, all_vars_set) == sylvan_false); + + return 0; +} + +int +test_compose() +{ + LACE_ME; + + BDD a = sylvan_ithvar(1); + BDD b = sylvan_ithvar(2); + + BDD a_or_b = sylvan_or(a, b); + + BDD one = make_random(3, 16); + BDD two = make_random(8, 24); + + BDDMAP map = sylvan_map_empty(); + + map = sylvan_map_add(map, 1, one); + map = sylvan_map_add(map, 2, two); + + test_assert(sylvan_map_key(map) == 1); + test_assert(sylvan_map_value(map) == one); + test_assert(sylvan_map_key(sylvan_map_next(map)) == 2); + test_assert(sylvan_map_value(sylvan_map_next(map)) == two); + + test_assert(testEqual(one, sylvan_compose(a, map))); + test_assert(testEqual(two, sylvan_compose(b, map))); + + test_assert(testEqual(sylvan_or(one, two), sylvan_compose(a_or_b, map))); + + map = sylvan_map_add(map, 2, one); + test_assert(testEqual(sylvan_compose(a_or_b, map), one)); + + map = sylvan_map_add(map, 1, two); + test_assert(testEqual(sylvan_or(one, two), sylvan_compose(a_or_b, map))); + + test_assert(testEqual(sylvan_and(one, two), sylvan_compose(sylvan_and(a, b), map))); + return 0; +} + +int runtests() +{ + // we are not testing garbage collection + sylvan_gc_disable(); + + if (test_bdd()) return 1; + for (int j=0;j<10;j++) if (test_cube()) return 1; + for (int j=0;j<10;j++) if (test_relprod()) return 1; + for (int j=0;j<10;j++) if (test_compose()) return 1; + for (int j=0;j<10;j++) if (test_operators()) return 1; + return 0; +} + +int main() +{ + // Standard Lace initialization with 1 worker + lace_init(1, 0); + lace_startup(0, NULL, NULL); + + // Simple Sylvan initialization, also initialize BDD support + sylvan_init_package(1LL<<20, 1LL<<20, 1LL<<16, 1LL<<16); + sylvan_init_bdd(1); + + int res = runtests(); + + sylvan_quit(); + lace_exit(); + + return res; +} diff --git a/resources/3rdparty/sylvan/test/test_cxx.cpp b/resources/3rdparty/sylvan/test/test_cxx.cpp index 007a21e71..c1d984b3f 100644 --- a/resources/3rdparty/sylvan/test/test_cxx.cpp +++ b/resources/3rdparty/sylvan/test/test_cxx.cpp @@ -1,19 +1,23 @@ /** * Just a small test file to ensure that Sylvan can compile in C++ - * Suggested by Shota Soga for testing C++ compatibility */ #include #include #include +#include "test_assert.h" + using namespace sylvan; -void test() +int runtest() { Bdd one = Bdd::bddOne(); Bdd zero = Bdd::bddZero(); + test_assert(one != zero); + test_assert(one == !zero); + Bdd v1 = Bdd::bddVar(1); Bdd v2 = Bdd::bddVar(2); @@ -22,25 +26,26 @@ void test() BddMap map; map.put(2, t); - assert(v2.Compose(map) == v1+v2); + test_assert(v2.Compose(map) == (v1 + v2)); + test_assert((t * v2) == v2); - t *= v2; - - assert(t == v2); + return 0; } int main() { - // Standard Lace initialization - lace_init(0, 1000000); + // Standard Lace initialization with 1 worker + lace_init(1, 0); lace_startup(0, NULL, NULL); - // Simple Sylvan initialization, also initialize BDD and LDD support + // Simple Sylvan initialization, also initialize BDD support sylvan_init_package(1LL<<16, 1LL<<16, 1LL<<16, 1LL<<16); sylvan_init_bdd(1); - test(); + int res = runtest(); sylvan_quit(); lace_exit(); + + return res; } diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp old mode 100644 new mode 100755 index 4e79a8dc0..1d225ec12 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -23,10 +23,10 @@ namespace storm { template bool ExprtkExpressionEvaluatorBase::asBool(Expression const& expression) const { - BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); + std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); + auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expressionPtr); + CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); return compiledExpression.value() == ValueType(1); } return expressionPair->second.value() == ValueType(1); @@ -34,22 +34,22 @@ namespace storm { template int_fast64_t ExprtkExpressionEvaluatorBase::asInt(Expression const& expression) const { - BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); + std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); + auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expressionPtr); + CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); return static_cast(compiledExpression.value()); } return static_cast(expressionPair->second.value()); } template - typename ExprtkExpressionEvaluatorBase::CompiledExpressionType& ExprtkExpressionEvaluatorBase::getCompiledExpression(BaseExpression const* expression) const { - std::pair result = this->compiledExpressions.emplace(expression, CompiledExpressionType()); + typename ExprtkExpressionEvaluatorBase::CompiledExpressionType& ExprtkExpressionEvaluatorBase::getCompiledExpression(storm::expressions::Expression const& expression) const { + std::pair result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType()); CompiledExpressionType& compiledExpression = result.first->second; compiledExpression.register_symbol_table(symbolTable); bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression); - STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk: " << *expression); + STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk: " << expression); return compiledExpression; } @@ -73,10 +73,10 @@ namespace storm { } double ExprtkExpressionEvaluator::asRational(Expression const& expression) const { - BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); + std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); + auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expressionPtr); + CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); return static_cast(compiledExpression.value()); } return static_cast(expressionPair->second.value()); diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h old mode 100644 new mode 100755 index 77fc94993..2ae6800ba --- a/src/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storage/expressions/ExprtkExpressionEvaluator.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_EXPRESSIONS_EXPRTKEXPRESSIONEVALUATOR_H_ #define STORM_STORAGE_EXPRESSIONS_EXPRTKEXPRESSIONEVALUATOR_H_ +#include #include #include @@ -26,14 +27,14 @@ namespace storm { protected: typedef double ValueType; typedef exprtk::expression CompiledExpressionType; - typedef std::unordered_map CacheType; + typedef std::unordered_map, CompiledExpressionType> CacheType; /*! * Adds a compiled version of the given expression to the internal storage. * * @param expression The expression that is to be compiled. */ - CompiledExpressionType& getCompiledExpression(BaseExpression const* expression) const; + CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const; // The parser used. mutable exprtk::parser parser;