diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-06 17:12:29 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-06 15:12:29 -0800 |
| commit | cbd86eb4ed8bafc17f28244b746a376a019462f1 (patch) | |
| tree | 69abc6102e61036f9e60c8276f350d68eaecb931 /src/theory/strings/infer_info.h | |
| parent | bef9df667e2788cab327b0c8c6590ba833297670 (diff) | |
Move more string utility functions (#3398)
This is work towards splitting a "core solver" object from TheoryStrings.
This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.
It also corrects an issue where we were maintaining two `d_conflict` fields.
Diffstat (limited to 'src/theory/strings/infer_info.h')
| -rw-r--r-- | src/theory/strings/infer_info.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 745a499d3..0f0329e61 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -87,6 +87,9 @@ std::ostream& operator<<(std::ostream& out, Inference i); */ enum LengthStatus { + // The length of the Skolem should not be constrained. This should be + // used for Skolems whose length is already implied. + LENGTH_IGNORE, // The length of the Skolem is not specified, and should be split on. LENGTH_SPLIT, // The length of the Skolem is exactly one. |