diff options
Diffstat (limited to 'src/theory/strings/inference_manager.h')
-rw-r--r-- | src/theory/strings/inference_manager.h | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index e052889f6..819e4b98f 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -61,7 +61,8 @@ class TheoryStrings; * to doPendingLemmas. * * It also manages other kinds of interaction with the output channel of the - * theory of strings, e.g. sendPhaseRequirement. + * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and + * with the extended theory object e.g. markCongruent. */ class InferenceManager { @@ -249,6 +250,19 @@ class InferenceManager * the node corresponding to their conjunction. */ void explain(TNode literal, std::vector<TNode>& assumptions) const; + /** + * Set that we are incomplete for the current set of assertions (in other + * words, we must answer "unknown" instead of "sat"); this calls the output + * channel's setIncomplete method. + */ + void setIncomplete(); + /** + * Mark that terms a and b are congruent in the current context. + * This makes a call to markCongruent in the extended theory object of + * the parent theory if the kind of a (and b) is owned by the extended + * theory. + */ + void markCongruent(Node a, Node b); private: /** |