diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-18 10:48:04 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-18 10:48:04 -0600 |
| commit | a51d41f2a267df30c7ef24de5b753ce73e0ac479 (patch) | |
| tree | 3bbf0450eb196604b9d1210dcef17c262d70aa87 /src/theory/strings/theory_strings.cpp | |
| parent | 84da041c64ef16b95f3028183e1a5a2c994d98ec (diff) | |
switch to total function str.to.int: maps invalid and non-digit strings to 0
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 056cd9eb5..d8b20d890 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -57,7 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); - d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -408,7 +408,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::STRING_CONCAT: case kind::STRING_SUBSTR_TOTAL: case kind::STRING_ITOS: - case kind::STRING_STOI_TOTAL: + case kind::STRING_STOI: d_equalityEngine.addTerm(n); break; //case kind::STRING_ITOS: |