make PrecedenceOrdering more robust for sp=frequency (usageCounts are…

… updated via getProperty, although not stored there!); and initialize _unitUsageCount, because it is nice
vprover · Mar 26, 2020 · 2a17f46 · 2a17f46
1 parent 3ea5e22
commit 2a17f46
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp
@@ -650,6 +650,10 @@ PrecedenceOrdering::PrecedenceOrdering(Problem& prb, const Options& opt)
   CALL("PrecedenceOrdering::PrecedenceOrdering");
   ASS_G(_predicates, 0);
 
+  // Make sure we (re-)compute usageCnt's for all the symbols;
+  // in particular, the sP's (the Tseitin predicates) and sK's (the Skolem functions), which only exists since preprocessing.
+  prb.getProperty();
+
   DArray<unsigned> aux(32);
   if(_functions) {
     aux.initFromIterator(getRangeIterator(0u, _functions), _functions);

diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
@@ -57,6 +57,7 @@ Signature::Symbol::Symbol(const vstring& nm,unsigned arity, bool interpreted, bo
     _type(0),
     _distinctGroups(0),
     _usageCount(0),
+    _unitUsageCount(0),
     _inGoal(0),
     _inUnit(0),
     _inductionSkolem(0),