proof-extra with data rather than strings

CMakeLists.txt

@@ -170,6 +170,7 @@ set(VAMPIRE_LIB_SOURCES
     Lib/Numbering.hpp
     Lib/PairUtils.hpp
     Lib/Portability.hpp
+    Lib/ProofExtra.hpp
     Lib/Random.hpp
     Lib/RatioKeeper.hpp
     Lib/Recycled.hpp
@@ -333,6 +334,8 @@ set(VAMPIRE_KERNEL_SOURCES
     Inferences/CasesSimp.hpp
     Inferences/Cases.cpp
     Inferences/Cases.hpp
+    Inferences/ProofExtra.hpp
+    Inferences/ProofExtra.cpp
     Shell/LambdaElimination.cpp
     Shell/LambdaElimination.hpp
     )

Inferences/BackwardDemodulation.cpp

@@ -176,10 +176,13 @@ struct BackwardDemodulation::ResultFn
 
     env.statistics->backwardDemodulations++;
     _removed->insert(qr.data->clause);
-
-    return BwSimplificationRecord(
-      qr.data->clause,
-      Clause::fromStack(*resLits, SimplifyingInference2(InferenceRule::BACKWARD_DEMODULATION, qr.data->clause, _cl)));
+    Clause *replacement = Clause::fromStack(
+      *resLits,
+      SimplifyingInference2(InferenceRule::BACKWARD_DEMODULATION, qr.data->clause, _cl)
+    );
+    if(env.options->proofExtra() == Options::ProofExtra::FULL)
+      env.proofExtra.insert(replacement, new BackwardDemodulationExtra(lhs, lhsS));
+    return BwSimplificationRecord(qr.data->clause, replacement);
   }
 private:
   Literal* _eqLit;

Inferences/BackwardDemodulation.hpp

@@ -20,8 +20,8 @@
 #include "Indexing/TermIndex.hpp"
 
 #include "DemodulationHelper.hpp"
-
 #include "InferenceEngine.hpp"
+#include "ProofExtra.hpp"
 
 namespace Inferences {
 
@@ -45,6 +45,7 @@ class BackwardDemodulation
   DemodulationHelper _helper;
 };
 
+using BackwardDemodulationExtra = RewriteInferenceExtra;
 };
 
 #endif /* __BackwardDemodulation__ */

Inferences/BinaryResolution.cpp

@@ -235,12 +235,17 @@ Clause* BinaryResolution::generateClause(
   if(nConstraints != 0){
     env.statistics->cResolution++;
   }
-  else{ 
+  else{
     env.statistics->resolution++;
   }
 
   inf_destroyer.disable(); // ownership passed to the the clause below
-  return Clause::fromStack(*resLits, inf);
+  Clause *cl = Clause::fromStack(*resLits, inf);
+  if(env.options->proofExtra() == Options::ProofExtra::FULL)
+    env.proofExtra.insert(cl, new BinaryResolutionExtra(queryLit, resultLit));
+
+  return cl;
+
 }
 
 ClauseIterator BinaryResolution::generateClauses(Clause* premise)

Inferences/BinaryResolution.hpp

@@ -19,6 +19,7 @@
 #include "Forwards.hpp"
 
 #include "InferenceEngine.hpp"
+#include "ProofExtra.hpp"
 #include "Kernel/Ordering.hpp"
 #include "Kernel/RobSubstitution.hpp"
 
@@ -50,6 +51,8 @@ class BinaryResolution
   BinaryResolutionIndex* _index;
 };
 
+using BinaryResolutionExtra = TwoLiteralInferenceExtra;
+
 };
 
 #endif /*__BinaryResolution__*/

Inferences/EqualityResolution.cpp

@@ -127,7 +127,10 @@ struct EqualityResolution::ResultFn
 
     env.statistics->equalityResolution++;
 
-    return Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_RESOLUTION, _cl));
+    Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_RESOLUTION, _cl));
+    if(env.options->proofExtra() == Options::ProofExtra::FULL)
+      env.proofExtra.insert(cl, new EqualityResolutionExtra(lit));
+    return cl;
   }
 private:
   bool _afterCheck;

Inferences/EqualityResolution.hpp

@@ -19,6 +19,7 @@
 #include "Forwards.hpp"
 
 #include "InferenceEngine.hpp"
+#include "Inferences/ProofExtra.hpp"
 #include "Shell/Options.hpp"
 
 namespace Inferences {
@@ -38,6 +39,7 @@ class EqualityResolution
   struct IsNegativeEqualityFn;
 };
 
+using EqualityResolutionExtra = LiteralInferenceExtra;
 
 };
 

Inferences/ForwardDemodulation.cpp

@@ -224,6 +224,8 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
 
         premises = pvi( getSingletonIterator(qr.data->clause));
         replacement = Clause::fromStack(*resLits, SimplifyingInference2(InferenceRule::FORWARD_DEMODULATION, cl, qr.data->clause));
+        if(env.options->proofExtra() == Options::ProofExtra::FULL)
+          env.proofExtra.insert(replacement, new ForwardDemodulationExtra(lhs, trm));
         return true;
       }
     }

Inferences/ForwardDemodulation.hpp

@@ -19,7 +19,9 @@
 #include "Forwards.hpp"
 #include "Indexing/TermIndex.hpp"
 
+#include "DemodulationHelper.hpp"
 #include "InferenceEngine.hpp"
+#include "ProofExtra.hpp"
 
 namespace Inferences
 {
@@ -53,6 +55,7 @@ class ForwardDemodulationImpl
 private:
 };
 
+using ForwardDemodulationExtra = RewriteInferenceExtra;
 
 };
 

Inferences/ProofExtra.cpp

@@ -0,0 +1,41 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ProofExtra.cpp
+ * Various objects that include "extra information" about an inference,
+ * e.g. selected literals, unifier, etc.
+ *
+ * @since 09/09/2024 Oxford
+ */
+
+#include "ProofExtra.hpp"
+
+namespace Inferences {
+
+void LiteralInferenceExtra::output(std::ostream &out) const {
+  out << "selected=(" << selectedLiteral->toString() << ')';
+}
+
+void TwoLiteralInferenceExtra::output(std::ostream &out) const {
+  LiteralInferenceExtra::output(out);
+  out << ",other=(" << otherLiteral->toString() << ')';
+}
+
+void RewriteInferenceExtra::output(std::ostream &out) const {
+  out << "lhs=" << lhs << ",target=" << target;
+}
+
+void TwoLiteralRewriteInferenceExtra::output(std::ostream &out) const {
+  TwoLiteralInferenceExtra::output(out);
+  out << ',';
+  RewriteInferenceExtra::output(out);
+}
+
+} // namespace Inferences

Inferences/ProofExtra.hpp

@@ -0,0 +1,72 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ProofExtra.hpp
+ * Various objects that include "extra information" about an inference,
+ * e.g. selected literals, unifier, etc.
+ *
+ * @since 09/09/2024 Oxford
+ */
+
+#ifndef __Inferences_ProofExtra__
+#define __Inferences_ProofExtra__
+
+#include "Kernel/Term.hpp"
+#include "Lib/ProofExtra.hpp"
+
+namespace Inferences {
+
+// inferences that use one literal from their main premise
+struct LiteralInferenceExtra : virtual public InferenceExtra {
+  LiteralInferenceExtra(Kernel::Literal *selected) : selectedLiteral(selected) {}
+
+  virtual void output(std::ostream &out) const override;
+
+  // the literal from the main premise
+  Kernel::Literal *selectedLiteral;
+};
+
+// inferences that use one literal from their side premise
+struct TwoLiteralInferenceExtra : public LiteralInferenceExtra {
+  TwoLiteralInferenceExtra(Kernel::Literal *selected, Kernel::Literal *other)
+    : LiteralInferenceExtra(selected), otherLiteral(other) {}
+
+  virtual void output(std::ostream &out) const override;
+
+  // the literal from the side premise
+  Kernel::Literal *otherLiteral;
+};
+
+struct RewriteInferenceExtra : virtual public InferenceExtra {
+  RewriteInferenceExtra(Kernel::TermList lhs, Kernel::TermList target)
+    : lhs(lhs), target(target) {}
+
+  virtual void output(std::ostream &out) const override;
+
+  // the LHS used to rewrite with
+  Kernel::TermList lhs;
+  // the rewritten term
+  Kernel::TermList target;
+};
+
+struct TwoLiteralRewriteInferenceExtra : public TwoLiteralInferenceExtra, public RewriteInferenceExtra {
+  TwoLiteralRewriteInferenceExtra(
+    Kernel::Literal *selected,
+    Kernel::Literal *other,
+    Kernel::TermList target,
+    Kernel::TermList rewritten
+  ) : TwoLiteralInferenceExtra(selected, other), RewriteInferenceExtra(target, rewritten) {}
+
+  virtual void output(std::ostream &out) const override;
+};
+
+}
+
+#endif

Inferences/SubVarSup.cpp

@@ -261,12 +261,6 @@ Clause* SubVarSup::performSubVarSup(
     return 0;
   }
 
-  // If proof extra is on let's compute the positions we have performed
-  // SubVarSup on 
-  if(env.options->proofExtra()==Options::ProofExtra::FULL){
-    //TODO update for proof extra
-  }
-
   bool afterCheck = getOptions().literalMaximalityAftercheck() && _salg->getLiteralSelector().isBGComplete();
 
   Inference inf(GeneratingInference2(InferenceRule::SUB_VAR_SUP, rwClause, eqClause));

Inferences/Superposition.cpp

@@ -529,32 +529,13 @@ Clause* Superposition::performSuperposition(
   inf_destroyer.disable(); // ownership passed to the the clause below
   auto clause = Clause::fromStack(*res, inf);
 
-  // If proof extra is on let's compute the positions we have performed
-  // superposition on 
-  if(env.options->proofExtra()==Options::ProofExtra::FULL){
-
-    // First find which literal it is in the clause, as selection has occured already
-    // this should remain the same...?
-    std::string rwPlace = Lib::Int::toString(rwClause->getLiteralPosition(rwLit));
-    std::string eqPlace = Lib::Int::toString(eqClause->getLiteralPosition(eqLit));
-
-    std::string rwPos="_";
-    ALWAYS(Kernel::positionIn(rwTerm,rwLit,rwPos));
-    std::string eqPos = "("+eqPlace+").2";
-    rwPos = "("+rwPlace+")."+rwPos;
-
-    std::string eqClauseNum = Lib::Int::toString(eqClause->number());
-    std::string rwClauseNum = Lib::Int::toString(rwClause->number());
-
-    std::string extra = eqClauseNum + " into " + rwClauseNum+", unify on "+
-        eqPos+" in "+eqClauseNum+" and "+
-        rwPos+" in "+rwClauseNum;
-
-    if (!env.proofExtra) {
-      env.proofExtra = new DHMap<const Unit*,std::string>();
-    }
-    env.proofExtra->insert(clause,extra);
-  }
+  if(env.options->proofExtra() == Options::ProofExtra::FULL)
+    env.proofExtra.insert(clause, new SuperpositionExtra(
+      rwLit,
+      eqLit,
+      eqLHS,
+      rwTerm
+    ));
 
   return clause;
 }

Inferences/Superposition.hpp

@@ -20,6 +20,7 @@
 #include "Indexing/TermIndex.hpp"
 
 #include "InferenceEngine.hpp"
+#include "Inferences/ProofExtra.hpp"
 #include "Kernel/RobSubstitution.hpp"
 
 namespace Inferences {
@@ -61,6 +62,7 @@ class Superposition
   SuperpositionLHSIndex* _lhsIndex;
 };
 
+using SuperpositionExtra = TwoLiteralRewriteInferenceExtra;
 
 };
 

Kernel/Clause.cpp

@@ -219,8 +219,8 @@ void Clause::destroy()
   static Stack<Clause*> toDestroy(32);
   Clause* cl = this;
   for(;;) {
-    if ((env.options->proofExtra()==Options::ProofExtra::FULL) && env.proofExtra) {
-      env.proofExtra->remove(cl);
+    if (env.options->proofExtra() == Options::ProofExtra::FULL) {
+      env.proofExtra.remove(cl);
     }
     Inference::Iterator it = cl->_inference.iterator();
     while (cl->_inference.hasNext(it)) {
@@ -383,7 +383,7 @@ std::string Clause::toString() const
   // print inference and ids of parent clauses
   result += " " + inferenceAsString();
 
-  if(env.options->proofExtra()!=Options::ProofExtra::OFF){
+  if(env.options->proofExtra() != Options::ProofExtra::OFF){
     // print statistics: each entry should have the form key:value
     result += std::string(" {");
 

Kernel/Unit.cpp

@@ -166,10 +166,15 @@ std::string Unit::inferenceAsString() const
     first = false;
     result += Int::toString(parent->number());
   }
-  // print Extra
-  std::string extra;
-  if (env.proofExtra && env.proofExtra->find(this,extra) && extra != "") {
-    result += ", " + extra;
+
+  // print extra if present
+  if(env.options->proofExtra() == Options::ProofExtra::FULL) {
+    auto *extra = env.proofExtra.find(this);
+    if(extra) {
+      if(!first)
+        result += ',';
+      result += extra->toString();
+    }
   }
 
   return result + ']';

Lib/Environment.hpp

@@ -23,6 +23,7 @@
 #include "Exception.hpp"
 #include "DHMap.hpp"
 #include "Kernel/Problem.hpp"
+#include "Lib/ProofExtra.hpp"
 
 namespace Lib {
 
@@ -51,7 +52,7 @@ class Environment
 
   DHMap<unsigned, unsigned>* predicateSineLevels;
 
-  DHMap<const Kernel::Unit*,std::string>* proofExtra; // maps Unit* pointers to the associated proof extra string, if available
+  ProofExtra proofExtra;
 
   /** Time remaining until the end of the time-limit in miliseconds */
   int remainingTime() const;