remove clause unblocking, unused

vprover · Nov 3, 2024 · fe3af4f · fe3af4f
1 parent d61c942
commit fe3af4f
Show file tree

Hide file tree

Showing 11 changed files with 0 additions and 278 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -196,7 +196,6 @@ source_group(lib_sys_source_files FILES ${VAMPIRE_LIB_SYS_SOURCES})
 set(VAMPIRE_KERNEL_SOURCES
     Kernel/Clause.cpp
     Kernel/ClauseQueue.cpp
-    Kernel/ColorHelper.cpp
     Kernel/ELiteralSelector.cpp
     Kernel/EqHelper.cpp
     Kernel/FlatTerm.cpp

diff --git a/Inferences/BinaryResolution.cpp b/Inferences/BinaryResolution.cpp
@@ -90,13 +90,6 @@ Clause* BinaryResolution::generateClause(
     if(opts.showBlocked()) {
       std::cout << "Blocked resolution of " << *queryCl << " and " << * resultCl << endl;
     }
-    if(opts.colorUnblocking()) {
-      SaturationAlgorithm* salg = SaturationAlgorithm::tryGetInstance();
-      if(salg) {
-        ColorHelper::tryUnblock(queryCl, salg);
-        ColorHelper::tryUnblock(resultCl, salg);
-      }
-    }
     return 0;
   }
 

diff --git a/Inferences/Narrow.cpp b/Inferences/Narrow.cpp
@@ -22,7 +22,6 @@
 #include "Lib/VirtualIterator.hpp"
 
 #include "Kernel/Clause.hpp"
-#include "Kernel/ColorHelper.hpp"
 #include "Kernel/EqHelper.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Ordering.hpp"

diff --git a/Inferences/SubVarSup.cpp b/Inferences/SubVarSup.cpp
@@ -22,7 +22,6 @@
 #include "Lib/DHSet.hpp"
 
 #include "Kernel/Clause.hpp"
-#include "Kernel/ColorHelper.hpp"
 #include "Kernel/EqHelper.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Ordering.hpp"

diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp
@@ -173,12 +173,6 @@ bool Superposition::checkClauseColorCompatibility(Clause* eqClause, Clause* rwCl
   if(getOptions().showBlocked()) {
     std::cout<<"Blocked superposition of "<<eqClause->toString()<<" into "<<rwClause->toString()<<std::endl;
   }
-  if(getOptions().colorUnblocking()) {
-    SaturationAlgorithm* salg = SaturationAlgorithm::tryGetInstance();
-    ASS(salg);
-    ColorHelper::tryUnblock(rwClause, salg);
-    ColorHelper::tryUnblock(eqClause, salg);
-  }
   env.statistics->inferencesSkippedDueToColors++;
   return false;
 }

diff --git a/Kernel/ColorHelper.cpp b/Kernel/ColorHelper.cpp
diff --git a/Kernel/ColorHelper.hpp b/Kernel/ColorHelper.hpp
@@ -18,15 +18,10 @@
 #include "Forwards.hpp"
 
 #include "Debug/Assertion.hpp"
-
-#include "Lib/DHMap.hpp"
 #include "Lib/Environment.hpp"
 
 namespace Kernel {
 
-using namespace Lib;
-using namespace Saturation;
-
 class ColorHelper {
 public:
 
@@ -49,22 +44,6 @@ class ColorHelper {
   static bool compatible(Color c1, Color c2) {
     return combine(c1,c2)!=COLOR_INVALID;
   }
-
-  static bool isTransparent(bool predicate, unsigned functor);
-  static bool hasColoredPredicates(Clause* c);
-  static Clause* skolemizeColoredConstants(Clause* c);
-  static Clause* skolemizeColoredTerms(Clause* c);
-
-  static void tryUnblock(Clause* c, SaturationAlgorithm* salg);
-
-private:
-  typedef DHMap<Term*, Term*> TermMap;
-
-  static void ensureSkolemReplacement(Term* t, TermMap& map);
-  static void collectSkolemReplacements(Clause* c, TermMap& map);
-
-  static Term* applyReplacement(Term* t, TermMap& map);
-  static void collectColoredConstants(Clause* c, Stack<Term*>& acc);
 };
 
 }

diff --git a/Makefile b/Makefile
@@ -167,7 +167,6 @@ VLS_OBJ= Lib/Sys/Multiprocessing.o
 
 VK_OBJ= Kernel/Clause.o\
         Kernel/ClauseQueue.o\
-        Kernel/ColorHelper.o\
         Kernel/EqHelper.o\
         Kernel/FlatTerm.o\
         Kernel/Formula.o\

diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
@@ -20,7 +20,6 @@
 #include "Lib/NameArray.hpp"
 #include "Lib/StringUtils.hpp"
 #include "Kernel/Clause.hpp"
-#include "Kernel/ColorHelper.hpp"
 #include "Kernel/Formula.hpp"
 #include "Kernel/FormulaUnit.hpp"
 #include "Kernel/Inference.hpp"

diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp
@@ -25,7 +25,6 @@
 #include "Indexing/LiteralIndexingStructure.hpp"
 
 #include "Kernel/Clause.hpp"
-#include "Kernel/ColorHelper.hpp"
 #include "Kernel/EqHelper.hpp"
 #include "Kernel/FormulaUnit.hpp"
 #include "Kernel/Inference.hpp"

diff --git a/Shell/Options.cpp b/Shell/Options.cpp
@@ -2371,13 +2371,6 @@ void Options::init()
     //*********************** Vinter???  *******************************
     //******************************************************************
 
-    _colorUnblocking = BoolOptionValue("color_unblocking","",false);
-    _colorUnblocking.description="";
-    _lookup.insert(&_colorUnblocking);
-    _colorUnblocking.setExperimental();
-    _colorUnblocking.tag(OptionTag::OTHER);
-
-
     _showInterpolant = ChoiceOptionValue<InterpolantMode>("show_interpolant","",InterpolantMode::OFF,
                                                           {"new_heur",
 #if VZ3