From 335476afd0aec4e95808b1536be484769ee8cee5 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Thu, 23 Apr 2026 15:07:36 +0200 Subject: [PATCH 01/10] Output new skolemization syntax. --- Kernel/InferenceStore.cpp | 71 ++++++++++++++++++++++++++++++++++----- Kernel/InferenceStore.hpp | 7 +++- Shell/Skolem.cpp | 30 +++++++++++------ Shell/Skolem.hpp | 6 +++- 4 files changed, 93 insertions(+), 21 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 37cd0f8099..a36fbd6cef 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -13,9 +13,11 @@ */ #include "Kernel/Theory.hpp" +#include "Kernel/Unit.hpp" #include "Lib/Allocator.hpp" #include "Lib/Environment.hpp" #include "Lib/Int.hpp" +#include "Lib/Metaiterators.hpp" #include "Lib/ScopedPtr.hpp" #include "Lib/SharedSet.hpp" #include "Lib/Stack.hpp" @@ -42,7 +44,9 @@ #include "InferenceStore.hpp" +#include #include +#include //TODO: when we delete clause, we should also delete all its records from the inference store @@ -82,6 +86,15 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars) +{ + SymbolStack* pStack; + _introducedSymbols.getValuePtr(u->number(),pStack); + _introducedSymbolReplacedVars.insert(number, replacedVar); + _introducedSymbolInScopeVars.insert(number, std::move(inScopeVars)); + pStack->push(SymbolId(st,number)); +} + /** * Record the introduction of a split name */ @@ -555,19 +568,24 @@ struct InferenceStore::TPTPProofPrinter std::string getNewSymbols(std::string origin, std::string symStr) { return "new_symbols(" + origin + ",[" +symStr + "])"; } + + std::string getSymbolName(SymbolId sym) { + if (sym.first == SymbolType::FUNC ) { + return env.signature->functionName(sym.second); + } else if (sym.first == SymbolType::PRED){ + return env.signature->predicateName(sym.second); + } else { + return env.signature->typeConName(sym.second); + } + } + /** It is an iterator over SymbolId */ template std::string getNewSymbols(std::string origin, It symIt) { std::ostringstream symsStr; while(symIt.hasNext()) { SymbolId sym = symIt.next(); - if (sym.first == SymbolType::FUNC ) { - symsStr << env.signature->functionName(sym.second); - } else if (sym.first == SymbolType::PRED){ - symsStr << env.signature->predicateName(sym.second); - } else { - symsStr << env.signature->typeConName(sym.second); - } + symsStr << getSymbolName(sym); if (symIt.hasNext()) { symsStr << ','; } @@ -585,6 +603,43 @@ struct InferenceStore::TPTPProofPrinter return getNewSymbols(origin, SymbolStack::ConstIterator(syms)); } +std::string getSkolemizeMap(Unit* u){ + ASS(hasNewSymbols(u)); + SymbolStack& syms = _is->_introducedSymbols.get(u->number()); + return getSkolemizeMap(SymbolStack::ConstIterator(syms)); +} + +template +std::string getSkolemizeMap(It symIt){ + std::ostringstream symsStr; + + while (symIt.hasNext()) { + symsStr << "skolemize("; + SymbolId a = symIt.next(); + auto res = _is->_introducedSymbolReplacedVars.find(a.second); + ASS(!res.isNone()); + symsStr << "X" << *res << ","; + symsStr << getSymbolName(a); + auto inScopeVars = _is->_introducedSymbolInScopeVars.get(a.second).get(); + if(inScopeVars->size() > 0) { + symsStr << "("; + auto iter = inScopeVars->iterator(); + while(iter.hasNext()){ + symsStr << "X" << iter.next(); + if(iter.hasNext()) { + symsStr << ","; + } + } + symsStr << ")"; + } + symsStr << ")"; + if(symIt.hasNext()) { + symsStr << ","; + } + } + return symsStr.str(); +} + void printStep(Unit* us) override { InferenceRule rule = us->inference().rule(); @@ -646,7 +701,7 @@ struct InferenceStore::TPTPProofPrinter ASS(parents.hasNext()); std::string statusStr; if (rule==InferenceRule::SKOLEMIZE) { - statusStr="status(esa),"+getNewSymbols("skolem",us); + statusStr="status(esa),"+getNewSymbols("skolem",us) + "," + getSkolemizeMap(us); } else if(rule==InferenceRule::NEGATED_CONJECTURE) { statusStr="status(cth)"; diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index 336cb0c816..68ca17a7ae 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -16,6 +16,7 @@ #ifndef __InferenceStore__ #define __InferenceStore__ +#include #include #include @@ -24,6 +25,7 @@ #include "Lib/Allocator.hpp" #include "Lib/DHMap.hpp" #include "Lib/DHMultiset.hpp" +#include "Lib/DHSet.hpp" #include "Lib/Stack.hpp" #include "Kernel/Clause.hpp" @@ -69,7 +71,9 @@ class InferenceStore void recordSplittingNameLiteral(Unit* us, Literal* lit); void recordIntroducedSymbol(Unit* u, SymbolType st, unsigned number); + void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars); void recordIntroducedSplitName(Unit* u, std::string name); + void outputUnsatCore(std::ostream& out, Unit* refutation); void outputProof(std::ostream& out, Unit* refutation); @@ -94,8 +98,9 @@ class InferenceStore typedef std::pair SymbolId; typedef Stack SymbolStack; DHMap _introducedSymbols; + DHMap _introducedSymbolReplacedVars; + DHMap>> _introducedSymbolInScopeVars; DHMap _introducedSplitNames; - }; }; diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 361aeb8b39..81adf4ddf7 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -23,6 +23,8 @@ #include "Kernel/FormulaUnit.hpp" #include "Kernel/SortHelper.hpp" #include "Kernel/TermIterators.hpp" +#include "Lib/DHSet.hpp" +#include "Lib/Metaiterators.hpp" #include "Lib/SharedSet.hpp" #include "Shell/Statistics.hpp" @@ -30,6 +32,7 @@ #include "Options.hpp" #include "Rectify.hpp" +#include #include "Skolem.hpp" using namespace std; @@ -81,7 +84,7 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) Formula* f = unit->formula(); preskolemise(f); ASS_EQ(_varOccs.size(),0); - + _currentFullSkolemisation = f; Formula* g = skolemise(f); _beingSkolemised = 0; @@ -97,18 +100,18 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) ASS(_introducedSkolemSyms.isNonEmpty()); while(_introducedSkolemSyms.isNonEmpty()) { auto symPair = _introducedSkolemSyms.pop(); - - if(symPair.first){ - InferenceStore::instance()->recordIntroducedSymbol(res,SymbolType::TYPE_CON,symPair.second); + + if(std::get<0>(symPair)){ + InferenceStore::instance()->recordIntroducedSkolemSymbol(res,SymbolType::TYPE_CON,std::get<1>(symPair),std::get<2>(symPair), std::move(std::get<3>(symPair))); } else { - InferenceStore::instance()->recordIntroducedSymbol(res,SymbolType::FUNC,symPair.second); + InferenceStore::instance()->recordIntroducedSkolemSymbol(res,SymbolType::FUNC,std::get<1>(symPair),std::get<2>(symPair), std::move(std::get<3>(symPair))); } if(unit->derivedFromGoal()){ - if(symPair.first){ - env.signature->getTypeCon(symPair.second)->markInGoal(); + if(std::get<0>(symPair)){ + env.signature->getTypeCon(std::get<1>(symPair))->markInGoal(); } else { - env.signature->getFunction(symPair.second)->markInGoal(); + env.signature->getFunction(std::get<1>(symPair))->markInGoal(); } } } @@ -324,6 +327,7 @@ Formula* Skolem::skolemise (Formula* f) if (fs == f->args()) { return f; } + _currentSubformulaOfFullSkolemisation = f; return new JunctionFormula(f->connective(),fs); } @@ -451,7 +455,11 @@ Formula* Skolem::skolemise (Formula* f) TermList head = TermList(Term::create(sym, typeVars.size(), typeVars.begin())); skolemTerm = HOL::create::app(head, termVars).term(); } - _introducedSkolemSyms.push(make_pair(skolemisingTypeVar, sym)); + std::unique_ptr> inScopeVars = std::unique_ptr>(new DHSet()); + for(auto it : dep->iter()){ + inScopeVars->insert(it); + } + _introducedSkolemSyms.push(std::make_tuple(skolemisingTypeVar, sym, v, std::move(inScopeVars))); env.statistics->skolemFunctions++; @@ -487,11 +495,11 @@ Formula* Skolem::skolemise (Formula* f) if (arity > 0) { def = new QuantifiedFormula(FORALL, vArgs.list(), def); } - + Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); UnitList::push(defUnit,_skolimizingDefinitions); } - + // drop the existential one: return skolemise(f->qarg()); } diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index c466458b38..8a93beac82 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -103,10 +103,14 @@ class Skolem DHMap _varSorts; // for some heuristic evaluations after we are done - Stack> _introducedSkolemSyms; + // Type, numberOfSymbol, replacedVar, inScopeVars + Stack>>> _introducedSkolemSyms; FormulaUnit* _beingSkolemised; + Formula* _currentFullSkolemisation; + Formula* _currentSubformulaOfFullSkolemisation; + // to create one big inference after we are done UnitList* _skolimizingDefinitions; From 65706a91ab9baed08edd7eba53be6cb8ee303370 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Wed, 29 Apr 2026 14:33:08 +0200 Subject: [PATCH 02/10] Adjust ordering and format Co-authored-by: Copilot --- Kernel/Inference.cpp | 2 +- Kernel/InferenceStore.cpp | 12 +++++++----- Kernel/InferenceStore.hpp | 5 +++-- Shell/Skolem.cpp | 9 +++++---- Shell/Skolem.hpp | 2 +- 5 files changed, 17 insertions(+), 13 deletions(-) diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp index 7b843e1b66..d542a9c2dd 100644 --- a/Kernel/Inference.cpp +++ b/Kernel/Inference.cpp @@ -587,7 +587,7 @@ std::string Kernel::ruleName(InferenceRule rule) case InferenceRule::REMOVE_DUPLICATE_LITERALS: return "duplicate literal removal"; case InferenceRule::SKOLEMIZE: - return "skolemisation"; + return "skolemize"; case InferenceRule::SKOLEM_SYMBOL_INTRODUCTION: return "skolem symbol introduction"; case InferenceRule::RESOLUTION: diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index a36fbd6cef..4109778294 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -47,6 +47,7 @@ #include #include #include +#include //TODO: when we delete clause, we should also delete all its records from the inference store @@ -86,7 +87,7 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } -void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars) +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars) { SymbolStack* pStack; _introducedSymbols.getValuePtr(u->number(),pStack); @@ -623,10 +624,11 @@ std::string getSkolemizeMap(It symIt){ auto inScopeVars = _is->_introducedSymbolInScopeVars.get(a.second).get(); if(inScopeVars->size() > 0) { symsStr << "("; - auto iter = inScopeVars->iterator(); - while(iter.hasNext()){ - symsStr << "X" << iter.next(); - if(iter.hasNext()) { + auto iter = inScopeVars->begin(); + while(iter != inScopeVars->end()){ + symsStr << "X" << *iter; + ++iter; + if(iter != inScopeVars->end()) { symsStr << ","; } } diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index 68ca17a7ae..a6873189d9 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -19,6 +19,7 @@ #include #include #include +#include #include "Forwards.hpp" @@ -71,7 +72,7 @@ class InferenceStore void recordSplittingNameLiteral(Unit* us, Literal* lit); void recordIntroducedSymbol(Unit* u, SymbolType st, unsigned number); - void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars); + void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars); void recordIntroducedSplitName(Unit* u, std::string name); @@ -99,7 +100,7 @@ class InferenceStore typedef Stack SymbolStack; DHMap _introducedSymbols; DHMap _introducedSymbolReplacedVars; - DHMap>> _introducedSymbolInScopeVars; + DHMap>> _introducedSymbolInScopeVars; DHMap _introducedSplitNames; }; diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 81adf4ddf7..072a17bc02 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -33,6 +33,7 @@ #include "Options.hpp" #include "Rectify.hpp" #include +#include #include "Skolem.hpp" using namespace std; @@ -455,9 +456,9 @@ Formula* Skolem::skolemise (Formula* f) TermList head = TermList(Term::create(sym, typeVars.size(), typeVars.begin())); skolemTerm = HOL::create::app(head, termVars).term(); } - std::unique_ptr> inScopeVars = std::unique_ptr>(new DHSet()); + std::unique_ptr> inScopeVars = std::unique_ptr>(new std::vector ()); for(auto it : dep->iter()){ - inScopeVars->insert(it); + inScopeVars->push_back(it); } _introducedSkolemSyms.push(std::make_tuple(skolemisingTypeVar, sym, v, std::move(inScopeVars))); @@ -496,8 +497,8 @@ Formula* Skolem::skolemise (Formula* f) def = new QuantifiedFormula(FORALL, vArgs.list(), def); } - Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); - UnitList::push(defUnit,_skolimizingDefinitions); + //Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); + //UnitList::push(defUnit,_skolimizingDefinitions); } // drop the existential one: diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index 8a93beac82..c8c00596ca 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -104,7 +104,7 @@ class Skolem // for some heuristic evaluations after we are done // Type, numberOfSymbol, replacedVar, inScopeVars - Stack>>> _introducedSkolemSyms; + Stack>>> _introducedSkolemSyms; FormulaUnit* _beingSkolemised; From 4a7a0d0d2ea345f628ad9d0b080350f9d236d78a Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Wed, 29 Apr 2026 14:46:23 +0200 Subject: [PATCH 03/10] Remove unnecessary code Co-authored-by: Copilot --- Shell/Skolem.cpp | 2 -- Shell/Skolem.hpp | 6 ++---- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 072a17bc02..574bab2574 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -85,7 +85,6 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) Formula* f = unit->formula(); preskolemise(f); ASS_EQ(_varOccs.size(),0); - _currentFullSkolemisation = f; Formula* g = skolemise(f); _beingSkolemised = 0; @@ -328,7 +327,6 @@ Formula* Skolem::skolemise (Formula* f) if (fs == f->args()) { return f; } - _currentSubformulaOfFullSkolemisation = f; return new JunctionFormula(f->connective(),fs); } diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index c8c00596ca..651e1def20 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -103,14 +103,12 @@ class Skolem DHMap _varSorts; // for some heuristic evaluations after we are done - // Type, numberOfSymbol, replacedVar, inScopeVars + + // Type, numberOfSymbol, Variable that was replaced by the skolem symbol, Variables that are in scope for a skolem symbol (for proof recording purposes) Stack>>> _introducedSkolemSyms; FormulaUnit* _beingSkolemised; - Formula* _currentFullSkolemisation; - Formula* _currentSubformulaOfFullSkolemisation; - // to create one big inference after we are done UnitList* _skolimizingDefinitions; From f339379c73cbb21938807931c879ba1e66566463 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Thu, 7 May 2026 14:30:03 +0200 Subject: [PATCH 04/10] Slight Cleanup --- Kernel/InferenceStore.cpp | 14 ++++++++------ Kernel/InferenceStore.hpp | 1 - Shell/Skolem.cpp | 3 +-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 4109778294..fe4d55f2bf 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -12,6 +12,7 @@ * Implements class InferenceStore. */ +#include "Debug/Assertion.hpp" #include "Kernel/Theory.hpp" #include "Kernel/Unit.hpp" #include "Lib/Allocator.hpp" @@ -618,17 +619,18 @@ std::string getSkolemizeMap(It symIt){ symsStr << "skolemize("; SymbolId a = symIt.next(); auto res = _is->_introducedSymbolReplacedVars.find(a.second); - ASS(!res.isNone()); + NEVER(res.isNone()); symsStr << "X" << *res << ","; symsStr << getSymbolName(a); - auto inScopeVars = _is->_introducedSymbolInScopeVars.get(a.second).get(); + auto inScopeVarsOpt = _is->_introducedSymbolInScopeVars.find(a.second); + NEVER(inScopeVarsOpt.isNone()); + auto inScopeVars = inScopeVarsOpt->get(); if(inScopeVars->size() > 0) { symsStr << "("; - auto iter = inScopeVars->begin(); - while(iter != inScopeVars->end()){ + + for(auto iter = inScopeVars->begin(); iter != inScopeVars->end(); iter++){ symsStr << "X" << *iter; - ++iter; - if(iter != inScopeVars->end()) { + if(iter+1 != inScopeVars->end()) { symsStr << ","; } } diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index a6873189d9..c8eefe7e72 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -26,7 +26,6 @@ #include "Lib/Allocator.hpp" #include "Lib/DHMap.hpp" #include "Lib/DHMultiset.hpp" -#include "Lib/DHSet.hpp" #include "Lib/Stack.hpp" #include "Kernel/Clause.hpp" diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 574bab2574..cd29a504df 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -23,7 +23,6 @@ #include "Kernel/FormulaUnit.hpp" #include "Kernel/SortHelper.hpp" #include "Kernel/TermIterators.hpp" -#include "Lib/DHSet.hpp" #include "Lib/Metaiterators.hpp" #include "Lib/SharedSet.hpp" @@ -454,7 +453,7 @@ Formula* Skolem::skolemise (Formula* f) TermList head = TermList(Term::create(sym, typeVars.size(), typeVars.begin())); skolemTerm = HOL::create::app(head, termVars).term(); } - std::unique_ptr> inScopeVars = std::unique_ptr>(new std::vector ()); + std::unique_ptr> inScopeVars = std::make_unique>(); for(auto it : dep->iter()){ inScopeVars->push_back(it); } From ff6628f3cbfee08f382008d2b1fa389fac408f52 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Wed, 13 May 2026 14:18:47 +0200 Subject: [PATCH 05/10] Review, fixed polymorphism bug in SubstHelper? --- Kernel/InferenceStore.cpp | 45 ++++++++++++++------------------------- Kernel/InferenceStore.hpp | 6 ++++-- Kernel/SubstHelper.hpp | 8 +++++-- Shell/Skolem.cpp | 42 ++++++++++++------------------------ Shell/Skolem.hpp | 7 +++--- 5 files changed, 43 insertions(+), 65 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index fe4d55f2bf..6ec777fa51 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -48,6 +48,7 @@ #include #include #include +#include #include //TODO: when we delete clause, we should also delete all its records from the inference store @@ -88,13 +89,12 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } -void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars) -{ +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned replacedVar, Term* symTerm){ SymbolStack* pStack; _introducedSymbols.getValuePtr(u->number(),pStack); - _introducedSymbolReplacedVars.insert(number, replacedVar); - _introducedSymbolInScopeVars.insert(number, std::move(inScopeVars)); - pStack->push(SymbolId(st,number)); + _introducedSymbolReplacedVars.insert(symTerm->functor(), replacedVar); + _introducedSkolemSymTerms.insert(symTerm->functor(), symTerm); + pStack->push(SymbolId(st,symTerm->functor())); } /** @@ -608,36 +608,23 @@ struct InferenceStore::TPTPProofPrinter std::string getSkolemizeMap(Unit* u){ ASS(hasNewSymbols(u)); SymbolStack& syms = _is->_introducedSymbols.get(u->number()); - return getSkolemizeMap(SymbolStack::ConstIterator(syms)); + return getSkolemizeMap(u->number(), SymbolStack::ConstIterator(syms)); } template -std::string getSkolemizeMap(It symIt){ +std::string getSkolemizeMap(unsigned unitNumber, It symIt){ std::ostringstream symsStr; - - while (symIt.hasNext()) { + bool hasNext = symIt.hasNext(); + while (hasNext) { symsStr << "skolemize("; SymbolId a = symIt.next(); - auto res = _is->_introducedSymbolReplacedVars.find(a.second); - NEVER(res.isNone()); - symsStr << "X" << *res << ","; - symsStr << getSymbolName(a); - auto inScopeVarsOpt = _is->_introducedSymbolInScopeVars.find(a.second); - NEVER(inScopeVarsOpt.isNone()); - auto inScopeVars = inScopeVarsOpt->get(); - if(inScopeVars->size() > 0) { - symsStr << "("; - - for(auto iter = inScopeVars->begin(); iter != inScopeVars->end(); iter++){ - symsStr << "X" << *iter; - if(iter+1 != inScopeVars->end()) { - symsStr << ","; - } - } - symsStr << ")"; - } - symsStr << ")"; - if(symIt.hasNext()) { + auto skolemTerm = _is->_introducedSkolemSymTerms.find(a.second); + NEVER(skolemTerm.isNone()); + auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find((*skolemTerm)->functor()); + NEVER(skolemizedVariable.isNone()); + symsStr << "X" << *skolemizedVariable << "," << (*skolemTerm)->toString() << ")"; + hasNext = symIt.hasNext(); + if(hasNext) { symsStr << ","; } } diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index c8eefe7e72..bf5e5631a0 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -71,7 +71,7 @@ class InferenceStore void recordSplittingNameLiteral(Unit* us, Literal* lit); void recordIntroducedSymbol(Unit* u, SymbolType st, unsigned number); - void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr> inScopeVars); + void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned replacedVar, Term* symTerm); void recordIntroducedSplitName(Unit* u, std::string name); @@ -98,8 +98,10 @@ class InferenceStore typedef std::pair SymbolId; typedef Stack SymbolStack; DHMap _introducedSymbols; + // symbol number -> existential variable name (number) that was replaced by the symbol DHMap _introducedSymbolReplacedVars; - DHMap>> _introducedSymbolInScopeVars; + // symbol number -> the term that is introduced when introducing the skolem symbol + DHMap _introducedSkolemSymTerms; DHMap _introducedSplitNames; }; diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index fbd17423f3..d6e7a3d8e0 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -529,10 +529,14 @@ Formula* SubstHelper::applyImpl(Formula* f, Applicator& applicator, bool noShari while(vit.hasNext()) { auto [v, sort] = vit.next(); TermList binding = applicator.apply(v); + TermList newSort = sort; + if(sort.isTerm()){ + newSort = TermList(applyImpl(sort.term(), applicator, noSharing)); + } ASS(binding.isVar()); unsigned newVar = binding.var(); - VSList::push({newVar, sort}, newVars); - if(newVar!=v) { + VSList::push({newVar, newSort}, newVars); + if(newVar!=v || newSort!=sort) { varsModified = true; } } diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index cd29a504df..af76d7d892 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -14,8 +14,10 @@ * @since 08/07/2007 flight Manchester-Cork, changed to new datastructures */ +#include "Forwards.hpp" #include "Kernel/HOL/HOL.hpp" #include "Kernel/Signature.hpp" +#include "Kernel/SubstHelper.hpp" #include "Kernel/Term.hpp" #include "Kernel/Inference.hpp" #include "Kernel/InferenceStore.hpp" @@ -23,6 +25,7 @@ #include "Kernel/FormulaUnit.hpp" #include "Kernel/SortHelper.hpp" #include "Kernel/TermIterators.hpp" +#include "Lib/Environment.hpp" #include "Lib/Metaiterators.hpp" #include "Lib/SharedSet.hpp" @@ -71,7 +74,7 @@ FormulaUnit* Skolem::skolemise (FormulaUnit* unit, bool appify) FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) { ASS(_introducedSkolemSyms.isEmpty()); - + _appify = appify; _beingSkolemised=unit; _skolimizingDefinitions = UnitList::empty(); @@ -99,18 +102,19 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) ASS(_introducedSkolemSyms.isNonEmpty()); while(_introducedSkolemSyms.isNonEmpty()) { auto symPair = _introducedSkolemSyms.pop(); + auto symTerm = symPair.second; - if(std::get<0>(symPair)){ - InferenceStore::instance()->recordIntroducedSkolemSymbol(res,SymbolType::TYPE_CON,std::get<1>(symPair),std::get<2>(symPair), std::move(std::get<3>(symPair))); + if(symTerm->kind()==TermKind::SORT){ + InferenceStore::instance()->recordIntroducedSkolemSymbol(res, SymbolType::TYPE_CON, symPair.first, symPair.second); } else { - InferenceStore::instance()->recordIntroducedSkolemSymbol(res,SymbolType::FUNC,std::get<1>(symPair),std::get<2>(symPair), std::move(std::get<3>(symPair))); + InferenceStore::instance()->recordIntroducedSkolemSymbol(res, Kernel::SymbolType::FUNC, symPair.first, symPair.second); } if(unit->derivedFromGoal()){ - if(std::get<0>(symPair)){ - env.signature->getTypeCon(std::get<1>(symPair))->markInGoal(); + if(symTerm->kind()==TermKind::SORT){ + env.signature->getTypeCon(symPair.second->functor())->markInGoal(); } else { - env.signature->getFunction(std::get<1>(symPair))->markInGoal(); + env.signature->getFunction(symPair.second->functor())->markInGoal(); } } } @@ -353,11 +357,9 @@ Formula* Skolem::skolemise (Formula* f) allVars.reset(); typeVars.reset(); - // for proof recording purposes, see below //We use a FIFO structure since in the polymorphic case //a variable list must be of the form [typevars, termvars] VSList::FIFO vArgs; - Formula* before = SubstHelper::apply(f, _subst); ExVarDepInfo& depInfo = _varDeps.get(f); @@ -453,11 +455,7 @@ Formula* Skolem::skolemise (Formula* f) TermList head = TermList(Term::create(sym, typeVars.size(), typeVars.begin())); skolemTerm = HOL::create::app(head, termVars).term(); } - std::unique_ptr> inScopeVars = std::make_unique>(); - for(auto it : dep->iter()){ - inScopeVars->push_back(it); - } - _introducedSkolemSyms.push(std::make_tuple(skolemisingTypeVar, sym, v, std::move(inScopeVars))); + _introducedSkolemSyms.push(std::make_pair(v, skolemTerm)); env.statistics->skolemFunctions++; @@ -486,20 +484,8 @@ Formula* Skolem::skolemise (Formula* f) } } - { - Formula* after = SubstHelper::apply(f->qarg(), _subst); - Formula* def = new BinaryFormula(IMP, before, after); - - if (arity > 0) { - def = new QuantifiedFormula(FORALL, vArgs.list(), def); - } - - //Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); - //UnitList::push(defUnit,_skolimizingDefinitions); - } - - // drop the existential one: - return skolemise(f->qarg()); + Formula* after = SubstHelper::apply(f->qarg(), _subst); + return skolemise(after); } case BOOL_TERM: diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index 651e1def20..5b1ffc0503 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -103,10 +103,9 @@ class Skolem DHMap _varSorts; // for some heuristic evaluations after we are done - - // Type, numberOfSymbol, Variable that was replaced by the skolem symbol, Variables that are in scope for a skolem symbol (for proof recording purposes) - Stack>>> _introducedSkolemSyms; - + + Stack> _introducedSkolemSyms; + FormulaUnit* _beingSkolemised; // to create one big inference after we are done From 0ba156c82be85b61aa388f65561bf6840ed442ca Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Wed, 13 May 2026 15:34:38 +0200 Subject: [PATCH 06/10] Bugfix --- Shell/Skolem.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index af76d7d892..89331f12d2 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -484,8 +484,9 @@ Formula* Skolem::skolemise (Formula* f) } } - Formula* after = SubstHelper::apply(f->qarg(), _subst); - return skolemise(after); + Formula* skolemised = skolemise(f->qarg()); + //Apply substitution to the entire formula again, after skolemising to fix skolemized sorts. + return SubstHelper::apply(skolemised, _subst); } case BOOL_TERM: From 7c228bc51783ee36c359ab84c0014e7bb482f40a Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Wed, 13 May 2026 17:29:08 +0200 Subject: [PATCH 07/10] Cleanup Imports, Fix keying --- Kernel/InferenceStore.cpp | 10 +++++----- Kernel/InferenceStore.hpp | 10 ++++------ Shell/Skolem.cpp | 2 -- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 6ec777fa51..69ec871159 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -92,8 +92,8 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned replacedVar, Term* symTerm){ SymbolStack* pStack; _introducedSymbols.getValuePtr(u->number(),pStack); - _introducedSymbolReplacedVars.insert(symTerm->functor(), replacedVar); - _introducedSkolemSymTerms.insert(symTerm->functor(), symTerm); + _introducedSymbolReplacedVars.insert(std::make_pair(st,symTerm->functor()), replacedVar); + _introducedSkolemSymTerms.insert(std::make_pair(st,symTerm->functor()), symTerm); pStack->push(SymbolId(st,symTerm->functor())); } @@ -617,10 +617,10 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){ bool hasNext = symIt.hasNext(); while (hasNext) { symsStr << "skolemize("; - SymbolId a = symIt.next(); - auto skolemTerm = _is->_introducedSkolemSymTerms.find(a.second); + SymbolId symbol = symIt.next(); + auto skolemTerm = _is->_introducedSkolemSymTerms.find(symbol); NEVER(skolemTerm.isNone()); - auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find((*skolemTerm)->functor()); + auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find(symbol); NEVER(skolemizedVariable.isNone()); symsStr << "X" << *skolemizedVariable << "," << (*skolemTerm)->toString() << ")"; hasNext = symIt.hasNext(); diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index bf5e5631a0..ec0a065590 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -16,10 +16,8 @@ #ifndef __InferenceStore__ #define __InferenceStore__ -#include #include #include -#include #include "Forwards.hpp" @@ -98,10 +96,10 @@ class InferenceStore typedef std::pair SymbolId; typedef Stack SymbolStack; DHMap _introducedSymbols; - // symbol number -> existential variable name (number) that was replaced by the symbol - DHMap _introducedSymbolReplacedVars; - // symbol number -> the term that is introduced when introducing the skolem symbol - DHMap _introducedSkolemSymTerms; + // symbol id -> existential variable name (number) that was replaced by the symbol + DHMap _introducedSymbolReplacedVars; + // symbol id -> the term that is introduced when introducing the skolem symbol + DHMap _introducedSkolemSymTerms; DHMap _introducedSplitNames; }; diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 89331f12d2..9eda4230c6 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -34,8 +34,6 @@ #include "Options.hpp" #include "Rectify.hpp" -#include -#include #include "Skolem.hpp" using namespace std; From 4683f90aa947e927710f6191e692b456e1bb59a0 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Thu, 21 May 2026 08:51:59 +0200 Subject: [PATCH 08/10] restore one-pass Skolemisation, fix SubstHelper's sort handling --- Kernel/SubstHelper.hpp | 5 +---- Shell/Skolem.cpp | 19 ++++++++++++++++--- 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index d6e7a3d8e0..e9acbae0bd 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -529,10 +529,7 @@ Formula* SubstHelper::applyImpl(Formula* f, Applicator& applicator, bool noShari while(vit.hasNext()) { auto [v, sort] = vit.next(); TermList binding = applicator.apply(v); - TermList newSort = sort; - if(sort.isTerm()){ - newSort = TermList(applyImpl(sort.term(), applicator, noSharing)); - } + TermList newSort = TermList(applyImpl(sort, applicator, noSharing)); ASS(binding.isVar()); unsigned newVar = binding.var(); VSList::push({newVar, newSort}, newVars); diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 9eda4230c6..276668a98c 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -334,10 +334,23 @@ Formula* Skolem::skolemise (Formula* f) case FORALL: { Formula* g = skolemise(f->qarg()); - if (g == f->qarg()) { + // if we have something like + // ![X : list(A)]: ... + // then we may need to apply the substitution to A + + VSList::FIFO vars; + bool changed = g != f->qarg(); + for(auto [var, sort] : iterTraits(f->vars()->iter())) { + TermList sort2 = SubstHelper::apply(sort, _subst); + if(sort != sort2) + changed = true; + vars.pushBack({var, sort2}); + } + if(!changed) { + VSList::destroy(vars.list()); return f; } - return new QuantifiedFormula(f->connective(), f->vars(), g); + return new QuantifiedFormula(FORALL, vars.list(), g); } case EXISTS: @@ -484,7 +497,7 @@ Formula* Skolem::skolemise (Formula* f) Formula* skolemised = skolemise(f->qarg()); //Apply substitution to the entire formula again, after skolemising to fix skolemized sorts. - return SubstHelper::apply(skolemised, _subst); + return skolemised; } case BOOL_TERM: From bc90ab48a605422c5aa5675b4e7e0fc2718a8d32 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Thu, 21 May 2026 10:06:57 +0200 Subject: [PATCH 09/10] Remove old comment, minor cleanup --- Kernel/InferenceStore.cpp | 7 ++----- Shell/Skolem.cpp | 4 +--- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 69ec871159..47913a3f26 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -45,12 +45,9 @@ #include "InferenceStore.hpp" -#include #include -#include -#include -#include - +#include +#include //TODO: when we delete clause, we should also delete all its records from the inference store namespace Kernel diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 276668a98c..101d39d6d5 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -495,9 +495,7 @@ Formula* Skolem::skolemise (Formula* f) } } - Formula* skolemised = skolemise(f->qarg()); - //Apply substitution to the entire formula again, after skolemising to fix skolemized sorts. - return skolemised; + return skolemise(f->qarg()); } case BOOL_TERM: From f5d1659ef38bbb6aebda845b001efd1fe6d831c0 Mon Sep 17 00:00:00 2001 From: Jonas Bodingbauer Date: Tue, 26 May 2026 09:16:10 +0200 Subject: [PATCH 10/10] A bit of documentation --- Kernel/InferenceStore.hpp | 2 ++ Shell/Skolem.cpp | 4 ++-- Shell/Skolem.hpp | 5 +++-- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index ec0a065590..b1ca34e249 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -95,11 +95,13 @@ class InferenceStore /** first records the type of the symbol (PRED,FUNC or TYPE_CON), second is symbol number */ typedef std::pair SymbolId; typedef Stack SymbolStack; + // unit id -> stack of introduced symbols (in order of introduction) DHMap _introducedSymbols; // symbol id -> existential variable name (number) that was replaced by the symbol DHMap _introducedSymbolReplacedVars; // symbol id -> the term that is introduced when introducing the skolem symbol DHMap _introducedSkolemSymTerms; + DHMap _introducedSplitNames; }; diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index 101d39d6d5..96c9241fa9 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -75,7 +75,7 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) _appify = appify; _beingSkolemised=unit; - _skolimizingDefinitions = UnitList::empty(); + _skolemizingDefinitions = UnitList::empty(); _varOccs.reset(); _varSorts.reset(); _subst.reset(); @@ -93,7 +93,7 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) return unit; } - UnitList* premiseList = new UnitList(unit,_skolimizingDefinitions); // making sure unit is the last inserted, i.e. first in the list + UnitList* premiseList = new UnitList(unit,_skolemizingDefinitions); // making sure unit is the last inserted, i.e. first in the list FormulaUnit* res = new FormulaUnit(g,FormulaClauseTransformationMany(InferenceRule::SKOLEMIZE,premiseList)); diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index 5b1ffc0503..c16a55d1c4 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -103,13 +103,14 @@ class Skolem DHMap _varSorts; // for some heuristic evaluations after we are done - + + // Pair: Stack> _introducedSkolemSyms; FormulaUnit* _beingSkolemised; // to create one big inference after we are done - UnitList* _skolimizingDefinitions; + UnitList* _skolemizingDefinitions; bool _appify; // a higher-order solution