diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 13:35:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 13:35:59 -0500 |
| commit | 9f77ec44decf18fe23c738988281373795dcca0d (patch) | |
| tree | 9772a0ae0bc73e3e00c8b716468b8a86b332f2c6 /src/theory/strings/theory_strings.cpp | |
| parent | c1da31ed532cd1767c20d5fc01df893c427e0e8e (diff) | |
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.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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 ); |