diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp index 7b843e1b6..d542a9c2d 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 37cd0f809..47913a3f2 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -12,10 +12,13 @@ * Implements class InferenceStore. */ +#include "Debug/Assertion.hpp" #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" @@ -43,7 +46,8 @@ #include "InferenceStore.hpp" #include - +#include +#include //TODO: when we delete clause, we should also delete all its records from the inference store namespace Kernel @@ -82,6 +86,14 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned replacedVar, Term* symTerm){ + SymbolStack* pStack; + _introducedSymbols.getValuePtr(u->number(),pStack); + _introducedSymbolReplacedVars.insert(std::make_pair(st,symTerm->functor()), replacedVar); + _introducedSkolemSymTerms.insert(std::make_pair(st,symTerm->functor()), symTerm); + pStack->push(SymbolId(st,symTerm->functor())); +} + /** * Record the introduction of a split name */ @@ -555,19 +567,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 +602,32 @@ 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(u->number(), SymbolStack::ConstIterator(syms)); +} + +template +std::string getSkolemizeMap(unsigned unitNumber, It symIt){ + std::ostringstream symsStr; + bool hasNext = symIt.hasNext(); + while (hasNext) { + symsStr << "skolemize("; + SymbolId symbol = symIt.next(); + auto skolemTerm = _is->_introducedSkolemSymTerms.find(symbol); + NEVER(skolemTerm.isNone()); + auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find(symbol); + NEVER(skolemizedVariable.isNone()); + symsStr << "X" << *skolemizedVariable << "," << (*skolemTerm)->toString() << ")"; + hasNext = symIt.hasNext(); + if(hasNext) { + symsStr << ","; + } + } + return symsStr.str(); +} + void printStep(Unit* us) override { InferenceRule rule = us->inference().rule(); @@ -646,7 +689,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 336cb0c81..b1ca34e24 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -69,7 +69,9 @@ class InferenceStore void recordSplittingNameLiteral(Unit* us, Literal* lit); void recordIntroducedSymbol(Unit* u, SymbolType st, unsigned number); + void recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned replacedVar, Term* symTerm); void recordIntroducedSplitName(Unit* u, std::string name); + void outputUnsatCore(std::ostream& out, Unit* refutation); void outputProof(std::ostream& out, Unit* refutation); @@ -93,9 +95,14 @@ 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; - DHMap _introducedSplitNames; + // 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/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index fbd17423f..e9acbae0b 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -529,10 +529,11 @@ Formula* SubstHelper::applyImpl(Formula* f, Applicator& applicator, bool noShari while(vit.hasNext()) { auto [v, sort] = vit.next(); TermList binding = applicator.apply(v); + TermList newSort = TermList(applyImpl(sort, 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 361aeb8b3..96c9241fa 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,8 @@ #include "Kernel/FormulaUnit.hpp" #include "Kernel/SortHelper.hpp" #include "Kernel/TermIterators.hpp" +#include "Lib/Environment.hpp" +#include "Lib/Metaiterators.hpp" #include "Lib/SharedSet.hpp" #include "Shell/Statistics.hpp" @@ -68,10 +72,10 @@ FormulaUnit* Skolem::skolemise (FormulaUnit* unit, bool appify) FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) { ASS(_introducedSkolemSyms.isEmpty()); - + _appify = appify; _beingSkolemised=unit; - _skolimizingDefinitions = UnitList::empty(); + _skolemizingDefinitions = UnitList::empty(); _varOccs.reset(); _varSorts.reset(); _subst.reset(); @@ -81,7 +85,6 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify) Formula* f = unit->formula(); preskolemise(f); ASS_EQ(_varOccs.size(),0); - Formula* g = skolemise(f); _beingSkolemised = 0; @@ -90,25 +93,26 @@ 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)); ASS(_introducedSkolemSyms.isNonEmpty()); while(_introducedSkolemSyms.isNonEmpty()) { auto symPair = _introducedSkolemSyms.pop(); - - if(symPair.first){ - InferenceStore::instance()->recordIntroducedSymbol(res,SymbolType::TYPE_CON,symPair.second); + auto symTerm = symPair.second; + + if(symTerm->kind()==TermKind::SORT){ + InferenceStore::instance()->recordIntroducedSkolemSymbol(res, SymbolType::TYPE_CON, symPair.first, symPair.second); } else { - InferenceStore::instance()->recordIntroducedSymbol(res,SymbolType::FUNC,symPair.second); + InferenceStore::instance()->recordIntroducedSkolemSymbol(res, Kernel::SymbolType::FUNC, symPair.first, symPair.second); } if(unit->derivedFromGoal()){ - if(symPair.first){ - env.signature->getTypeCon(symPair.second)->markInGoal(); + if(symTerm->kind()==TermKind::SORT){ + env.signature->getTypeCon(symPair.second->functor())->markInGoal(); } else { - env.signature->getFunction(symPair.second)->markInGoal(); + env.signature->getFunction(symPair.second->functor())->markInGoal(); } } } @@ -330,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: @@ -351,11 +368,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); @@ -451,7 +466,7 @@ 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)); + _introducedSkolemSyms.push(std::make_pair(v, skolemTerm)); env.statistics->skolemFunctions++; @@ -480,19 +495,6 @@ 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()); } diff --git a/Shell/Skolem.hpp b/Shell/Skolem.hpp index c466458b3..c16a55d1c 100644 --- a/Shell/Skolem.hpp +++ b/Shell/Skolem.hpp @@ -103,12 +103,14 @@ class Skolem DHMap _varSorts; // for some heuristic evaluations after we are done - Stack> _introducedSkolemSyms; + // Pair: + Stack> _introducedSkolemSyms; + FormulaUnit* _beingSkolemised; // to create one big inference after we are done - UnitList* _skolimizingDefinitions; + UnitList* _skolemizingDefinitions; bool _appify; // a higher-order solution