Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
sylvan.h
Go to the documentation of this file.
1#pragma once
2
3#pragma clang diagnostic push
4#pragma clang diagnostic ignored "-Wextra-semi"
5#pragma clang diagnostic ignored "-Wzero-length-array"
6#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments"
7#pragma clang diagnostic ignored "-Wdeprecated-register"
8#pragma clang diagnostic ignored "-Wc99-extensions"
9#pragma clang diagnostic ignored "-Wunknown-pragmas"
10#pragma GCC diagnostic push
11#pragma GCC diagnostic ignored "-Wpedantic"
12
13#pragma GCC system_header // Only way to suppress some warnings atm.
14
15#include "sylvan_obj.hpp"
16#include "sylvan_storm_rational_function.h"
17#include "sylvan_storm_rational_number.h"
18
19#define cas(ptr, old, new) (__sync_bool_compare_and_swap((ptr), (old), (new)))
20#define ATOMIC_READ(x) (*(volatile decltype(x) *)&(x))
21
22namespace storm {
23namespace dd {
24
33bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0);
34
43bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0);
44
45} // namespace dd
46} // namespace storm
47
48#pragma GCC diagnostic pop
49#pragma clang diagnostic pop
bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset)
Retrieves whether the topmost variable in the BDD is the one with the given index.
Definition sylvan.cpp:6
bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset)
Retrieves whether the topmost variable in the MTBDD is the one with the given index.
Definition sylvan.cpp:10
LabParser.cpp.
Definition cli.cpp:18