Merge pull request #507 from vprover/martin-fix-urr

fix URR to be (really) complete also under AVATAR

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;
       }
     }

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;

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());

Shell/Options.cpp

@@ -1658,13 +1658,16 @@ void Options::init()
     _equationalTautologyRemoval.onlyUsefulWith(ProperSaturationAlgorithm());
     _equationalTautologyRemoval.tag(OptionTag::INFERENCES);
 
-    _unitResultingResolution = ChoiceOptionValue<URResolution>("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on"});
+    _unitResultingResolution = ChoiceOptionValue<URResolution>("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 and 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) {

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 {

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

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

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