Print DFA in HOA format

.github/workflows/build_cmake.yml

@@ -61,3 +61,6 @@ jobs:
           name: codecov-umbrella
           yml: ./codecov.yml
           fail_ci_if_error: true
+      - name: Benchmarks
+        run: |
+          ./scripts/_ci-bench.sh

.gitmodules

@@ -13,3 +13,9 @@
 [submodule "third_party/CLI11"]
 	path = third_party/CLI11
 	url = https://github.com/CLIUtils/CLI11.git
+[submodule "third_party/google/benchmark"]
+	path = third_party/google/benchmark
+	url = https://github.com/google/benchmark.git
+[submodule "third_party/cpphoafparser"]
+	path = third_party/cpphoafparser
+	url = https://github.com/whitemech/cpphoafparser.git

CMakeLists.txt

@@ -27,10 +27,31 @@ project (Lydia
 
 set_property (GLOBAL PROPERTY USE_FOLDERS ON)
 
+message("Using build type ${CMAKE_BUILD_TYPE}")
+
 set (CMAKE_CXX_STANDARD 17)
 set (CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
 
+# TODO introduce '-Werror', eventually
+set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic")
+
+# these cannot be added due to Flex/Bison
+#set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS} -fno-exceptions")
+#set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS} -fno-rtti")
+
+if (CMAKE_BUILD_TYPE EQUAL "Debug" AND ENABLE_COVERAGE)
+    message("-- Code coverage enabled")
+    set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -O0")
+    set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -fprofile-arcs")
+    set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -ftest-coverage")
+    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
+endif()
+
+if (PROFILE)
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-omit-frame-pointer")
+endif()
+
 # TODO include this eventually
 #set(CMAKE_CXX_CLANG_TIDY
 #        clang-tidy;
@@ -48,15 +69,6 @@ set(CMAKE_MODULE_PATH
 set( CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin )
 set( CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib )
 
-if (ENABLE_COVERAGE)
-    message("-- Code coverage enabled")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g ")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fprofile-arcs")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ftest-coverage")
-    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
-endif()
-
 set (THREADS_PREFER_PTHREAD_FLAG ON)
 find_package (Threads REQUIRED)
 find_package(cudd REQUIRED)

README.md

@@ -88,7 +88,8 @@ Afterwards, to run the tests:
 make test
 ```
 
-To configure the build for development, use the flag `-DENABLE_COVERAGE=ON`
+To configure the build for development, 
+use the flag `-DCMAKE_BUILD_TYPE=Debug`
 
 ## Scripts
 
@@ -106,6 +107,9 @@ For building:
 - `build.sh`: for normal build
 - `build-dev.sh` for development build
 
+For benchmarking, use `./scripts/benchmark.sh` 
+(after `./scripts/build.sh`). 
+
 ## Docker development image
 
 We provide a Docker image for development.

app/mona2sym/src/main.cpp

@@ -38,14 +38,15 @@
  * @param filename the path to the MONA DFA file.
  * @return nothing.
  */
-void transform(const std::string &input, const std::string &output_dir) {
-  auto my_dfa = whitemech::lydia::dfa::read_from_file(input);
-  // TODO reintroduce <filesystem> and make it work on CI...
+void transform(const std::string &input, const std::string &output_dir,
+               const CUDD::Cudd &mgr) {
+  auto my_dfa = whitemech::lydia::dfa::read_from_file(input, mgr);
+  // TODO try to use <filesystem>, check CI
   //  std::filesystem::create_directory(output_dir);
   auto cmd = "mkdir " + output_dir;
   std::system(cmd.c_str());
-  my_dfa->bdd2dot(output_dir);
-  dfa_to_graphviz(*my_dfa, "output", "svg");
+  my_dfa.bdd2dot(output_dir);
+  dfa_to_graphviz(my_dfa, "output", "svg");
 }
 
 int main(int argc, char **argv) {
@@ -63,7 +64,7 @@ int main(int argc, char **argv) {
 
   CLI11_PARSE(app, argc, argv);
 
-  transform(input_file, output_directory);
-
+  auto mgr = CUDD::Cudd();
+  transform(input_file, output_directory, mgr);
   return 0;
 }

lib/CMakeLists.txt

@@ -57,3 +57,4 @@ set (LIB_NAME ${LIB_NAME} PARENT_SCOPE)
 #test
 enable_testing ()
 add_subdirectory (test)
+add_subdirectory (benchmark)

lib/benchmark/CMakeLists.txt

@@ -0,0 +1,44 @@
+#
+# This file is part of Lydia.
+#
+# Lydia 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.
+#
+# Lydia 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 Lydia.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+# CMake build : library tests
+
+#configure variables
+set (BENCHMARK_APP_NAME "${LIB_NAME}Bench")
+
+#configure directories
+set (BENCHMARK_MODULE_PATH "${LIBRARY_MODULE_PATH}/benchmark")
+
+#configure benchmark directories
+set (BENCHMARK_SRC_PATH  "${BENCHMARK_MODULE_PATH}/src" )
+
+#set includes
+include_directories (${LIBRARY_INCLUDE_PATH} ${TEST_THIRD_PARTY_INCLUDE_PATH})
+
+#set test sources
+file (GLOB BENCHMARK_SOURCE_FILES "${BENCHMARK_SRC_PATH}/*.cpp")
+
+#set target executable
+add_executable (${BENCHMARK_APP_NAME} ${BENCHMARK_SOURCE_FILES})
+
+#add the library
+target_link_libraries (${BENCHMARK_APP_NAME} ${LIB_NAME} Threads::Threads benchmark::benchmark ${CUDD_LIBRARIES})
+
+add_custom_target(lydia-benchmark
+        COMMAND ${CMAKE_BINARY_DIR}/bin/${BENCHMARK_APP_NAME}
+        DEPENDS lydia
+        COMMENT "Run benchmarks." VERBATIM)

lib/benchmark/src/dfa.cpp

@@ -0,0 +1,47 @@
+/*
+ * This file is part of Lydia.
+ *
+ * Lydia 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.
+ *
+ * Lydia 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 Lydia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "logic.hpp"
+#include "translate.hpp"
+#include "utils/benchmark.hpp"
+#include <benchmark/benchmark.h>
+#include <random>
+
+namespace whitemech::lydia::Benchmark {
+
+static void BM_cudd_manager_instantiation(benchmark::State &state) {
+  for (auto _ : state) {
+    auto mgr = CUDD::Cudd();
+    escape(&mgr);
+    (void)mgr;
+  }
+}
+BENCHMARK(BM_cudd_manager_instantiation);
+
+static void BM_dfa_instantiation(benchmark::State &state) {
+  // we keep this outside since it's the operation that takes more time
+  // preallocate
+  auto mgr = CUDD::Cudd();
+  for (auto _ : state) {
+    auto my_dfa = dfa(mgr, 1, 1);
+    escape(&my_dfa);
+    (void)my_dfa;
+  }
+}
+BENCHMARK(BM_dfa_instantiation);
+
+} // namespace whitemech::lydia::Benchmark

lib/benchmark/src/logic.cpp

@@ -0,0 +1,96 @@
+/*
+ * This file is part of Lydia.
+ *
+ * Lydia 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.
+ *
+ * Lydia 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 Lydia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "logic.hpp"
+#include "utils/benchmark.hpp"
+#include <benchmark/benchmark.h>
+#include <random>
+
+namespace whitemech::lydia::Benchmark {
+
+static void BM_boolean_from_constructor(benchmark::State &state) {
+  for (auto _ : state) {
+    auto x = LDLfBooleanAtom(true);
+    escape(&x);
+    (void)x;
+  }
+}
+BENCHMARK(BM_boolean_from_constructor);
+
+static void BM_shared_boolean_from_constructor(benchmark::State &state) {
+  for (auto _ : state) {
+    auto x = std::make_shared<LDLfBooleanAtom>(true);
+    escape(&x);
+    (void)x;
+  }
+}
+BENCHMARK(BM_shared_boolean_from_constructor);
+
+static void BM_boolean_from_static_pointer(benchmark::State &state) {
+  for (auto _ : state) {
+    std::shared_ptr<const LDLfBooleanAtom> x = boolean(true);
+    escape(&x);
+    (void)x;
+  }
+}
+BENCHMARK(BM_boolean_from_static_pointer);
+
+static void BM_set_of_booleans_from_pointers(benchmark::State &state) {
+  for (auto _ : state) {
+    auto true_ = boolean(true);
+    auto false_ = boolean(false);
+    auto s = set_formulas{true_, false_};
+    escape(&s);
+    (void)s;
+  }
+}
+BENCHMARK(BM_set_of_booleans_from_pointers);
+
+static void BM_set_of_booleans_from_shared_pointers(benchmark::State &state) {
+  for (auto _ : state) {
+    auto true_ = std::make_shared<const LDLfBooleanAtom>(true);
+    auto false_ = std::make_shared<const LDLfBooleanAtom>(false);
+    auto s = set_formulas{true_, false_};
+    escape(&s);
+    (void)s;
+  }
+}
+BENCHMARK(BM_set_of_booleans_from_shared_pointers);
+
+static void BM_and_true_false(benchmark::State &state) {
+  for (auto _ : state) {
+    std::shared_ptr<const LDLfBooleanAtom> true_ = boolean(true);
+    std::shared_ptr<const LDLfBooleanAtom> false_ = boolean(false);
+    auto and_ = LDLfAnd(set_formulas{true_, false_});
+    escape(&and_);
+    (void)and_;
+  }
+}
+BENCHMARK(BM_and_true_false);
+
+static void BM_shared_and_true_false(benchmark::State &state) {
+  for (auto _ : state) {
+    std::shared_ptr<const LDLfBooleanAtom> true_ = boolean(true);
+    std::shared_ptr<const LDLfBooleanAtom> false_ = boolean(false);
+    auto and_ = std::make_shared<LDLfAnd>(set_formulas{true_, false_});
+    escape(&and_);
+    (void)and_;
+  }
+}
+BENCHMARK(BM_shared_and_true_false);
+
+} // namespace whitemech::lydia::Benchmark

lib/benchmark/src/main.cpp

@@ -0,0 +1,20 @@
+/*
+ * This file is part of Lydia.
+ *
+ * Lydia 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.
+ *
+ * Lydia 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 Lydia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <benchmark/benchmark.h>
+
+BENCHMARK_MAIN();