Skolemization format update

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:

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 <set>
-
+#include<string>
+#include<vector>
 //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<class It>
   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<class It>
+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)";

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<SymbolType,unsigned> SymbolId;
   typedef Stack<SymbolId> SymbolStack;
+  // unit id -> stack of introduced symbols (in order of introduction)
   DHMap<unsigned,SymbolStack> _introducedSymbols;
-  DHMap<unsigned,std::string> _introducedSplitNames;
+  // symbol id -> existential variable name (number) that was replaced by the symbol
+  DHMap<SymbolId, unsigned> _introducedSymbolReplacedVars;
+  // symbol id -> the term that is introduced when introducing the skolem symbol
+  DHMap<SymbolId, Term*> _introducedSkolemSymTerms;
 
+  DHMap<unsigned,std::string> _introducedSplitNames;
 };
 
 };

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<ProcessSpecVars>(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;
       }
     }

Shell/Skolem.cpp

@@ -14,15 +14,19 @@
  * @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"
 #include "Kernel/Formula.hpp"
 #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());
     }
 

Shell/Skolem.hpp

@@ -103,12 +103,14 @@ class Skolem
   DHMap<unsigned,TermList> _varSorts;
 
   // for some heuristic evaluations after we are done
-  Stack<std::pair<bool, unsigned>> _introducedSkolemSyms;
 
+  // Pair: <variable that was replaced by the new skolem symbol, the new skolem symbol (with args)>
+  Stack<std::pair<unsigned, Term*>> _introducedSkolemSyms;
+
   FormulaUnit* _beingSkolemised;
 
   // to create one big inference after we are done
-  UnitList* _skolimizingDefinitions;
+  UnitList* _skolemizingDefinitions;
 
   bool _appify; // a higher-order solution