Merge pull request #525 from vprover/rule-induction-sorting

Induction improvements

CASC/PortfolioMode.cpp

@@ -402,9 +402,15 @@ void PortfolioMode::getSchedules(const Property& prop, Schedule& quick, Schedule
   case Options::Schedule::INTEGER_INDUCTION:
     Schedules::getIntegerInductionSchedule(prop,quick,fallback);
     break;
+  case Options::Schedule::INTIND_OEIS:
+    Schedules::getIntindOeisSchedule(prop,quick,fallback);
+    break;
   case Options::Schedule::STRUCT_INDUCTION:
     Schedules::getStructInductionSchedule(prop,quick,fallback);
     break;
+  case Options::Schedule::STRUCT_INDUCTION_TIP:
+    Schedules::getStructInductionTipSchedule(prop,quick,fallback);
+    break;
   }
 }
 

CASC/Schedules.hpp

@@ -45,7 +45,9 @@ class Schedules
 
   static void getInductionSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
   static void getIntegerInductionSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
+  static void getIntindOeisSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
   static void getStructInductionSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
+  static void getStructInductionTipSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
 
   static void getSnakeTptpUnsSchedule(const Shell::Property& property, Schedule& quick);
   static void getSnakeTptpSatSchedule(const Shell::Property& property, Schedule& quick);

CMakeLists.txt

@@ -405,6 +405,7 @@ set(VAMPIRE_INFERENCE_SOURCES
     Inferences/ForwardLiteralRewriting.cpp
     Inferences/ForwardSubsumptionAndResolution.cpp
     Inferences/ForwardSubsumptionDemodulation.cpp
+    Inferences/FunctionDefinitionRewriting.cpp
     Inferences/GlobalSubsumption.cpp
     Inferences/InnerRewriting.cpp
     Inferences/EquationalTautologyRemoval.cpp
@@ -441,6 +442,7 @@ set(VAMPIRE_INFERENCE_SOURCES
     Inferences/ForwardDemodulation.hpp
     Inferences/ForwardLiteralRewriting.hpp
     Inferences/ForwardSubsumptionAndResolution.hpp
+    Inferences/FunctionDefinitionRewriting.hpp
     Inferences/GlobalSubsumption.hpp
     Inferences/InnerRewriting.hpp
     Inferences/EquationalTautologyRemoval.hpp
@@ -550,6 +552,7 @@ set(VAMPIRE_SHELL_SOURCES
     Shell/FunctionDefinition.cpp
     Shell/GeneralSplitting.cpp
     Shell/GoalGuessing.cpp
+    Shell/FunctionDefinitionHandler.cpp
     Shell/InequalitySplitting.cpp
     Shell/InterpolantMinimizer.cpp
     Shell/Interpolants.cpp
@@ -601,6 +604,7 @@ set(VAMPIRE_SHELL_SOURCES
     Shell/EqualityProxyMono.hpp
     Shell/Flattening.hpp
     Shell/FunctionDefinition.hpp
+    Shell/FunctionDefinitionHandler.hpp
     Shell/GeneralSplitting.hpp
     Shell/InequalitySplitting.hpp
     Shell/InterpolantMinimizer.hpp
@@ -731,6 +735,9 @@ set(UNIT_TESTS
     UnitTests/tStack.cpp
     UnitTests/tSet.cpp
     UnitTests/tDeque.cpp
+    UnitTests/tTermAlgebra.cpp
+    UnitTests/tFunctionDefinitionHandler.cpp
+    UnitTests/tFunctionDefinitionRewriting.cpp
     )
 source_group(unit_tests FILES ${UNIT_TESTS})
 

Forwards.hpp

@@ -188,5 +188,6 @@ namespace Shell
 class Options;
 class Property;
 class Statistics;
+class FunctionDefinitionHandler;
 }
 #endif /* __Forwards__ */

Indexing/TermIndex.cpp

@@ -131,26 +131,34 @@ void InductionTermIndex::handleClause(Clause* c, bool adding)
 {
   TIME_TRACE("induction term index maintenance");
 
-  if (InductionHelper::isInductionClause(c)) {
+  if (!InductionHelper::isInductionClause(c)) {
+    return;
+  }
+
   // Iterate through literals & check if the literal is suitable for induction
-    for (unsigned i=0;i<c->length();i++) {
-      Literal* lit = (*c)[i];
-      if (InductionHelper::isInductionLiteral(lit)) {
-        SubtermIterator it(lit);
-        while (it.hasNext()) {
-          TermList tl = it.next();
-          if (!tl.term()) continue;
-          // TODO: each term (and its subterms) should be processed
-          // only once per literal, see DemodulationSubtermIndex
-          Term* t = tl.term();
-          if (InductionHelper::isInductionTermFunctor(t->functor()) &&
-              InductionHelper::isIntInductionTermListInLiteral(t, lit)) {
-            if (adding) {
-              _is->insert(TypedTermList(t), lit, c);
-            } else {
-              _is->remove(TypedTermList(t), lit, c);
-            }
-          }
+  for (unsigned i=0;i<c->length();i++) {
+    Literal* lit = (*c)[i];
+    if (!InductionHelper::isInductionLiteral(lit)) {
+      continue;
+    }
+
+    DHSet<Term*> done;
+    NonVariableNonTypeIterator it(lit);
+    while (it.hasNext()) {
+      Term* t = it.next();
+      if (!done.insert(t)) {
+        it.right();
+        continue;
+      }
+      if (t->isLiteral()) {
+        continue;
+      }
+      if (InductionHelper::isInductionTermFunctor(t->functor()) &&
+          InductionHelper::isIntInductionTermListInLiteral(t, lit)) {
+        if (adding) {
+          _is->insert(TypedTermList(t), lit, c);
+        } else {
+          _is->remove(TypedTermList(t), lit, c);
         }
       }
     }
@@ -162,23 +170,24 @@ void StructInductionTermIndex::handleClause(Clause* c, bool adding)
   if (!InductionHelper::isInductionClause(c)) {
     return;
   }
-  static DHSet<TermList> inserted;
+  static DHSet<Term*> inserted;
   // Iterate through literals & check if the literal is suitable for induction
   for (unsigned i=0;i<c->length();i++) {
     inserted.reset();
     Literal* lit = (*c)[i];
     if (!lit->ground()) {
       continue;
     }
-    SubtermIterator it(lit);
+    NonVariableNonTypeIterator it(lit);
     while (it.hasNext()) {
-      TermList tl = it.next();
-      if (!inserted.insert(tl)) {
+      Term* t = it.next();
+      if (!inserted.insert(t)) {
         it.right();
         continue;
       }
-      ASS(tl.isTerm());
-      Term* t = tl.term();
+      if (t->isLiteral()) {
+        continue;
+      }
       if (InductionHelper::isInductionTermFunctor(t->functor()) &&
           InductionHelper::isStructInductionTerm(t)) {
         if (adding) {

Inferences/BackwardSubsumptionDemodulation.cpp

@@ -76,39 +76,6 @@ void BackwardSubsumptionDemodulation::detach()
 }
 
 
-template <typename Iterator>
-class STLIterator
-{
-  private:
-    Iterator begin;
-    Iterator end;
-
-  public:
-    using value_type = typename Iterator::value_type;
-    DECL_ELEMENT_TYPE(value_type);
-
-    STLIterator(Iterator begin, Iterator end)
-      : begin(begin), end(end)
-    { }
-
-    bool hasNext() {
-      return begin != end;
-    }
-
-    value_type next() {
-      value_type x = *begin;
-      ++begin;
-      return x;
-    }
-};
-
-template <typename Iterator>
-STLIterator<Iterator> getSTLIterator(Iterator begin, Iterator end)
-{
-  return STLIterator<Iterator>(begin, end);
-}
-
-
 void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRecordIterator& simplifications)
 {
   ASSERT_VALID(*sideCl);