diff options
Diffstat (limited to 'src/theory/strings/solver_state.cpp')
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 32ed6896c..28ab63d05 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -90,6 +90,10 @@ Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te) // typically shouldnt be necessary lengthTerm = t; } + else + { + lengthTerm = lengthTerm[0]; + } Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm << std::endl; if (te != lengthTerm) @@ -135,13 +139,14 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps) return false; } -void SolverState::setPendingPrefixConflictWhen(Node conf) +void SolverState::setPendingMergeConflict(Node conf, InferenceId id) { - if (conf.isNull() || d_pendingConflictSet.get()) + if (d_pendingConflictSet.get()) { + // already set conflict return; } - InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT); + InferInfo iiPrefixConf(id); iiPrefixConf.d_conc = d_false; utils::flattenOp(AND, conf, iiPrefixConf.d_premises); setPendingConflict(iiPrefixConf); @@ -188,7 +193,6 @@ void SolverState::separateByLength( // not have an associated length in the mappings above, if the length of // an equivalence class is unknown. std::map<unsigned, std::vector<Node> > eqc_to_strings; - NodeManager* nm = NodeManager::currentNM(); for (const Node& eqc : n) { Assert(d_ee->getRepresentative(eqc) == eqc); @@ -197,7 +201,6 @@ void SolverState::separateByLength( Node lt = ei ? ei->d_lengthTerm : Node::null(); if (!lt.isNull()) { - lt = nm->mkNode(STRING_LENGTH, lt); Node r = d_ee->getRepresentative(lt); std::pair<Node, TypeNode> lkey(r, tnEqc); if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end()) |