summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_rewriter.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/sequences_rewriter.h')
-rw-r--r--src/theory/strings/sequences_rewriter.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 5aba4ab6f..a98ad97ac 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -23,6 +23,7 @@
#include <vector>
#include "expr/attribute.h"
+#include "theory/strings/rewrites.h"
#include "theory/theory_rewriter.h"
#include "theory/type_enumerator.h"
@@ -149,7 +150,7 @@ class SequencesRewriter : public TheoryRewriter
/**
* Called when node rewrites to ret.
*
- * The string c indicates the justification for the rewrite, which is printed
+ * The rewrite r indicates the justification for the rewrite, which is printed
* by this function for debugging.
*
* If node is not an equality and ret is an equality, this method applies
@@ -157,7 +158,7 @@ class SequencesRewriter : public TheoryRewriter
* additional rewrites on ret, after which we return the result of this call.
* Otherwise, this method simply returns ret.
*/
- static Node returnRewrite(Node node, Node ret, const char* c);
+ static Node returnRewrite(Node node, Node ret, Rewrite r);
public:
RewriteResponse postRewrite(TNode node) override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback