From 544d422f14f4306370d6e795c1708985bdaee90e Mon Sep 17 00:00:00 2001 From: Rockjack00 Date: Fri, 21 Mar 2025 18:06:18 +0100 Subject: [PATCH 01/10] Capitalized CMAKE_BUILD_HOL value --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5639d5cff0..a903f6043e 100644 --- a/CMakeLists.txt +++ b/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() From 7b44b1c2f9ef91688ffd1e54c78e5819f24bea18 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Tue, 1 Jul 2025 09:55:10 +0100 Subject: [PATCH 02/10] emergency GDV fixes for HOL --- Kernel/InferenceStore.cpp | 56 +++++++++++++++------------------------ 1 file changed, 21 insertions(+), 35 deletions(-) diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 794b660276..dabe6d7c60 100644 --- a/Kernel/InferenceStore.cpp +++ b/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,9 +760,15 @@ 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()); @@ -769,6 +776,12 @@ struct InferenceStore::TPTPProofPrinter 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<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< Date: Tue, 17 Feb 2026 17:05:09 +0100 Subject: [PATCH 03/10] multiple conjectures are fine (the E-way) --- Parse/TPTP.cpp | 5 +---- Parse/TPTP.hpp | 2 -- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index 92fab67d2a..594d5e25cb 100644 --- a/Parse/TPTP.cpp +++ b/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 @@ -3768,8 +3767,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(f); diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp index dd11767e08..6f3df997a8 100644 --- a/Parse/TPTP.hpp +++ b/Parse/TPTP.hpp @@ -890,8 +890,6 @@ class TPTP DHMap _typeConstructorArities; bool _filterReserved; - bool _seenConjecture; - #if VDEBUG void printStates(vstring extra); From 158095b53ef1b39fd747e7143ffb4e5808f2cd0f Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 24 Feb 2026 08:49:34 +0100 Subject: [PATCH 04/10] let's try tgt (for HOL) which does not name higher-order creatures --- Shell/TweeGoalTransformation.cpp | 3 +++ z3 | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp index 0d7e471c52..b4a48f1353 100644 --- a/Shell/TweeGoalTransformation.cpp +++ b/Shell/TweeGoalTransformation.cpp @@ -124,6 +124,9 @@ class Definizator : public BottomUpTermTransformer { Term* t = trm.term(); if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm; + // let's try tgt (for HOL) which does not name higher-order creatures + if (SortHelper::getResultSort(t).isArrowSort()) return trm; + #if VHOL if (env.property->higherOrder() && trm.containsLooseIndex()) { return trm; } diff --git a/z3 b/z3 index e417f7d785..3c47fd96cf 160000 --- a/z3 +++ b/z3 @@ -1 +1 @@ -Subproject commit e417f7d78509b2d0c9ebc911fee7632e6ef546b6 +Subproject commit 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 From d35094f0a6044f88e642ef7a4e54fb221e6d3608 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 24 Feb 2026 09:15:29 +0100 Subject: [PATCH 05/10] guard the new modification of HOL tgt behind an option --- Shell/Options.cpp | 12 ++++++++++++ Shell/Options.hpp | 4 +++- Shell/TweeGoalTransformation.cpp | 5 +++-- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 411ac4aa9c..d97114a9a4 100644 --- a/Shell/Options.cpp +++ b/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. " diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 3f018ba0f2..451b026950 100644 --- a/Shell/Options.hpp +++ b/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; - + BoolOptionValue _tweeSkipArrows; + BoolOptionValue _generalSplitting; BoolOptionValue _globalSubsumption; ChoiceOptionValue _globalSubsumptionSatSolverPower; diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp index b4a48f1353..08fce56cc7 100644 --- a/Shell/TweeGoalTransformation.cpp +++ b/Shell/TweeGoalTransformation.cpp @@ -124,8 +124,9 @@ class Definizator : public BottomUpTermTransformer { Term* t = trm.term(); if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm; - // let's try tgt (for HOL) which does not name higher-order creatures - if (SortHelper::getResultSort(t).isArrowSort()) return trm; + if(env.options->tweeSkipArrows() && SortHelper::getResultSort(t).isArrowSort()) { + return trm; + } #if VHOL if (env.property->higherOrder() && trm.containsLooseIndex()) From 4de6185f0fe19b0ad30eee95658e215ec8b468ef Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Mon, 2 Mar 2026 12:51:25 +0100 Subject: [PATCH 06/10] introduce typeCons early during parsing --- Parse/TPTP.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index 594d5e25cb..77522ba241 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -1438,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); From 7a1527ef91289ff2205a83e460e6c4ee2f507c5c Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 3 Mar 2026 15:28:46 +0100 Subject: [PATCH 07/10] no use of FORALL/EXISTS proxy --- Kernel/Signature.hpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index dfab065992..4ed099f200 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -66,13 +66,11 @@ 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, @@ -80,8 +78,8 @@ class Signature SIGMA, EQUALS, NOT_PROXY - }; - + }; + class Symbol { protected: From ff55bca2a60b97083f38198aae916c0f1cd775ef Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 4 Mar 2026 12:31:01 +0100 Subject: [PATCH 08/10] some ad hoc fixing of statistics --- Shell/Statistics.hpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp index 2f602496d9..c13f126c1a 100644 --- a/Shell/Statistics.hpp +++ b/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 */ From b486e5b564fe79005560e19a0a07a82a99baa9f9 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Mon, 23 Mar 2026 16:04:38 +0100 Subject: [PATCH 09/10] fix: pushed proxies are terms (TM) --- Parse/TPTP.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index 77522ba241..43b647db56 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -1554,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: @@ -1589,6 +1591,7 @@ void TPTP::holFormula() ASS(_connectives.top() == NOT); _connectives.pop(); _termLists.push(createFunctionApplication("vNOT", 0)); + _lastPushed = TM; return; } From db9c0aa6873c6d4406ef74354abd5bbb9c45d21c Mon Sep 17 00:00:00 2001 From: Matthias Hetzenberger Date: Thu, 11 Jun 2026 15:54:51 +0200 Subject: [PATCH 10/10] Fix compilation for g++ 15 --- Inferences/Induction.hpp | 2 +- Lib/Hash.hpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index c9c3b81a94..0e2fbc786c 100644 --- a/Inferences/Induction.hpp +++ b/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) { diff --git a/Lib/Hash.hpp b/Lib/Hash.hpp index dd07d06ee3..1f17d06d7d 100644 --- a/Lib/Hash.hpp +++ b/Lib/Hash.hpp @@ -18,6 +18,7 @@ #include #include #include +#include #include "Forwards.hpp" #include "VString.hpp"