diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-25 08:48:14 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-25 08:48:14 -0500 |
commit | b71f00097394c5f292abb002e31f49a07aff0b58 (patch) | |
tree | 0d43b34aeed35abc267fad67f69ca7a5e2600e85 /src/theory/strings/inference_manager.cpp | |
parent | d19b800ac00feb44bfc6302f02695c8700e15c12 (diff) |
Generalize more uses of string-specific functions (#4145)
Towards theory of sequences.
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index eebad2274..e931c5c1a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" using namespace std; using namespace CVC4::context; @@ -370,12 +371,13 @@ Node InferenceManager::getSymbolicDefinition(Node n, void InferenceManager::registerLength(Node n) { + Assert(n.getType().isStringLike()); NodeManager* nm = NodeManager::currentNM(); // register length information: // for variables, split on empty vs positive length // for concat/const/replace, introduce proxy var and state length relation Node lsum; - if (n.getKind() != STRING_CONCAT && n.getKind() != CONST_STRING) + if (n.getKind() != STRING_CONCAT && !n.isConst()) { Node lsumb = nm->mkNode(STRING_LENGTH, n); lsum = Rewriter::rewrite(lsumb); @@ -422,9 +424,9 @@ void InferenceManager::registerLength(Node n) lsum = nm->mkNode(PLUS, nodeVec); lsum = Rewriter::rewrite(lsum); } - else if (n.getKind() == CONST_STRING) + else if (n.isConst()) { - lsum = nm->mkConst(Rational(n.getConst<String>().size())); + lsum = nm->mkConst(Rational(Word::getLength(n))); } Assert(!lsum.isNull()); d_proxyVarToLength[sk] = lsum; |