Improve accuracy of resource limitation (#4763)

The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime

It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.

Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.

11 files changed, 296 insertions, 27 deletions

diff --git a/contrib/learn_resource_weights.py b/contrib/learn_resource_weights.py
new file mode 100755
index 000000000..8f5213ec2
--- /dev/null
+++ b/contrib/learn_resource_weights.py
@@ -0,0 +1,188 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import gzip
+import json
+import logging
+import re
+from sklearn import linear_model
+import statistics
+
+
+def parse_commandline():
+    """Parse commandline arguments"""
+    epilog = """
+This script can be used to compute good resource weights based on benchmark
+results. The resource weights are used by cvc4 to approximate the running time
+by the spent resources, multiplied with their weights.
+
+In the first stage ("parse") this script reads the output files of a benchmark
+run as generated on our cluster. The output files are expected to be named
+"*.smt2/output.log" and should contain the statistics (by use of "--stats").
+The result is a gziped json file that contains all the relevant information
+in a compact form.
+
+In the second stage ("analyze") this script loads the gziped json file and uses
+a linear regression model to learn resource weights. The resulting weights can
+be used as constants for the resource options ("--*-step=n"). Additionally,
+this script performs some analysis on the results to identify outliers where
+the linear model performs particularly bad, i.e., the runtime estimation is way
+off.
+    """
+    usage = """
+    first stage to parse the solver output:
+    %(prog)s parse <output directory>
+    
+    second stage to learn resource weights:
+    %(prog)s analyze
+    """
+    parser = argparse.ArgumentParser(description='export and analyze resources from statistics',
+                                     formatter_class=argparse.ArgumentDefaultsHelpFormatter,
+                                     epilog=epilog,
+                                     usage=usage)
+    parser.add_argument('command', choices=[
+                        'parse', 'analyze'], help='task to perform')
+    parser.add_argument('basedir', default=None, nargs='?',
+                        help='path of benchmark results')
+    parser.add_argument('-v', '--verbose',
+                        action='store_true', help='be more verbose')
+    parser.add_argument('--json', default='data.json.gz',
+                        help='path of json file')
+    parser.add_argument('--threshold', metavar='SEC', type=int, default=1,
+                        help='ignore benchmarks with a runtime below this threshold')
+    parser.add_argument('--mult', type=int, default=1000,
+                        help='multiply running times with this factor for regression')
+
+    return parser.parse_args()
+
+
+def load_zipped_json(filename):
+    """Load data from a gziped json file"""
+    with gzip.GzipFile(args.json, 'r') as fin:
+        return json.loads(fin.read().decode('utf-8'))
+
+
+def save_zipped_json(filename, data):
+    """Store data to a gziped json file"""
+    with gzip.GzipFile(args.json, 'w') as fout:
+        fout.write(json.dumps(data).encode('utf-8'))
+
+
+def get_sorted_values(data):
+    """Transform [['name', value], ...] to [value, ...] sorted by names"""
+    return [d[1] for d in sorted(data)]
+
+
+def parse(args):
+    if args.basedir is None:
+        raise Exception('Specify basedir for parsing!')
+    filename_re = re.compile('(.*\\.smt2)/output\\.log')
+    resource_re = re.compile('resource::([^,]+), ([0-9]+)')
+    result_re = re.compile('driver::sat/unsat, ([a-z]+)')
+    totaltime_re = re.compile('driver::totalTime, ([0-9\\.]+)')
+
+    logging.info('Parsing files from {}'.format(args.basedir))
+    data = {}
+    failed = 0
+    for file in glob.iglob('{}/**/output.log'.format(args.basedir), recursive=True):
+        content = open(file).read()
+        try:
+            filename = filename_re.match(file).group(1)
+            r = resource_re.findall(content)
+            r = list(map(lambda x: (x[0], int(x[1])), r))
+            data[filename] = {
+                'resources': r,
+                'result': result_re.search(content).group(1),
+                'time': float(totaltime_re.search(content).group(1)),
+            }
+        except Exception as e:
+            logging.debug('Failed to parse {}: {}'.format(file, e))
+            failed += 1
+
+    if failed > 0:
+        logging.info('Failed to parse {} out of {} files'.format(
+            failed, failed + len(data)))
+    logging.info('Dumping data to {}'.format(args.json))
+    save_zipped_json(args.json, data)
+
+
+def analyze(args):
+    logging.info('Loading data from {}'.format(args.json))
+    data = load_zipped_json(args.json)
+
+    logging.info('Extracting resources')
+    resources = set()
+    for f in data:
+        for r in data[f]['resources']:
+            resources.add(r[0])
+    resources = list(sorted(resources))
+
+    vals = {r: [] for r in resources}
+
+    logging.info('Collecting data from {} benchmarks'.format(len(data)))
+    x = []
+    y = []
+    for filename in data:
+        d = data[filename]
+        if d['time'] < args.threshold:
+            continue
+        x.append(get_sorted_values(d['resources']))
+        y.append(d['time'] * args.mult)
+
+        for r in d['resources']:
+            vals[r[0]].append(r[1])
+
+    logging.info('Training regression model')
+    clf = linear_model.LinearRegression()
+    r = clf.fit(x, y)
+    coeffs = zip(resources, r.coef_)
+    for c in sorted(coeffs, key=lambda c: c[1]):
+        minval = min(vals[c[0]])
+        maxval = max(vals[c[0]])
+        avgval = statistics.mean(vals[c[0]])
+        medval = statistics.median(vals[c[0]])
+        impact = c[1] * avgval
+        logging.info('{:23}-> {:15.10f}\t({} .. {:10}, avg {:9.2f}, med {:8}, impact {:7.3f})'.format(
+            *c, minval, maxval, avgval, medval, impact))
+
+    logging.info('Comparing regression model with reality')
+    outliers = {
+        'over-estimated': [],
+        'under-estimated': []
+    }
+    for filename in data:
+        d = data[filename]
+        actual = d['time']
+        if actual < args.threshold:
+            continue
+        vals = get_sorted_values(d['resources'])
+        predict = float(r.predict([vals])) / args.mult
+        outliers['over-estimated'].append([predict / actual, predict, actual, filename])
+        outliers['under-estimated'].append([actual / predict, predict, actual, filename])
+
+    for out in outliers:
+        logging.info('Showing outliers for {}'.format(out))
+        filtered = outliers[out]
+        for vals in sorted(filtered)[-5:]:
+            logging.info(
+                '  -> {:6.2f} ({:6.2f}, actual {:6.2f}): {}'.format(*vals))
+
+    cur = 0
+    gnuplot = open('plot.data', 'w')
+    for out in sorted(outliers['under-estimated']):
+        gnuplot.write('{}\t{}\n'.format(cur, out[0]))
+        cur += 1
+
+
+if __name__ == "__main__":
+    logging.basicConfig(format='[%(levelname)s] %(message)s')
+    args = parse_commandline()
+    if args.verbose:
+        logging.getLogger().setLevel(level=logging.DEBUG)
+    else:
+        logging.getLogger().setLevel(level=logging.INFO)
+    if args.command == 'parse':
+        parse(args)
+    elif args.command == 'analyze':
+        analyze(args)
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 55ba43ce9..405abfc4f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -497,6 +497,24 @@ header = "options/smt_options.h"
   help       = "enable resource limiting per query"
 
 [[option]]
+  name       = "arithPivotStep"
+  category   = "expert"
+  long       = "arith-pivot-step=N"
+  type       = "unsigned"
+  default    = "1"
+  read_only  = true
+  help       = "amount of resources spent for each arithmetic pivot step"
+
+[[option]]
+  name       = "arithNlLemmaStep"
+  category   = "expert"
+  long       = "arith-nl-lemma-step=N"
+  type       = "unsigned"
+  default    = "1"
+  read_only  = true
+  help       = "amount of resources spent for each arithmetic nonlinear lemma step"
+
+[[option]]
   name       = "rewriteStep"
   category   = "expert"
   long       = "rewrite-step=N"
@@ -569,6 +587,15 @@ header = "options/smt_options.h"
   help       = "amount of resources spent when adding lemmas"
 
 [[option]]
+  name       = "newSkolemStep"
+  category   = "expert"
+  long       = "new-skolem-step=N"
+  type       = "unsigned"
+  default    = "1"
+  read_only  = true
+  help       = "amount of resources spent when adding new skolems"
+
+[[option]]
   name       = "restartStep"
   category   = "expert"
   long       = "restart-step=N"
@@ -623,6 +650,24 @@ header = "options/smt_options.h"
   help       = "amount of resources spent for each sat conflict (bitvectors)"
 
 [[option]]
+  name       = "bvSatPropagateStep"
+  category   = "expert"
+  long       = "bv-sat-propagate-step=N"
+  type       = "unsigned"
+  default    = "1"
+  read_only  = true
+  help       = "amount of resources spent for each sat propagate (bitvectors)"
+
+[[option]]
+  name       = "bvSatSimplifyStep"
+  category   = "expert"
+  long       = "bv-sat-simplify-step=N"
+  type       = "unsigned"
+  default    = "1"
+  read_only  = true
+  help       = "amount of resources spent for each sat simplify (bitvectors)"
+
+[[option]]
   name       = "forceNoLimitCpuWhileDump"
   category   = "regular"
   long       = "force-no-limit-cpu-while-dump"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index f7ba14acd..704ea0e20 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -886,6 +886,8 @@ bool Solver::simplify()
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
         return true;
 
+    d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
+
     // Remove satisfied clauses:
     removeSatisfied(learnts);
     if (remove_satisfied)        // Can be turned off.
@@ -922,6 +924,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
     starts++;
 
     for (;;){
+        d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
         CRef confl = propagate();
         if (confl != CRef_Undef){
             // CONFLICT
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 8936fb584..7dcd3f910 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -54,7 +54,6 @@ CnfStream::CnfStream(SatSolver* satSolver,
       d_nodeToLiteralMap(context),
       d_literalToNodeMap(context),
       d_fullLitToNodeMap(fullLitToNodeMap),
-      d_convertAndAssertCounter(0),
       d_registrar(registrar),
       d_name(name),
       d_cnfProof(nullptr),
@@ -744,11 +743,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   Trace("cnf") << "convertAndAssert(" << node
                << ", negated = " << (negated ? "true" : "false") << ")\n";
 
-  if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
-    d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
-    d_convertAndAssertCounter = 0;
-  }
-  ++d_convertAndAssertCounter;
+  d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
 
   switch(node.getKind()) {
     case kind::AND: convertAndAssertAnd(node, negated); break;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index dd7fbc15f..74ead0d22 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -202,12 +202,6 @@ class CnfStream {
    */
   const bool d_fullLitToNodeMap;
 
-  /**
-   * Counter for resource limiting that is used to spend a resource
-   * every ResourceManager::resourceCounter calls to convertAndAssert.
-   */
-  unsigned long d_convertAndAssertCounter;
-
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
 
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 5bd02cf19..22a69cadb 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -161,6 +161,8 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
   for (const NlLemma& lem : lemmas)
   {
     sum += filterLemma(lem, out);
+    d_containing.getOutputChannel().spendResource(
+        ResourceManager::Resource::ArithNlLemmaStep);
   }
   lemmas.clear();
   return sum;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e4fa4a82c..ac9ec7e77 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3479,6 +3479,13 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   }
   d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
 
+  size_t nPivots = options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
+  for (std::size_t i = 0; i < d_fcSimplex.getPivots(); ++i)
+  {
+    d_containing.d_out->spendResource(
+        ResourceManager::Resource::ArithPivotStep);
+  }
+
   Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
                       << "pre approx cuts" << endl;
   if(!d_approxCuts.empty()){
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 7ebacee92..3a4941328 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -219,11 +219,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
   }
   // Rewrite until the stack is empty
   for (;;){
-
-    if (hasSmtEngine &&
-		d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
+    if (hasSmtEngine)
+    {
       rm->spendResource(ResourceManager::Resource::RewriteStep);
-      d_iterationCount = 0;
     }
 
     // Get the top of the recursion stack
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e36426a81..572662483 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -201,8 +201,6 @@ class Rewriter {
   /** Theory rewriters used by this rewriter instance */
   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 
-  unsigned long d_iterationCount = 0;
-
   /** Rewriter table for prewrites. Maps kinds to rewriter function. */
   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
       d_preRewriters[kind::LAST_KIND];
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index f85e06b12..9afa79ef0 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -66,13 +66,18 @@ struct ResourceManager::Statistics
 {
   ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
   IntStat d_spendResourceCalls;
+  IntStat d_numArithPivotStep;
+  IntStat d_numArithNlLemmaStep;
   IntStat d_numBitblastStep;
   IntStat d_numBvEagerAssertStep;
   IntStat d_numBvPropagationStep;
   IntStat d_numBvSatConflictsStep;
+  IntStat d_numBvSatPropagateStep;
+  IntStat d_numBvSatSimplifyStep;
   IntStat d_numCnfStep;
   IntStat d_numDecisionStep;
   IntStat d_numLemmaStep;
+  IntStat d_numNewSkolemStep;
   IntStat d_numParseStep;
   IntStat d_numPreprocessStep;
   IntStat d_numQuantifierStep;
@@ -90,13 +95,18 @@ struct ResourceManager::Statistics
 ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
     : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
       d_spendResourceCalls("resource::spendResourceCalls", 0),
+      d_numArithPivotStep("resource::ArithPivotStep", 0),
+      d_numArithNlLemmaStep("resource::ArithNlLemmaStep", 0),
       d_numBitblastStep("resource::BitblastStep", 0),
       d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
       d_numBvPropagationStep("resource::BvPropagationStep", 0),
       d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
+      d_numBvSatPropagateStep("resource::BvSatPropagateStep", 0),
+      d_numBvSatSimplifyStep("resource::BvSatSimplifyStep", 0),
       d_numCnfStep("resource::CnfStep", 0),
       d_numDecisionStep("resource::DecisionStep", 0),
       d_numLemmaStep("resource::LemmaStep", 0),
+      d_numNewSkolemStep("resource::NewSkolemStep", 0),
       d_numParseStep("resource::ParseStep", 0),
       d_numPreprocessStep("resource::PreprocessStep", 0),
       d_numQuantifierStep("resource::QuantifierStep", 0),
@@ -108,13 +118,18 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
 {
   d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
   d_statisticsRegistry.registerStat(&d_spendResourceCalls);
+  d_statisticsRegistry.registerStat(&d_numArithPivotStep);
+  d_statisticsRegistry.registerStat(&d_numArithNlLemmaStep);
   d_statisticsRegistry.registerStat(&d_numBitblastStep);
   d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
   d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
   d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.registerStat(&d_numBvSatPropagateStep);
+  d_statisticsRegistry.registerStat(&d_numBvSatSimplifyStep);
   d_statisticsRegistry.registerStat(&d_numCnfStep);
   d_statisticsRegistry.registerStat(&d_numDecisionStep);
   d_statisticsRegistry.registerStat(&d_numLemmaStep);
+  d_statisticsRegistry.registerStat(&d_numNewSkolemStep);
   d_statisticsRegistry.registerStat(&d_numParseStep);
   d_statisticsRegistry.registerStat(&d_numPreprocessStep);
   d_statisticsRegistry.registerStat(&d_numQuantifierStep);
@@ -128,13 +143,18 @@ ResourceManager::Statistics::~Statistics()
 {
   d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
   d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
+  d_statisticsRegistry.unregisterStat(&d_numArithPivotStep);
+  d_statisticsRegistry.unregisterStat(&d_numArithNlLemmaStep);
   d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
   d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
   d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
   d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvSatPropagateStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvSatSimplifyStep);
   d_statisticsRegistry.unregisterStat(&d_numCnfStep);
   d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
   d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
+  d_statisticsRegistry.unregisterStat(&d_numNewSkolemStep);
   d_statisticsRegistry.unregisterStat(&d_numParseStep);
   d_statisticsRegistry.unregisterStat(&d_numPreprocessStep);
   d_statisticsRegistry.unregisterStat(&d_numQuantifierStep);
@@ -146,8 +166,6 @@ ResourceManager::Statistics::~Statistics()
 
 /*---------------------------------------------------------------------------*/
 
-const uint64_t ResourceManager::s_resourceCount = 1000;
-
 ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
     : d_perCallTimer(),
       d_timeBudgetPerCall(0),
@@ -219,7 +237,8 @@ void ResourceManager::spendResource(unsigned amount)
   if (out())
   {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
-    Trace("limit") << "          on call " << d_statistics->d_spendResourceCalls.getData() << std::endl;
+    Trace("limit") << "          on call "
+                   << d_statistics->d_spendResourceCalls.getData() << std::endl;
     if (outOfTime())
     {
       Trace("limit") << "ResourceManager::spendResource: elapsed time"
@@ -238,6 +257,14 @@ void ResourceManager::spendResource(Resource r)
   uint32_t amount = 0;
   switch (r)
   {
+    case Resource::ArithPivotStep:
+      amount = d_options[options::arithPivotStep];
+      ++d_statistics->d_numArithPivotStep;
+      break;
+    case Resource::ArithNlLemmaStep:
+      amount = d_options[options::arithNlLemmaStep];
+      ++d_statistics->d_numArithNlLemmaStep;
+      break;
     case Resource::BitblastStep:
       amount = d_options[options::bitblastStep];
       ++d_statistics->d_numBitblastStep;
@@ -254,6 +281,14 @@ void ResourceManager::spendResource(Resource r)
       amount = d_options[options::bvSatConflictStep];
       ++d_statistics->d_numBvSatConflictsStep;
       break;
+    case Resource::BvSatPropagateStep:
+      amount = d_options[options::bvSatPropagateStep];
+      ++d_statistics->d_numBvSatPropagateStep;
+      break;
+    case Resource::BvSatSimplifyStep:
+      amount = d_options[options::bvSatSimplifyStep];
+      ++d_statistics->d_numBvSatSimplifyStep;
+      break;
     case Resource::CnfStep:
       amount = d_options[options::cnfStep];
       ++d_statistics->d_numCnfStep;
@@ -266,6 +301,10 @@ void ResourceManager::spendResource(Resource r)
       amount = d_options[options::lemmaStep];
       ++d_statistics->d_numLemmaStep;
       break;
+    case Resource::NewSkolemStep:
+      amount = d_options[options::newSkolemStep];
+      ++d_statistics->d_numNewSkolemStep;
+      break;
     case Resource::ParseStep:
       amount = d_options[options::parseStep];
       ++d_statistics->d_numParseStep;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index e67598afc..f6cff2e7f 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -10,7 +10,7 @@
  ** directory for licensing information.\endverbatim
  **
  ** \brief Provides mechanisms to limit resources.
-  **
+ **
  ** This file provides the ResourceManager class. It can be used to impose
  ** (cumulative and per-call) resource limits on the solver, as well as per-call
  ** time limits.
@@ -81,13 +81,18 @@ class CVC4_PUBLIC ResourceManager
   /** Types of resources. */
   enum class Resource
   {
+    ArithPivotStep,
+    ArithNlLemmaStep,
     BitblastStep,
     BvEagerAssertStep,
     BvPropagationStep,
     BvSatConflictsStep,
+    BvSatPropagateStep,
+    BvSatSimplifyStep,
     CnfStep,
     DecisionStep,
     LemmaStep,
+    NewSkolemStep,
     ParseStep,
     PreprocessStep,
     QuantifierStep,
@@ -159,8 +164,6 @@ class CVC4_PUBLIC ResourceManager
    */
   void endCall();
 
-  static uint64_t getFrequencyCount() { return s_resourceCount; }
-
   /**
    * Registers a listener that is notified on a resource out or (per-call)
    * timeout.
@@ -195,9 +198,6 @@ class CVC4_PUBLIC ResourceManager
   /** A flag indicating whether resource limitation is active. */
   bool d_on;
 
-  /** Counter indicating how often to check resource manager in loops */
-  static const uint64_t s_resourceCount;
-
   /** Receives a notification on reaching a limit. */
   std::vector<Listener*> d_listeners;