Put applicators into anonymous namespaces to avoid linker collisions

vprover · Apr 26, 2024 · e3f9e87 · e3f9e87
1 parent ca653da
commit e3f9e87
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 2 deletions.
diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp
@@ -85,6 +85,8 @@ struct BackwardDemodulation::RewritableClausesFn
   DemodulationSubtermIndex* _index;
 };
 
+namespace {
+
 struct Applicator : SubstApplicator {
   Applicator(ResultSubstitution* subst) : subst(subst) {}
   TermList operator()(unsigned v) const override {
@@ -93,6 +95,8 @@ struct Applicator : SubstApplicator {
   ResultSubstitution* subst;
 };
 
+} // end namespace
+
 struct BackwardDemodulation::ResultFn
 {
   typedef DHMultiset<Clause*> ClauseSet;

diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp
@@ -53,6 +53,8 @@ using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
 
+namespace {
+
 struct Applicator : SubstApplicator {
   Applicator(ResultSubstitution* subst) : subst(subst) {}
   TermList operator()(unsigned v) const override {
@@ -70,6 +72,8 @@ struct ApplicatorWithEqSort : SubstApplicator {
   const RobSubstitution& vSubst;
 };
 
+} // end namespace
+
 void ForwardDemodulation::attach(SaturationAlgorithm* salg)
 {
   ForwardSimplificationEngine::attach(salg);

diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp
@@ -47,10 +47,10 @@ class LPO
   using PrecedenceOrdering::compare;
   Result compare(TermList tl1, TermList tl2) const override;
   Result compare(AppliedTerm tl1, AppliedTerm tl2) const override;
-  void showConcrete(std::ostream&) const override;
-
   bool isGreater(AppliedTerm tl1, AppliedTerm tl2) const override;
 
+  void showConcrete(std::ostream&) const override;
+
 protected:
   Result comparePredicates(Literal* l1, Literal* l2) const override;
   Result comparePrecedences(const Term* t1, const Term* t2) const;