diff options
Diffstat (limited to 'src/theory/strings/inference_manager.h')
-rw-r--r-- | src/theory/strings/inference_manager.h | 34 |
1 files changed, 25 insertions, 9 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index c9d483c73..bd2f85d29 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -210,18 +210,23 @@ class InferenceManager * exists, otherwise it returns null. */ Node getProxyVariableFor(Node n) const; - /** register length + /** register term + * + * This method is called on non-constant string terms n. It returns a lemma + * that should be sent on the output channel of theory of strings upon + * registration of this term, or null if no lemma is necessary. * - * This method is called on non-constant string terms n. It sends a lemma - * on the output channel that ensures that the length n satisfies its assigned - * status (given by argument s). + * If n is an atomic term, the method registerTermAtomic is called for n + * and s = LENGTH_SPLIT and no lemma is returned. */ - void registerLength(Node n); + Node registerTerm(Node n); /** register length * - * This method is called on non-constant string terms n. It sends a lemma - * on the output channel that ensures that the length n satisfies its assigned - * status (given by argument s). + * This method is called on non-constant string terms n that are "atomic" + * with respect to length. That is, the rewritten form of len(n) is itself. + * + * It sends a lemma on the output channel that ensures that the length n + * satisfies its assigned status (given by argument s). * * If the status is LENGTH_ONE, we send the lemma len( n ) = 1. * @@ -238,7 +243,7 @@ class InferenceManager * In contrast to the above functions, it makes immediate calls to the output * channel instead of adding them to pending lists. */ - void registerLength(Node n, LengthStatus s); + void registerTermAtomic(Node n, LengthStatus s); //---------------------------- end proxy variables and length elaboration //----------------------------constructing antecedants @@ -337,6 +342,17 @@ class InferenceManager * equality engine of this class. */ void sendInfer(Node eq_exp, Node eq, const char* c); + /** + * Get the lemma required for registering the length information for + * atomic term n given length status s. For details, see registerTermAtomic. + * + * Additionally, this method may map literals to a required polarity in the + * argument reqPhase, which should be processed by a call to requiredPhase by + * the caller of this method. + */ + Node getRegisterTermAtomicLemma(Node n, + LengthStatus s, + std::map<Node, bool>& reqPhase); /** the parent theory of strings object */ TheoryStrings& d_parent; |