From 9a28dccfede6aae03761879561c97929c35758d7 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Fri, 17 Apr 2026 15:00:21 +0200 Subject: [PATCH 1/5] Separate generalizing term index that only uses code trees --- Indexing/CodeTree.cpp | 2 +- Indexing/CodeTree.hpp | 4 ++-- Indexing/CodeTreeInterfaces.cpp | 31 ++++++++------------------- Indexing/CodeTreeInterfaces.hpp | 15 ++++--------- Indexing/Index.hpp | 2 +- Indexing/IndexManager.cpp | 2 +- Indexing/TermCodeTree.cpp | 12 +++++++---- Indexing/TermCodeTree.hpp | 2 +- Indexing/TermIndex.cpp | 22 ++++++------------- Indexing/TermIndex.hpp | 24 +++++++++++++++------ Indexing/TermIndexingStructure.hpp | 4 ---- Indexing/TermSubstitutionTree.hpp | 8 ------- Inferences/ALASCA/Demodulation.hpp | 2 +- Inferences/ALASCA/FwdDemodulation.cpp | 4 ++-- Inferences/ALASCA/FwdDemodulation.hpp | 2 +- Inferences/Induction.cpp | 4 ++-- Inferences/Induction.hpp | 4 ++-- Kernel/ALASCA/Index.hpp | 20 +++++++++++++---- Shell/FunctionDefinitionHandler.cpp | 2 +- 19 files changed, 77 insertions(+), 89 deletions(-) diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 27b6fbe362..a25924b995 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -618,7 +618,7 @@ bool CodeTree::Matcher::execute() } template -void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) +void CodeTree::Matcher::init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) { tree=tree_; entry=entry_; diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 02d7a0aacc..8d8e7995af 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -385,7 +385,7 @@ class CodeTree } protected: - void init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_ = 0, + void init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_ = 0, size_t linfoCnt_ = 0, Stack* firstsInBlocks_ = 0); bool backtrack(); @@ -419,7 +419,7 @@ class CodeTree Stack> btStack; CodeOp* entry; - CodeTree* tree; + CodeTree const* tree; /** * Array of alternative LitInfo objects diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index 0e973033f0..945aa19aa6 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -15,6 +15,7 @@ #include "Indexing/Index.hpp" #include "Indexing/ResultSubstitution.hpp" +#include "Inferences/ALASCA/Demodulation.hpp" #include "Lib/Allocator.hpp" #include "Lib/Recycled.hpp" #include "Debug/TimeProfiling.hpp" @@ -91,11 +92,11 @@ class CodeTreeTIS::ResultIterator : public IteratorCore> { public: - ResultIterator(CodeTreeTIS* tree, TermList t, bool retrieveSubstitutions) + ResultIterator(const CodeTreeTIS& tree, TermList t, bool retrieveSubstitutions) : _retrieveSubstitutions(retrieveSubstitutions), _found(0), _finished(false), _tree(tree) { - _matcher->init(&_tree->_ct, t); + _matcher->init(&_tree._ct, t); if(_retrieveSubstitutions) { _subst = new CodeTreeSubstitution(&_matcher->bindings, &*_resultNormalizer); @@ -134,7 +135,7 @@ class CodeTreeTIS::ResultIterator if (_retrieveSubstitutions) { if constexpr (!is_indexed_data_normalized::value) { _resultNormalizer->reset(); - _resultNormalizer->normalizeVariables(_found->term); + _resultNormalizer->normalizeVariables(_found->key()); } subs = ResultSubstitutionSP(_subst, /* nondisposable */ true); } @@ -149,40 +150,26 @@ class CodeTreeTIS::ResultIterator bool _retrieveSubstitutions; Data* _found; bool _finished; - CodeTreeTIS* _tree; + const CodeTreeTIS& _tree; Recycled::TermMatcher> _matcher; }; template -VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) +VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) const { if(_ct.isEmpty()) { return VirtualIterator>::getEmpty(); } - return vi( new ResultIterator(this, t, retrieveSubstitutions) ); -} - -template -bool CodeTreeTIS::generalizationExists(TermList t) -{ - if(_ct.isEmpty()) { - return false; - } - - static typename TermCodeTree::TermMatcher tm; - - tm.init(&_ct, t); - bool res=tm.next(); - tm.reset(); - - return res; + return vi( new ResultIterator(*this, t, retrieveSubstitutions) ); } template class CodeTreeTIS; template class CodeTreeTIS; template class CodeTreeTIS; template class CodeTreeTIS; +template class CodeTreeTIS; +template class CodeTreeTIS>; ///////////////// CodeTreeSubsumptionIndex ////////////////////// diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index db5b25fd02..4132319a1f 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -21,7 +21,6 @@ #include "ClauseCodeTree.hpp" #include "Index.hpp" -#include "TermIndexingStructure.hpp" namespace Indexing { @@ -29,17 +28,15 @@ namespace Indexing using namespace Kernel; using namespace Lib; - /** * Term indexing structure using code trees to retrieve generalizations */ - template -class CodeTreeTIS : public TermIndexingStructure +class CodeTreeTIS { public: /* INFO: we ignore unifying the sort of the keys here */ - void handle(Data data, bool insert) final + void handle(Data data, bool insert) { if (insert) { auto ti = new Data(std::move(data)); @@ -49,13 +46,9 @@ class CodeTreeTIS : public TermIndexingStructure } } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) final ; - // TODO use TypedTermList here too - bool generalizationExists(TermList t) final ; - // TODO: get rid of NOT_IMPLEMENTED - VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration) override { NOT_IMPLEMENTED; } + VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const; - void output(std::ostream& out) const final { out << _ct; } + void output(std::ostream& out) const { out << _ct; } private: class ResultIterator; diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp index 97ae146c38..f5c5e9567a 100644 --- a/Indexing/Index.hpp +++ b/Indexing/Index.hpp @@ -95,7 +95,7 @@ struct TermLiteralClause Literal* literal = nullptr; Clause* clause = nullptr; - TypedTermList const& key() const { return term; } + TypedTermList key() const { return term; } auto asTuple() const { return std::make_tuple(clause->number(), literal->getId(), term); } diff --git a/Indexing/IndexManager.cpp b/Indexing/IndexManager.cpp index 8e3b382497..21e0b9295b 100644 --- a/Indexing/IndexManager.cpp +++ b/Indexing/IndexManager.cpp @@ -31,7 +31,7 @@ using namespace Lib; using namespace Indexing; -SIMP_INDEX_IMPL(AlascaIndex) +SIMP_INDEX_IMPL(GeneralizingAlascaIndex) SIMP_INDEX_IMPL(AlascaIndex) SIMP_INDEX_IMPL(DemodulationLHSIndex) SIMP_INDEX_IMPL(DemodulationLHSIndex) diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 804bd5822f..8d580b32bb 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -12,6 +12,8 @@ * Implements class TermCodeTree. */ +#include "Inferences/ALASCA/Demodulation.hpp" + #include "Kernel/FlatTerm.hpp" #include "Kernel/Term.hpp" @@ -46,7 +48,7 @@ void TermCodeTree::insert(Data* data) static CodeStack code; code.reset(); - TermList t=data->term; + TermList t=data->key(); if (t.isVar()) { code.push(CodeOp::getTermOp(ASSIGN_VAR,0)); } @@ -73,7 +75,7 @@ void TermCodeTree::remove(const Data& data) static Stack firstsInBlocks; firstsInBlocks.reset(); - FlatTerm* ft=FlatTerm::create(data.term); + FlatTerm* ft=FlatTerm::create(data.key()); rtm.init(ft, this, &firstsInBlocks); Data* dptr = nullptr; @@ -142,7 +144,7 @@ TermCodeTree::TermMatcher::TermMatcher() } template -void TermCodeTree::TermMatcher::init(CodeTree* tree, TermList t) +void TermCodeTree::TermMatcher::init(CodeTree const* tree, TermList t) { Base::init(tree,tree->getEntryPoint(),/*linfos_=*/0,/*linfoCnt_=*/0); @@ -179,9 +181,11 @@ Data* TermCodeTree::TermMatcher::next() return Base::op->template getSuccessResult(); } +template class TermCodeTree; template class TermCodeTree; -template class TermCodeTree; template class TermCodeTree; template class TermCodeTree; +template class TermCodeTree; +template class TermCodeTree>; }; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 1119a2b6f9..207322536c 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -59,7 +59,7 @@ class TermCodeTree : public CodeTree using Base = Matcher; using Base::ft; - void init(CodeTree* tree, TermList t); + void init(CodeTree const* tree, TermList t); void reset(); Data* next(); diff --git a/Indexing/TermIndex.cpp b/Indexing/TermIndex.cpp index f46774570a..61e61295f0 100644 --- a/Indexing/TermIndex.cpp +++ b/Indexing/TermIndex.cpp @@ -114,8 +114,7 @@ template class DemodulationSubtermIndex; template DemodulationLHSIndex::DemodulationLHSIndex(SaturationAlgorithm& salg) -: TermIndex(new CodeTreeTIS()), _ord(salg.getOrdering()), - _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {}; +: _ord(salg.getOrdering()), _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {} template void DemodulationLHSIndex::handleClause(Clause* c, bool adding) @@ -129,9 +128,7 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding) Literal* lit=(*c)[0]; auto [lhsi, preordered] = EqHelper::getDemodulationLHSIterator(lit, _preordered, _ord); - while (lhsi.hasNext()) { - auto lhs = lhsi.next(); - + for (const auto& lhs : iterTraits(std::move(lhsi))) { // DemodulatorData expects lhs and rhs to be normalized Renaming r; r.normalizeVariables(lhs); @@ -141,7 +138,7 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding) r.apply(EqHelper::getOtherEqualitySide(lit, lhs)), c, preordered, _ord ); - _is->handle(std::move(dd), adding); + GeneralizingTermIndex::_ct.handle(std::move(dd), adding); } } @@ -190,7 +187,7 @@ void InductionTermIndex::handleClause(Clause* c, bool adding) } StructInductionTermIndex::StructInductionTermIndex(SaturationAlgorithm& salg) -: TermIndex(new TermSubstitutionTree()), _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {} +: _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {} void StructInductionTermIndex::handleClause(Clause* c, bool adding) { @@ -214,22 +211,17 @@ void StructInductionTermIndex::handleClause(Clause* c, bool adding) } if (InductionHelper::isInductionTerm(t) && InductionHelper::isStructInductionTerm(t)) { - if (adding) { - _is->insert(TermLiteralClause{ t, lit, c }); - } else { - _is->remove(TermLiteralClause{ t, lit, c }); - } + _ct.handle(TermLiteralClause{ t, lit, c }, adding); } } } } -SkolemisingFormulaIndex::SkolemisingFormulaIndex(SaturationAlgorithm&) - : TermIndex(new TermSubstitutionTree>()) {} +SkolemisingFormulaIndex::SkolemisingFormulaIndex(SaturationAlgorithm&) {} void SkolemisingFormulaIndex::insertFormula(TermList formula, TermList skolem) { - _is->insert(TermWithValue(TypedTermList(formula.term()), skolem)); + _ct.handle(TermWithValue(TypedTermList(formula.term()), skolem), /*insert=*/true); } } // namespace Indexing diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index 95a0ad57e4..b44cf05eb8 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -17,6 +17,7 @@ #define __TermIndex__ #include "Index.hpp" +#include "Indexing/CodeTreeInterfaces.hpp" #include "TermIndexingStructure.hpp" namespace Indexing { @@ -34,9 +35,6 @@ class TermIndex VirtualIterator> getUnifications(TypedTermList t, bool retrieveSubstitutions = true) { return _is->getUnifications(t, retrieveSubstitutions); } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) - { return _is->getGeneralizations(t, retrieveSubstitutions); } - VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { return _is->getInstances(t, retrieveSubstitutions); } @@ -48,6 +46,20 @@ class TermIndex std::unique_ptr> _is; }; +template +class GeneralizingTermIndex +: public Index +{ +public: + auto getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const + { return iterTraits(_ct.getGeneralizations(t, retrieveSubstitutions)); } + + friend std::ostream& operator<<(std::ostream& out, GeneralizingTermIndex const& self) + { return out << self._ct; } +protected: + CodeTreeTIS _ct; +}; + class SuperpositionSubtermIndex : public TermIndex { @@ -92,7 +104,7 @@ class DemodulationSubtermIndex */ template class DemodulationLHSIndex -: public TermIndex +: public GeneralizingTermIndex { public: DemodulationLHSIndex(SaturationAlgorithm& salg); @@ -121,7 +133,7 @@ class InductionTermIndex * Term index for structural induction */ class StructInductionTermIndex -: public TermIndex +: public GeneralizingTermIndex { public: StructInductionTermIndex(SaturationAlgorithm& salg); @@ -132,7 +144,7 @@ class StructInductionTermIndex }; class SkolemisingFormulaIndex -: public TermIndex> +: public GeneralizingTermIndex> { public: SkolemisingFormulaIndex(SaturationAlgorithm&); diff --git a/Indexing/TermIndexingStructure.hpp b/Indexing/TermIndexingStructure.hpp index e43d3a460a..a8cb4d34a1 100644 --- a/Indexing/TermIndexingStructure.hpp +++ b/Indexing/TermIndexingStructure.hpp @@ -31,12 +31,8 @@ class TermIndexingStructure { virtual VirtualIterator> getUnifications(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) = 0; - virtual VirtualIterator> getUnificationsUsingSorts(TypedTermList tt, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual bool generalizationExists(TermList t) { NOT_IMPLEMENTED; } - virtual void output(std::ostream& output) const = 0; friend std::ostream& operator<<(std::ostream& out, TermIndexingStructure const& self) diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index d3a97ea14a..92e0a2a76a 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/Indexing/TermSubstitutionTree.hpp @@ -44,7 +44,6 @@ class TermSubstitutionTree using BindingMap = typename SubstitutionTree::BindingMap; using Node = typename SubstitutionTree::Node; using FastInstancesIterator = typename SubstitutionTree::FastInstancesIterator; - using FastGeneralizationsIterator = typename SubstitutionTree::FastGeneralizationsIterator; using LDIterator = typename SubstitutionTree::LDIterator; using Leaf = typename SubstitutionTree::Leaf; using LeafIterator = typename SubstitutionTree::LeafIterator; @@ -67,9 +66,6 @@ class TermSubstitutionTree { return iterTraits(_inner.template iterator(query, retrieveSubstitutions, /* reversed */ false, std::move(args)...)) ; } - bool generalizationExists(TermList t) override - { return t.isVar() ? false : _inner.generalizationExists(TypedTermList(t.term())); } - void output(std::ostream& out) const final { out << *this; } friend std::ostream& operator<<(std::ostream& out, TermSubstitutionTree const& self) @@ -81,10 +77,6 @@ class TermSubstitutionTree VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions) final { return pvi(getResultIterator(t, retrieveSubstitutions)); } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions) final - { return pvi(getResultIterator(t, retrieveSubstitutions)); } - - VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) final { return pvi(getResultIterator>>(t, /* retrieveSubstitutions */ true, AbstractingUnifier::empty(AbstractionOracle(uwa)), AbstractionOracle(uwa), fixedPointIteration)); } diff --git a/Inferences/ALASCA/Demodulation.hpp b/Inferences/ALASCA/Demodulation.hpp index d9fc3a66cd..a2fa2cb323 100644 --- a/Inferences/ALASCA/Demodulation.hpp +++ b/Inferences/ALASCA/Demodulation.hpp @@ -44,7 +44,7 @@ class Demodulation struct Lhs : public SelectedEquality { Lhs(SelectedEquality self) : SelectedEquality(std::move(self)) {} static const char* name() { return "alasca demodulation lhs"; } - TypedTermList key() { return TypedTermList(SelectedEquality::biggerSide().term()); } + TypedTermList key() const { return TypedTermList(SelectedEquality::biggerSide().term()); } static auto iter(AlascaState& shared, Clause* simplifyWith) { return iterTraits(iterItems(simplifyWith)) diff --git a/Inferences/ALASCA/FwdDemodulation.cpp b/Inferences/ALASCA/FwdDemodulation.cpp index 32650af88e..80c7a8154e 100644 --- a/Inferences/ALASCA/FwdDemodulation.cpp +++ b/Inferences/ALASCA/FwdDemodulation.cpp @@ -22,7 +22,7 @@ namespace Inferences { namespace ALASCA { FwdDemodulation::FwdDemodulation(SaturationAlgorithm& salg) - : _shared(salg.alascaState()), _index(salg.getSimplifyingIndex>()) + : _shared(salg.alascaState()), _index(salg.getSimplifyingIndex>()) {} //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -44,7 +44,7 @@ bool FwdDemodulation::perform(Clause* toSimplify, Clause*& replacement, ClauseIt Stack simplified; for (auto rhs : Rhs::iter(_shared, toSimplify)) { // DEBUG("simplifyable position: ", pos.term, " in ", *pos.lit) - for (auto lhs : _index->generalizations(rhs.term)) { + for (auto lhs : _index->getGeneralizations(rhs.term)) { auto simplified = Demodulation::apply(_shared, *lhs.data, rhs); if (simplified.isSome()) { replacement = simplified.unwrap(); diff --git a/Inferences/ALASCA/FwdDemodulation.hpp b/Inferences/ALASCA/FwdDemodulation.hpp index a437ff2f8b..7cf4326294 100644 --- a/Inferences/ALASCA/FwdDemodulation.hpp +++ b/Inferences/ALASCA/FwdDemodulation.hpp @@ -44,7 +44,7 @@ class FwdDemodulation private: AlascaState& _shared; - std::shared_ptr> _index; + std::shared_ptr> _index; }; } // namespaceALASCA diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index 1799e5a7bf..97cd976378 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -505,7 +505,7 @@ Induction::Induction(SaturationAlgorithm& salg) ClauseIterator Induction::generateClauses(Clause* premise) { return pvi(InductionClauseIterator(premise, InductionHelper(_comparisonIndex.get(), _inductionTermIndex.get()), - _salg, _structInductionTermIndex.get(), _formulaIndex)); + _salg, *_structInductionTermIndex.get(), _formulaIndex)); } void InductionClauseIterator::processClause(Clause* premise) @@ -731,7 +731,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) .map([this](Stack ts) { auto res = VirtualIterator>::getEmpty(); for (const auto& t : ts) { - res = pvi(concatIters(std::move(res), _structInductionTermIndex->getGeneralizations(t, false))); + res = pvi(concatIters(std::move(res), _structInductionTermIndex.getGeneralizations(t, false))); } return make_pair(ts, std::move(res)); })); diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index 145aea20c8..c8493babf2 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -291,7 +291,7 @@ class InductionClauseIterator public: // all the work happens in the constructor! InductionClauseIterator(Clause* premise, InductionHelper helper, const SaturationAlgorithm& salg, - TermIndex* structInductionTermIndex, InductionFormulaIndex& formulaIndex) + const StructInductionTermIndex& structInductionTermIndex, InductionFormulaIndex& formulaIndex) : _helper(helper), _opt(salg.getOptions()), _structInductionTermIndex(structInductionTermIndex), _formulaIndex(formulaIndex), _fnDefHandler(salg.getFunctionDefinitionHandler()) { @@ -355,7 +355,7 @@ class InductionClauseIterator Stack _clauses; InductionHelper _helper; const Options& _opt; - TermIndex* _structInductionTermIndex; + const StructInductionTermIndex& _structInductionTermIndex; InductionFormulaIndex& _formulaIndex; FunctionDefinitionHandler& _fnDefHandler; }; diff --git a/Kernel/ALASCA/Index.hpp b/Kernel/ALASCA/Index.hpp index f786479c19..8cd1a471d5 100644 --- a/Kernel/ALASCA/Index.hpp +++ b/Kernel/ALASCA/Index.hpp @@ -13,6 +13,7 @@ #include "Indexing/SubstitutionTree.hpp" +#include "Indexing/TermIndex.hpp" #include "Kernel/ALASCA.hpp" #include "Debug/TimeProfiling.hpp" @@ -54,10 +55,6 @@ class AlascaIndex : public Indexing::Index { return iterTraits(_index.template getUwa(state, key, _shared.uwaMode(), _shared.uwaFixedPointIteration)) .timeTraced(_lookupStr.c_str()); } - - auto generalizations(TypedTermList key, bool retrieveSubstitutions = true) - { return iterTraits(_index.getGeneralizations(key, retrieveSubstitutions)); } - auto instances(TypedTermList key, bool retrieveSubstitutions = true) { return iterTraits(_index.getInstances(key, retrieveSubstitutions)); } @@ -90,6 +87,21 @@ class AlascaIndex : public Indexing::Index template std::string AlascaIndex::_lookupStr = T::name() + std::string(" lookup"); template std::string AlascaIndex::_maintenanceStr = T::name() + std::string(" maintenance"); +template +class GeneralizingAlascaIndex : public Indexing::GeneralizingTermIndex +{ +public: + GeneralizingAlascaIndex(SaturationAlgorithm& salg) : _shared(salg.alascaState()) {} + + void handleClause(Clause* c, bool adding) override { + for (auto appl : T::iter(_shared, c)) { + Indexing::GeneralizingTermIndex::_ct.handle(std::move(appl), adding); + } + } +private: + Kernel::AlascaState& _shared; +}; + } // namespace Indexing #undef DEBUG diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp index 12f725df50..42214aede9 100644 --- a/Shell/FunctionDefinitionHandler.cpp +++ b/Shell/FunctionDefinitionHandler.cpp @@ -139,7 +139,7 @@ void FunctionDefinitionHandler::initAndPreprocessLate(Problem& prb,const Options defCl->setSplits(SplitSet::getEmpty()); defCl->incRefCnt(); ASS_EQ(condLits.size()+1,lits.size()); - _is->insert(TermLiteralClause {lhs.term(), lits.top(), defCl}); + _is->handle(TermLiteralClause {lhs.term(), lits.top(), defCl}, /*insert=*/true); // TODO should we store this clause anywhere else? } else { it.replace(defCl); From a5ccff3d09efe4f1bb12428aeec1c7251c029c04 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sat, 18 Apr 2026 17:48:28 +0200 Subject: [PATCH 2/5] Remove ResultSubstitution dependency from CodeTree matching --- Indexing/CodeTreeInterfaces.cpp | 70 +++------------------- Indexing/CodeTreeInterfaces.hpp | 36 ++++++++++- Inferences/ForwardDemodulation.cpp | 18 +++--- Inferences/ForwardGroundJoinability.cpp | 11 ++-- Inferences/FunctionDefinitionRewriting.cpp | 15 +++-- Inferences/HOL/CNFOnTheFly.cpp | 2 +- Inferences/Induction.cpp | 6 +- Shell/FunctionDefinitionHandler.hpp | 2 +- 8 files changed, 66 insertions(+), 94 deletions(-) diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index 945aa19aa6..70223ab803 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -14,7 +14,6 @@ */ #include "Indexing/Index.hpp" -#include "Indexing/ResultSubstitution.hpp" #include "Inferences/ALASCA/Demodulation.hpp" #include "Lib/Allocator.hpp" #include "Lib/Recycled.hpp" @@ -22,7 +21,6 @@ #include "Lib/VirtualIterator.hpp" #include "Kernel/Renaming.hpp" -#include "Kernel/SubstHelper.hpp" #include "Kernel/Term.hpp" #include "ClauseCodeTree.hpp" @@ -36,60 +34,9 @@ namespace Indexing using namespace Lib; using namespace Kernel; -template -class CodeTreeSubstitution -: public ResultSubstitution -{ -public: - CodeTreeSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer) - : _bindings(bindings), _resultNormalizer(resultNormalizer) - {} - - USE_ALLOCATOR(CodeTreeSubstitution); - - TermList apply(unsigned var) - { - if constexpr (is_indexed_data_normalized::value) { - return (*_bindings)[var]; - } else { - ASS(_resultNormalizer->contains(var)); - unsigned nvar=_resultNormalizer->get(var); - TermList res=(*_bindings)[nvar]; - ASS(res.isTerm()||res.isOrdinaryVar()); - ASSERT_VALID(res); - return res; - } - } - - TermList applyToBoundResult(unsigned v) override - { - return apply(v); - } - - TermList applyToBoundResult(TermList t) override - { - return SubstHelper::apply(t, *this); - } - - Literal* applyToBoundResult(Literal* lit) override - { - return SubstHelper::apply(lit, *this); - } - - bool isIdentityOnQueryWhenResultBound() override {return true;} -private: - void output(std::ostream& out) const final - { out << "CodeTreeSubstitution()"; } - - CodeTree::BindingArray* _bindings; - Renaming* _resultNormalizer; -}; - -/////////////////////////////////////// - template class CodeTreeTIS::ResultIterator -: public IteratorCore> +: public IteratorCore*, Data>> { public: ResultIterator(const CodeTreeTIS& tree, TermList t, bool retrieveSubstitutions) @@ -99,7 +46,7 @@ class CodeTreeTIS::ResultIterator _matcher->init(&_tree._ct, t); if(_retrieveSubstitutions) { - _subst = new CodeTreeSubstitution(&_matcher->bindings, &*_resultNormalizer); + _subst = new GenSubstitution(&_matcher->bindings, &*_resultNormalizer); } } @@ -127,25 +74,22 @@ class CodeTreeTIS::ResultIterator return _found; } - QueryRes next() override + QueryRes*, Data> next() override { ASS(_found); - ResultSubstitutionSP subs; if (_retrieveSubstitutions) { if constexpr (!is_indexed_data_normalized::value) { _resultNormalizer->reset(); _resultNormalizer->normalizeVariables(_found->key()); } - subs = ResultSubstitutionSP(_subst, /* nondisposable */ true); } - auto out = QueryRes(subs, _found); + auto out = QueryRes*, Data>(_subst, _found); _found=0; return out; } private: - - CodeTreeSubstitution* _subst; + GenSubstitution* _subst = nullptr; Recycled _resultNormalizer; bool _retrieveSubstitutions; Data* _found; @@ -155,10 +99,10 @@ class CodeTreeTIS::ResultIterator }; template -VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) const +VirtualIterator*, Data>> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) const { if(_ct.isEmpty()) { - return VirtualIterator>::getEmpty(); + return VirtualIterator*, Data>>::getEmpty(); } return vi( new ResultIterator(*this, t, retrieveSubstitutions) ); diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index 4132319a1f..3da9a54e1f 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -28,6 +28,40 @@ namespace Indexing using namespace Kernel; using namespace Lib; +template +class GenSubstitution +{ +public: + GenSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer) + : _bindings(bindings), _resultNormalizer(resultNormalizer) {} + + USE_ALLOCATOR(GenSubstitution); + + TermList apply(unsigned var) const { + if constexpr (is_indexed_data_normalized::value) { + return (*_bindings)[var]; + } else { + ASS(_resultNormalizer->contains(var)); + unsigned nvar=_resultNormalizer->get(var); + TermList res=(*_bindings)[nvar]; + ASS(res.isTerm()||res.isOrdinaryVar()); + ASSERT_VALID(res); + return res; + } + } + + TermList apply(TermList t) const { + return SubstHelper::apply(t, *this); + } + + Literal* apply(Literal* lit) const { + return SubstHelper::apply(lit, *this); + } +private: + CodeTree::BindingArray* _bindings; + Renaming* _resultNormalizer; +}; + /** * Term indexing structure using code trees to retrieve generalizations */ @@ -46,7 +80,7 @@ class CodeTreeTIS } } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const; + VirtualIterator*, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const; void output(std::ostream& out) const { out << _ct; } diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index dc27c6905b..a57ed96c02 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -50,19 +50,19 @@ using namespace Saturation; namespace { struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} + Applicator(const GenSubstitution* subst) : subst(subst) {} TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); + return subst->apply(v); } - ResultSubstitution* subst; + const GenSubstitution* subst; }; struct ApplicatorWithEqSort : SubstApplicator { - ApplicatorWithEqSort(ResultSubstitution* subst, const RobSubstitution& vSubst) : subst(subst), vSubst(vSubst) {} + ApplicatorWithEqSort(const GenSubstitution* subst, const RobSubstitution& vSubst) : subst(subst), vSubst(vSubst) {} TermList operator()(unsigned v) const override { - return vSubst.apply(subst->applyToBoundResult(v), 0); + return vSubst.apply(subst->apply(v), 0); } - ResultSubstitution* subst; + const GenSubstitution* subst; const RobSubstitution& vSubst; }; @@ -143,10 +143,8 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, } auto subs = qr.unifier; - ASS(subs->isIdentityOnQueryWhenResultBound()); - - ApplicatorWithEqSort applWithEqSort(subs.ptr(), eqSortSubs); - Applicator applWithoutEqSort(subs.ptr()); + ApplicatorWithEqSort applWithEqSort(subs, eqSortSubs); + Applicator applWithoutEqSort(subs); auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort; AppliedTerm rhsApplied(qr.data->rhs,appl,true); diff --git a/Inferences/ForwardGroundJoinability.cpp b/Inferences/ForwardGroundJoinability.cpp index ea7e0af657..bc72ec662b 100644 --- a/Inferences/ForwardGroundJoinability.cpp +++ b/Inferences/ForwardGroundJoinability.cpp @@ -39,11 +39,11 @@ using namespace std; namespace { struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} + Applicator(const GenSubstitution* subst) : subst(subst) {} TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); + return subst->apply(v); } - ResultSubstitution* subst; + const GenSubstitution* subst; }; } // end namespace @@ -128,10 +128,7 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replace TermList rhs = qr.data->rhs; - auto subs = qr.unifier; - ASS(subs->isIdentityOnQueryWhenResultBound()); - Applicator appl(subs.ptr()); - + Applicator appl(qr.unifier); AppliedTerm rhsApplied(rhs, &appl, true); #if VDEBUG diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index f00d165e6e..c078ac770b 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -37,17 +37,17 @@ using namespace Saturation; namespace { struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} + Applicator(const GenSubstitution* subst) : subst(subst) {} TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); + return subst->apply(v); } - ResultSubstitution* subst; + const GenSubstitution* subst; }; } Clause* performRewriting( Clause *rwClause, Literal *rwLit, TermList rwTerm, Clause *eqClause, - Literal *eqLit, TermList eqLHS, ResultSubstitutionSP subst, + Literal *eqLit, TermList eqLHS, const GenSubstitution* subst, const DemodulationHelper* helper, bool& isEqTautology, Inference&& inf) { ASS(!eqLHS.isVar()); @@ -55,10 +55,9 @@ Clause* performRewriting( TermList tgtTerm = EqHelper::getOtherEqualitySide(eqLit, eqLHS); // This should be the case for code trees - ASS(subst->isIdentityOnQueryWhenResultBound()); - TermList tgtTermS = subst->applyToBoundResult(tgtTerm); + TermList tgtTermS = subst->apply(tgtTerm); - Applicator appl(subst.ptr()); + Applicator appl(subst); if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,&appl)) { return 0; @@ -92,7 +91,7 @@ Clause* performRewriting( if (curr == eqLit) { continue; } - Literal* currAfter = subst->applyToBoundResult(curr); + Literal* currAfter = subst->apply(curr); if (EqHelper::isEqTautology(currAfter)) { isEqTautology = true; diff --git a/Inferences/HOL/CNFOnTheFly.cpp b/Inferences/HOL/CNFOnTheFly.cpp index 0e9bd99daa..5c3fe0894f 100644 --- a/Inferences/HOL/CNFOnTheFly.cpp +++ b/Inferences/HOL/CNFOnTheFly.cpp @@ -195,7 +195,7 @@ ClauseIterator produceClauses(Clause* c, bool generating, SkolemisingFormulaInde if(results.hasNext()){ auto tqr = results.next(); TermList skolemTerm = tqr.data->value; - skolemTerm = tqr.unifier->applyToBoundResult(skolemTerm); + skolemTerm = tqr.unifier->apply(skolemTerm); newTerm = HOL::create::app(srt, args[0], skolemTerm); newTermCreated = true; } diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index 97cd976378..b28241b375 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -543,7 +543,7 @@ struct InductionContextFn { InductionContextFn(Clause* premise, Literal* lit) : _premise(premise), _lit(lit) {} - VirtualIterator operator()(pair, VirtualIterator>> arg) { + VirtualIterator operator()(pair, VirtualIterator*, TermLiteralClause>>> arg) { auto indDepth = _premise->inference().inductionDepth(); // heuristic 2 if (indDepth) { @@ -722,14 +722,14 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) } } // collect term queries for each induction term - auto sideLitsIt = VirtualIterator, VirtualIterator>>>::getEmpty(); + auto sideLitsIt = VirtualIterator, VirtualIterator*, TermLiteralClause>>>>::getEmpty(); if (_opt.nonUnitInduction()) { sideLitsIt = pvi(iterTraits(getSTLIterator(ta_terms.begin(), ta_terms.end())) .map([](const auto& kv){ return kv.first; }) .map([this](Stack ts) { - auto res = VirtualIterator>::getEmpty(); + auto res = VirtualIterator*, TermLiteralClause>>::getEmpty(); for (const auto& t : ts) { res = pvi(concatIters(std::move(res), _structInductionTermIndex.getGeneralizations(t, false))); } diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index 0ecf8b9467..2f87cc08e7 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -97,7 +97,7 @@ class FunctionDefinitionHandler auto getGeneralizations(TypedTermList t) { if (_is.isEmpty()) { - return VirtualIterator>::getEmpty(); + return VirtualIterator*, TermLiteralClause>>::getEmpty(); } return _is->getGeneralizations(t, true); } From f15191945faa4243ec939b77330f1a63ecc7ce1c Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sun, 19 Apr 2026 12:26:40 +0200 Subject: [PATCH 3/5] Fix sorted variable equality case in demodulation --- Indexing/CodeTreeInterfaces.cpp | 2 +- Indexing/CodeTreeInterfaces.hpp | 7 ++- Indexing/Index.hpp | 2 +- Indexing/TermCodeTree.cpp | 57 +++++++++++----------- Indexing/TermCodeTree.hpp | 14 ++++-- Indexing/TermIndex.cpp | 5 +- Inferences/ForwardDemodulation.cpp | 50 ++----------------- Inferences/FunctionDefinitionRewriting.cpp | 14 +----- Inferences/Induction.cpp | 4 +- Kernel/EqHelper.cpp | 18 ++++--- Kernel/Term.cpp | 2 +- Kernel/TypedTermList.hpp | 17 +++++++ UnitTests/tInferences_Demodulation.cpp | 34 +++++++++++++ 13 files changed, 116 insertions(+), 110 deletions(-) diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index 70223ab803..9b48accb46 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -39,7 +39,7 @@ class CodeTreeTIS::ResultIterator : public IteratorCore*, Data>> { public: - ResultIterator(const CodeTreeTIS& tree, TermList t, bool retrieveSubstitutions) + ResultIterator(const CodeTreeTIS& tree, TypedTermList t, bool retrieveSubstitutions) : _retrieveSubstitutions(retrieveSubstitutions), _found(0), _finished(false), _tree(tree) { diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index 3da9a54e1f..6741bbf5a1 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -30,6 +30,7 @@ using namespace Lib; template class GenSubstitution + : public SubstApplicator { public: GenSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer) @@ -37,7 +38,7 @@ class GenSubstitution USE_ALLOCATOR(GenSubstitution); - TermList apply(unsigned var) const { + TermList operator()(unsigned var) const override { if constexpr (is_indexed_data_normalized::value) { return (*_bindings)[var]; } else { @@ -50,6 +51,10 @@ class GenSubstitution } } + TermList apply(unsigned var) const { + return (*this)(var); + } + TermList apply(TermList t) const { return SubstHelper::apply(t, *this); } diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp index f5c5e9567a..3b905eb99b 100644 --- a/Indexing/Index.hpp +++ b/Indexing/Index.hpp @@ -114,7 +114,7 @@ struct TermLiteralClause * left- and right-hand side normalized and cache preorderedness. */ struct DemodulatorData { - DemodulatorData(TypedTermList term, TermList rhs, Clause* clause, bool preordered, const Ordering& ord) + DemodulatorData(TypedTermList term, TypedTermList rhs, Clause* clause, bool preordered, const Ordering& ord) : term(term), rhs(rhs), clause(clause), preordered(preordered), tod(ord.createTermOrderingDiagram()) { // insert pointer to owner as non-null value representing success diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 8d580b32bb..348376b776 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -15,6 +15,7 @@ #include "Inferences/ALASCA/Demodulation.hpp" #include "Kernel/FlatTerm.hpp" +#include "Kernel/Matcher.hpp" #include "Kernel/Term.hpp" #include "Index.hpp" @@ -48,9 +49,14 @@ void TermCodeTree::insert(Data* data) static CodeStack code; code.reset(); - TermList t=data->key(); + auto t = data->key(); if (t.isVar()) { code.push(CodeOp::getTermOp(ASSIGN_VAR,0)); + // we match the variable sort separately, but the binding array has to be prepared + for (const auto& v : iterTraits(VariableIterator(t.sort()))) { + ASS_G(v.var(), 0); // X0 is reserved for the term itself + if (v.var()+1 > _maxVarCnt) { _maxVarCnt = v.var()+1; } + } } else { ASS(t.isTerm()); @@ -61,7 +67,7 @@ void TermCodeTree::insert(Data* data) } code.push(CodeOp::getSuccess(data)); - incorporate(code); + incorporate(code); //@b incorporate should empty the code stack ASS(code.isEmpty()); } @@ -77,7 +83,7 @@ void TermCodeTree::remove(const Data& data) FlatTerm* ft=FlatTerm::create(data.key()); rtm.init(ft, this, &firstsInBlocks); - + Data* dptr = nullptr; for(;;) { if (!rtm.execute()) { @@ -90,34 +96,14 @@ void TermCodeTree::remove(const Data& data) break; } } - + rtm.op->makeFail(); ASS(dptr); delete dptr; ft->destroy(); - - optimizeMemoryAfterRemoval(&firstsInBlocks, rtm.op); - /* - - static TermMatcher tm; - - tm.init(this, ti.t); - - for(;;) { - TermInfo* found=tm.next(); - if (!found) { - INVALID_OPERATION("term being removed was not found"); - } - if (*found==ti) { - tm.op->makeFail(); - delete found; - break; - } - } - tm.deinit(); - */ + optimizeMemoryAfterRemoval(&firstsInBlocks, rtm.op); } // TermCodeTree::remove template @@ -125,7 +111,7 @@ void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_) { Base::init(tree_, tree_->getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); - + Base::firstsInBlocks->push(Base::entry); Base::ft=ft_; @@ -144,12 +130,13 @@ TermCodeTree::TermMatcher::TermMatcher() } template -void TermCodeTree::TermMatcher::init(CodeTree const* tree, TermList t) +void TermCodeTree::TermMatcher::init(CodeTree const* tree, TypedTermList t) { Base::init(tree,tree->getEntryPoint(),/*linfos_=*/0,/*linfoCnt_=*/0); ASS(!ft); ft = FlatTerm::create(t); + _querySort = t.sort(); Base::op=Base::entry; Base::tp=0; @@ -171,14 +158,26 @@ Data* TermCodeTree::TermMatcher::next() //all possible matches are exhausted return 0; } - + Base::_matched=Base::execute(); if (!Base::_matched) { return 0; } ASS(Base::op->isSuccess()); - return Base::op->template getSuccessResult(); + auto res = Base::op->template getSuccessResult(); + if (res->key().isVar()) { + // match the variable sort separately + Substitution subst; + if (!MatchingUtils::matchTerms(res->key().sort(), _querySort, subst)) { + return nullptr; + } + for (const auto& [v,t] : iterTraits(subst.items())) { + ASS_G(v, 0); // X0 is reserved for the term itself + Base::bindings[v] = t; + } + } + return res; } template class TermCodeTree; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 207322536c..84b6205e79 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -20,6 +20,8 @@ #include "Lib/Allocator.hpp" #include "Lib/Stack.hpp" +#include "Kernel/TypedTermList.hpp" + #include "CodeTree.hpp" @@ -29,11 +31,11 @@ using namespace Lib; using namespace Kernel; template -class TermCodeTree : public CodeTree +class TermCodeTree : public CodeTree { protected: static void onCodeOpDestroying(CodeOp* op); - + public: TermCodeTree(); @@ -59,12 +61,14 @@ class TermCodeTree : public CodeTree using Base = Matcher; using Base::ft; - void init(CodeTree const* tree, TermList t); + void init(CodeTree const* tree, TypedTermList t); void reset(); - + Data* next(); - + USE_ALLOCATOR(TermMatcher); + private: + TermList _querySort; }; }; diff --git a/Indexing/TermIndex.cpp b/Indexing/TermIndex.cpp index 61e61295f0..dbd9f5de0f 100644 --- a/Indexing/TermIndex.cpp +++ b/Indexing/TermIndex.cpp @@ -132,10 +132,11 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding) // DemodulatorData expects lhs and rhs to be normalized Renaming r; r.normalizeVariables(lhs); + auto sortR = r.apply(lhs.sort()); DemodulatorData dd( - TypedTermList(r.apply(lhs),r.apply(lhs.sort())), - r.apply(EqHelper::getOtherEqualitySide(lit, lhs)), + TypedTermList(r.apply(lhs),sortR), + TypedTermList(r.apply(EqHelper::getOtherEqualitySide(lit, lhs)),sortR), c, preordered, _ord ); GeneralizingTermIndex::_ct.handle(std::move(dd), adding); diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index a57ed96c02..629227698b 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -25,7 +25,6 @@ #include "Kernel/Term.hpp" #include "Kernel/TermIterators.hpp" #include "Kernel/ColorHelper.hpp" -#include "Kernel/RobSubstitution.hpp" #include "Indexing/Index.hpp" #include "Indexing/TermIndex.hpp" @@ -47,27 +46,6 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; -namespace { - -struct Applicator : SubstApplicator { - Applicator(const GenSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->apply(v); - } - const GenSubstitution* subst; -}; - -struct ApplicatorWithEqSort : SubstApplicator { - ApplicatorWithEqSort(const GenSubstitution* subst, const RobSubstitution& vSubst) : subst(subst), vSubst(vSubst) {} - TermList operator()(unsigned v) const override { - return vSubst.apply(subst->apply(v), 0); - } - const GenSubstitution* subst; - const RobSubstitution& vSubst; -}; - -} // end namespace - template ForwardDemodulation::ForwardDemodulation(SaturationAlgorithm& salg) : _preorderedOnly(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED), @@ -124,30 +102,8 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, } auto lhs = qr.data->term; - - // TODO: - // to deal with polymorphic matching - // Ideally, we would like to extend the substitution - // returned by the index to carry out the sort match. - // However, ForwardDemodulation uses a CodeTree as its - // indexing mechanism, and it is not clear how to extend - // the substitution returned by a code tree. - static RobSubstitution eqSortSubs; - if(lhs.isVar()){ - eqSortSubs.reset(); - TermList querySort = trm.sort(); - TermList eqSort = qr.data->term.sort(); - if(!eqSortSubs.match(eqSort, 0, querySort, 1)){ - continue; - } - } - auto subs = qr.unifier; - ApplicatorWithEqSort applWithEqSort(subs, eqSortSubs); - Applicator applWithoutEqSort(subs); - auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort; - - AppliedTerm rhsApplied(qr.data->rhs,appl,true); + AppliedTerm rhsApplied(qr.data->rhs,subs,true); bool preordered = qr.data->preordered; ASS_EQ(_ord.compare(trm,rhsApplied),Ordering::reverse(_ord.compare(rhsApplied,trm))); @@ -156,7 +112,7 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, #if VDEBUG auto dcomp = _ord.compareUnidirectional(trm,rhsApplied); #endif - qr.data->tod->init(appl); + qr.data->tod->init(subs); if (!preordered && (_preorderedOnly || !qr.data->tod->next())) { ASS_NEQ(dcomp,Ordering::GREATER); continue; @@ -182,7 +138,7 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, TermList rhsS = rhsApplied.apply(); - if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, appl)) { + if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, subs)) { continue; } diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index c078ac770b..cd7b16927f 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -35,16 +35,6 @@ using namespace Lib; using namespace Kernel; using namespace Saturation; -namespace { -struct Applicator : SubstApplicator { - Applicator(const GenSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->apply(v); - } - const GenSubstitution* subst; -}; -} - Clause* performRewriting( Clause *rwClause, Literal *rwLit, TermList rwTerm, Clause *eqClause, Literal *eqLit, TermList eqLHS, const GenSubstitution* subst, @@ -57,9 +47,7 @@ Clause* performRewriting( // This should be the case for code trees TermList tgtTermS = subst->apply(tgtTerm); - Applicator appl(subst); - - if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,&appl)) { + if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,subst)) { return 0; } diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index b28241b375..218bd2109c 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -505,7 +505,7 @@ Induction::Induction(SaturationAlgorithm& salg) ClauseIterator Induction::generateClauses(Clause* premise) { return pvi(InductionClauseIterator(premise, InductionHelper(_comparisonIndex.get(), _inductionTermIndex.get()), - _salg, *_structInductionTermIndex.get(), _formulaIndex)); + _salg, _structInductionTermIndex.get(), _formulaIndex)); } void InductionClauseIterator::processClause(Clause* premise) @@ -731,7 +731,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) .map([this](Stack ts) { auto res = VirtualIterator*, TermLiteralClause>>::getEmpty(); for (const auto& t : ts) { - res = pvi(concatIters(std::move(res), _structInductionTermIndex.getGeneralizations(t, false))); + res = pvi(concatIters(std::move(res), _structInductionTermIndex->getGeneralizations(t, false))); } return make_pair(ts, std::move(res)); })); diff --git a/Kernel/EqHelper.cpp b/Kernel/EqHelper.cpp index 6c3d603db5..6b7bd42f93 100644 --- a/Kernel/EqHelper.cpp +++ b/Kernel/EqHelper.cpp @@ -302,8 +302,10 @@ std::pair,bool> EqHelper::getDemodulationLHSItera if (lit->isNegative()) { return { VirtualIterator::getEmpty(), isPreordered }; } - TermList t0=*lit->nthArgument(0); - TermList t1=*lit->nthArgument(1); + auto [lhs, rhs] = lit->eqArgs(); + auto sort = lit->eqArgSort(); + TypedTermList t0(lhs, sort); + TypedTermList t1(rhs, sort); switch(ord.getEqualityArgumentOrder(lit)) { case Ordering::INCOMPARABLE: @@ -315,24 +317,24 @@ std::pair,bool> EqHelper::getDemodulationLHSItera // If the equation is its own variant when oriented // reversed, there's no need to index both sides if (MatchingUtils::matchReversedArgs(lit, lit)) { - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; } - return { withEqualitySort(lit, iterItems(t0, t1)), isPreordered }; + return { pvi(iterItems(t0, t1)), isPreordered }; } - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; } if (t1.containsAllVariablesOf(t0)) { - return { withEqualitySort(lit, getSingletonIterator(t1) ), isPreordered }; + return { pvi(getSingletonIterator(t1)), isPreordered }; } break; case Ordering::GREATER: ASS(t0.containsAllVariablesOf(t1)); isPreordered = true; - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; case Ordering::LESS: ASS(t1.containsAllVariablesOf(t0)); isPreordered = true; - return { withEqualitySort(lit, getSingletonIterator(t1) ), isPreordered }; + return { pvi(getSingletonIterator(t1)), isPreordered }; //there should be no equality literals of equal terms case Ordering::EQUAL: ASSERTION_VIOLATION_REP(*lit); diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp index b54c76704b..9db1764f1f 100644 --- a/Kernel/Term.cpp +++ b/Kernel/Term.cpp @@ -1612,7 +1612,7 @@ Literal* Literal::create(unsigned predicate, unsigned arity, bool polarity, GetA for (auto i : range(0, arity)) { auto a = normArg(i); *l->nthArgument(i) = a; - ASS(a.isVar() || predicate != 0 || SortHelper::getResultSort(a.term()) != AtomicSort::superSort()) + ASS(a.isVar() || predicate != 0 || a.term()->isSpecial() || SortHelper::getResultSort(a.term()) != AtomicSort::superSort()) } if (twoVarEqSort) { ASS(*twoVarEqSort != AtomicSort::superSort()) diff --git a/Kernel/TypedTermList.hpp b/Kernel/TypedTermList.hpp index 6f6b78ecc5..e72c964538 100644 --- a/Kernel/TypedTermList.hpp +++ b/Kernel/TypedTermList.hpp @@ -16,6 +16,7 @@ #include "Term.hpp" #include "SortHelper.hpp" #include "Lib/Reflection.hpp" +#include "Lib/Set.hpp" namespace Kernel { using SortId = Kernel::TermList; @@ -40,6 +41,22 @@ class TypedTermList : public TermList } TypedTermList(Term* t) : TypedTermList(TermList(t), SortHelper::getResultSort(t)) {} + VirtualIterator varIter() const { + if (isVar()) { + return pvi(concatIters(getSingletonIterator(untyped()), Term::getVariableIterator(_sort))); + } + return Term::getVariableIterator(untyped()); + } + + bool containsAllVariablesOf(TypedTermList other) const { + Set vars; + vars.insertFromIterator(varIter()); + + return iterTraits(other.varIter()).all([&vars](TermList v) { + return vars.contains(v); + }); + } + friend std::ostream& operator<<(std::ostream& out, TypedTermList const& self) { return out << (TermList const&) self << ": " << self._sort; } }; diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index 8b008db539..16ca18433f 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -25,14 +25,18 @@ using namespace Test; */ #define MY_SYNTAX_SUGAR \ DECL_DEFAULT_VARS \ + DECL_DEFAULT_SORT_VARS \ DECL_VAR(u, 3) \ DECL_SORT(s) \ + DECL_SORT(s2) \ DECL_LEFT_FUNC(left, {s}, s) \ DECL_RIGHT_FUNC(right, {s}, s) \ + DECL_POLY_CONST(h, 1, alpha) \ DECL_FUNC(f, {s, s}, s) \ DECL_FUNC(g, {s}, s) \ DECL_CONST(a, s) \ DECL_CONST(b, s) \ + DECL_CONST(c, s2) \ DECL_PRED (p, {s}) \ DECL_PRED (q, {s}) @@ -179,4 +183,34 @@ TEST_SIMPLIFICATION(test15, .expected({ clause({ g(left(b)) == left(a) }) }) ) +// demodulation with variable equality +TEST_SIMPLIFICATION(test16, + tester() + .simplifyWith({ clause({ TermSugar(TermList::var(0), s) == b }) }) + .toSimplify({ clause({ f(b,a) != a }) }) + .expected({ clause({ b != a }) }) +) + +TEST_SIMPLIFICATION(test17, + tester() + .simplifyWith({ clause({ x == h(y) }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ clause({ h(s) != a }) }) +) + +TEST_SIMPLIFICATION(test18, + tester() + .simplifyWith({ clause({ y == h(x) }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ clause({ h(s) != a }) }) +) + +TEST_SIMPLIFICATION(test19, + tester() + .simplifyWith({ clause({ x == c }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + } From 29152013ba95cc3317347bedc5293b1d4c72ed0e Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sun, 19 Apr 2026 12:40:55 +0200 Subject: [PATCH 4/5] Rename SubstApplicator::operator() to apply to conform with SubstHelper binders --- Indexing/CodeTreeInterfaces.hpp | 6 +----- Inferences/BackwardDemodulation.cpp | 4 ++-- Inferences/DemodulationHelper.cpp | 2 +- Inferences/ForwardGroundJoinability.cpp | 18 ++---------------- Inferences/Induction.hpp | 4 ++-- Kernel/SubstHelper.hpp | 11 +++++------ Shell/PartialRedundancyHandler.cpp | 2 +- 7 files changed, 14 insertions(+), 33 deletions(-) diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index 6741bbf5a1..83600e1644 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -38,7 +38,7 @@ class GenSubstitution USE_ALLOCATOR(GenSubstitution); - TermList operator()(unsigned var) const override { + TermList apply(unsigned var) const override { if constexpr (is_indexed_data_normalized::value) { return (*_bindings)[var]; } else { @@ -51,10 +51,6 @@ class GenSubstitution } } - TermList apply(unsigned var) const { - return (*this)(var); - } - TermList apply(TermList t) const { return SubstHelper::apply(t, *this); } diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index 0f326bd2dd..6abe79f685 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -56,8 +56,8 @@ namespace { struct Applicator : SubstApplicator { Applicator(ResultSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->applyToBoundQuery(TermList(v,false)); + TermList apply(unsigned v) const override { + return subst->applyToBoundQuery(TermList::var(v)); } ResultSubstitution* subst; }; diff --git a/Inferences/DemodulationHelper.cpp b/Inferences/DemodulationHelper.cpp index e8e34cea70..29e5a3ea77 100644 --- a/Inferences/DemodulationHelper.cpp +++ b/Inferences/DemodulationHelper.cpp @@ -61,7 +61,7 @@ bool DemodulationHelper::isRenamingOn(const SubstApplicator* applicator, TermLis continue; } - TermList vSubst = (*applicator)(v.var()); + TermList vSubst = applicator->apply(v.var()); if (!vSubst.isVar()) { return false; } diff --git a/Inferences/ForwardGroundJoinability.cpp b/Inferences/ForwardGroundJoinability.cpp index bc72ec662b..bb0d4d5d35 100644 --- a/Inferences/ForwardGroundJoinability.cpp +++ b/Inferences/ForwardGroundJoinability.cpp @@ -36,18 +36,6 @@ using namespace Indexing; using namespace Saturation; using namespace std; -namespace { - -struct Applicator : SubstApplicator { - Applicator(const GenSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->apply(v); - } - const GenSubstitution* subst; -}; - -} // end namespace - template ForwardGroundJoinability::ForwardGroundJoinability(SaturationAlgorithm& salg) : _ord(salg.getOrdering()), @@ -127,9 +115,7 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replace } TermList rhs = qr.data->rhs; - - Applicator appl(qr.unifier); - AppliedTerm rhsApplied(rhs, &appl, true); + AppliedTerm rhsApplied(rhs, qr.unifier, true); #if VDEBUG POStruct dpo_struct(tpo); @@ -147,7 +133,7 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replace #endif POStruct po_struct(tpo); - if (!TermOrderingDiagram::extendVarsGreater(qr.data->tod.get(), &appl, po_struct)) { + if (!TermOrderingDiagram::extendVarsGreater(qr.data->tod.get(), qr.unifier, po_struct)) { // TODO this check sometimes fails when the debug code can detect the // extension to get GREATER due to elimination of linear expressions // ASS(!success); diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index c8493babf2..a3267fe734 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -291,7 +291,7 @@ class InductionClauseIterator public: // all the work happens in the constructor! InductionClauseIterator(Clause* premise, InductionHelper helper, const SaturationAlgorithm& salg, - const StructInductionTermIndex& structInductionTermIndex, InductionFormulaIndex& formulaIndex) + const StructInductionTermIndex* structInductionTermIndex, InductionFormulaIndex& formulaIndex) : _helper(helper), _opt(salg.getOptions()), _structInductionTermIndex(structInductionTermIndex), _formulaIndex(formulaIndex), _fnDefHandler(salg.getFunctionDefinitionHandler()) { @@ -355,7 +355,7 @@ class InductionClauseIterator Stack _clauses; InductionHelper _helper; const Options& _opt; - const StructInductionTermIndex& _structInductionTermIndex; + const StructInductionTermIndex* _structInductionTermIndex; InductionFormulaIndex& _formulaIndex; FunctionDefinitionHandler& _fnDefHandler; }; diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index fbd17423f3..58616b77cc 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -30,8 +30,7 @@ using namespace Lib; struct SubstApplicator { virtual ~SubstApplicator() = default; - virtual TermList operator()(unsigned v) const = 0; - TermList apply(unsigned v) const { return (*this)(v); } + virtual TermList apply(unsigned v) const = 0; }; /** @@ -67,11 +66,11 @@ struct AppliedTerm * null is @b aboveVar is false. */ AppliedTerm(TermList t, const SubstApplicator* applicator, bool aboveVar) - : term(aboveVar && t.isVar() ? (*applicator)(t.var()) : t), + : term(aboveVar && t.isVar() ? applicator->apply(t.var()) : t), aboveVar(aboveVar && t.isVar() ? false : aboveVar), applicator(applicator) {} AppliedTerm(TermList t, AppliedTerm parent) - : term(parent.aboveVar && t.isVar() ? (*parent.applicator)(t.var()) : t), + : term(parent.aboveVar && t.isVar() ? parent.applicator->apply(t.var()) : t), aboveVar(parent.aboveVar && t.isVar() ? false : parent.aboveVar), applicator(parent.applicator) {} /** @@ -91,12 +90,12 @@ struct AppliedTerm return term.containsSubterm(var); } if (term.isVar()) { - return (*applicator)(term.var()).containsSubterm(var); + return applicator->apply(term.var()).containsSubterm(var); } VariableIterator vit(term.term()); while (vit.hasNext()) { auto v = vit.next(); - if ((*applicator)(v.var()).containsSubterm(var)) { + if (applicator->apply(v.var()).containsSubterm(var)) { return true; } } diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 161b69b131..fac1c01cd5 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -134,7 +134,7 @@ class PartialRedundancyHandler::ConstraintIndex static SubstMatcher matcher; struct Applicator : public SubstApplicator { - TermList operator()(unsigned v) const override { return matcher.bindings[v]; } + TermList apply(unsigned v) const override { return matcher.bindings[v]; } } applicator; matcher.init(this, ts); From 1cf4131f468ad2ac5ad5ca67995130a57b118cfc Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 23 Apr 2026 09:44:08 +0200 Subject: [PATCH 5/5] Create inner loop in CodeTree::TermMatcher::next to avoid falsely signaling termination to the caller --- Indexing/TermCodeTree.cpp | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 5984825909..a0fd192678 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -164,25 +164,23 @@ Data* TermCodeTree::TermMatcher::next() return 0; } - Base::_matched=Base::execute(); - if (!Base::_matched) { - return 0; - } - - ASS(Base::op->isSuccess()); - auto res = Base::op->template getSuccessResult(); - if (res->key().isVar()) { - // match the variable sort separately - Substitution subst; - if (!MatchingUtils::matchTerms(res->key().sort(), _querySort, subst)) { - return nullptr; - } - for (const auto& [v,t] : iterTraits(subst.items())) { - ASS_G(v, 0); // X0 is reserved for the term itself - Base::bindings[v] = t; + while ((Base::_matched=Base::execute())) { + ASS(Base::op->isSuccess()); + auto res = Base::op->template getSuccessResult(); + if (res->key().isVar()) { + // match the variable sort separately + Substitution subst; + if (!MatchingUtils::matchTerms(res->key().sort(), _querySort, subst)) { + continue; + } + for (const auto& [v,t] : iterTraits(subst.items())) { + ASS_G(v, 0); // X0 is reserved for the term itself + Base::bindings[v] = t; + } } + return res; } - return res; + return nullptr; } template class TermCodeTree;