Removing unused files, dead code.

[MichaelRawson]

Some code in Vampire's tree appears to no longer be used. While this is not a problem in itself, it adds to the noise for new contributors and some dead code is still being compiled or even linked (see e.g. PR #153 to remove Lingeling sources). Additionally, changes to interfaces require more effort as code that is no longer used needs fixing.

After some discussion with others, I believe some of the following could be removed:

• [x] Saturation/Limits are empty files.
• [x] Shell/SimplifyProver isn't used anywhere - used to be support for the Simplify theorem prover's language
• [x] similar but not the same, the mysterious Shell/ProofSimplifier
• [x] BFNT and BFNTMainLoop is an old form of finite model building.
• [x] Inferences/InterpretedSimplifier commented out
• [x] Indexing/ArithmeticIndex commented out
• [x] VUtil and friends - no longer build, not touched in several years
• [x] various "frontends":
  • [x] vutil
  • [x] ucompit
  • [x] vclausify
  • [x] vcompit
  • [x] vground
  • [x] vsat
  • [x] vltb
  • [x] vtest
• [x] Significant chunk of Test
• [x] value in TimeCounterUnit: TC_BDD etc.
• [x] SMTLIB 1 support?
• [x] TWLSolver
• [x] Lib::InPlaceStack
• [x] Many things commented out in build system:
  • [x] Lib::Graph
  • [x] MatchTag
  • [x] OptionsReader
  • [x] FormulaIndex
  • [x] CTFwSubsAndRes
  • [x] CParser
  • [x] EqualityAxiomatiser
  • [x] GlobalOptions
  • [x] Refutation
  • [x] PDUtils
• [x] other fluff in build systems that doesn't exist any more
• [x] code guarded by #if GNUMP
• [x] methods in SAT::Preprocess
• [x] Inferences::SLQueryForwardSubsumption, Inferences::RefutationSeekerFSE
• [x] references to EGSubstitution
• [x] commented-out functions in Kernel/RobSubstitution
• [x] commented-out functions in Kernel/SortHelper
• [x] Kernel/Currifier.hpp
• [x] Term::askDistinctVars
• [x] "grounding" mode
• [x] Lib::LastCopyWatcher
• [x] Inferences::HyperSuperposition
• [x] PortfolioMode::waitForChildAndCheckIfProofFound
• [x] commented-out functions in Formula.cpp
• [x] DECLARE_PLACEMENT_NEW
• [x] TermSharing::insertRecurrently
• [x] Lib::TimeCounter
• [x] Shell::Profile
• [x] FoolAwareSubformulaIterator and FoolAwareSubtermIterator
• [x] InstGen
• [x] ArrayTheoryISE
• [x] Api/
• [x] LTB
• [x] env.out()
• [x] Lib::MemoryLeak
• [ ] Minisat's limitMemory, we control its allocations.
• [ ] Lib::MultiCounter
• [ ] applyToLiteral in SubstHelper
• [ ] Various things in Matcher: OCMatchIterator, regular MatchIterator...
• [ ] Some of the scripts in scripts seem like they might no longer serve a purpose.
• [ ] SortHelper::getTermSort
• [ ] old question-answering logic, see #442

• [ ] combinatory HOL approach, superseded by HOL branch

  Some things might be used in the near future, but currently are not.

• [ ] CodeTreeSubsumptionIndex and ClauseCodeTree, orphaned by CTFwSubsAndRes - see below.

Credit to @quickbeam123, @ibnyusuf and @selig for identifying some of these. What I'd like from the team is help to identify more unused files or dead code, as well as rescuing files that need to be kept.

Eventually things that are still on the list will be removed by PR. Fear not, however, one of the many virtues of source control is the ability to reanimate code from beyond the grave. Thank you!

[quickbeam123]

What about the whole API folder?

There is also some mysterious looking ProofSimplifier in Shell.

[MichaelRawson]

Very possibly @quickbeam123! I'm going to chat with Giles Monday about any politics I need to be aware of, then start deleting things in order of least-likely-to-be-wanted first.

[ibnyusuf]

Inferences/InterpretedSimplifier is completed commented out. Perhaps it can be removed.

[quickbeam123]

Some values in TimeCounterUnit most likely don't occur in the code anymore... Like TC_BDD_CLAUSIFICATION, etc. Could be removed as well!

[quickbeam123]

There also some code, authored by Ioan, generally guarded by #if GNUMP and thus not compiled currently, which could perhaps be removed.

[quickbeam123]

Got another one: CTFwSubsAndRes.*

• maybe useful if at some point want to revive code trees for subsumption, but currently not even compiled
• by the way IndexManager holds a reference to CodeTreeSubsumptionIndex via FW_SUBSUMPTION_CODE_TREE, but only CTFwSubsAndRes would ever request this index.

So, transitively, CodeTreeSubsumptionIndex is also unused and maybe some other indices are formally alive but unused because of how IndexManager works.

[MichaelRawson]

@quickbeam123 - good spot, I think @JakobR plans to fix something in this region - perhaps they can comment to see what they need?

[JakobR]

@MichaelRawson feel free to remove CTFwSubsAndRes; I will revive it from the history in case I need it later.

It would be nice if we could keep CodeTreeSubsumptionIndex and ClauseCodeTree though (they're both compiled now, but probably unused). But if they're too much of a hassle to keep around, you can remove them as well and I will deal with it later.

[MichaelRawson]

@JakobR - thanks. OK, CTFw can go but I'll keep code trees - I'm not in a hurry to delete stuff people want, only the stuff nobody wants. :-)

[MichaelRawson]

@easychair and/or @quickbeam123 - a reminder, do you have some data about which options are/are not useful in terms of schedules? Naturally it's not the only consideration when removing something, but it's a pretty good indicator.

[quickbeam123]

I have lot's of data, but it's not so easy to interpret it. Most notably, it's not entirely clear where draw the line and call an option/value not worth maintaining. For most of the cases, one can find a problem that the database cannot solve otherwise... (then how many lost solution can be reclaimed by more search, or how many lost solutions are worth sacrificing for better maintenance?)

[MichaelRawson]

Most notably, it's not entirely clear where draw the line and call an option/value not worth maintaining

I think this is the crux of it. Maybe we can start by ranking options in terms of effectiveness? Is that a reasonable thing to do?