change List::destroy() to static function to allow calls on empty lists

ModelWriter · Sep 29, 2017 · 3969e86 · 3969e86
1 parent 7a97d34
commit 3969e86
Show file tree

Hide file tree

Showing 36 changed files with 65 additions and 71 deletions.
diff --git a/CASC/CLTBMode.cpp b/CASC/CLTBMode.cpp
@@ -301,10 +301,9 @@ void CLTBMode::learnFromSolutionFile(vstring& solnFileName)
       UnitList* units = parser.units();
       UnitList::Iterator it(units);
       while (it.hasNext()) {
-        Unit* unit = it.next();
-        unit->destroy();
+        it.next()->destroy();
       }
-      units->destroy();
+      UnitList::destroy(units);
     }
 
     UnitList::DelIterator it(solnUnits);

diff --git a/Indexing/ClauseVariantIndex.cpp b/Indexing/ClauseVariantIndex.cpp
@@ -78,7 +78,7 @@ class ClauseVariantIndex::ResultClauseToVariantClauseFn
 
   fin:
     for(unsigned i=0;i<_length;i++) {
-      alts[i]->destroy();
+      LiteralList::destroy(alts[i]);
     }
 
     if(fail) {
@@ -149,11 +149,11 @@ SubstitutionTreeClauseVariantIndex::~SubstitutionTreeClauseVariantIndex()
     }
   }
 
-  _emptyClauses->destroy();
+  ClauseList::destroy(_emptyClauses);
 
   DHMap<Literal*, ClauseList*>::Iterator it(_groundUnits);
   while (it.hasNext()) {
-    it.next()->destroy();
+    ClauseList::destroy(it.next());
   }
 }
 
@@ -229,7 +229,7 @@ HashingClauseVariantIndex::~HashingClauseVariantIndex()
 //      maxval->destroy();
 //      maxval = lst;
 //    } else {
-      lst->destroy();
+    ClauseList::destroy(lst);
 //    }
   }
 

diff --git a/Indexing/SubstitutionTree_Nodes.cpp b/Indexing/SubstitutionTree_Nodes.cpp
@@ -26,9 +26,7 @@ class SubstitutionTree::UListLeaf
   UListLeaf(TermList ts) : Leaf(ts), _children(0), _size(0) {}
   ~UListLeaf()
   {
-    if(_children) {
-      _children->destroy();
-    }
+    LDList::destroy(_children);
   }
 
   inline

diff --git a/Inferences/BackwardSubsumptionResolution.cpp b/Inferences/BackwardSubsumptionResolution.cpp
@@ -260,7 +260,7 @@ void BackwardSubsumptionResolution::perform(Clause* cl,
 
   match_fail:
     for(unsigned bi=0; bi<clen; bi++) {
-      matchedLits[bi]->destroy();
+      LiteralList::destroy(matchedLits[bi]);
       matchedLits[bi]=0;
     }
   }
@@ -406,7 +406,7 @@ void BackwardSubsumptionResolution::perform(Clause* cl,
 
   match_fail2:
     for(unsigned bi=0; bi<clen; bi++) {
-      matchedLits[bi]->destroy();
+      LiteralList::destroy(matchedLits[bi]);
       matchedLits[bi]=0;
     }
   }

diff --git a/Inferences/Condensation.cpp b/Inferences/Condensation.cpp
@@ -118,7 +118,7 @@ Clause* Condensation::simplify(Clause* cl)
     // We will jump here if we do not find a match, in this case success will be false
     match_fin:
       for(unsigned i=0;i<newLen;i++) {
-	alts[i]->destroy();
+        LiteralList::destroy(alts[i]);
       }
 
       if(success) {

diff --git a/Inferences/ForwardSubsumptionAndResolution.cpp b/Inferences/ForwardSubsumptionAndResolution.cpp
@@ -81,7 +81,7 @@ struct ClauseMatches {
   {
     unsigned clen=_cl->length();
     for(unsigned i=0;i<clen;i++) {
-      _matches[i]->destroy();
+      LiteralList::destroy(_matches[i]);
     }
     DEALLOC_KNOWN(_matches, clen*sizeof(void*), "Inferences::ClauseMatches");
   }
@@ -366,11 +366,12 @@ bool ForwardSubsumptionAndResolution::perform(Clause* cl, Clause*& replacement,
 	if(checkForSubsumptionResolution(cl, cms, resLit) && ColorHelper::compatible(cl->color(), cms->_cl->color())) {
 	  resolutionClause=generateSubsumptionResolutionClause(cl,resLit,cms->_cl);
 	  env.statistics->forwardSubsumptionResolution++;
-    premises = pvi( getSingletonIterator(cms->_cl) );
-    replacement = resolutionClause;
-    result = true;
+          premises = pvi( getSingletonIterator(cms->_cl) );
+          replacement = resolutionClause;
+          result = true;
 	  goto fin;
 	}
+
       }
     }
   }

diff --git a/Inferences/SLQueryBackwardSubsumption.cpp b/Inferences/SLQueryBackwardSubsumption.cpp
@@ -261,7 +261,7 @@ void SLQueryBackwardSubsumption::perform(Clause* cl,
 
   match_fail:
     for(unsigned bi=0; bi<clen; bi++) {
-      matchedLits[bi]->destroy();
+      LiteralList::destroy(matchedLits[bi]);
       matchedLits[bi]=0;
     }
   }
@@ -270,7 +270,7 @@ void SLQueryBackwardSubsumption::perform(Clause* cl,
   if(subsumed) {
     simplifications=getPersistentIterator(
 	    getMappingIterator(ClauseList::Iterator(subsumed), ClauseToBwSimplRecordFn()));
-    subsumed->destroy();
+    ClauseList::destroy(subsumed);
   }
   return;
 }

diff --git a/Kernel/BestLiteralSelector.hpp b/Kernel/BestLiteralSelector.hpp
@@ -216,7 +216,7 @@ class CompleteBestLiteralSelector
       }
       c->setSelected(1);
     }
-    maximals->destroy();
+    LiteralList::destroy(maximals);
 
     ensureSomeColoredSelected(c, eligible);
   }

diff --git a/Kernel/ELiteralSelector.cpp b/Kernel/ELiteralSelector.cpp
@@ -143,7 +143,7 @@ void ELiteralSelector::doSelection(Clause* c, unsigned eligible)
   }
 
   if(singleSel) {
-    sel->destroy();
+    LiteralList::destroy(sel);
     sel = LiteralList::empty();
     LiteralList::push(singleSel,sel);
   } else if (!sel) {

diff --git a/Kernel/FormulaTransformer.cpp b/Kernel/FormulaTransformer.cpp
@@ -160,7 +160,7 @@ Formula* FormulaTransformer::applyJunction(Formula* f)
     }
   }
   if(!modified) {
-    resArgs->destroy();
+    FormulaList::destroy(resArgs);
     return f;
   }
   //we want to keep arguments in the same order as the input ones

diff --git a/Kernel/FormulaUnit.cpp b/Kernel/FormulaUnit.cpp
@@ -48,8 +48,8 @@ unsigned FormulaUnit::varCnt()
   Formula::VarList* bv = frm->boundVariables();
 
   unsigned res = fv->length() + bv->length();
-  fv->destroy();
-  bv->destroy();
+  Formula::VarList::destroy(fv);
+  Formula::VarList::destroy(bv);
   return res;
 }
 

diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp
@@ -411,7 +411,7 @@ class InferenceMany
 {
 public:
   InferenceMany(Rule rule,UnitList* premises);
-  virtual ~InferenceMany() { _premises->destroy(); }
+  virtual ~InferenceMany() { UnitList::destroy(_premises); }
 
   virtual void destroy();
   virtual Iterator iterator();

diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp
@@ -802,11 +802,11 @@ struct InferenceStore::TPTPProofPrinter
     ASS(!first);
 
     compStr=getQuantifiedStr(compOnlyVars, compStr, multiple);
-    compOnlyVars->destroy();
+    List<unsigned>::destroy(compOnlyVars);
 
     vstring defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString();
     defStr=getQuantifiedStr(nameVars, defStr);
-    nameVars->destroy();
+    List<unsigned>::destroy(nameVars);
 
     SymbolId nameSymbol = SymbolId(false,nameLit->functor());
     vostringstream originStm;

diff --git a/Kernel/LookaheadLiteralSelector.cpp b/Kernel/LookaheadLiteralSelector.cpp
@@ -310,7 +310,7 @@ void LookaheadLiteralSelector::doSelection(Clause* c, unsigned eligible)
 
 selection_done:
   if(singleSel) {
-    maximals->destroy();
+    LiteralList::destroy(maximals);
     maximals=0;
     LiteralList::push(singleSel,maximals);
   }

diff --git a/Kernel/MLVariant.cpp b/Kernel/MLVariant.cpp
@@ -495,7 +495,7 @@ bool MLVariant::isVariant(Literal* const * cl1Lits, Clause* cl2, bool complement
 
 fin:
   for(unsigned i=0;i<clen;i++) {
-    alts[i]->destroy();
+    LiteralList::destroy(alts[i]);
   }
 
   return !fail;

diff --git a/Kernel/MaximalLiteralSelector.cpp b/Kernel/MaximalLiteralSelector.cpp
@@ -50,7 +50,7 @@ void MaximalLiteralSelector::doSelection(Clause* c, unsigned eligible)
     }
   }
   if(singleSel) {
-    sel->destroy();
+    LiteralList::destroy(sel);
     sel=0;
     LiteralList::push(singleSel,sel);
   }

diff --git a/Kernel/SpassLiteralSelector.cpp b/Kernel/SpassLiteralSelector.cpp
@@ -61,7 +61,7 @@ void SpassLiteralSelector::doSelection(Clause* c, unsigned eligible)
   LiteralList* sel = LiteralList::empty();
 
   if(singleSel) {
-    maximals->destroy();
+    LiteralList::destroy(maximals);
     sel = LiteralList::empty();
     LiteralList::push(singleSel,sel);
   } else if (maximals) {

diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp
@@ -503,7 +503,7 @@ Formula* SubstHelper::applyImpl(Formula* f, Applicator& applicator, bool noShari
 
     Formula* arg = applyImpl<ProcessSpecVars>(f->qarg(), applicator, noSharing);
     if (!varsModified && arg == f->qarg()) {
-      newVars->destroy();
+      Formula::VarList::destroy(newVars);
       return f;
     }
     //TODO compute an updated sorts list

diff --git a/Lib/List.hpp b/Lib/List.hpp
@@ -162,12 +162,12 @@ class List
   } // list::setTail
 
   /** Destroy the list */
-  void destroy ()
+  static void destroy (List *l)
   {
     CALL("List::destroy");
 
-    if (isEmpty(this)) return;
-    List* current = this;
+    if (isEmpty(l)) return;
+    List* current = l;
 
     for (;;) {
       List* next = current->tail();

diff --git a/Lib/MapToLIFO.hpp b/Lib/MapToLIFO.hpp
@@ -39,8 +39,7 @@ class MapToLIFO
     }
     typename InnerMap::Iterator it(_data);
     while(it.hasNext()) {
-      ValList* lst=it.next();
-      lst->destroy();
+      ValList::destroy(it.next());
     }
     _data.reset();
   }
@@ -182,8 +181,7 @@ class MapToLIFO
   {
     typename InnerMap::Iterator it(_data);
     while(it.hasNext()) {
-      ValList* lst=it.next();
-      lst->destroy();
+      ValList::destroy(it.next());
     }
     _data.reset();
   }

diff --git a/Lib/Metaiterators.hpp b/Lib/Metaiterators.hpp
@@ -849,7 +849,7 @@ class PersistentIterator
   ~PersistentIterator()
   {
     if(_items) {
-      _items->destroy();
+      List<T>::destroy(_items);
     }
   }
   inline bool hasNext() { return _items; };
@@ -908,7 +908,7 @@ class UniquePersistentIterator
   ~UniquePersistentIterator()
   {
     if(_items) {
-      _items->destroy();
+      ItemList::destroy(_items);
     }
   }
   inline bool hasNext() { return _items; };

diff --git a/Lib/Sys/Multiprocessing.cpp b/Lib/Sys/Multiprocessing.cpp
@@ -37,9 +37,9 @@ Multiprocessing::Multiprocessing()
 
 Multiprocessing::~Multiprocessing()
 {
-  _preFork->destroy();
-  _postForkParent->destroy();
-  _postForkChild->destroy();
+  VoidFuncList::destroy(_preFork);
+  VoidFuncList::destroy(_postForkParent);
+  VoidFuncList::destroy(_postForkChild);
 }
 
 void Multiprocessing::registerForkHandlers(VoidFunc before, VoidFunc afterParent, VoidFunc afterChild)

diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
@@ -1564,7 +1564,7 @@ bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp)
         res = new JunctionFormula( (fs==FS_AND) ? AND : OR, argLst);
       } else {
         res = argLst->head();
-        argLst->destroy();
+        FormulaList::destroy(argLst);
       }
       _results.push(ParseResult(res));
 

diff --git a/SAT/Preprocess.cpp b/SAT/Preprocess.cpp
@@ -137,7 +137,7 @@ bool Preprocess::filterPureLiterals(unsigned varCnt, SATClauseList*& res)
 
   ASS(SATClauseList::isEmpty(occurences[0]));
   for(unsigned i=1;i<=varCnt;i++) {
-    occurences[i]->destroy();
+    SATClauseList::destroy(occurences[i]);
   }
 
 #if VDEBUG
@@ -178,8 +178,8 @@ void Preprocess::propagateUnits(SATClauseIterator clauses,
       bool oldPolarity;
       if(unitBindings.find(unit.var(), oldPolarity)) {
 	if(oldPolarity!=unit.isPositive()) {
-	  res->destroy();
-	  units->destroy();
+	  SATClauseList::destroy(res);
+          SATClauseList::destroy(units);
 	  resUnits=SATClauseIterator::getEmpty();
 	  resNonUnits=pvi( getSingletonIterator(new(0) SATClause(0, true)) );
 	  return;

diff --git a/SAT/SATInference.hpp b/SAT/SATInference.hpp
@@ -55,7 +55,7 @@ class PropInference : public SATInference
 
   ~PropInference()
   {
-    _premises->destroy();
+    SATClauseList::destroy(_premises);
   }
 
   virtual InfType getType() const { return PROP_INF; }

diff --git a/SAT/TWLSolver.cpp b/SAT/TWLSolver.cpp
@@ -618,9 +618,7 @@ bool TWLSolver::isRedundant(SATLiteral lit, ArraySet& seenVars, SATClauseList*&
     varsSeenHere.insert(clVar);
     SATClause* cl = _assignmentPremises[clVar];
     if(!cl) {
-      if(redundancyPremises) {
-	redundancyPremises->destroy();
-      }
+      SATClauseList::destroy(redundancyPremises);
       return false;
     }
     if(_generateProofs) {

diff --git a/Saturation/Splitter.cpp b/Saturation/Splitter.cpp
@@ -282,7 +282,7 @@ void SplittingBranchSelector::handleSatRefutation()
         Formula* clFla;
         if (cl->size() == 1) {
           clFla = disjuncts->head();
-          disjuncts->destroy();
+          FormulaList::destroy(disjuncts);
         } else {
           clFla = JunctionFormula::generalJunction(OR, disjuncts);
         }
@@ -292,7 +292,7 @@ void SplittingBranchSelector::handleSatRefutation()
 
       if (conj_cnt == 1) {
         interpolant = conjuncts->head();
-        conjuncts->destroy();
+        FormulaList::destroy(conjuncts);
       } else {
         interpolant = JunctionFormula::generalJunction(AND, conjuncts);
       }

diff --git a/Shell/Interpolants.cpp b/Shell/Interpolants.cpp
@@ -84,8 +84,8 @@ struct Interpolants::ItemState
   {
     CALL("ItemState::destroy");
 
-    leftInts->destroy();
-    rightInts->destroy();
+    List<UIPair>::destroy(leftInts);
+    List<UIPair>::destroy(rightInts);
   }
 
   Unit* us() const { return _us; }
@@ -467,12 +467,12 @@ void Interpolants::generateInterpolant(ItemState& st)
 	<<"\ninterpolant "<<interpolant->toString()<<endl<<endl);
   UIPair uip=make_pair(unitFormula, interpolant);
   if(st.inheritedColor==COLOR_LEFT) {
-    st.leftInts->destroy();
+    List<UIPair>::destroy(st.leftInts);
     st.leftInts=0;
     List<UIPair>::push(uip,st.leftInts);
   }
   else if(st.inheritedColor==COLOR_RIGHT) {
-    st.rightInts->destroy();
+    List<UIPair>::destroy(st.rightInts);
     st.rightInts=0;
     List<UIPair>::push(uip,st.rightInts);
   }