added feature to compute the hamming distance of a formula

libs/core/include/cynthia/hamming_distance.hpp

@@ -0,0 +1,54 @@
+#pragma once
+/*
+ * This file is part of Cynthia.
+ *
+ * Cynthia 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.
+ *
+ * Cynthia 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 Cynthia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <cynthia/logic/visitor.hpp>
+
+namespace cynthia {
+namespace core {
+
+class HammingDistanceVisitor : public logic::Visitor {
+private:
+  size_t result;
+
+public:
+  void visit(const logic::LTLfTrue&) override;
+  void visit(const logic::LTLfFalse&) override;
+  void visit(const logic::LTLfPropTrue&) override;
+  void visit(const logic::LTLfPropFalse&) override;
+  void visit(const logic::LTLfAtom&) override;
+  void visit(const logic::LTLfNot&) override;
+  void visit(const logic::LTLfPropositionalNot&) override;
+  void visit(const logic::LTLfAnd&) override;
+  void visit(const logic::LTLfOr&) override;
+  void visit(const logic::LTLfImplies&) override;
+  void visit(const logic::LTLfEquivalent&) override;
+  void visit(const logic::LTLfXor&) override;
+  void visit(const logic::LTLfNext&) override;
+  void visit(const logic::LTLfWeakNext&) override;
+  void visit(const logic::LTLfUntil&) override;
+  void visit(const logic::LTLfRelease&) override;
+  void visit(const logic::LTLfEventually&) override;
+  void visit(const logic::LTLfAlways&) override;
+
+  size_t apply(const logic::LTLfFormula& formula);
+};
+
+size_t hamming_distance(const logic::LTLfFormula& formula);
+
+} // namespace core
+} // namespace cynthia

libs/core/src/hamming_distance.cpp

@@ -0,0 +1,100 @@
+/*
+ * This file is part of Cynthia.
+ *
+ * Cynthia 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.
+ *
+ * Cynthia 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 Cynthia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <algorithm>
+#include <cynthia/hamming_distance.hpp>
+#include <cynthia/logic/ltlf.hpp>
+#include <numeric>
+
+namespace cynthia {
+namespace core {
+
+void HammingDistanceVisitor::visit(const logic::LTLfTrue& formula) {
+  result = 0;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfFalse& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfPropTrue& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfPropFalse& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfAtom& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfNot& formula) {
+  logic::throw_expected_nnf();
+}
+void HammingDistanceVisitor::visit(const logic::LTLfPropositionalNot& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfAnd& formula) {
+  std::vector<size_t> values;
+  values.resize(formula.args.size());
+  std::transform(formula.args.begin(), formula.args.end(), values.begin(),
+                 [this](const logic::ltlf_ptr& arg) { return apply(*arg); });
+  result = std::accumulate(values.begin(), values.end(), 0);
+}
+void HammingDistanceVisitor::visit(const logic::LTLfOr& formula) {
+  std::vector<size_t> values;
+  values.resize(formula.args.size());
+  std::transform(formula.args.begin(), formula.args.end(), values.begin(),
+                 [this](const logic::ltlf_ptr& arg) { return apply(*arg); });
+  result = *min_element(values.begin(), values.end());
+}
+void HammingDistanceVisitor::visit(const logic::LTLfImplies& formula) {
+  result = apply(*simplify(formula));
+}
+void HammingDistanceVisitor::visit(const logic::LTLfEquivalent& formula) {
+  result = apply(*simplify(formula));
+}
+void HammingDistanceVisitor::visit(const logic::LTLfXor& formula) {
+  result = apply(*simplify(formula));
+}
+void HammingDistanceVisitor::visit(const logic::LTLfNext& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfWeakNext& formula) {
+  result = 0;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfUntil& formula) {
+  result = 1;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfRelease& formula) {
+  result = 0;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfEventually& formula) {
+  result = false;
+}
+void HammingDistanceVisitor::visit(const logic::LTLfAlways& formula) {
+  result = 0;
+}
+
+size_t HammingDistanceVisitor::apply(const logic::LTLfFormula& formula) {
+  formula.accept(*this);
+  return result;
+}
+
+size_t hamming_distance(const logic::LTLfFormula& formula) {
+  HammingDistanceVisitor visitor{};
+  return visitor.apply(formula);
+}
+
+} // namespace core
+} // namespace cynthia

libs/core/tests/unit/test_hamming_distance.cpp

@@ -0,0 +1,103 @@
+/*
+ * This file is part of Cynthia.
+ *
+ * Cynthia 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.
+ *
+ * Cynthia 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 Cynthia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <catch.hpp>
+#include <cynthia/hamming_distance.hpp>
+
+namespace cynthia {
+namespace core {
+namespace Test {
+
+TEST_CASE("Test hamming_distance of tt", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto tt = context.make_tt();
+  REQUIRE(hamming_distance(*tt) == 0);
+}
+
+TEST_CASE("Test hamming_distance of ff", "[core][SDD]") {
+  auto context = logic::Context();
+  auto ff = context.make_ff();
+  REQUIRE(hamming_distance(*ff) == 1);
+}
+
+TEST_CASE("Test hamming_distance of true", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto true_ = context.make_prop_true();
+  REQUIRE(hamming_distance(*true_) == 1);
+}
+
+TEST_CASE("Test hamming_distance of false", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto false_ = context.make_prop_false();
+  REQUIRE(hamming_distance(*false_) == 1);
+}
+
+TEST_CASE("Test hamming_distance of a", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  REQUIRE(hamming_distance(*a) == 1);
+}
+
+TEST_CASE("Test hamming_distance of !a", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  auto not_a = context.make_prop_not(a);
+  REQUIRE(hamming_distance(*not_a) == 1);
+}
+
+TEST_CASE("Test hamming_distance of a & b", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  auto b = context.make_atom("b");
+  auto a_and_b = context.make_and(logic::vec_ptr{a, b});
+  REQUIRE(hamming_distance(*a_and_b) == 2);
+}
+
+TEST_CASE("Test hamming_distance of a | b", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  auto b = context.make_atom("b");
+  auto a_or_b = context.make_or(logic::vec_ptr{a, b});
+  REQUIRE(hamming_distance(*a_or_b) == 1);
+}
+
+TEST_CASE("Test hamming_distance of X[!]a", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  auto next_a = context.make_next(a);
+  REQUIRE(hamming_distance(*next_a) == 1);
+}
+
+TEST_CASE("Test hamming_distance of X a", "[core][SDD]") {
+  auto context = logic::Context();
+
+  auto a = context.make_atom("a");
+  auto weak_next_a = context.make_weak_next(a);
+  REQUIRE(hamming_distance(*weak_next_a) == 0);
+}
+
+} // namespace Test
+} // namespace core
+} // namespace cynthia