HOL extra changes (don't merge)

CMakeLists.txt

@@ -808,7 +808,7 @@ elseif(CMAKE_BUILD_TYPE STREQUAL Release)
   add_compile_definitions(VDEBUG=0)
 endif()
 
-if(CMAKE_BUILD_HOL STREQUAL On)
+if(CMAKE_BUILD_HOL STREQUAL ON)
   message(STATUS "Building with HOL support")
   add_compile_definitions(VHOL=1)
 else()

Inferences/Induction.hpp

@@ -63,7 +63,7 @@ class SkolemSquashingTermReplacement : public TermReplacement {
 
 struct InductionContext {
   explicit InductionContext(Term* t)
-    : _indTerm(t) {}
+    : _indTerm(t), _cls({}) {}
   InductionContext(Term* t, Literal* l, Clause* cl)
     : InductionContext(t)
   {

Kernel/InferenceStore.cpp

@@ -576,6 +576,10 @@ struct InferenceStore::TPTPProofPrinter
       }
     case InferenceRule::NEGATED_CONJECTURE:
       return "negated_conjecture";
+    case InferenceRule::AVATAR_DEFINITION:
+    case InferenceRule::FUNCTION_DEFINITION:
+    case InferenceRule::GENERAL_SPLITTING_COMPONENT:
+      return "definition";
     default:
       return "plain";
     }
@@ -722,9 +726,6 @@ struct InferenceStore::TPTPProofPrinter
     UnitIterator parents=_is->getParents(us, rule);
 
     switch(rule) {
-    //case Inference::AVATAR_COMPONENT:
-    //  printSplittingComponentIntroduction(us);
-    //  return;
     case InferenceRule::GENERAL_SPLITTING_COMPONENT:
       printGeneralSplittingComponent(us);
       return;
@@ -759,16 +760,28 @@ struct InferenceStore::TPTPProofPrinter
     else if (!parents.hasNext()) {
       vstring newSymbolInfo;
       if (hasNewSymbols(us)) {
-	newSymbolInfo = getNewSymbols("naming",us);
+        vstring newSymbOrigin;
+        if (rule == InferenceRule::FUNCTION_DEFINITION) {
+          newSymbOrigin = "definition";
+        } else {
+          newSymbOrigin = "naming";
+        }
+	      newSymbolInfo = getNewSymbols(newSymbOrigin,us);
       }
-      inferenceStr="introduced("+tptpRuleName(rule)+",["+newSymbolInfo+"])";
+      inferenceStr="introduced(definition,["+newSymbolInfo+"],["+tptpRuleName(rule)+"])";
     }
     else {
       ASS(parents.hasNext());
       vstring statusStr;
       if (rule==InferenceRule::SKOLEMIZE) {
 	statusStr="status(esa),"+getNewSymbols("skolem",us);
       }
+      else if(rule==InferenceRule::NEGATED_CONJECTURE) {
+	statusStr="status(cth)";
+      }
+      else {
+	statusStr="status(thm)";
+      }
 
       inferenceStr="inference("+tptpRuleName(rule);
 
@@ -880,39 +893,12 @@ struct InferenceStore::TPTPProofPrinter
 
     SymbolId nameSymbol = SymbolId(SymbolType::PRED,nameLit->functor());
     vostringstream originStm;
-    originStm << "introduced(" << tptpRuleName(rule)
-	      << ",[" << getNewSymbols("naming",getSingletonIterator(nameSymbol))
-	      << "])";
-
-    out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
-  }
-
-  void printSplittingComponentIntroduction(Unit* us)
-  {
-    CALL("InferenceStore::TPTPProofPrinter::printSplittingComponentIntroduction");
-    ASS(us->isClause());
-
-    Clause* cl=us->asClause();
-    ASS(cl->splits());
-    ASS_EQ(cl->splits()->size(),1);
-
-    InferenceRule rule=InferenceRule::AVATAR_COMPONENT;
-
-    vstring defId=tptpDefId(us);
-    vstring splitPred = splitsToString(cl->splits());
-    vstring defStr=getQuantifiedStr(cl)+" <=> ~"+splitPred;
-
-    out<<getFofString(tptpUnitId(us), getFormulaString(us),
-  "inference("+tptpRuleName(InferenceRule::CLAUSIFY)+",[],["+defId+"])", InferenceRule::CLAUSIFY)<<endl;
-
-    vstringstream originStm;
-    originStm << "introduced(" << tptpRuleName(rule)
-        << ",[" << getNewSymbols("naming",splitPred)
-        << "])";
+    originStm << "introduced(definition,["
+	      << getNewSymbols("naming",getSingletonIterator(nameSymbol))
+	      << "],[" << tptpRuleName(rule) << "])";
 
     out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
   }
-
 };
 
 struct InferenceStore::ProofCheckPrinter

Kernel/Signature.hpp

@@ -66,22 +66,20 @@ class Signature
   static const unsigned REAL_SRT_CON=4;
   /** this is not a sort, it is just used to denote the first index of a user-define sort */
   static const unsigned FIRST_USER_CON=5;
-  
+
   enum Proxy {
     AND,
     OR,
     IMP,
-    FORALL,
-    EXISTS,
     IFF,
     XOR,
     NOT,
     PI,
     SIGMA,
     EQUALS,
     NOT_PROXY
-  };  
-  
+  };
+
   class Symbol {
 
   protected:

Lib/Hash.hpp

@@ -18,6 +18,7 @@
 #include <utility>
 #include <functional>
 #include <type_traits>
+#include <cstdint>
 
 #include "Forwards.hpp"
 #include "VString.hpp"

Parse/TPTP.cpp

@@ -99,8 +99,7 @@ TPTP::TPTP(istream& in)
     _modelDefinition(false),
     _insideEqualityArgument(0),
     _unitSources(0),
-    _filterReserved(false),
-    _seenConjecture(false)
+    _filterReserved(false)
 {
 } // TPTP::TPTP
 
@@ -1439,19 +1438,23 @@ void TPTP::tff()
         resetToks();
         unsigned arity = getConstructorArity();
         bool added = false;
+        /*
         unsigned fun = arity == 0
             ? addUninterpretedConstant(nm, _overflow, added)
             : env.signature->addFunction(nm, arity, added);
         Signature::Symbol* symbol = env.signature->getFunction(fun);
+        */
+        unsigned typeCon = env.signature->addTypeCon(nm,arity,added);
+        Signature::Symbol* symbol = env.signature->getTypeCon(typeCon);
         OperatorType* ot = OperatorType::getTypeConType(arity);
         if (!added) {
           if(symbol->fnType()!=ot){
             PARSE_ERROR("Type constructor declared with two different types",tok);
           }
         } else{
-          symbol->setType(ot);  
+          symbol->setType(ot);
           _typeConstructorArities.insert(nm, arity);
-        }       
+        }
         //cout << "added type constuctor " + nm + " of type " + symbol->fnType()->toString() << endl;
         while (lpars--) {
           consumeToken(T_RPAR);
@@ -1551,13 +1554,15 @@ void TPTP::holFormula()
   case T_SIGMA:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vSIGMA", 1));    
+    _termLists.push(createFunctionApplication("vSIGMA", 1));
+    _lastPushed = TM;
     return;
 
   case T_PI:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vPI", 1));      
+    _termLists.push(createFunctionApplication("vPI", 1));
+    _lastPushed = TM;
     return;
 
   case T_FORALL:
@@ -1586,6 +1591,7 @@ void TPTP::holFormula()
     ASS(_connectives.top() == NOT);
     _connectives.pop();
     _termLists.push(createFunctionApplication("vNOT", 0));
+    _lastPushed = TM;
     return;
   }
 
@@ -3768,8 +3774,6 @@ void TPTP::endFof()
   switch (_lastInputType) {
   case UnitInputType::CONJECTURE:
     if(!isFof) USER_ERROR("conjecture is not allowed in cnf");
-    if(_seenConjecture) USER_ERROR("Vampire only supports a single conjecture in a problem");
-    _seenConjecture=true;
     if (_isQuestion && ((env.options->mode() == Options::Mode::CLAUSIFY) || (env.options->mode() == Options::Mode::TCLAUSIFY)) && f->connective() == EXISTS) {
       // create an answer predicate
       QuantifiedFormula* g = static_cast<QuantifiedFormula*>(f);

Parse/TPTP.hpp

@@ -890,8 +890,6 @@ class TPTP
   DHMap<vstring, unsigned> _typeConstructorArities;
 
   bool _filterReserved;
-  bool _seenConjecture;
-
 
 #if VDEBUG
   void printStates(vstring extra);

Shell/Options.cpp

@@ -522,6 +522,18 @@ void Options::init()
     _tweeGoalTransformation.setExperimental();
     _lookup.insert(&_tweeGoalTransformation);
 
+    // At least on higher-order TPTP, tgt with tsa=off sucks badly
+    // TODO: investigate perhaps less invasive options of restraining general tgt
+    // in HOL, that would still be performant
+    _tweeSkipArrows = BoolOptionValue("twee_skip_arrows","tsa",true);
+    _tweeSkipArrows.description =
+      "During twee_goal_transformation, when in HOL, "
+      "don't introduce definitions for other subterms than those "
+      "whose type is not an arrow type.";
+    _tweeSkipArrows.tag(OptionTag::PREPROCESSING);
+    _tweeSkipArrows.setExperimental();
+    _lookup.insert(&_tweeSkipArrows);
+
     _generalSplitting = BoolOptionValue("general_splitting","gsp",false);
     _generalSplitting.description=
     "Splits clauses in order to reduce number of different variables in each clause. "

Shell/Options.hpp

@@ -2329,6 +2329,7 @@ bool _hard;
   bool skolemReuse() const { return _skolemReuse.actualValue; }
   bool definitionReuse() const { return _definitionReuse.actualValue; }
   TweeGoalTransformation tweeGoalTransformation() const { return _tweeGoalTransformation.actualValue; }
+  bool tweeSkipArrows() const { return _tweeSkipArrows.actualValue; }
   bool outputAxiomNames() const { return _outputAxiomNames.actualValue; }
   void setOutputAxiomNames(bool newVal) { _outputAxiomNames.actualValue = newVal; }
   QuestionAnsweringMode questionAnswering() const { return _questionAnswering.actualValue; }
@@ -2656,7 +2657,8 @@ bool _hard;
   BoolOptionValue _skolemReuse;
   BoolOptionValue _definitionReuse;
   ChoiceOptionValue<TweeGoalTransformation> _tweeGoalTransformation;
-
+  BoolOptionValue _tweeSkipArrows;
+
   BoolOptionValue _generalSplitting;
   BoolOptionValue _globalSubsumption;
   ChoiceOptionValue<GlobalSubsumptionSatSolverPower> _globalSubsumptionSatSolverPower;

Shell/Statistics.hpp

@@ -63,9 +63,9 @@ class Statistics
   /** number of formula names re-used during preprocessing */
   unsigned reusedFormulaNames;
   /** number of skolem functions (also predicates in FOOL) introduced during skolemization */
-  unsigned skolemFunctions;
+  unsigned skolemFunctions = 0;
   /** number of formula names re-used during preprocessing */
-  unsigned reusedSkolemFunctions;
+  unsigned reusedSkolemFunctions = 0;
   /** number of initial clauses */
   unsigned initialClauses;
   /** number of inequality splittings performed */
@@ -83,7 +83,7 @@ class Statistics
   /** number of iterations before SInE reached fixpoint */
   unsigned sineIterations;
   /** number of detected blocked clauses */
-  unsigned blockedClauses;
+  unsigned blockedClauses = 0;
 
   //Generating inferences
   /** number of clauses generated by factoring*/
@@ -240,7 +240,7 @@ class Statistics
   unsigned taAcyclicityGeneratedDisequalities;
 
   // Saturation
-  unsigned activations;
+  unsigned activations = 0;
   /** all clauses ever occurring in the unprocessed queue */
   unsigned generatedClauses;
   /** all passive clauses */

Shell/TweeGoalTransformation.cpp

@@ -124,6 +124,10 @@ class Definizator : public BottomUpTermTransformer {
       Term* t = trm.term();
       if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm;
 
+      if(env.options->tweeSkipArrows() && SortHelper::getResultSort(t).isArrowSort()) {
+        return trm;
+      }
+
 #if VHOL
       if (env.property->higherOrder() && trm.containsLooseIndex())
       { return trm; }