output proofs in the TPTP fragment of the input problem

FMB/FunctionRelationshipInference.cpp

@@ -59,7 +59,7 @@ void FunctionRelationshipInference::findFunctionRelationships(ClauseIterator cla
   Options opt; // default saturation algorithm options
 
   Problem* inputProblem = env.getMainProblem();
-  env.setMainProblem(&prb);
+  env.setMainProblem(&prb, /* isInputProblem */ false);
   unsigned useTimeLimit = env.options->fmbDetectSortBoundsTimeLimit();
   opt.setSplitting(false);
   opt.resolveAwayAutoValues0();
@@ -76,7 +76,7 @@ void FunctionRelationshipInference::findFunctionRelationships(ClauseIterator cla
     // This is expected behaviour
   }
 
-  env.setMainProblem(inputProblem);
+  env.setMainProblem(inputProblem, /* isInputProblem */ false);
 
   Stack<unsigned> foundLabels = labelFinder->getFoundLabels();
 

Kernel/Formula.cpp

@@ -196,7 +196,11 @@ std::string Formula::toString () const
             res += ",";
           }
           res += Term::variableToString(var);
-          if (sort != AtomicSort::defaultSort() || env.getMainProblem()->hasNonDefaultSorts()) {
+          // a variable of a sort other than $i must always be annotated, and
+          // preprocessing is not expected to introduce such a sort into an
+          // initially untyped problem
+          ASS(sort == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts());
+          if (env.initiallyHasNonDefaultSorts()) {
             res += " : " + sort.toString();
           }
           first = false;

Kernel/InferenceStore.cpp

@@ -117,10 +117,14 @@ std::string getQuantifiedStr(const VarContainer& vars, std::string inner, DHMap<
     std::string ty="";
     TermList t;
 
-    if(t_map.find(var,t) && env.getMainProblem()->hasNonDefaultSorts()){
-      //hasNonDefaultSorts is true if the problem contains a sort
-      //that is not $i and not a variable
-      ty=" : " + t.toString();
+    if(t_map.find(var,t)){
+      //a variable of a sort other than $i must always be annotated, and
+      //preprocessing is not expected to introduce such a sort into an
+      //initially untyped problem. Same predicate as Formula::toString.
+      ASS(t == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts());
+      if(env.initiallyHasNonDefaultSorts()){
+        ty=" : " + t.toString();
+      }
     }
     if(ty == " : $tType"){
       if (!first) { varStr = "," + varStr; }
@@ -145,18 +149,6 @@ std::string getQuantifiedStr(const VarContainer& vars, std::string inner, DHMap<
   }
 }
 
-/**
- * Return @b inner quentified over variables in @b vars
- *
- * It is caller's responsibility to ensure that variables in @b vars are unique.
- */
-template<typename VarContainer>
-std::string getQuantifiedStr(const VarContainer& vars, std::string inner, bool innerParentheses=true)
-{
-  static DHMap<unsigned,TermList> d;
-  return getQuantifiedStr(vars,inner,d,innerParentheses);
-}
-
 /**
  * Return std::string containing quantified unit @b u.
  */
@@ -439,9 +431,14 @@ struct InferenceStore::TPTPProofPrinter
 
   void print() override
   {
-    //outputSymbolDeclarations also deals with sorts for now
-    //UIHelper::outputSortDeclarations(out);
-    UIHelper::outputSymbolDeclarations(out);
+    //an fof proof needs no type declarations, and the signature can hold a
+    //typed symbol no unit ever used, whose declaration would put a tff line
+    //into an otherwise fof proof
+    if(env.initiallyHasNonDefaultSorts() || env.initiallyHigherOrder()){
+      //outputSymbolDeclarations also deals with sorts for now
+      //UIHelper::outputSortDeclarations(out);
+      UIHelper::outputSymbolDeclarations(out);
+    }
     ProofPrinter::print();
   }
 
@@ -518,9 +515,14 @@ struct InferenceStore::TPTPProofPrinter
 
   std::string getFofString(std::string id, std::string formula, std::string inference, InferenceRule rule, UnitInputType origin=UnitInputType::AXIOM)
   {
+    // use the fragment of the unpreprocessed input: the problem's own
+    // hasNonDefaultSorts() and isHigherOrder() are recomputed from the current
+    // unit list, so they forget sorts that preprocessing removed, and TPTP
+    // conventions allow a proof in a weaker fragment than the input but not in
+    // a stronger one
     std::string kind = "fof";
-    if(env.getMainProblem()->hasNonDefaultSorts()){ kind="tff"; }
-    if(env.getMainProblem()->isHigherOrder()){ kind="thf"; }
+    if(env.initiallyHasNonDefaultSorts()){ kind="tff"; }
+    if(env.initiallyHigherOrder()){ kind="thf"; }
 
     return kind+"("+id+","+getRole(rule,origin)+",("+"\n"
 	+"  "+formula+"),\n"
@@ -772,6 +774,11 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
 
     Literal* nameLit=_is->_splittingNameLiterals.get(us->number()); //the name literal must always be stored
 
+    //sorts of the clause's variables, so the quantifiers of the definition
+    //below are annotated like every other formula in the proof
+    DHMap<unsigned,TermList> t_map;
+    SortHelper::collectVariableSorts(us, t_map);
+
     std::string defId=tptpDefId(us);
 
     out<<getFofString(tptpUnitId(us), getFormulaString(us),
@@ -813,11 +820,11 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
     }
     ASS(!first);
 
-    compStr=getQuantifiedStr(compOnlyVars, compStr, multiple);
+    compStr=getQuantifiedStr(compOnlyVars, compStr, t_map, multiple);
     List<unsigned>::destroy(compOnlyVars);
 
     std::string defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString();
-    defStr=getQuantifiedStr(nameVars, defStr);
+    defStr=getQuantifiedStr(nameVars, defStr, t_map);
     List<unsigned>::destroy(nameVars);
 
     SymbolId nameSymbol = SymbolId(SymbolType::PRED,nameLit->functor());
@@ -842,13 +849,17 @@ struct InferenceStore::ProofCheckPrinter
     InferenceRule rule = cs->inference().rule();
     UnitIterator parents= cs->getParents();
 
-    //outputSymbolDeclarations also deals with sorts for now
-    //UIHelper::outputSortDeclarations(out);
-    UIHelper::outputSymbolDeclarations(out);
+    //an fof proof needs no type declarations, see TPTPProofPrinter::print
+    if(env.initiallyHasNonDefaultSorts() || env.initiallyHigherOrder()){
+      //outputSymbolDeclarations also deals with sorts for now
+      //UIHelper::outputSortDeclarations(out);
+      UIHelper::outputSymbolDeclarations(out);
+    }
 
+    // fragment of the unpreprocessed input, see the comment in getFofString
     std::string kind = "fof";
-    if(env.getMainProblem()->hasNonDefaultSorts()){ kind="tff"; }
-    if(env.getMainProblem()->isHigherOrder()){ kind="thf"; }
+    if(env.initiallyHasNonDefaultSorts()){ kind="tff"; }
+    if(env.initiallyHigherOrder()){ kind="thf"; }
 
     out << kind
         << "(r"<< cs->number()

Lib/Environment.hpp

@@ -64,9 +64,21 @@ class Environment
    * be explicitly passed to all the functions interested in knowing...)
    */
   Kernel::Problem* getMainProblem() { return _problem; }
-  void setMainProblem(Kernel::Problem* p) {
+  /**
+   * Set the problem accessed through getMainProblem(). When @b isInputProblem
+   * is true, additionally record which TPTP fragment (fof/tff/thf) the problem
+   * starts out in, so that proof output can keep printing that fragment after
+   * preprocessing has changed the unit list. Pass false when temporarily
+   * swapping in an auxiliary problem (see FunctionRelationshipInference), so
+   * the recorded fragment of the input problem survives the swap.
+   */
+  void setMainProblem(Kernel::Problem* p, bool isInputProblem = true) {
     _problem = p;
     _higherOrder = _problem->isHigherOrder();
+    if (isInputProblem) {
+      _initiallyHigherOrder = _higherOrder;
+      _initiallyHasNonDefaultSorts = _problem->hasNonDefaultSorts();
+    }
   }
 
   bool higherOrder() const {
@@ -77,9 +89,22 @@ class Environment
     _higherOrder = value;
   }
 
+  bool initiallyHigherOrder() const {
+    return _initiallyHigherOrder;
+  }
+
+  bool initiallyHasNonDefaultSorts() const {
+    return _initiallyHasNonDefaultSorts;
+  }
+
 private:
   Kernel::Problem* _problem;
   bool _higherOrder;
+  // the fragment of the input problem before preprocessing: Problem's own
+  // hasNonDefaultSorts() and isHigherOrder() are recomputed from the current
+  // unit list, so they forget sorts whose last occurrence preprocessing removed
+  bool _initiallyHigherOrder = false;
+  bool _initiallyHasNonDefaultSorts = false;
 }; // class Environment
 
 extern Environment env;

Shell/UIHelper.cpp

@@ -685,7 +685,9 @@ void UIHelper::outputSymbolTypeDeclarationIfNeeded(std::ostream& out, bool funct
 
   //don't output type of app. It is an internal Vampire thing
   if(!(function && env.signature->isAppFun(symNumber))){
-    out << (env.getMainProblem()->isHigherOrder() ? "thf(" : "tff(")
+    //match the fragment used for the proof steps (see
+    //InferenceStore's getFofString), so one proof does not mix languages
+    out << (env.initiallyHigherOrder() ? "thf(" : "tff(")
         << (function ? "func" : (typeCon ?  "type" : "pred"))
         << "_def_" << symNumber << ", type, "
         << symName << ": ";

checks/Problems/ARI/ARI496_1.p

@@ -0,0 +1,34 @@
+%------------------------------------------------------------------------------
+% File     : ARI496_1 : TPTP v9.3.0. Released v5.0.0.
+% Domain   : Arithmetic
+% Problem  : Mixed: 6 is an integer
+% Version  : Especial.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.00 v6.2.0, 0.20 v6.1.0, 0.11 v6.0.0, 0.12 v5.4.0, 0.25 v5.3.0, 0.29 v5.2.0, 0.40 v5.1.0, 0.50 v5.0.0
+% Syntax   : Number of formulae    :    1 (   1 unt;   0 typ;   0 def)
+%            Number of atoms       :    1 (   0 equ)
+%            Maximal formula atoms :    1 (   1 avg)
+%            Number of connectives :    0 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%            Maximal formula depth :    1 (   1 avg)
+%            Maximal term depth    :    1 (   1 avg)
+%            Number arithmetic     :    2 (   1 atm;   0 fun;   1 num;   0 var)
+%            Number of types       :    0 (   0 usr)
+%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :    1 (   0 usr;   0 prp; 1-1 aty)
+%            Number of functors    :    1 (   0 usr;   1 con; 0-0 aty)
+%            Number of variables   :    0 (   0   !;   0   ?;   0   :)
+% SPC      : TF0_THM_NEQ_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(mixed_types_problem_1,conjecture,
+    $is_int(6) ).
+
+%------------------------------------------------------------------------------

checks/proof/gsp-typed.p

@@ -0,0 +1,11 @@
+% expected: with -gsp on, the proof contains a general splitting definition
+% whose quantified variables carry their $int sorts.
+tff(pp_decl,type, pp: $int > $o ).
+tff(qq_decl,type, qq: ($int * $int) > $o ).
+tff(rr_decl,type, rr: ($int * $int) > $o ).
+tff(ss_decl,type, ss: $int > $o ).
+tff(ax1,axiom, ![X:$int, Y:$int, Z:$int]: (pp(X) | qq(X,Y) | rr(Y,Z) | ss(Z)) ).
+tff(ax2,axiom, ![X:$int]: ~pp(X) ).
+tff(ax3,axiom, ![Z:$int]: ~ss(Z) ).
+tff(ax4,axiom, ![Y:$int, Z:$int]: ~rr(Y,Z) ).
+tff(c,conjecture, qq(1,2) ).

checks/proof/mixed-language.p

@@ -0,0 +1,6 @@
+% expected: the whole proof is tff, with no fof lines after p's type
+% declaration.
+tff(p_decl,type, p: $int > $o ).
+tff(erased,axiom, p(1) | $is_int(6) ).
+fof(a1,axiom, q(a) ).
+fof(c1,conjecture, q(a) ).

checks/proof/unused-typed-symbol.p

@@ -0,0 +1,4 @@
+% expected: the proof stays fof even though p has a typed declaration.
+tff(p_decl,type, p: $int > $o ).
+fof(a1,axiom, q(a) ).
+fof(c1,conjecture, q(a) ).