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.
// 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<std::vector<Node> > cols;
- std::vector<Node> lts;
+ std::map<TypeNode, std::vector<std::vector<Node> > > cols;
+ std::map<TypeNode, std::vector<Node> > lts;
d_state.separateByLength(d_stringsEqc, cols, lts);
+ for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols)
+ {
+ checkCardinalityType(c.first, c.second, lts[c.first]);
+ }
+}
+
+void BaseSolver::checkCardinalityType(TypeNode tn,
+ std::vector<std::vector<Node> >& cols,
+ std::vector<Node>& lts)
+{
NodeManager* nm = NodeManager::currentNM();
Trace("strings-card") << "Check cardinality...." << std::endl;
// for each collection
// 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<double>(cols[i].size());
std::vector<Node>& 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<std::vector<Node> >& cols,
+ std::vector<Node>& lts);
/** The solver state object */
SolverState& d_state;
/** The (custom) output channel of the theory of strings */
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<Node>& deqs = d_state.getDisequalityList();
}
}
- 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<TypeNode, std::vector<std::vector<Node> > > colsT;
+ std::map<TypeNode, std::vector<Node> > ltsT;
+ d_state.separateByLength(d_strings_eqc, colsT, ltsT);
+ for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& ct : colsT)
+ {
+ std::vector<std::vector<Node> >& cols = ct.second;
for( unsigned i=0; i<cols.size(); i++ ){
if (cols[i].size() > 1 && !d_im.hasPendingLemma())
{
return d_valuation.entailmentCheck(mode, lit);
}
-void SolverState::separateByLength(const std::vector<Node>& n,
- std::vector<std::vector<Node> >& cols,
- std::vector<Node>& lts)
+void SolverState::separateByLength(
+ const std::vector<Node>& n,
+ std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
+ std::map<TypeNode, std::vector<Node>>& lts)
{
unsigned leqc_counter = 0;
- std::map<Node, unsigned> eqc_to_leqc;
- std::map<unsigned, Node> leqc_to_eqc;
+ // map (length, type) to an equivalence class identifier
+ std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
+ // backwards map
+ std::map<unsigned, std::pair<Node, TypeNode>> 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<unsigned, std::vector<Node> > 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<Node, TypeNode> 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
{
}
for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
{
- cols.push_back(std::vector<Node>());
- 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);
}
}
*
* 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<Node>& n,
- std::vector<std::vector<Node> >& cols,
- std::vector<Node>& lts);
+ void separateByLength(
+ const std::vector<Node>& n,
+ std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
+ std::map<TypeNode, std::vector<Node>>& lts);
+
private:
/** Common constants */
Node d_zero;
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);
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;
}
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;
}
else
{
- Unimplemented() << "Collect model info not implemented for type " << tn;
+ sel.reset(new SeqEnumLen(tn, nullptr, currLen, currLen));
}
for (const Node& eqc : pure_eq)
{
}
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];
}
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
/** 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<Node, NodeHashFunction>& repSet,
+ std::vector<std::vector<Node> >& col,
+ std::vector<Node>& lts,
TheoryModel* m);
/** assert pending fact
projects / cvc5.git / commitdiff