diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-22 21:05:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-22 21:05:37 -0700 |
commit | c9b7c3d6fcd49b6d75a85e1316e9918374d1ebbe (patch) | |
tree | 481ebcabeb01c576c5ae51269275ecd7ade9d4f3 /src/theory/strings/inference_manager.h | |
parent | c98ba7775ecb8a192e2a93735885163234546be3 (diff) |
Collect statistics about normal form inferences (#4127)
This commit adds code to count the number of inferences made of each
inference type for normal form inferences. It extends the Inference
enum in `infer_info.h` and adds two new `sendInference()` methods in the
`InferenceManager` to send and count inferences that have a corresonding
entry in the `Inference` enum.
Diffstat (limited to 'src/theory/strings/inference_manager.h')
-rw-r--r-- | src/theory/strings/inference_manager.h | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 50cfdb6fb..c9d483c73 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" +#include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" #include "theory/uf/equality_engine.h" @@ -76,7 +77,8 @@ class InferenceManager context::UserContext* u, SolverState& s, SkolemCache& skc, - OutputChannel& out); + OutputChannel& out, + SequencesStatistics& statistics); ~InferenceManager() {} /** send internal inferences @@ -141,6 +143,28 @@ class InferenceManager Node eq, const char* c, bool asLemma = false); + + /** + * The same as `sendInference()` above but with an `Inference` instead of a + * string. This variant updates the statistics about the number of inferences + * made of each type. + */ + void sendInference(const std::vector<Node>& exp, + const std::vector<Node>& exp_n, + Node eq, + Inference infer, + bool asLemma = false); + + /** + * The same as `sendInference()` above but with an `Inference` instead of a + * string. This variant updates the statistics about the number of inferences + * made of each type. + */ + void sendInference(const std::vector<Node>& exp, + Node eq, + Inference infer, + bool asLemma = false); + /** Send inference * * Makes the appropriate call to send inference based on the infer info @@ -327,6 +351,10 @@ class InferenceManager * This is a reference to the output channel of the theory of strings. */ OutputChannel& d_out; + + /** Reference to the statistics for the theory of strings/sequences. */ + SequencesStatistics& d_statistics; + /** Common constants */ Node d_emptyString; Node d_true; @@ -366,6 +394,7 @@ class InferenceManager NodeNodeMap d_proxyVarToLength; /** List of terms that we have register length for */ NodeSet d_lengthLemmaTermsCache; + /** infer substitution proxy vars * * This method attempts to (partially) convert the formula n into a |