summaryrefslogtreecommitdiff
path: root/src/theory/strings/inference_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/inference_manager.h')
-rw-r--r--src/theory/strings/inference_manager.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index e052889f6..b63f7ea71 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -163,6 +163,9 @@ class InferenceManager
* decided with polarity pol.
*/
void sendPhaseRequirement(Node lit, bool pol);
+
+ Node reqLengthGeqOne(Node n);
+
/** register length
*
* This method is called on non-constant string terms n. It sends a lemma
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback