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.

3 files changed, 4 insertions, 12 deletions

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;