From 9f77ec44decf18fe23c738988281373795dcca0d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Mar 2020 13:35:59 -0500 Subject: Convert more uses of strings to words (#3921) Towards theory of sequences. Also adds documentation to strncmp/rstrncmp and adds them to the Word interface. --- src/theory/strings/theory_strings.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/theory/strings/theory_strings.cpp') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a5604925c..5015db3f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -29,6 +29,7 @@ #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/type_enumerator.h" +#include "theory/strings/word.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -111,7 +112,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + d_emptyString = Word::mkEmptyWord(CONST_STRING); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); -- cgit v1.2.3