diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ae8b3b682..d1b18df13 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -363,9 +363,15 @@ bool TheoryStrings::collectModelInfoType( NormalForm& nfe = d_csolver->getNormalForm(eqc); if (nfe.d_nf.size() == 1) { + // is it an equivalence class with a seq.unit term? + if (nfe.d_nf[0].getKind() == SEQ_UNIT) + { + pure_eq_assign[eqc] = nfe.d_nf[0]; + Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; + } // does it have a code and the length of these equivalence classes are // one? - if (d_termReg.hasStringCode() && lts_values[i] == d_one) + else if (d_termReg.hasStringCode() && lts_values[i] == d_one) { EqcInfo* eip = d_state.getOrMakeEqcInfo(eqc, false); if (eip && !eip->d_codeTerm.get().isNull()) @@ -419,7 +425,7 @@ bool TheoryStrings::collectModelInfoType( std::unique_ptr<SEnumLen> sel; Trace("strings-model") << "Cardinality of alphabet is " << utils::getAlphabetCardinality() << std::endl; - if (tn.isString()) + if (tn.isString()) // string-only { sel.reset(new StringEnumLen( currLen, currLen, utils::getAlphabetCardinality())); @@ -535,7 +541,6 @@ bool TheoryStrings::collectModelInfoType( nc.push_back(r.isConst() ? r : processed[r]); } Node cc = utils::mkNConcat(nc, tn); - Assert(cc.isConst()); Trace("strings-model") << "*** Determined constant " << cc << " for " << rn << std::endl; processed[rn] = cc; @@ -543,12 +548,17 @@ bool TheoryStrings::collectModelInfoType( { // this should never happen due to the model soundness argument // for strings - Unreachable() << "TheoryStrings::collectModelInfoType: " "Inconsistent equality (unprocessed eqc)" << std::endl; return false; } + else if (!cc.isConst()) + { + // the value may be specified by seq.unit components, ensure this + // is marked as the skeleton for constructing values in this class. + m->assertSkeleton(cc); + } } } //Trace("strings-model") << "String Model : Assigned." << std::endl; |