From 6a71f98f2852fca9a520eff72ff688d6c9c18c2f Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sat, 2 Aug 2025 11:48:53 +0200 Subject: [PATCH 1/7] Break symmetries if we have incomparable equations --- Inferences/BackwardDemodulation.cpp | 2 +- Inferences/DemodulationHelper.cpp | 8 +++++--- Inferences/DemodulationHelper.hpp | 2 +- Inferences/ForwardDemodulation.cpp | 2 +- Inferences/FunctionDefinitionRewriting.cpp | 2 +- Shell/PartialRedundancyHandler.cpp | 14 +++++++++++++- 6 files changed, 22 insertions(+), 8 deletions(-) diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index 0062a495e5..114aee492d 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -150,7 +150,7 @@ struct BackwardDemodulation::ResultFn TermList rhsS=subs->applyToBoundQuery(rhs); if (_helper.redundancyCheckNeededForPremise(qr.data->clause,qr.data->literal,lhsS) && - !_helper.isPremiseRedundant(qr.data->clause,qr.data->literal,lhsS,rhsS,lhs,&appl)) + !_helper.isPremiseRedundant(qr.data->clause,qr.data->literal,lhsS,rhsS,_cl,lhs,&appl)) { return BwSimplificationRecord(0); } diff --git a/Inferences/DemodulationHelper.cpp b/Inferences/DemodulationHelper.cpp index 2e547a8b6a..9d257653ea 100644 --- a/Inferences/DemodulationHelper.cpp +++ b/Inferences/DemodulationHelper.cpp @@ -75,18 +75,20 @@ bool DemodulationHelper::isRenamingOn(const SubstApplicator* applicator, TermLis } bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermList rwTerm, - TermList tgtTerm, TermList eqLHS, const SubstApplicator* eqApplicator) const + TermList tgtTerm, Clause* eqCl, TermList eqLHS, const SubstApplicator* eqApplicator) const { ASS(redundancyCheckNeededForPremise(rwCl, rwLit, rwTerm)); TermList other=EqHelper::getOtherEqualitySide(rwLit, rwTerm); - if (_ord->compare(tgtTerm, other) == Ordering::LESS) { + auto tord = _ord->compare(tgtTerm, other); + if (tord == Ordering::LESS) { return true; } if (_encompassing) { // under _encompassing, we know there are no other literals in rwCl - return !isRenamingOn(eqApplicator,eqLHS); + return !isRenamingOn(eqApplicator,eqLHS) || + (tord == Ordering::INCOMPARABLE && rwCl->number() > eqCl->number()); } // return early to avoid creation of eqLitS diff --git a/Inferences/DemodulationHelper.hpp b/Inferences/DemodulationHelper.hpp index 34e5029a7c..bff46a22d3 100644 --- a/Inferences/DemodulationHelper.hpp +++ b/Inferences/DemodulationHelper.hpp @@ -28,7 +28,7 @@ class DemodulationHelper { bool redundancyCheckNeededForPremise(Clause* rwCl, Literal* rwLit, TermList rwTerm) const; bool isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermList rwTerm, TermList tgtTerm, - TermList eqLHS, const SubstApplicator* applicator) const; + Clause* eqCl, TermList eqLHS, const SubstApplicator* applicator) const; private: bool _redundancyCheck; diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index 3606919b1e..5a7aee3665 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -202,7 +202,7 @@ bool ForwardDemodulationImpl::perform(Clause* cl, Clause*& replacement, ClauseIt TermList rhsS = rhsApplied.apply(); - if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, appl)) { + if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, qr.data->clause, lhs, appl)) { continue; } diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index 51d890a68f..435a64cc7e 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -64,7 +64,7 @@ Clause* performRewriting( Applicator appl(subst.ptr()); - if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,&appl)) { + if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqClause,eqLHS,&appl)) { return 0; } diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index d0b191cd5a..c5ba75e59d 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -528,7 +528,19 @@ bool PartialRedundancyHandlerImpl::compareWithSupe return true; } // case 2.b. - return checkOrConstrainGreater(_ord->compare(other, tgtTermS), other, tgtTermS, cons); + auto tord = _ord->compare(other, tgtTermS); + switch (tord) { + case Ordering::GREATER: + return true; + case Ordering::EQUAL: + env.statistics->generalizedInductionApplication++; + return rwCl->number() > eqCl->number(); + case Ordering::LESS: + return false; + case Ordering::INCOMPARABLE: + env.statistics->generalizedInductionApplicationInProof++; + return rwCl->number() > eqCl->number() || checkOrConstrainGreater(tord, other, tgtTermS, cons); + } } // case 2.c. if (!MatchingUtils::matchTerms(rwTerm, eqLHS)) { From 1327347fc5808e3cfe0e6838ddf46781fc89162d Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Mon, 6 Apr 2026 13:15:37 +0200 Subject: [PATCH 2/7] remove stats --- Shell/PartialRedundancyHandler.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index f51edee0d7..4351d56d89 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -529,12 +529,10 @@ bool PartialRedundancyHandlerImpl::compareWithSupe case Ordering::GREATER: return true; case Ordering::EQUAL: - env.statistics->generalizedInductionApplication++; return rwCl->number() > eqCl->number(); case Ordering::LESS: return false; case Ordering::INCOMPARABLE: - env.statistics->generalizedInductionApplicationInProof++; return rwCl->number() > eqCl->number() || checkOrConstrainGreater(tord, other, tgtTermS, cons); } } From d896e66c16ca45a7ad1aaeb55318ab910df1d0d4 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 15 Oct 2026 14:15:06 +0200 Subject: [PATCH 3/7] Add option to enable --- Inferences/DemodulationHelper.cpp | 3 ++- Inferences/DemodulationHelper.hpp | 1 + Shell/Options.cpp | 3 ++- Shell/Options.hpp | 3 +++ Shell/PartialRedundancyHandler.cpp | 22 +++++++++++++--------- Shell/PartialRedundancyHandler.hpp | 2 ++ 6 files changed, 23 insertions(+), 11 deletions(-) diff --git a/Inferences/DemodulationHelper.cpp b/Inferences/DemodulationHelper.cpp index 951cc01ce3..c36d9d06c8 100644 --- a/Inferences/DemodulationHelper.cpp +++ b/Inferences/DemodulationHelper.cpp @@ -25,6 +25,7 @@ using namespace Kernel; DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering* ord) : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF), _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), + _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED), _ord(ord) { } @@ -57,7 +58,7 @@ bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermLi if (_encompassing) { // under _encompassing, we know there are no other literals in rwCl return !isRenamingOn(eqApplicator,eqLHS) || - (tord == Ordering::INCOMPARABLE && rwCl->number() > eqCl->number()); + (_labeled && tord == Ordering::INCOMPARABLE && rwCl->number() > eqCl->number()); } // return early to avoid creation of eqLitS diff --git a/Inferences/DemodulationHelper.hpp b/Inferences/DemodulationHelper.hpp index cdb686debb..6fb5cdef10 100644 --- a/Inferences/DemodulationHelper.hpp +++ b/Inferences/DemodulationHelper.hpp @@ -58,6 +58,7 @@ class DemodulationHelper { private: bool _redundancyCheck; bool _encompassing; + bool _labeled; const Ordering* _ord; }; diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 878f945fab..8821b0df1d 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -685,7 +685,7 @@ Options::Options () .description = "Perform condensation. If 'fast' is specified, we only perform condensations that are easy to check for.", .tag = OptionTag::INFERENCES}) , _demodulationRedundancyCheck("demodulation_redundancy_check",this, - DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass"}, + DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass", "labeled"}, {.short_name = "drc", .description = "The following cases of backward and forward demodulation do not preserve completeness:\n" "s = t s = t1 \\/ C \t s = t s != t1 \\/ C\n" @@ -693,6 +693,7 @@ Options::Options () "--------------------- \t ---------------------\n" "t = t1 \\/ C \t\t t != t1 \\/ C\n" "where t > t1 and s = t > C (RHS replaced)\n" + "With `labeled`, we have `encompass` but we also demodulate one equation with another (equally general but incomparable) equation if one was generated earlier (labeled smaller)." "With `encompass`, we treat demodulations (both forward and backward) as encompassment demodulations (as defined by Duarte and Korovin in 2022's IJCAR paper).\n" "With `ordering`, we check this condition and don't demodulate if we could violate completeness.\n" "With `off`, we skip the checks, save time, but become incomplete.", diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 4c25cc6c0f..5edd305f96 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -463,6 +463,9 @@ class Options ENCOMPASS, // (1) positive unit equations (PUE) are smaller than non-PUE clauses, // (2) more general PUE are smaller than less general PUE, and // (3) equally general PUEs are ordered based on term ordering. + LABELED, // similar to encompass, but a PUE is smaller than another when + // they are equally general ordered but incomparable equations + // and the label (clause number) is smaller then that of the other. }; enum class TheoryAxiomLevel : unsigned int { diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 0983d5ed7c..c5665c5e0c 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -524,15 +524,19 @@ bool PartialRedundancyHandlerImpl::compareWithSupe } // case 2.b. auto tord = _ord->compare(other, tgtTermS); - switch (tord) { - case Ordering::GREATER: - return true; - case Ordering::EQUAL: - return rwCl->number() > eqCl->number(); - case Ordering::LESS: - return false; - case Ordering::INCOMPARABLE: - return rwCl->number() > eqCl->number() || checkOrConstrainGreater(tord, other, tgtTermS, cons); + if (_labeled) { + switch (tord) { + case Ordering::GREATER: + return true; + case Ordering::EQUAL: + return rwCl->number() > eqCl->number(); + case Ordering::LESS: + return false; + case Ordering::INCOMPARABLE: + return rwCl->number() > eqCl->number() || checkOrConstrainGreater(tord, other, tgtTermS, cons); + } + } else { + return checkOrConstrainGreater(tord, other, tgtTermS, cons); } } // case 2.c. diff --git a/Shell/PartialRedundancyHandler.hpp b/Shell/PartialRedundancyHandler.hpp index c3ba46e838..d300aed95c 100644 --- a/Shell/PartialRedundancyHandler.hpp +++ b/Shell/PartialRedundancyHandler.hpp @@ -128,6 +128,7 @@ class PartialRedundancyHandlerImpl PartialRedundancyHandlerImpl(const Options& opts, const Ordering* ord, Splitter* splitter) : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF), _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), + _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED), _ord(ord), _splitter(splitter) {} /** Returns false if superposition should be skipped. */ @@ -156,6 +157,7 @@ class PartialRedundancyHandlerImpl bool _redundancyCheck; bool _encompassing; + bool _labeled; const Ordering* _ord; Splitter* _splitter; }; From d05848fd2fc8dd123c083e15433546c280bf595d Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 15 Oct 2026 14:15:37 +0200 Subject: [PATCH 4/7] Enable by default for now --- Shell/Options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 8821b0df1d..8ee294b583 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -685,7 +685,7 @@ Options::Options () .description = "Perform condensation. If 'fast' is specified, we only perform condensations that are easy to check for.", .tag = OptionTag::INFERENCES}) , _demodulationRedundancyCheck("demodulation_redundancy_check",this, - DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass", "labeled"}, + DemodulationRedundancyCheck::LABELED,{"off","ordering","encompass", "labeled"}, {.short_name = "drc", .description = "The following cases of backward and forward demodulation do not preserve completeness:\n" "s = t s = t1 \\/ C \t s = t s != t1 \\/ C\n" From ba21902c50d1256fd7b716fde5ed7cb4d2e36de1 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 15 Oct 2026 14:27:07 +0200 Subject: [PATCH 5/7] Fix labeled not including encompassment; use const wherever possible in DemodulationHelper --- Inferences/BackwardDemodulation.cpp | 2 +- Inferences/BackwardDemodulation.hpp | 2 +- Inferences/DemodulationHelper.cpp | 8 ++++---- Inferences/DemodulationHelper.hpp | 11 +++++------ Inferences/ForwardDemodulation.cpp | 4 +--- Inferences/FunctionDefinitionRewriting.cpp | 4 ++-- Inferences/FunctionDefinitionRewriting.hpp | 2 +- Shell/PartialRedundancyHandler.hpp | 4 ++-- 8 files changed, 17 insertions(+), 20 deletions(-) diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index 8ab9629086..4fdf1bec63 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -50,7 +50,7 @@ BackwardDemodulation::BackwardDemodulation(SaturationAlgorithm& sal : _ord(salg.getOrdering()), _preordered(salg.getOptions().backwardDemodulation() == Options::Demodulation::PREORDERED), _index(salg.getSimplifyingIndex>()), - _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())) + _helper(salg.getOptions(), salg.getOrdering()) {} namespace { diff --git a/Inferences/BackwardDemodulation.hpp b/Inferences/BackwardDemodulation.hpp index bf094a6193..f31e814a94 100644 --- a/Inferences/BackwardDemodulation.hpp +++ b/Inferences/BackwardDemodulation.hpp @@ -42,7 +42,7 @@ class BackwardDemodulation const Ordering& _ord; const bool _preordered; std::shared_ptr> _index; - DemodulationHelper _helper; + const DemodulationHelper _helper; }; using BackwardDemodulationExtra = RewriteInferenceExtra; diff --git a/Inferences/DemodulationHelper.cpp b/Inferences/DemodulationHelper.cpp index c36d9d06c8..598f16b070 100644 --- a/Inferences/DemodulationHelper.cpp +++ b/Inferences/DemodulationHelper.cpp @@ -22,10 +22,10 @@ namespace Inferences { using namespace Kernel; -DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering* ord) +DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering& ord) : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF), - _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED), + _encompassing(_labeled || opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), _ord(ord) { } @@ -50,7 +50,7 @@ bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermLi ASS(redundancyCheckNeededForPremise(rwCl, rwLit, rwTerm)); TermList other=EqHelper::getOtherEqualitySide(rwLit, rwTerm); - auto tord = _ord->compare(tgtTerm, other); + auto tord = _ord.compare(tgtTerm, other); if (tord == Ordering::LESS) { return true; } @@ -78,7 +78,7 @@ bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermLi // Hence we need to check if there are any literals // in rwCl greater than eqLitS. return rwCl->iterLits().any([rwLit,this,eqLitS](Literal* lit) { - return lit != rwLit && _ord->compare(eqLitS, lit)==Ordering::LESS; + return lit != rwLit && _ord.compare(eqLitS, lit)==Ordering::LESS; }); } diff --git a/Inferences/DemodulationHelper.hpp b/Inferences/DemodulationHelper.hpp index 6fb5cdef10..92c5d489f2 100644 --- a/Inferences/DemodulationHelper.hpp +++ b/Inferences/DemodulationHelper.hpp @@ -25,8 +25,7 @@ using namespace Shell; class DemodulationHelper { public: - DemodulationHelper() = default; - DemodulationHelper(const Options& opts, const Ordering* ord); + DemodulationHelper(const Options& opts, const Ordering& ord); template static bool isRenamingOn(const SubstApplicator* applicator, Object obj) { @@ -56,10 +55,10 @@ class DemodulationHelper { Clause* eqCl, TermList eqLHS, const SubstApplicator* applicator) const; private: - bool _redundancyCheck; - bool _encompassing; - bool _labeled; - const Ordering* _ord; + const bool _redundancyCheck; + const bool _labeled; + const bool _encompassing; + const Ordering& _ord; }; }; diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index 29c289c78c..66eb450341 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -36,8 +36,6 @@ #include "Shell/Statistics.hpp" #include "Debug/TimeProfiling.hpp" -#include "DemodulationHelper.hpp" - #include "ForwardDemodulation.hpp" namespace Inferences { @@ -53,7 +51,7 @@ ForwardDemodulation::ForwardDemodulation(SaturationAlgorithm& salg) _encompassing(salg.getOptions().demodulationRedundancyCheck()==Options::DemodulationRedundancyCheck::ENCOMPASS), _useTermOrderingDiagrams(salg.getOptions().forwardDemodulationTermOrderingDiagrams()), _skipNonequationalLiterals(salg.getOptions().demodulationOnlyEquational()), - _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())), + _helper(salg.getOptions(), salg.getOrdering()), _ord(salg.getOrdering()), _index(salg.getSimplifyingIndex()) {} diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index ba9f05559c..8251c71344 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -92,7 +92,7 @@ Clause* performRewriting( } FunctionDefinitionRewriting::FunctionDefinitionRewriting(SaturationAlgorithm& salg) - : _salg(salg), _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())) + : _salg(salg), _helper(salg.getOptions(), salg.getOrdering()) {} Kernel::ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *premise) @@ -117,7 +117,7 @@ Kernel::ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *prem } FunctionDefinitionDemodulation::FunctionDefinitionDemodulation(SaturationAlgorithm& salg) - : _ord(salg.getOrdering()), _helper(salg.getOptions(), &_ord), _fnDefHandler(salg.getFunctionDefinitionHandler()) + : _ord(salg.getOrdering()), _helper(salg.getOptions(), _ord), _fnDefHandler(salg.getFunctionDefinitionHandler()) {} bool FunctionDefinitionDemodulation::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) diff --git a/Inferences/FunctionDefinitionRewriting.hpp b/Inferences/FunctionDefinitionRewriting.hpp index 6173a14e05..443d3c082e 100644 --- a/Inferences/FunctionDefinitionRewriting.hpp +++ b/Inferences/FunctionDefinitionRewriting.hpp @@ -47,7 +47,7 @@ class FunctionDefinitionRewriting private: const SaturationAlgorithm& _salg; - DemodulationHelper _helper; + const DemodulationHelper _helper; }; /** diff --git a/Shell/PartialRedundancyHandler.hpp b/Shell/PartialRedundancyHandler.hpp index d300aed95c..6f0f6a10b4 100644 --- a/Shell/PartialRedundancyHandler.hpp +++ b/Shell/PartialRedundancyHandler.hpp @@ -127,8 +127,8 @@ class PartialRedundancyHandlerImpl public: PartialRedundancyHandlerImpl(const Options& opts, const Ordering* ord, Splitter* splitter) : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF), - _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED), + _encompassing(_labeled || opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS), _ord(ord), _splitter(splitter) {} /** Returns false if superposition should be skipped. */ @@ -156,8 +156,8 @@ class PartialRedundancyHandlerImpl LiteralSet&& lits, SplitSet* splits) const; bool _redundancyCheck; - bool _encompassing; bool _labeled; + bool _encompassing; const Ordering* _ord; Splitter* _splitter; }; From 55b8cf5cfa697eb0e518db7d3a21ed795ff76ebd Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Fri, 16 Oct 2026 09:42:57 +0200 Subject: [PATCH 6/7] Add unit test; change back default value of drc --- Shell/Options.cpp | 2 +- Shell/Options.hpp | 2 +- UnitTests/tInferences_Demodulation.cpp | 18 ++++++++++++++++++ 3 files changed, 20 insertions(+), 2 deletions(-) diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 8ee294b583..576de71ac4 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -685,7 +685,7 @@ Options::Options () .description = "Perform condensation. If 'fast' is specified, we only perform condensations that are easy to check for.", .tag = OptionTag::INFERENCES}) , _demodulationRedundancyCheck("demodulation_redundancy_check",this, - DemodulationRedundancyCheck::LABELED,{"off","ordering","encompass", "labeled"}, + DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass","labeled"}, {.short_name = "drc", .description = "The following cases of backward and forward demodulation do not preserve completeness:\n" "s = t s = t1 \\/ C \t s = t s != t1 \\/ C\n" diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 5edd305f96..e55cad5bc0 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -465,7 +465,7 @@ class Options // (3) equally general PUEs are ordered based on term ordering. LABELED, // similar to encompass, but a PUE is smaller than another when // they are equally general ordered but incomparable equations - // and the label (clause number) is smaller then that of the other. + // and the label (clause number) is smaller than that of the other. }; enum class TheoryAxiomLevel : unsigned int { diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index 16ca18433f..07a3cbd9a6 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -213,4 +213,22 @@ TEST_SIMPLIFICATION(test19, .justifications({ /* nothing */ }) ) +// encompassment does not work with equally general but incomparable equations +TEST_SIMPLIFICATION(test20, + tester() + .simplifyWith({ clause({ g(f(x,y)) == f(x,y) }) }) + .toSimplify({ clause({ g(f(x,y)) == f(y,x) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }); +) + +// labeled demodulates equally general but incomparable equation +TEST_SIMPLIFICATION(test21, + tester() + .simplifyWith({ clause({ g(f(x,y)) == f(x,y) }) }) + .toSimplify({ clause({ g(f(x,y)) == f(y,x) }) }) + .expected({ clause({ f(x,y) == f(y,x) }) }) + .options({ { "term_ordering", "lpo" }, { "demodulation_redundancy_check", "labeled" } }); +) + } From efb802e8831a6fd7328524a5c011982c1f4d4bb4 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 20 Oct 2026 08:14:06 +0000 Subject: [PATCH 7/7] update samplers --- samplers/samplerFNT.smp | 2 +- samplers/samplerFOL.smp | 4 ++-- samplers/samplerHOL.smp | 4 ++-- samplers/samplerIND.smp | 2 +- samplers/samplerSMT.smp | 2 +- samplers/samplerUEQ.smp | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/samplers/samplerFNT.smp b/samplers/samplerFNT.smp index 8d0bbcb50b..ba97277c21 100644 --- a/samplers/samplerFNT.smp +++ b/samplers/samplerFNT.smp @@ -156,7 +156,7 @@ sa!=fmb > fd ~cat all:500,off:41,preordered:168 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554 +sa!=fmb $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554 # forward_demodulation_term_ordering_diagrams sa!=fmb fd!=off > fdtod ~cat on:1,off:1 diff --git a/samplers/samplerFOL.smp b/samplers/samplerFOL.smp index 67012b774d..22210491b8 100644 --- a/samplers/samplerFOL.smp +++ b/samplers/samplerFOL.smp @@ -208,8 +208,8 @@ sa!=fmb > fd ~cat all:500,off:41,preordered:168 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -intent=unsat sa!=fmb $drc=1 > drc ~cat encompass:500,ordering:500,off:354 -intent=sat sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554 +intent=unsat sa!=fmb $drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354 +intent=sat sa!=fmb $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554 # forward_demodulation_term_ordering_diagrams sa!=fmb fd!=off > fdtod ~cat on:1,off:1 diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp index bbadf19013..821eff942c 100644 --- a/samplers/samplerHOL.smp +++ b/samplers/samplerHOL.smp @@ -210,8 +210,8 @@ er!=off > erml ~cat 0:3,2:1,3:1 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -intent=unsat $drc=1 > drc ~cat encompass:500,ordering:500,off:354 -intent=sat $drc=1 > drc ~cat ordering:643,encompass:554 +intent=unsat $drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354 +intent=sat $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554 # forward_demodulation_term_ordering_diagrams fd!=off > fdtod ~cat on:1,off:1 diff --git a/samplers/samplerIND.smp b/samplers/samplerIND.smp index e8532286c1..746b8b0632 100644 --- a/samplers/samplerIND.smp +++ b/samplers/samplerIND.smp @@ -213,7 +213,7 @@ er!=off > erml ~cat 0:3,2:1,3:1 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -$drc=1 > drc ~cat encompass:500,ordering:500,off:354 +$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354 # forward_demodulation_term_ordering_diagrams fd!=off > fdtod ~cat on:1,off:1 diff --git a/samplers/samplerSMT.smp b/samplers/samplerSMT.smp index 410659a115..87749552fa 100644 --- a/samplers/samplerSMT.smp +++ b/samplers/samplerSMT.smp @@ -216,7 +216,7 @@ er!=off > erml ~cat 0:3,2:1,3:1 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -$drc=1 > drc ~cat encompass:500,ordering:500,off:354 +$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354 # forward_demodulation_term_ordering_diagrams fd!=off > fdtod ~cat on:1,off:1 diff --git a/samplers/samplerUEQ.smp b/samplers/samplerUEQ.smp index fff8d50937..4ade6afcfb 100644 --- a/samplers/samplerUEQ.smp +++ b/samplers/samplerUEQ.smp @@ -168,7 +168,7 @@ er!=off > erml ~cat 0:3,2:1,3:1 > $drc ~cat 0:1 fd!=off > $drc ~cat 1:1 bd!=off > $drc ~cat 1:1 -$drc=1 > drc ~cat encompass:500,ordering:500,off:354 +$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354 # forward_demodulation_term_ordering_diagrams fd!=off > fdtod ~cat on:1,off:1