From 1778675c10b94f56e1b826bcef9d37c0dd528b6c Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 29 Nov 2023 13:02:53 +0100 Subject: [PATCH 1/3] fix URR to be (really) complete also under AVATAR --- Inferences/URResolution.cpp | 22 ++++++++++++---------- Inferences/URResolution.hpp | 6 +++--- Saturation/SaturationAlgorithm.cpp | 2 +- Shell/Options.cpp | 12 ++++++++---- Shell/Options.hpp | 3 ++- 5 files changed, 26 insertions(+), 19 deletions(-) diff --git a/Inferences/URResolution.cpp b/Inferences/URResolution.cpp index 51eb742b9e..76040645fd 100644 --- a/Inferences/URResolution.cpp +++ b/Inferences/URResolution.cpp @@ -48,8 +48,8 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; -URResolution::URResolution() -: _selectedOnly(false), _unitIndex(0), _nonUnitIndex(0) {} +URResolution::URResolution(bool full) +: _full(full), _selectedOnly(false), _unitIndex(0), _nonUnitIndex(0) {} /** * Creates URResolution object with explicitely supplied @@ -58,9 +58,9 @@ URResolution::URResolution() * For objects created using this constructor it is not allowed * to call the @c attach() function. */ -URResolution::URResolution(bool selectedOnly, UnitClauseLiteralIndex* unitIndex, +URResolution::URResolution(bool full, bool selectedOnly, UnitClauseLiteralIndex* unitIndex, NonUnitClauseLiteralIndex* nonUnitIndex) -: _emptyClauseOnly(false), _selectedOnly(selectedOnly), _unitIndex(unitIndex), _nonUnitIndex(nonUnitIndex) {} +: _full(full), _emptyClauseOnly(false), _selectedOnly(selectedOnly), _unitIndex(unitIndex), _nonUnitIndex(nonUnitIndex) {} void URResolution::attach(SaturationAlgorithm* salg) { @@ -99,8 +99,8 @@ void URResolution::detach() struct URResolution::Item { - USE_ALLOCATOR(URResolution::Item); - + USE_ALLOCATOR(URResolution::Item); + Item(Clause* cl, bool selectedOnly, URResolution& parent, bool mustResolveAll) : _orig(cl), _color(cl->color()), _parent(parent) { @@ -151,7 +151,7 @@ struct URResolution::Item if (!_ansLit) { _ansLit = premAnsLit; } else if (_ansLit != premAnsLit) { - bool neg = rlit->isNegative(); + bool neg = rlit->isNegative(); Literal* resolved = unif.substitution->apply(rlit, !useQuerySubstitution); if (neg) { resolved = Literal::complementaryLiteral(resolved); @@ -311,9 +311,11 @@ void URResolution::processLiteral(ItemList*& itms, unsigned idx) itm2->resolveLiteral(idx, unif, unif.clause, true); iit.insert(itm2); - if(itm->_atMostOneNonGround && (!synthesis || !unif.clause->hasAnswerLiteral())) { - //if there is only one non-ground literal left, there is no need to retrieve - //all unifications + if(!_full && itm->_atMostOneNonGround && (!synthesis || !unif.clause->hasAnswerLiteral())) { + /* if there is only one non-ground literal left, there is no need to retrieve all unifications. + However, this does not hold under AVATAR where different empty clauses may close different + splitting branches, that's why only "full" URR is complete under AVATAR (see Options::complete) + */ break; } } diff --git a/Inferences/URResolution.hpp b/Inferences/URResolution.hpp index aee40695f8..c2d6497182 100644 --- a/Inferences/URResolution.hpp +++ b/Inferences/URResolution.hpp @@ -30,8 +30,8 @@ class URResolution : public GeneratingInferenceEngine { public: - URResolution(); - URResolution(bool selectedOnly, UnitClauseLiteralIndex* unitIndex, + URResolution(bool full); + URResolution(bool full, bool selectedOnly, UnitClauseLiteralIndex* unitIndex, NonUnitClauseLiteralIndex* nonUnitIndex); void attach(SaturationAlgorithm* salg); @@ -49,7 +49,7 @@ class URResolution void doBackwardInferences(Clause* cl, ClauseList*& acc); - + bool _full; bool _emptyClauseOnly; bool _selectedOnly; UnitClauseLiteralIndex* _unitIndex; diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 5a6c7a3536..7fc7f1910e 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1559,7 +1559,7 @@ SaturationAlgorithm* SaturationAlgorithm::createFromOptions(Problem& prb, const gie->addFront(new BinaryResolution()); } if (opt.unitResultingResolution() != Options::URResolution::OFF) { - gie->addFront(new URResolution()); + gie->addFront(new URResolution(opt.unitResultingResolution() == Options::URResolution::FULL)); } if (opt.extensionalityResolution() != Options::ExtensionalityResolution::OFF) { gie->addFront(new ExtensionalityResolution()); diff --git a/Shell/Options.cpp b/Shell/Options.cpp index d7dabf4529..977520befe 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1658,13 +1658,16 @@ void Options::init() _equationalTautologyRemoval.onlyUsefulWith(ProperSaturationAlgorithm()); _equationalTautologyRemoval.tag(OptionTag::INFERENCES); - _unitResultingResolution = ChoiceOptionValue("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on"}); + _unitResultingResolution = ChoiceOptionValue("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on","full"}); _unitResultingResolution.description= - "Uses unit resulting resolution only to derive empty clauses (may be useful for splitting)"; + "Uses unit resulting resolution only to derive empty clauses (may be useful for splitting)." + " 'ec_only' only derives empty clauses, 'on' does everything (but implements a heuristic to skip deriving more than one empty clause)" + " 'full' ignores this heuristic is thus complete also under AVATAR."; _lookup.insert(&_unitResultingResolution); _unitResultingResolution.tag(OptionTag::INFERENCES); _unitResultingResolution.onlyUsefulWith(ProperSaturationAlgorithm()); _unitResultingResolution.addProblemConstraint(notJustEquality()); + _unitResultingResolution.addConstraint(If(equal(URResolution::FULL)).then(_splitting.is(equal(true)))); // If br has already been set off then this will be forced on, if br has not yet been set // then setting this to off will force br on @@ -3414,9 +3417,10 @@ bool Options::complete(const Problem& prb) const if (!hasEquality) { if (_binaryResolution.actualValue) return true; - if (_unitResultingResolution.actualValue!=URResolution::ON) return false; // binary resolution is off - return prop.category() == Property::HNE; // URR is complete for Horn problems + if (_unitResultingResolution.actualValue!=URResolution::FULL && + (_unitResultingResolution.actualValue!=URResolution::ON || _splitting.actualValue) ) return false; + return prop.category() == Property::HNE; // enough URR is complete for Horn problems } if (_demodulationRedundancyCheck.actualValue == DemodulationRedunancyCheck::OFF) { diff --git a/Shell/Options.hpp b/Shell/Options.hpp index ad2eb6f14c..5d81a5c598 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -531,7 +531,8 @@ class Options enum class URResolution : unsigned int { EC_ONLY = 0, OFF = 1, - ON = 2 + ON = 2, + FULL = 3 }; enum class TermOrdering : unsigned int { From f43eb76698f220511d7b83ac3054d2d9b7314565 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 29 Nov 2023 16:38:49 +0100 Subject: [PATCH 2/3] update the sampler accordingly --- samplerFNT.txt | 9 ++++++--- samplerFOL.txt | 9 ++++++--- samplerSMT.txt | 9 ++++++--- 3 files changed, 18 insertions(+), 9 deletions(-) diff --git a/samplerFNT.txt b/samplerFNT.txt index 51568936bd..e289e01fe6 100644 --- a/samplerFNT.txt +++ b/samplerFNT.txt @@ -154,9 +154,6 @@ er!=off > erml ~cat 0:3,2:1,3:1 # inner_rewriting > irw ~cat off:165,on:6 -# unit_resulting_resolution -> urr ~cat off:1200,ec_only:162,on:340 - # binary_resolution urr=on > br ~cat on:10,off:1 @@ -269,6 +266,12 @@ av=on > sac ~cat off:3,on:1 # TODO: consider enabling this for vampire_z3 compiles! # av=on > sas ~cat minisat:10,z3:1 +# BACK TO PREPROCESSING + +# unit_resulting_resolution +av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 +av=off > urr ~cat off:1200,ec_only:162,on:340 + # AVATAR SPLIT QUEUE # avatar_split_queue diff --git a/samplerFOL.txt b/samplerFOL.txt index 473bfea7c6..330aa763f4 100644 --- a/samplerFOL.txt +++ b/samplerFOL.txt @@ -190,9 +190,6 @@ er!=off > erml ~cat 0:3,2:1,3:1 # inner_rewriting > irw ~cat off:165,on:6 -# unit_resulting_resolution -> urr ~cat off:1200,ec_only:162,on:340 - # SINE LEVELS and shit # sine_to_age @@ -302,6 +299,12 @@ av=on > sac ~cat off:3,on:1 # TODO: consider enabling this for vampire_z3 compiles! # av=on > sas ~cat minisat:10,z3:1 +# BACK TO PREPROCESSING + +# unit_resulting_resolution +av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 +av=off > urr ~cat off:1200,ec_only:162,on:340 + # AVATAR SPLIT QUEUE # avatar_split_queue diff --git a/samplerSMT.txt b/samplerSMT.txt index fd279c6f30..4e7463fd8e 100644 --- a/samplerSMT.txt +++ b/samplerSMT.txt @@ -216,9 +216,6 @@ er!=off > erml ~cat 0:3,2:1,3:1 # inner_rewriting > irw ~cat off:165,on:6 -# unit_resulting_resolution -> urr ~cat off:1200,ec_only:162,on:340 - # SINE LEVELS and shit # sine_to_age @@ -328,6 +325,12 @@ av=on > sac ~cat off:3,on:1 # TODO: consider enabling this for vampire_z3 compiles! # av=on > sas ~cat minisat:10,z3:1 +# BACK TO PREPROCESSING + +# unit_resulting_resolution +av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 +av=off > urr ~cat off:1200,ec_only:162,on:340 + # AVATAR SPLIT QUEUE # avatar_split_queue From 5cb1320ea4a51b0f6aeb3dff1921ccff6e82e5a4 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Fri, 1 Dec 2023 20:20:49 +0100 Subject: [PATCH 3/3] fix description --- Shell/Options.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 977520befe..82da264f1f 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1661,8 +1661,8 @@ void Options::init() _unitResultingResolution = ChoiceOptionValue("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on","full"}); _unitResultingResolution.description= "Uses unit resulting resolution only to derive empty clauses (may be useful for splitting)." - " 'ec_only' only derives empty clauses, 'on' does everything (but implements a heuristic to skip deriving more than one empty clause)" - " 'full' ignores this heuristic is thus complete also under AVATAR."; + " 'ec_only' only derives empty clauses, 'on' does everything (but implements a heuristic to skip deriving more than one empty clause)," + " 'full' ignores this heuristic and is thus complete also under AVATAR."; _lookup.insert(&_unitResultingResolution); _unitResultingResolution.tag(OptionTag::INFERENCES); _unitResultingResolution.onlyUsefulWith(ProperSaturationAlgorithm());