Transformers: Remove Logic from SimpleChainSummarizer

The reference to logic is now stored in the graph, thus, the transformer
does not need to remember the reference anymore.

src/ChcInterpreter.cc

@@ -323,7 +323,7 @@ void ChcInterpreterContext::interpretCheckSat() {
     }
 
     TransformationPipeline::pipeline_t transformations;
-    transformations.push_back(std::make_unique<SimpleChainSummarizer>(logic));
+    transformations.push_back(std::make_unique<SimpleChainSummarizer>());
     transformations.push_back(std::make_unique<RemoveUnreachableNodes>());
     transformations.push_back(std::make_unique<SimpleNodeEliminator>());
     auto [newGraph, translator] = TransformationPipeline(std::move(transformations)).transform(std::move(hypergraph));

src/transformers/SimpleChainSummarizer.cc

@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2022, Martin Blicha <[email protected]>
+ * Copyright (c) 2022-2023, Martin Blicha <[email protected]>
  *
  * SPDX-License-Identifier: MIT
  */
@@ -9,7 +9,7 @@
 #include "CommonUtils.h"
 
 Transformer::TransformationResult SimpleChainSummarizer::transform(std::unique_ptr<ChcDirectedHyperGraph> graph) {
-    auto translator = std::make_unique<SimpleChainBackTranslator>(logic, graph->predicateRepresentation());
+    auto translator = std::make_unique<BackTranslator>(graph->getLogic(), graph->predicateRepresentation());
     while(true) {
         AdjacencyListsGraphRepresentation adjacencyList = AdjacencyListsGraphRepresentation::from(*graph);
         auto isTrivial = [&](SymRef sym) {
@@ -55,7 +55,7 @@ Transformer::TransformationResult SimpleChainSummarizer::transform(std::unique_p
     return {std::move(graph), std::move(translator)};
 }
 
-InvalidityWitness SimpleChainSummarizer::SimpleChainBackTranslator::translate(InvalidityWitness witness) {
+InvalidityWitness SimpleChainSummarizer::BackTranslator::translate(InvalidityWitness witness) {
     if (summarizedChains.empty()) { return witness; }
 
     for (auto const & [chain, replacingEdge] : summarizedChains) {
@@ -73,7 +73,7 @@ InvalidityWitness SimpleChainSummarizer::SimpleChainBackTranslator::translate(In
     return witness;
 }
 
-ValidityWitness SimpleChainSummarizer::SimpleChainBackTranslator::translate(ValidityWitness witness) {
+ValidityWitness SimpleChainSummarizer::BackTranslator::translate(ValidityWitness witness) {
     if (summarizedChains.empty()) { return witness; }
     auto definitions = witness.getDefinitions();
     // TODO: assert that we have true and false already

src/transformers/SimpleChainSummarizer.h

@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2022, Martin Blicha <[email protected]>
+ * Copyright (c) 2022-2023, Martin Blicha <[email protected]>
  *
  * SPDX-License-Identifier: MIT
  */
@@ -13,11 +13,11 @@ class SimpleChainSummarizer : public Transformer {
 public:
     TransformationResult transform(std::unique_ptr<ChcDirectedHyperGraph> graph) override;
 
-    SimpleChainSummarizer(Logic & logic) : logic(logic) {}
+    SimpleChainSummarizer() = default;
 
-    class SimpleChainBackTranslator : public WitnessBackTranslator {
+    class BackTranslator : public WitnessBackTranslator {
     public:
-        SimpleChainBackTranslator(Logic & logic, NonlinearCanonicalPredicateRepresentation predicateRepresentation)
+        BackTranslator(Logic & logic, NonlinearCanonicalPredicateRepresentation predicateRepresentation)
         : logic(logic), predicateRepresentation(std::move(predicateRepresentation)) {}
 
         InvalidityWitness translate(InvalidityWitness witness) override;
@@ -33,9 +33,6 @@ class SimpleChainSummarizer : public Transformer {
         Logic & logic;
         NonlinearCanonicalPredicateRepresentation predicateRepresentation;
     };
-private:
-    Logic & logic;
-
 };
 
 

test/test_Transformers.cc

@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2022, Martin Blicha <[email protected]>
+ * Copyright (c) 2022-2023, Martin Blicha <[email protected]>
  *
  * SPDX-License-Identifier: MIT
  */
@@ -67,7 +67,7 @@ TEST_F(Transformer_test, test_SingleChain_NoLoop) {
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     ValidityWitness witness{};
     auto translatedWitness = translator->translate(witness);
     Validator validator(logic);
@@ -101,7 +101,7 @@ TEST_F(Transformer_test, test_TwoChains_WithLoop) {
     );
     auto hypergraph = systemToGraph(system);
     auto originalGraph = *hypergraph;
-    auto [newGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hypergraph));
+    auto [newGraph, translator] = SimpleChainSummarizer().transform(std::move(hypergraph));
     VersionManager manager{logic};
     PTRef predicate = manager.sourceFormulaToBase(newGraph->getStateVersion(s2));
     PTRef var = logic.getPterm(predicate)[0];
@@ -139,7 +139,7 @@ TEST_F(Transformer_test, test_OutputFromEngine) {
     );
     auto hypergraph = systemToGraph(system);
     auto originalGraph = *hypergraph;
-    auto [newGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hypergraph));
+    auto [newGraph, translator] = SimpleChainSummarizer().transform(std::move(hypergraph));
     hypergraph = std::move(newGraph);
     auto res = Spacer(logic, options).solve(*hypergraph);
     ASSERT_EQ(res.getAnswer(), VerificationAnswer::SAFE);
@@ -161,7 +161,7 @@ TEST_F(Transformer_test, test_ChainSummarizer_TwoStepChain_Unsafe) {
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     Options options;
     options.addOption(Options::COMPUTE_WITNESS, "true");
     auto res = Spacer(logic, options).solve(*summarizedGraph);
@@ -190,7 +190,7 @@ TEST_F(Transformer_test, test_ChainSummarizer_ThreeStepChain_Unsafe) {
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     Options options;
     options.addOption(Options::COMPUTE_WITNESS, "true");
     auto res = Spacer(logic, options).solve(*summarizedGraph);
@@ -229,7 +229,7 @@ TEST_F(Transformer_test, test_ChainSummarizer_TwoChains_Unsafe) {
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     Options options;
     options.addOption(Options::COMPUTE_WITNESS, "true");
     auto res = Spacer(logic, options).solve(*summarizedGraph);
@@ -259,7 +259,7 @@ TEST_F(Transformer_test, test_ChainSummarizer_SameChainTwice_SafeFact_Unsafe) {
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     Options options;
     options.addOption(Options::COMPUTE_WITNESS, "true");
     auto res = Spacer(logic, options).solve(*summarizedGraph);
@@ -289,7 +289,7 @@ TEST_F(Transformer_test, test_ChainSummarizer_SameChainTwice_DifferentFact_Unsaf
     );
     auto hyperGraph = systemToGraph(system);
     auto originalGraph = *hyperGraph;
-    auto [summarizedGraph, translator] = SimpleChainSummarizer(logic).transform(std::move(hyperGraph));
+    auto [summarizedGraph, translator] = SimpleChainSummarizer().transform(std::move(hyperGraph));
     Options options;
     options.addOption(Options::COMPUTE_WITNESS, "true");
     auto res = Spacer(logic, options).solve(*summarizedGraph);