diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-26 02:34:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-26 07:34:14 +0000 |
| commit | b6d3dc39fcd1cd71d263a4ff6949d77d671c73b9 (patch) | |
| tree | 8707c0bbd4913952bb79f1d15edba18bf9208ae0 | |
| parent | f809439274390d754c158bc105f769df3a55ee42 (diff) | |
Do not process looping word equations over sequences (#6434)
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 2abe2de82..ed220c1eb 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1771,23 +1771,27 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, int index, CoreInferInfo& info) { + NodeManager* nm = NodeManager::currentNM(); + Node conc; + const std::vector<Node>& veci = nfi.d_nf; + const std::vector<Node>& vecoi = nfj.d_nf; + + TypeNode stype = veci[loop_index].getType(); + if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT) { throw LogicException("Looping word equation encountered."); } - else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE) + else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE + || stype.isSequence()) { + // note we cannot convert looping word equations into regular expressions if + // we are handling sequences, since there is no analog for regular + // expressions over sequences currently d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP); return ProcessLoopResult::SKIPPED; } - NodeManager* nm = NodeManager::currentNM(); - Node conc; - const std::vector<Node>& veci = nfi.d_nf; - const std::vector<Node>& vecoi = nfj.d_nf; - - TypeNode stype = veci[loop_index].getType(); - Trace("strings-loop") << "Detected possible loop for " << veci[loop_index] << std::endl; Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; |