Rewriters: Hide internal details of rewriters

DivModRewriter is exposed to the outside world, but it was broken, because it was including "OsmtInternalException.h" which is not suppose to be exposed and which we do not install. Thus, trying to include "DivModRewriter.h" in another application results in a compilation error. We fix this problem by hiding the existing rewriters and exposing to the outside world only API methods to use this functionality.
usi-verification-and-security · Jul 16, 2024 · 3661f5e · 3661f5e
1 parent 810046a
commit 3661f5e
Show file tree

Hide file tree

Showing 13 changed files with 119 additions and 98 deletions.
diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc
@@ -1,10 +1,11 @@
 #include "ArithLogic.h"
 
-#include "DivModRewriter.h"
 #include "FastRational.h"
 #include "OsmtApiException.h"
 #include "OsmtInternalException.h"
 #include "Polynomial.h"
+#include "Rewriter.h"
+#include "Rewritings.h"
 #include "PtStore.h"
 #include "SStore.h"
 #include "StringConv.h"
@@ -1147,16 +1148,9 @@ PTRef ArithLogic::removeAuxVars(PTRef tr) {
     class AuxSymbolMatcherConfig : public DefaultRewriterConfig {
         ArithLogic & logic;
     public:
-        AuxSymbolMatcherConfig(ArithLogic & logic) : logic(logic) {}
+        explicit AuxSymbolMatcherConfig(ArithLogic & logic) : logic(logic) {}
         PTRef rewrite(PTRef tr) override {
-            if (not logic.isVar(tr)) return tr; // Only variables can match
-            auto symName = std::string_view(logic.getSymName(tr));
-            if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::divPrefix) == 0) {
-                return DivModConfig::getDivTermFor(logic, tr);
-            } else if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::modPrefix) == 0){
-                return DivModConfig::getModTermFor(logic, tr);
-            }
-            return tr;
+            return opensmt::rewritings::tryGetOriginalDivModTerm(logic, tr).value_or(tr);
         }
     };
     // Note: this has negligible impact on performance, no need to check if there are divs or mods

diff --git a/src/logics/ArrayTheory.cc b/src/logics/ArrayTheory.cc
@@ -7,7 +7,9 @@
 #include "ArrayTheory.h"
 
 #include "ArrayHelpers.h"
-#include "DistinctRewriter.h"
+#include "Rewritings.h"
+
+using namespace opensmt::rewritings;
 
 PTRef ArrayTheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
     // TODO: simplify select over store on the same index

diff --git a/src/logics/LATheory.h b/src/logics/LATheory.h
@@ -10,8 +10,7 @@
 #define OPENSMT_LATHEORY_H
 #include "Theory.h"
 #include "ArithmeticEqualityRewriter.h"
-#include "DistinctRewriter.h"
-#include "DivModRewriter.h"
+#include "Rewritings.h"
 
 template<typename LinAlgLogic, typename LinAlgTHandler>
 class LATheory : public Theory
@@ -40,14 +39,14 @@ PTRef rewriteDivMod(TLogic &, PTRef fla) { return fla; }
 template<>
 PTRef rewriteDivMod<ArithLogic>(ArithLogic & logic, PTRef fla) {
     // Real logic cannot have div and mod
-    return not logic.hasIntegers() ? fla : DivModRewriter(logic).rewrite(fla);
+    return not logic.hasIntegers() ? fla : opensmt::rewritings::rewriteDivMod(logic,fla);
 }
 
 }
 
 template<typename LinAlgLogic, typename LinAlgTSHandler>
 PTRef LATheory<LinAlgLogic,LinAlgTSHandler>::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
-    fla = rewriteDistincts(getLogic(), fla);
+    fla = opensmt::rewritings::rewriteDistincts(getLogic(), fla);
     fla = rewriteDivMod<LinAlgLogic>(lalogic, fla);
     ArithmeticEqualityRewriter equalityRewriter(lalogic);
     fla = equalityRewriter.rewrite(fla);

diff --git a/src/logics/UFLATheory.cc b/src/logics/UFLATheory.cc
@@ -2,12 +2,13 @@
 
 #include "ArithmeticEqualityRewriter.h"
 #include "ArrayHelpers.h"
-#include "DistinctRewriter.h"
 #include "LATheory.h"
 #include "OsmtInternalException.h"
-#include "Substitutor.h"
+#include "Rewritings.h"
 #include "TreeOps.h"
 
+using namespace opensmt::rewritings;
+
 PTRef UFLATheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
     fla = rewriteDistincts(getLogic(), fla);
     fla = rewriteDivMod<ArithLogic>(logic, fla);

diff --git a/src/logics/UFTheory.cc b/src/logics/UFTheory.cc
@@ -1,6 +1,8 @@
 #include "Theory.h"
 #include "TreeOps.h"
-#include "DistinctRewriter.h"
+#include "Rewritings.h"
+
+using namespace opensmt::rewritings;
 
 PTRef UFTheory::preprocessBeforeSubstitutions(PTRef fla, PreprocessingContext const & context) {
     return context.perPartition ? fla : getLogic().mkAnd(fla, getLogic().learnEqTransitivity(fla));

diff --git a/src/rewriters/CMakeLists.txt b/src/rewriters/CMakeLists.txt
@@ -1,12 +1,12 @@
 add_library(rewriters OBJECT "")
 
 target_sources(rewriters
-    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/DistinctRewriter.cc"
+    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Rewritings.cc"
 )
 
 install(FILES
     Substitutor.h
     Rewriter.h
-    DivModRewriter.h
+    Rewritings.h
     DESTINATION ${INSTALL_HEADERS_DIR}
     )
diff --git a/src/rewriters/DistinctRewriter.cc b/src/rewriters/DistinctRewriter.cc
diff --git a/src/rewriters/DistinctRewriter.h b/src/rewriters/DistinctRewriter.h
@@ -73,10 +73,6 @@ class KeepTopLevelDistinctRewriter : public Rewriter<KeepTopLevelDistinctRewrite
         : Rewriter<KeepTopLevelDistinctRewriteConfig>(logic, config), config(logic, std::move(topLevelDistincts)) {}
 };
 
-inline PTRef rewriteDistincts(Logic & logic, PTRef fla) {
-    return DistinctRewriter(logic).rewrite(fla);
-}
 
-PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla);
 
 #endif // OPENSMT_DISTINCTREWRITER_H
diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2021-2022, Martin Blicha <martin.blicha@gmail.com>
+ * Copyright (c) 2021-2024, Martin Blicha <martin.blicha@gmail.com>
  *
  *  SPDX-License-Identifier: MIT
  *
@@ -8,17 +8,10 @@
 #ifndef OPENSMT_DIVMODREWRITER_H
 #define OPENSMT_DIVMODREWRITER_H
 
-#include "Rewriter.h"
-
 #include "ArithLogic.h"
-#include "PTRef.h"
-
-#include "OsmtApiException.h"
 #include "OsmtInternalException.h"
-#include "TypeUtils.h"
+#include "Rewriter.h"
 
-#include <string>
-#include <unordered_map>
 
 class DivModConfig : public DefaultRewriterConfig {
     ArithLogic & logic;
@@ -64,7 +57,7 @@ class DivModConfig : public DefaultRewriterConfig {
     static std::string_view constexpr divPrefix = ".div";
     static std::string_view constexpr modPrefix = ".mod";
 
-    DivModConfig(ArithLogic & logic) : logic(logic) {}
+    explicit DivModConfig(ArithLogic & logic) : logic(logic) {}
 
     PTRef rewrite(PTRef term) override {
         SymRef symRef = logic.getSymRef(term);
@@ -125,7 +118,7 @@ class DivModRewriter : Rewriter<DivModConfig> {
     DivModConfig config;
 
 public:
-    DivModRewriter(ArithLogic & logic) : Rewriter<DivModConfig>(logic, config), logic(logic), config(logic) {}
+    explicit DivModRewriter(ArithLogic & logic) : Rewriter<DivModConfig>(logic, config), logic(logic), config(logic) {}
 
     PTRef rewrite(PTRef term) override {
         if (term == PTRef_Undef or not logic.hasSortBool(term)) {
@@ -139,9 +132,4 @@ class DivModRewriter : Rewriter<DivModConfig> {
     }
 };
 
-// Simple single-use version
-inline PTRef rewriteDivMod(ArithLogic & logic, PTRef root) {
-    return DivModRewriter(logic).rewrite(root);
-}
-
-#endif // OPENSMT_DIVMODEREWRITER_H
+#endif // OPENSMT_DIVMODREWRITER_H
diff --git a/src/rewriters/Rewritings.cc b/src/rewriters/Rewritings.cc
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+#include "Rewritings.h"
+
+#include "DistinctRewriter.h"
+#include "DivModRewriter.h"
+#include "TreeOps.h"
+
+namespace opensmt::rewritings {
+
+    PTRef rewriteDistincts(Logic & logic, PTRef fla) {
+        return DistinctRewriter(logic).rewrite(fla);
+    }
+
+    PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla) {
+        vec<PTRef> topLevelConjuncts = ::topLevelConjuncts(logic, fla);
+        KeepTopLevelDistinctRewriter::TopLevelDistincts topLevelDistincts;
+        for (PTRef conj : topLevelConjuncts) {
+            if (logic.isDisequality(conj)) { topLevelDistincts.insert(conj); }
+        }
+        return KeepTopLevelDistinctRewriter(logic, std::move(topLevelDistincts)).rewrite(fla);
+    }
+
+    PTRef rewriteDivMod(ArithLogic & logic, PTRef term) {
+        return DivModRewriter(logic).rewrite(term);
+    }
+
+    std::optional<PTRef> tryGetOriginalDivModTerm(ArithLogic & logic, PTRef tr) {
+        if (not logic.isVar(tr)) return std::nullopt; // Only variables can match
+        auto symName = std::string_view(logic.getSymName(tr));
+        if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::divPrefix) == 0) {
+            return DivModConfig::getDivTermFor(logic, tr);
+        } else if (symName.compare(0, DivModConfig::modPrefix.size(), DivModConfig::modPrefix) == 0) {
+            return DivModConfig::getModTermFor(logic, tr);
+        }
+        return std::nullopt;
+    }
+}
diff --git a/src/rewriters/Rewritings.h b/src/rewriters/Rewritings.h
@@ -0,0 +1,28 @@
+/*
+ * Copyright (c) 2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+#ifndef OPENSMT_REWRITINGS_H
+#define OPENSMT_REWRITINGS_H
+
+#include "ArithLogic.h"
+#include "PTRef.h"
+
+#include <optional>
+
+namespace opensmt::rewritings {
+
+    PTRef rewriteDistincts(Logic & logic, PTRef fla);
+
+    PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla);
+
+    PTRef rewriteDivMod(ArithLogic & logic, PTRef fla);
+
+    std::optional<PTRef> tryGetOriginalDivModTerm(ArithLogic & logic, PTRef term);
+
+} // opensmt::rewritings
+
+#endif // OPENSMT_REWRITINGS_H
diff --git a/test/unit/test_LIALogicMkTerms.cc b/test/unit/test_LIALogicMkTerms.cc
@@ -3,9 +3,9 @@
 //
 
 #include <gtest/gtest.h>
-#include <ArithLogic.h>
-#include "DivModRewriter.h"
+#include "ArithLogic.h"
 #include "IteHandler.h"
+#include "Rewritings.h"
 #include "TreeOps.h"
 
 #include <algorithm>
@@ -194,27 +194,10 @@ TEST_F(LIALogicMkTermsTest, test_EqualityNormalization_EqualityToConstant) {
 }
 
 TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) {
-
-    static constexpr std::initializer_list<std::string_view> prefixes = {IteHandler::itePrefix, DivModConfig::divPrefix, DivModConfig::modPrefix};
-
-
     auto hasAuxSymbols = [this](PTRef tr) {
-        class AuxSymbolMatcher {
-            ArithLogic const & logic;
-
-        public:
-            AuxSymbolMatcher(ArithLogic const & logic) : logic(logic) {}
-            bool operator()(PTRef tr) {
-                std::string_view const name = logic.getSymName(tr);
-                return std::any_of(prefixes.begin(), prefixes.end(), [&name](std::string_view const prefix) {
-                    return name.compare(0, prefix.size(), prefix) == 0;
-                });
-            };
-        };
-        auto predicate = AuxSymbolMatcher(logic);
-        auto config = TermCollectorConfig(predicate);
-        TermVisitor(logic, config).visit(tr);
-        return config.extractCollectedTerms().size() > 0;
+        auto auxiliaryVarsInTerm = matchingSubTerms(logic, tr, [&](PTRef subTerm) {
+            return opensmt::rewritings::tryGetOriginalDivModTerm(logic, subTerm).has_value(); });
+        return auxiliaryVarsInTerm.size() > 0;
     };
 
     PTRef a = logic.mkIntVar("a");
@@ -231,8 +214,7 @@ TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) {
     PTRef nested = logic.mkEq(logic.getTerm_IntZero(), logic.mkMod(ite, c));
 
     for (PTRef tr : {term, eq, nested}) {
-
-        PTRef termWithAux = DivModRewriter(logic).rewrite(IteHandler(logic).rewrite(tr));
+        PTRef termWithAux = opensmt::rewritings::rewriteDivMod(logic, IteHandler(logic).rewrite(tr));
         ASSERT_TRUE(hasAuxSymbols(termWithAux));
 
         PTRef termWithoutAux = logic.removeAuxVars(termWithAux);

diff --git a/test/unit/test_Rewriting.cc b/test/unit/test_Rewriting.cc
@@ -1,18 +1,22 @@
-//
-// Created by Martin Blicha on 17.05.20.
-//
+/*
+ * Copyright (c) 2020-2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
 
 #include <gtest/gtest.h>
-#include <ArithLogic.h>
-#include <BoolRewriting.h>
-#include <Logic.h>
-#include <ArithmeticEqualityRewriter.h>
-#include <DivModRewriter.h>
-#include <MainSolver.h>
-#include <DistinctRewriter.h>
+
+#include "ArithLogic.h"
+#include "BoolRewriting.h"
+#include "Logic.h"
+#include "ArithmeticEqualityRewriter.h"
+#include "MainSolver.h"
+#include "Rewritings.h"
 
 #include <algorithm>
 
+using namespace opensmt::rewritings;
 
 TEST(Rewriting_test, test_RewriteClassicConjunction)
 {
@@ -79,7 +83,7 @@ TEST(Rewriting_test, test_RewriteDivMod) {
     PTRef div = logic.mkIntDiv(x,two);
     PTRef mod = logic.mkMod(x,two);
     PTRef fla = logic.mkAnd(logic.mkEq(div, two), logic.mkEq(mod, logic.getTerm_IntZero()));
-    PTRef rewritten = DivModRewriter(logic).rewrite(fla);
+    PTRef rewritten = rewriteDivMod(logic, fla);
 //    std::cout << logic.printTerm(rewritten) << std::endl;
     SMTConfig config;
     MainSolver solver(logic, config, "test");
@@ -112,16 +116,16 @@ class RewriteDistinctTest : public ::testing::Test {
 TEST_F(RewriteDistinctTest, test_RewriteDistinct_TopLevel) {
     PTRef dist = logic.mkDistinct({x, y, z});
     PTRef fla = logic.mkAnd(b, dist); // dist is top-level distinct
-    EXPECT_NE(::rewriteDistincts(logic, fla), fla); // fla should be rewritten
-    EXPECT_EQ(::rewriteDistinctsKeepTopLevel(logic, fla), fla); // fla should be kept the same
+    EXPECT_NE(rewriteDistincts(logic, fla), fla); // fla should be rewritten
+    EXPECT_EQ(rewriteDistinctsKeepTopLevel(logic, fla), fla); // fla should be kept the same
 }
 
 TEST_F(RewriteDistinctTest, test_RewriteDistinct_Negated) {
     PTRef dist = logic.mkDistinct({x, y, z});
     PTRef fla = logic.mkNot(dist); // dist is not top-level distinct
-    PTRef rewritten1 = ::rewriteDistincts(logic, fla);
+    PTRef rewritten1 = rewriteDistincts(logic, fla);
     EXPECT_NE(rewritten1, fla); // fla should be rewritten
-    PTRef rewritten2 = ::rewriteDistinctsKeepTopLevel(logic, fla);
+    PTRef rewritten2 = rewriteDistinctsKeepTopLevel(logic, fla);
     EXPECT_NE(rewritten2, fla); // fla should be rewritten
     EXPECT_EQ(rewritten1, rewritten2);
     ASSERT_TRUE(logic.isNot(rewritten1));