diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 19:00:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-06 19:00:13 -0500 |
commit | fab7010523fd2e635c2c9dfd382acdefdb96d6b4 (patch) | |
tree | d69370211e672c9d32534a39d01d6108c24e2261 /src/theory/strings/inference_manager.h | |
parent | 45e489e2d48e3edde15be2187e32893fc35d859b (diff) |
Enum for all remaining string inferences (#4220)
Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.
Diffstat (limited to 'src/theory/strings/inference_manager.h')
-rw-r--r-- | src/theory/strings/inference_manager.h | 54 |
1 files changed, 15 insertions, 39 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 2a361aa44..af1f28a23 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -92,15 +92,17 @@ class InferenceManager * sendInference below in that it does not introduce any new non-constant * terms to the state. * - * The argument c is a string identifying the reason for the inference. - * This string is used for debugging purposes. + * The argument infer identifies the reason for the inference. + * This is used for debugging and statistics purposes. * * Return true if the inference is complete, in the sense that we infer * inferences that are equivalent to conc. This returns false e.g. if conc * (or one of its conjuncts if it is a conjunction) was not inferred due * to the criteria mentioned above. */ - bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c); + bool sendInternalInference(std::vector<Node>& exp, + Node conc, + Inference infer); /** send inference * * This function should be called when ( exp ^ exp_n ) => eq. The set exp @@ -127,8 +129,9 @@ class InferenceManager * exp_n is empty. In particular, lemmas must be used whenever exp_n is * non-empty, conflicts are used when exp_n is empty and eq is false. * - * The argument c is a string identifying the reason for inference, used for - * debugging. + * The argument infer identifies the reason for inference, used for + * debugging. This updates the statistics about the number of inferences made + * of each type. * * If the flag asLemma is true, then this method will send a lemma instead * of an inference whenever applicable. @@ -136,30 +139,9 @@ class InferenceManager void sendInference(const std::vector<Node>& exp, const std::vector<Node>& exp_n, Node eq, - const char* c, - bool asLemma = false); - /** same as above, but where exp_n is empty */ - void sendInference(const std::vector<Node>& exp, - 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. - */ + /** same as above, but where exp_n is empty */ void sendInference(const std::vector<Node>& exp, Node eq, Inference infer, @@ -177,19 +159,13 @@ class InferenceManager * lemma. We additionally request a phase requirement for the equality a=b * with polarity preq. * - * The argument c is a string identifying the reason for inference, used for - * debugging. + * The argument infer identifies the reason for inference, used for + * debugging. This updates the statistics about the number of + * inferences made of each type. * * This method returns true if the split was non-trivial, and false * otherwise. A split is trivial if a=b rewrites to a constant. */ - bool sendSplit(Node a, Node b, const char* c, bool preq = true); - - /** - * The same as `sendSplit()` above but with an `Inference` instead of a - * string. This variant updates the statistics about the number of - * inferences made of each type. - */ bool sendSplit(Node a, Node b, Inference infer, bool preq = true); /** Send phase requirement @@ -339,17 +315,17 @@ class InferenceManager * above lemma to the lemma cache d_pending_lem, which may be flushed * later within the current call to TheoryStrings::check. * - * The argument c is a string identifying the reason for inference, used for + * The argument infer identifies the reason for inference, used for * debugging. */ - void sendLemma(Node ant, Node conc, const char* c); + void sendLemma(Node ant, Node conc, Inference infer); /** * Indicates that conc should be added to the equality engine of this class * with explanation eq_exp. It must be the case that eq_exp is a (conjunction * of) literals that each are explainable, i.e. they already hold in the * equality engine of this class. */ - void sendInfer(Node eq_exp, Node eq, const char* c); + void sendInfer(Node eq_exp, Node eq, Inference infer); /** * Get the lemma required for registering the length information for * atomic term n given length status s. For details, see registerTermAtomic. |