From fe3af4ffed36701a6578512daeb68d03000b72bf Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Sun, 3 Nov 2024 16:23:22 +0000 Subject: [PATCH] remove clause unblocking, unused --- CMakeLists.txt | 1 - Inferences/BinaryResolution.cpp | 7 - Inferences/Narrow.cpp | 1 - Inferences/SubVarSup.cpp | 1 - Inferences/Superposition.cpp | 6 - Kernel/ColorHelper.cpp | 231 ----------------------------- Kernel/ColorHelper.hpp | 21 --- Makefile | 1 - Parse/SMTLIB2.cpp | 1 - Saturation/SaturationAlgorithm.cpp | 1 - Shell/Options.cpp | 7 - 11 files changed, 278 deletions(-) delete mode 100644 Kernel/ColorHelper.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ba6518a54..c18d189cb3 100644 --- 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 index b80dae2762..85a9aeb9cb 100644 --- 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 index 02d39b26d2..8752804630 100644 --- 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 index 037e7eecc0..a130b46579 100644 --- 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 index 7cc844bb0b..55de9b223a 100644 --- 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 "<toString()<<" into "<toString()<inferencesSkippedDueToColors++; return false; } diff --git a/Kernel/ColorHelper.cpp b/Kernel/ColorHelper.cpp deleted file mode 100644 index 4dbda5c3ca..0000000000 --- a/Kernel/ColorHelper.cpp +++ /dev/null @@ -1,231 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file ColorHelper.cpp - * Implements class ColorHelper. - */ - -#include "Lib/DHMap.hpp" -#include "Lib/Environment.hpp" - -#include "Saturation/SaturationAlgorithm.hpp" - -#include "Shell/Options.hpp" - -#include "Clause.hpp" -#include "EqHelper.hpp" -#include "Inference.hpp" -#include "Renaming.hpp" -#include "Signature.hpp" -#include "Term.hpp" -#include "TermIterators.hpp" - -#include "ColorHelper.hpp" - -namespace Kernel -{ - -using namespace std; - -/** - * Return true if symbol number @c functor is transparent. If @c predicate - * is true, we assume @c functor to be predicate number, otherwise it is - * a function number. - */ -bool ColorHelper::isTransparent(bool predicate, unsigned functor) -{ - Signature::Symbol* sym; - if (predicate) { - sym = env.signature->getPredicate(functor); - } - else { - sym = env.signature->getFunction(functor); - } - return sym->color()==COLOR_TRANSPARENT; -} - -bool ColorHelper::hasColoredPredicates(Clause* c) -{ - unsigned clen = c->length(); - for (unsigned i=0; ifunctor())) { - return true; - } - } - return false; -} - -/** - * collect all occurrences colored constants of a clause c in the stack acc - * @since 04/05/2013 Manchester, improved to use new NonVariableIterator - * @author Andrei Voronkov - */ -void ColorHelper::collectColoredConstants(Clause* c, Stack& acc) -{ - unsigned clen = c->length(); - for (unsigned i=0; icolor() == COLOR_TRANSPARENT) { - tit.right(); - continue; - } - if (t->arity() == 0) { - acc.push(t); - } - } - } -} // collectColoredConstants - -Clause* ColorHelper::skolemizeColoredConstants(Clause* c) -{ - Stack coloredConstants; - collectColoredConstants(c,coloredConstants); - if (coloredConstants.isEmpty()) { - return 0; - } - - unsigned clen = c->length(); - static LiteralStack resStack; - resStack.reset(); - resStack.loadFromIterator(c->iterLits()); - - ASS_EQ(resStack.size(), clen); - - while (coloredConstants.isNonEmpty()) { - TermList replaced = TermList(coloredConstants.pop()); - - unsigned newFn = env.signature->addSkolemFunction(0); - TermList newTrm = TermList(Term::create(newFn, 0, 0)); - - for (unsigned i=0; igetDistinctVars(); - unsigned newFn = env.signature->addSkolemFunction(varCnt, "CU"); - - static Stack argStack; - argStack.reset(); - //variables in normalized term are X0,..X, so we put the - //same into the Skolem term - for (unsigned i=0; ilength(); - for (unsigned i=0; ifunctor())) { - ensureSkolemReplacement(t, map); - //we will replace this term, so we do not descend into it - tit.right(); - } - } - } -} - -Term* ColorHelper::applyReplacement(Term* t, TermMap& map) -{ - Renaming r; - r.normalizeVariables(t); - Term* norm = r.apply(t); - ASS(map.find(norm)); - Term* tgtNorm = map.get(norm); - - Renaming inv; - inv.makeInverse(r); - Term* tgt = inv.apply(tgtNorm); - ASS(tgt->containsAllVariablesOf(t)); - ASS(t->containsAllVariablesOf(tgt)); - ASS_EQ(tgt->color(), COLOR_TRANSPARENT); - return tgt; -} - -Clause* ColorHelper::skolemizeColoredTerms(Clause* c) -{ - static TermMap replMap; - replMap.reset(); - - collectSkolemReplacements(c, replMap); - if (replMap.isEmpty()) { - return 0; - } - - static LiteralStack resStack; - resStack.reset(); - - unsigned clen = c->length(); - for (unsigned i=0; ifunctor())) { - //here we each time remove at least one colored symbol - Term* newTrm = applyReplacement(t,replMap); - lit = EqHelper::replace(lit,TermList(t),TermList(newTrm)); - goto start_replacing; - } - } - resStack.push(lit); - } - - ASS_EQ(resStack.size(), clen); - Clause* res = Clause::fromStack(resStack, NonspecificInference1(InferenceRule::COLOR_UNBLOCKING, c)); - return res; -} - -void ColorHelper::tryUnblock(Clause* c, SaturationAlgorithm* salg) -{ -// if (hasOnlyColoredConstants(c)) { - if (!hasColoredPredicates(c)) { -// Clause* unblocked = skolemizeColoredConstants(c); - Clause* unblocked = skolemizeColoredTerms(c); - if (unblocked) { - if (env.options->showBlocked()) { - cout<<"Unblocking clause "<toString()<addNewClause(unblocked); - } - } - -} - -} // namespace Kernel diff --git a/Kernel/ColorHelper.hpp b/Kernel/ColorHelper.hpp index b16313692c..f7a1a86340 100644 --- 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 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& acc); }; } diff --git a/Makefile b/Makefile index 0f7f78eff9..aeab50c2d3 100644 --- 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 index 55491afc35..e5c9c1e74c 100644 --- 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 index 589fc6b667..e4197f31ff 100644 --- 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 index d3ff3c8d7c..f5a55b3c3c 100644 --- 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("show_interpolant","",InterpolantMode::OFF, {"new_heur", #if VZ3