PR to track HOL changes, don't merge

.github/workflows/CI.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-20.04
     steps:
     - name: Checkout Tree
       uses: actions/checkout@v3

CASC/PortfolioMode.cpp

@@ -200,12 +200,15 @@ bool PortfolioMode::prepareScheduleAndPerform(const Shell::Property& prop)
     addScheduleExtra(sOrig,sWithExtras,"avsq=on:plsq=on");             // split queues
     addScheduleExtra(sOrig,sWithExtras,"av=on:atotf=0.5");             // turn AVATAR off
 
+#if VHOL
     if(!prop.higherOrder()){
+#endif      
       //these options are not currently HOL compatible
       addScheduleExtra(sOrig,sWithExtras,"bsd=on:fsd=on"); // subsumption demodulation
       addScheduleExtra(sOrig,sWithExtras,"to=lpo");        // lpo
+#if VHOL      
     }
-
+#endif
     // If contains integers, rationals and reals
     if(prop.props() & (Property::PR_HAS_INTEGERS | Property::PR_HAS_RATS | Property::PR_HAS_REALS)){
       addScheduleExtra(sOrig,sWithExtras,"hsm=on");             // Sets a sensible set of Joe's arithmetic rules (TACAS-21) 
@@ -267,12 +270,11 @@ bool PortfolioMode::prepareScheduleAndPerform(const Shell::Property& prop)
 
     schedule.loadFromIterator(main.iterFifo());
     addScheduleExtra(main,schedule,"rp=on:de=on"); // random polarities, demodulation encompassment
-
   } else if (env.options->schedule() == Options::Schedule::SNAKE_TPTP_SAT) {
     ASS(fallback.isEmpty());
 
     schedule.loadFromIterator(main.iterFifo());
-    addScheduleExtra(main,schedule,"rp=on:fmbksg=on:de=on"); // random polarities, demodulation encompassment for saturation, fmbksg for the fmb's    
+    addScheduleExtra(main,schedule,"rp=on:fmbksg=on:de=on"); // random polarities, demodulation encompassment for saturation, fmbksg for the fmb's
   } else {
     // all other schedules just get loaded plain
 
@@ -369,6 +371,15 @@ void PortfolioMode::getSchedules(const Property& prop, Schedule& quick, Schedule
     Schedules::getSnakeTptpSatSchedule(prop,quick);
     break;
 
+#if VHOL
+  case Options::Schedule::SNAKE_TPTP_HOL:
+    Schedules::getSnakeTptpHolSchedule(prop,quick);
+    break;
+  case Options::Schedule::SNAKE_SLH:
+    Schedules::getSnakeSlhSchedule(prop,quick);
+    break;
+#endif
+
   case Options::Schedule::CASC_2019:
   case Options::Schedule::CASC:
     Schedules::getCasc2019Schedule(prop,quick,fallback);
@@ -379,9 +390,6 @@ void PortfolioMode::getSchedules(const Property& prop, Schedule& quick, Schedule
     Schedules::getCascSat2019Schedule(prop,quick,fallback);
     break;
 
-  case Options::Schedule::CASC_HOL_2020:
-    Schedules::getHigherOrderSchedule2020(quick,fallback);
-    break;
 
   case Options::Schedule::SMTCOMP:
   case Options::Schedule::SMTCOMP_2018:

CASC/Schedules.hpp

@@ -26,8 +26,6 @@ class Schedules
 {
 public:
   static void getScheduleFromFile(const vstring& filename, Schedule& quick);
-
-  static void getHigherOrderSchedule2020(Schedule& quick, Schedule& fallback);
   static void getCasc2019Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
 
   static void getCascSat2019Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
@@ -46,6 +44,12 @@ class Schedules
 
   static void getSnakeTptpUnsSchedule(const Shell::Property& property, Schedule& quick);
   static void getSnakeTptpSatSchedule(const Shell::Property& property, Schedule& quick);
+
+#if VHOL  
+  static void getSnakeTptpHolSchedule(const Shell::Property& property, Schedule& quick);
+  static void getSnakeSlhSchedule(const Shell::Property& property, Schedule& quick);
+#endif
+
 };
 
 }

CMakeLists.txt

@@ -233,6 +233,8 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/Problem.cpp
     Kernel/Renaming.cpp
     Kernel/RobSubstitution.cpp
+    Kernel/HOLUnification.cpp
+    Kernel/HOLMatching.cpp    
     Kernel/MismatchHandler.cpp
     Kernel/Signature.cpp
     Kernel/SortHelper.cpp
@@ -283,6 +285,8 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/RCClauseStack.hpp
     Kernel/Renaming.hpp
     Kernel/RobSubstitution.hpp
+    Kernel/HOLUnification.hpp 
+    Kernel/HOLMatching.hpp   
     Kernel/MismatchHandler.hpp
     Kernel/Signature.hpp
     Kernel/SortHelper.hpp
@@ -306,22 +310,20 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/PolynomialNormalizer.cpp
     Kernel/ApplicativeHelper.hpp
     Kernel/ApplicativeHelper.cpp
-    Kernel/SKIKBO.hpp
-    Kernel/SKIKBO.cpp
     Inferences/CNFOnTheFly.cpp
     Inferences/CNFOnTheFly.hpp
-    Inferences/CombinatorDemodISE.cpp
-    Inferences/CombinatorDemodISE.hpp
-    Inferences/CombinatorNormalisationISE.hpp
-    Inferences/CombinatorNormalisationISE.cpp
+    Inferences/BetaEtaISE.cpp
+    Inferences/BetaEtaISE.hpp
+    Inferences/FlexFlexSimplify.cpp
+    Inferences/FlexFlexSimplify.hpp    
+    Inferences/ImitateProject.hpp
+    Inferences/ImitateProject.cpp
     Inferences/ArgCong.hpp
     Inferences/ArgCong.cpp
     Inferences/NegativeExt.cpp
     Inferences/NegativeExt.hpp
-    Inferences/Narrow.hpp
-    Inferences/Narrow.cpp
-    Inferences/SubVarSup.hpp
-    Inferences/SubVarSup.cpp
+    Inferences/PositiveExt.cpp
+    Inferences/PositiveExt.hpp    
     Inferences/BoolEqToDiseq.hpp
     Inferences/BoolEqToDiseq.cpp
     Inferences/PrimitiveInstantiation.cpp
@@ -338,8 +340,8 @@ set(VAMPIRE_KERNEL_SOURCES
     Inferences/CasesSimp.hpp
     Inferences/Cases.cpp
     Inferences/Cases.hpp
-    Shell/LambdaElimination.cpp
-    Shell/LambdaElimination.hpp
+    Shell/LambdaConversion.cpp
+    Shell/LambdaConversion.hpp
     )
 source_group(kernel_source_files FILES ${VAMPIRE_KERNEL_SOURCES})
 
@@ -358,15 +360,16 @@ set(VAMPIRE_INDEXING_SOURCES
     Indexing/LiteralSubstitutionTree.cpp
     Indexing/ResultSubstitution.cpp
     Indexing/SubstitutionTree.cpp
+    Indexing/HOLSubstitutionTree.cpp
     Indexing/SubstitutionTree_FastGen.cpp
     Indexing/SubstitutionTree_FastInst.cpp
     Indexing/SubstitutionTree_Nodes.cpp
     Indexing/TermCodeTree.cpp
     Indexing/TermIndex.cpp
     Indexing/TermSharing.cpp
     Indexing/TermSubstitutionTree.cpp
-    Indexing/AcyclicityIndex.hpp
-    Indexing/ClauseCodeTree.hpp
+#    Indexing/AcyclicityIndex.hpp
+    Indexing/ClauseCodeTree.hpp    
     Indexing/ClauseVariantIndex.hpp
     Indexing/CodeTree.hpp
     Indexing/CodeTreeInterfaces.hpp
@@ -380,6 +383,7 @@ set(VAMPIRE_INDEXING_SOURCES
     Indexing/LiteralSubstitutionTree.hpp
     Indexing/ResultSubstitution.hpp
     Indexing/SubstitutionTree.hpp
+    Indexing/HOLSubstitutionTree.hpp    
     Indexing/TermCodeTree.hpp
     Indexing/TermIndex.hpp
     Indexing/TermIndexingStructure.hpp
@@ -713,6 +717,7 @@ set(UNIT_TESTS
     UnitTests/tDHMap.cpp
     UnitTests/tQuotientE.cpp
     UnitTests/tUnificationWithAbstraction.cpp
+    UnitTests/tHOLMatching.cpp    
     UnitTests/tGaussianElimination.cpp
     UnitTests/tPushUnaryMinus.cpp
     UnitTests/tArithmeticSubtermGeneralization.cpp
@@ -729,7 +734,7 @@ set(UNIT_TESTS
     UnitTests/tBinaryHeap.cpp
     UnitTests/tSafeRecursion.cpp
     UnitTests/tKBO.cpp
-    UnitTests/tSKIKBO.cpp
+#    UnitTests/tSKIKBO.cpp
     UnitTests/tLPO.cpp
     UnitTests/tRatioKeeper.cpp
     UnitTests/tTwoVampires.cpp
@@ -739,9 +744,12 @@ set(UNIT_TESTS
     UnitTests/tBottomUpEvaluation.cpp
     UnitTests/tCoproduct.cpp
     UnitTests/tEqualityResolution.cpp
+    UnitTests/tEqualityFactoring.cpp
+    UnitTests/tImitateProject.cpp
     UnitTests/tIterator.cpp
     UnitTests/tOption.cpp
     UnitTests/tStack.cpp
+    UnitTests/tBetaReduction.cpp    
     )
 source_group(unit_tests FILES ${UNIT_TESTS})
 
@@ -800,6 +808,13 @@ elseif(CMAKE_BUILD_TYPE STREQUAL Release)
   add_compile_definitions(VDEBUG=0)
 endif()
 
+if(CMAKE_BUILD_HOL STREQUAL On)
+  message(STATUS "Building with HOL support")
+  add_compile_definitions(VHOL=1)
+else()
+  message(STATUS "Building without HOL support")
+  add_compile_definitions(VHOL=0)
+endif()
 add_compile_definitions(VTIME_PROFILING=1)
 
 if (CYGWIN)
@@ -915,7 +930,7 @@ endif() # COMPILE_TESTS
 #################################################################
 # automated generation of Vampire revision information from git #
 #################################################################
-set(VAMPIRE_VERSION_NUMBER 4.7)
+set(VAMPIRE_VERSION_NUMBER 4.8)
 
 execute_process(
     COMMAND git rev-parse --is-inside-work-tree

Forwards.hpp

@@ -67,7 +67,6 @@ typedef List<unsigned> VList; // a list of variables (which are unsigned)
 typedef List<TermList> SList; // a list of sorts (which are now, with polymorphism, TermLists)
 typedef const SharedSet<unsigned> VarSet;
 
-
 class Literal;
 typedef List<Literal*> LiteralList;
 typedef Stack<Literal*> LiteralStack;
@@ -97,9 +96,13 @@ class Problem;
 class Renaming;
 class Substitution;
 
-class RobSubstitution;
-typedef VirtualIterator<RobSubstitution*> SubstIterator;
-typedef Lib::SmartPtr<RobSubstitution> RobSubstitutionSP;
+class RobSubstitutionTL;
+typedef VirtualIterator<RobSubstitutionTL*> SubstIterator;
+typedef Lib::SmartPtr<RobSubstitutionTL> RobSubstitutionSP;
+
+class RobSubstitutionTS;
+typedef VirtualIterator<RobSubstitutionTS*> SubstIteratorTS;
+typedef Lib::SmartPtr<RobSubstitutionTS> RobSubstitutionTSSP;
 
 class Matcher;
 typedef VirtualIterator<Matcher*> MatchIterator;
@@ -130,10 +133,14 @@ enum Color {
   COLOR_INVALID = 3u
 };
 
+enum class SymbolType{FUNC, PRED, TYPE_CON};
+
 };
 
 namespace Indexing
 {
+
+
 class Index;
 class IndexManager;
 class LiteralIndex;
@@ -145,6 +152,14 @@ class TermSharing;
 
 class ResultSubstitution;
 typedef Lib::SmartPtr<ResultSubstitution> ResultSubstitutionSP;
+//typedef Lib::VirtualIterator<ResultSubstitutionSP> SubstSPIterator;
+
+enum class SplittingAlgo { NONE 
+#if VHOL
+  , HOL_MATCH
+  , HOL_UNIF
+#endif
+                         };
 
 };
 

Indexing/AcyclicityIndex.cpp

@@ -16,6 +16,7 @@
 #include "Kernel/RobSubstitution.hpp"
 #include "Kernel/Signature.hpp"
 #include "Kernel/SortHelper.hpp"
+#include "Kernel/TypedTermList.hpp"
 
 #include "Lib/Backtrackable.hpp"
 #include "Lib/Environment.hpp"
@@ -199,9 +200,11 @@ namespace Indexing
                         AcyclicityIndex& aindex)
       :
       _queryLit(queryLit),
+      _index(nullptr),
+      _tis(nullptr),
       _nextResult(nullptr),
       _stack(0),
-      _subst(new RobSubstitution()),
+      _subst(new RobSubstitutionTS()),
       _substChanges(0),
       _nextAvailableIndex(0),
       _currentDepth(0)
@@ -275,8 +278,9 @@ namespace Indexing
     {
       CALL("Acyclicity::pushUnificationOnStack");
 
+      ASS(t.isTerm());
       ASS(_tis);
-      TermQueryResultIterator tqrIt = _tis->getUnifications(t);
+      TermQueryResultIterator tqrIt = _tis->getUnifications(TypedTermList(t.term()));
       int index;
       while (tqrIt.hasNext()) {
         TermQueryResult tqr = tqrIt.next();
@@ -386,10 +390,10 @@ namespace Indexing
   private:
     Literal *_queryLit;
     SIndex *_index;
-    TermIndexingStructure *_tis;    
+    TermIndexingStructure *_tis;
     CycleQueryResult *_nextResult;
     Stack<CycleSearchTreeNode*> _stack;
-    RobSubstitution *_subst;
+    RobSubstitutionTS *_subst;
     Stack<BacktrackData> _substChanges;
     int _nextAvailableIndex;
     unsigned _currentDepth;
@@ -432,7 +436,7 @@ namespace Indexing
       ULit ulit = make_pair(lit, c);
       if (!index->find(ulit)) {
         index->insert(ulit, new IndexEntry(lit, c, *t, getSubterms(fs->term())));
-        _tis->insert(*t, lit, c);
+        _tis->insert(TypedTermList(t->term()), lit, c);
       }
     }
   }
@@ -451,7 +455,7 @@ namespace Indexing
         return;
 
       _sIndexes.get(sort)->remove(ulit);
-     _tis->remove(*t, lit, c);
+     _tis->remove(TypedTermList(t->term()), lit, c);
     }
   }
 

Indexing/CodeTreeInterfaces.cpp

@@ -177,22 +177,22 @@ class CodeTreeTIS::ResultIterator
   Recycled<TermCodeTree::TermMatcher> _matcher;
 };
 
-void CodeTreeTIS::insert(TermList t, Literal* lit, Clause* cls)
+void CodeTreeTIS::insert(TypedTermList t, Literal* lit, Clause* cls)
 {
   CALL("CodeTreeTIS::insert");
 
   TermCodeTree::TermInfo* ti=new TermCodeTree::TermInfo(t,lit,cls);
   _ct.insert(ti);
 }
 
-void CodeTreeTIS::remove(TermList t, Literal* lit, Clause* cls)
+void CodeTreeTIS::remove(TypedTermList t, Literal* lit, Clause* cls)
 {
   CALL("CodeTreeTIS::remove");
 
   _ct.remove(TermCodeTree::TermInfo(t,lit,cls));
 }
 
-TermQueryResultIterator CodeTreeTIS::getGeneralizations(TermList t, bool retrieveSubstitutions)
+TermQueryResultIterator CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions)
 {
   CALL("CodeTreeTIS::getGeneralizations");
 

Indexing/CodeTreeInterfaces.hpp

@@ -43,19 +43,20 @@ class CodeTreeTIS : public TermIndexingStructure
   CLASS_NAME(CodeTreeTIS);
   USE_ALLOCATOR(CodeTreeTIS);
 
-  void insert(TermList t, Literal* lit, Clause* cls);
-  void remove(TermList t, Literal* lit, Clause* cls);
+  void insert(TypedTermList t, Literal* lit, Clause* cls);
+  void remove(TypedTermList t, Literal* lit, Clause* cls);
 
-  TermQueryResultIterator getGeneralizations(TermList t, bool retrieveSubstitutions = true);
+  TermQueryResultIterator getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true);
   bool generalizationExists(TermList t);
   // TODO: get rid of NOT_IMPLEMENTED
-  VirtualIterator<TQueryRes<AbstractingUnifier*>> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration) { NOT_IMPLEMENTED; }
+  TermQueryResultIterator getUwa(TypedTermList t) { NOT_IMPLEMENTED; }
 
 #if VDEBUG
   virtual void markTagged(){ NOT_IMPLEMENTED; } 
-  virtual void output(std::ostream& out) const { out << "CodeTree"; }
 #endif
 
+  virtual void output(std::ostream& out) const { out << "CodeTree"; }
+
 private:
   class ResultIterator;