diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-26 09:52:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-26 09:52:28 -0500 |
commit | c9fd28a391cfff767b899a65ad365742745910fe (patch) | |
tree | 663ffc3b744c9df9de3781aaf292fa6b79851fdc /src/theory/strings/inference_manager.h | |
parent | 9523b4248da9764fa14f078659b42085a7fe2654 (diff) |
Add stats for string reductions, lemmas and conflicts (#4149)
This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).
Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
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; |