diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 35 |
1 files changed, 22 insertions, 13 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d83d5ca49..5ac8b8f7e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -108,6 +108,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE); + d_equalityEngine.addFunctionKind(kind::SEQ_UNIT); // extended functions d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); @@ -296,7 +297,14 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) std::unordered_set<Node, NodeHashFunction> >& rst : repSet) { - if (!collectModelInfoType(rst.first, rst.second, m)) + // get partition of strings of equal lengths, per type + std::map<TypeNode, std::vector<std::vector<Node> > > colT; + std::map<TypeNode, std::vector<Node> > ltsT; + std::vector<Node> repVec(rst.second.begin(), rst.second.end()); + d_state.separateByLength(repVec, colT, ltsT); + // now collect model info for the type + TypeNode st = rst.first; + if (!collectModelInfoType(st, rst.second, colT[st], ltsT[st], m)) { return false; } @@ -307,14 +315,12 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) bool TheoryStrings::collectModelInfoType( TypeNode tn, const std::unordered_set<Node, NodeHashFunction>& repSet, + std::vector<std::vector<Node> >& col, + std::vector<Node>& lts, TheoryModel* m) { NodeManager* nm = NodeManager::currentNM(); - std::vector<Node> nodes(repSet.begin(), repSet.end()); std::map< Node, Node > processed; - std::vector< std::vector< Node > > col; - std::vector< Node > lts; - d_state.separateByLength(nodes, col, lts); //step 1 : get all values for known lengths std::vector< Node > lts_values; std::map<unsigned, Node> values_used; @@ -445,7 +451,7 @@ bool TheoryStrings::collectModelInfoType( } else { - Unimplemented() << "Collect model info not implemented for type " << tn; + sel.reset(new SeqEnumLen(tn, nullptr, currLen, currLen)); } for (const Node& eqc : pure_eq) { @@ -521,13 +527,15 @@ bool TheoryStrings::collectModelInfoType( } Trace("strings-model") << "String Model : Pure Assigned." << std::endl; //step 4 : assign constants to all other equivalence classes - for( unsigned i=0; i<nodes.size(); i++ ){ - if( processed.find( nodes[i] )==processed.end() ){ - NormalForm& nf = d_csolver->getNormalForm(nodes[i]); + for (const Node& rn : repSet) + { + if (processed.find(rn) == processed.end()) + { + NormalForm& nf = d_csolver->getNormalForm(rn); if (Trace.isOn("strings-model")) { Trace("strings-model") - << "Construct model for " << nodes[i] << " based on normal form "; + << "Construct model for " << rn << " based on normal form "; for (unsigned j = 0, size = nf.d_nf.size(); j < size; j++) { Node n = nf.d_nf[j]; @@ -553,9 +561,10 @@ bool TheoryStrings::collectModelInfoType( } Node cc = utils::mkNConcat(nc, tn); Assert(cc.isConst()); - Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; - processed[nodes[i]] = cc; - if (!m->assertEquality(nodes[i], cc, true)) + Trace("strings-model") + << "*** Determined constant " << cc << " for " << rn << std::endl; + processed[rn] = cc; + if (!m->assertEquality(rn, cc, true)) { // this should never happen due to the model soundness argument // for strings |