From: Andrew Reynolds Date: Fri, 12 Jun 2020 13:07:47 +0000 (-0500) Subject: Cardinality-related inferences per type in theory of strings (#4585) X-Git-Tag: cvc5-1.0.0~3223 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c733d68aabc1c90b4f0f8a3e7a6a25f24896744;p=cvc5.git Cardinality-related inferences per type in theory of strings (#4585) Towards theory of sequences. This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type. --- diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 16c83de78..4a03637d0 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -432,9 +432,19 @@ void BaseSolver::checkCardinality() // are pairwise propagated to be equal. We do not require disequalities // between the lengths of each collection, since we split on disequalities // between lengths of string terms that are disequal (DEQ-LENGTH-SP). - std::vector > cols; - std::vector lts; + std::map > > cols; + std::map > lts; d_state.separateByLength(d_stringsEqc, cols, lts); + for (std::pair > >& c : cols) + { + checkCardinalityType(c.first, c.second, lts[c.first]); + } +} + +void BaseSolver::checkCardinalityType(TypeNode tn, + std::vector >& cols, + std::vector& lts) +{ NodeManager* nm = NodeManager::currentNM(); Trace("strings-card") << "Check cardinality...." << std::endl; // for each collection @@ -448,6 +458,11 @@ void BaseSolver::checkCardinality() // no restriction on sets in the partition of size 1 continue; } + if (!tn.isString()) + { + // TODO (cvc4-projects #23): how to handle sequence for finite types? + continue; + } // size > c^k unsigned card_need = 1; double curr = static_cast(cols[i].size()); diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 1960b8352..334fdf596 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -200,6 +200,19 @@ class BaseSolver std::vector& vecc, bool ensureConst = true, bool isConst = true); + /** + * Check cardinality for type tn. This adds a lemma corresponding to + * cardinality for terms of type tn, if applicable. + * + * @param tn The string-like type of terms we are considering, + * @param cols The list of collections of equivalence classes. This is a + * partition of all string equivalence classes, grouped by those with equal + * lengths. + * @param lts The length of each of the collections in cols. + */ + void checkCardinalityType(TypeNode tn, + std::vector >& cols, + std::vector& lts); /** The solver state object */ SolverState& d_state; /** The (custom) output channel of the theory of strings */ diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 604abb1d7..b23562862 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2239,8 +2239,6 @@ bool CoreSolver::isNormalFormPair( Node n1, Node n2 ) { void CoreSolver::checkNormalFormsDeq() { eq::EqualityEngine* ee = d_state.getEqualityEngine(); - std::vector< std::vector< Node > > cols; - std::vector< Node > lts; std::map< Node, std::map< Node, bool > > processed; const context::CDList& deqs = d_state.getDisequalityList(); @@ -2270,9 +2268,18 @@ void CoreSolver::checkNormalFormsDeq() } } - if (!d_im.hasProcessed()) + if (d_im.hasProcessed()) { - d_state.separateByLength(d_strings_eqc, cols, lts); + // added splitting lemma above + return; + } + // otherwise, look at pairs of equivalence classes with equal lengths + std::map > > colsT; + std::map > ltsT; + d_state.separateByLength(d_strings_eqc, colsT, ltsT); + for (std::pair > >& ct : colsT) + { + std::vector >& cols = ct.second; for( unsigned i=0; i 1 && !d_im.hasPendingLemma()) { diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 622e919f7..465b237ba 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -297,31 +297,39 @@ std::pair SolverState::entailmentCheck(options::TheoryOfMode mode, return d_valuation.entailmentCheck(mode, lit); } -void SolverState::separateByLength(const std::vector& n, - std::vector >& cols, - std::vector& lts) +void SolverState::separateByLength( + const std::vector& n, + std::map>>& cols, + std::map>& lts) { unsigned leqc_counter = 0; - std::map eqc_to_leqc; - std::map leqc_to_eqc; + // map (length, type) to an equivalence class identifier + std::map, unsigned> eqc_to_leqc; + // backwards map + std::map> leqc_to_eqc; + // Collection of eqc for each identifier. Notice that some identifiers may + // not have an associated length in the mappings above, if the length of + // an equivalence class is unknown. std::map > eqc_to_strings; NodeManager* nm = NodeManager::currentNM(); for (const Node& eqc : n) { Assert(d_ee.getRepresentative(eqc) == eqc); + TypeNode tnEqc = eqc.getType(); EqcInfo* ei = getOrMakeEqcInfo(eqc, false); Node lt = ei ? ei->d_lengthTerm : Node::null(); if (!lt.isNull()) { lt = nm->mkNode(STRING_LENGTH, lt); Node r = d_ee.getRepresentative(lt); - if (eqc_to_leqc.find(r) == eqc_to_leqc.end()) + std::pair lkey(r, tnEqc); + if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end()) { - eqc_to_leqc[r] = leqc_counter; - leqc_to_eqc[leqc_counter] = r; + eqc_to_leqc[lkey] = leqc_counter; + leqc_to_eqc[leqc_counter] = lkey; leqc_counter++; } - eqc_to_strings[eqc_to_leqc[r]].push_back(eqc); + eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc); } else { @@ -331,9 +339,11 @@ void SolverState::separateByLength(const std::vector& n, } for (const std::pair >& p : eqc_to_strings) { - cols.push_back(std::vector()); - cols.back().insert(cols.back().end(), p.second.begin(), p.second.end()); - lts.push_back(leqc_to_eqc[p.first]); + Assert(!p.second.empty()); + // get the type of the collection + TypeNode stn = p.second[0].getType(); + cols[stn].emplace_back(p.second.begin(), p.second.end()); + lts[stn].push_back(leqc_to_eqc[p.first].first); } } diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index d43c600f4..5db3a3707 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -171,11 +171,14 @@ class SolverState * * Separate the string representatives in argument n into a partition cols * whose collections have equal length. The i^th vector in cols has length - * lts[i] for all elements in col. + * lts[i] for all elements in col. These vectors are furthmore separated + * by string-like type. */ - void separateByLength(const std::vector& n, - std::vector >& cols, - std::vector& lts); + void separateByLength( + const std::vector& n, + std::map>>& cols, + std::map>& lts); + private: /** Common constants */ Node d_zero; 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 >& rst : repSet) { - if (!collectModelInfoType(rst.first, rst.second, m)) + // get partition of strings of equal lengths, per type + std::map > > colT; + std::map > ltsT; + std::vector 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& repSet, + std::vector >& col, + std::vector& lts, TheoryModel* m) { NodeManager* nm = NodeManager::currentNM(); - std::vector 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 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; igetNormalForm(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 diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7c99b6968..6468f1d3a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -281,13 +281,17 @@ class TheoryStrings : public Theory { /** Collect model info for type tn * * Assigns model values (in m) to all relevant terms of the string-like type - * tn in the current context, which are stored in repSet. + * tn in the current context, which are stored in repSet. Furthermore, + * col is a partition of repSet where equivalence classes are grouped into + * sets having equal length, where these lengths are stored in lts. * * Returns false if a conflict is discovered while doing this assignment. */ bool collectModelInfoType( TypeNode tn, const std::unordered_set& repSet, + std::vector >& col, + std::vector& lts, TheoryModel* m); /** assert pending fact