diff --git a/FMB/FunctionRelationshipInference.cpp b/FMB/FunctionRelationshipInference.cpp index 208fb119ac..7f94e465a6 100644 --- a/FMB/FunctionRelationshipInference.cpp +++ b/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 foundLabels = labelFinder->getFoundLabels(); diff --git a/Kernel/Formula.cpp b/Kernel/Formula.cpp index aed8ed75dc..53eb6a1aab 100644 --- a/Kernel/Formula.cpp +++ b/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; diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index b09d322ef3..1545fc2b91 100644 --- a/Kernel/InferenceStore.cpp +++ b/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 -std::string getQuantifiedStr(const VarContainer& vars, std::string inner, bool innerParentheses=true) -{ - static DHMap 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 t_map; + SortHelper::collectVariableSorts(us, t_map); + std::string defId=tptpDefId(us); out<::destroy(compOnlyVars); std::string defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString(); - defStr=getQuantifiedStr(nameVars, defStr); + defStr=getQuantifiedStr(nameVars, defStr, t_map); List::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() diff --git a/Lib/Environment.hpp b/Lib/Environment.hpp index 5d3807e314..fc625247f8 100644 --- a/Lib/Environment.hpp +++ b/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; diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index 4d4718e8e0..d9e3143a24 100644 --- a/Shell/UIHelper.cpp +++ b/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 << ": "; diff --git a/checks/Problems/ARI/ARI496_1.p b/checks/Problems/ARI/ARI496_1.p new file mode 100644 index 0000000000..a553a26526 --- /dev/null +++ b/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) ). + +%------------------------------------------------------------------------------ diff --git a/checks/proof/gsp-typed.p b/checks/proof/gsp-typed.p new file mode 100644 index 0000000000..b7be8b14f0 --- /dev/null +++ b/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) ). diff --git a/checks/proof/mixed-language.p b/checks/proof/mixed-language.p new file mode 100644 index 0000000000..1585d2f777 --- /dev/null +++ b/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) ). diff --git a/checks/proof/unused-typed-symbol.p b/checks/proof/unused-typed-symbol.p new file mode 100644 index 0000000000..2462372094 --- /dev/null +++ b/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) ).