diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-25 09:43:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-25 09:43:19 -0500 |
| commit | 18d42bc7f76b5b144ec498d3b4d3e906224e629f (patch) | |
| tree | 739103f85e160de6ba9464d43f52e3d0b47dc555 /src/theory/strings/inference_manager.h | |
| parent | 9ab6fb41bc06883aa7d2071133291aff18466afd (diff) | |
Split infer info data structure in strings (#3107)
Diffstat (limited to 'src/theory/strings/inference_manager.h')
| -rw-r--r-- | src/theory/strings/inference_manager.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 71651f7df..bb78b4a1a 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -24,6 +24,7 @@ #include "context/context.h" #include "expr/node.h" #include "theory/output_channel.h" +#include "theory/strings/infer_info.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -125,16 +126,22 @@ class InferenceManager * If the flag asLemma is true, then this method will send a lemma instead * of an inference whenever applicable. */ - void sendInference(std::vector<Node>& exp, - std::vector<Node>& exp_n, + 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(std::vector<Node>& exp, + void sendInference(const std::vector<Node>& exp, Node eq, const char* c, bool asLemma = false); + /** Send inference + * + * Makes the appropriate call to send inference based on the infer info + * data structure (see sendInference documentation above). + */ + void sendInference(const InferInfo& i); /** Send split * * This requests that ( a = b V a != b ) is sent on the output channel as a |