From: Andrew Reynolds Date: Mon, 2 Mar 2020 17:57:26 +0000 (-0600) Subject: Split collect model info by types in strings (#3847) X-Git-Tag: cvc5-1.0.0~3573 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d85eefdf97566c22dddc94a3cf27ae19c24ec4f3;p=cvc5.git Split collect model info by types in strings (#3847) Towards a theory of sequences. We will need to do similar splits per type for most of the functions throughout strings. --- diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b003a7861..945462dd6 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -298,7 +298,11 @@ Node TypeNode::mkGroundValue() const return *te; } -bool TypeNode::isStringLike() const { return isString(); } +bool TypeNode::isStringLike() const +{ + // TODO (cvc4-projects #23): sequence here + return isString(); +} bool TypeNode::isSubtypeOf(TypeNode t) const { if(*this == t) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2fbf16552..a5604925c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -259,18 +259,36 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) return false; } - std::unordered_set repSet; - NodeManager* nm = NodeManager::currentNM(); + std::map > repSet; // Generate model // get the relevant string equivalence classes for (const Node& s : termSet) { - if (s.getType().isString()) + TypeNode tn = s.getType(); + if (tn.isStringLike()) { Node r = d_state.getRepresentative(s); - repSet.insert(r); + repSet[tn].insert(r); + } + } + for (const std::pair >& rst : + repSet) + { + if (!collectModelInfoType(rst.first, rst.second, m)) + { + return false; } } + return true; +} + +bool TheoryStrings::collectModelInfoType( + TypeNode tn, + const std::unordered_set& repSet, + TheoryModel* m) +{ + NodeManager* nm = NodeManager::currentNM(); std::vector nodes(repSet.begin(), repSet.end()); std::map< Node, Node > processed; std::vector< std::vector< Node > > col; @@ -394,7 +412,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) //use type enumerator Assert(lts_values[i].getConst() <= Rational(String::maxSize())) << "Exceeded UINT32_MAX in string model"; - StringEnumeratorLength sel(lts_values[i].getConst().getNumerator().toUnsignedInt()); + StringEnumeratorLength sel( + tn, + lts_values[i].getConst().getNumerator().toUnsignedInt()); for (const Node& eqc : pure_eq) { Node c; @@ -490,7 +510,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) nc.push_back(r.isConst() ? r : processed[r]); } Node cc = utils::mkNConcat(nc); - Assert(cc.getKind() == kind::CONST_STRING); + 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)) diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 79681a5f9..84c9e60c6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -121,6 +121,11 @@ class TheoryStrings : public Theory { std::vector& vars, std::vector& subs, std::map >& exp) override; + /** + * Get all relevant information in this theory regarding the current + * model. Return false if a contradiction is discovered. + */ + bool collectModelInfo(TheoryModel* m) override; // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -231,11 +236,6 @@ private: std::map< Node, Node > d_eqc_to_len_term; - ///////////////////////////////////////////////////////////////////////////// - // MODEL GENERATION - ///////////////////////////////////////////////////////////////////////////// - public: - bool collectModelInfo(TheoryModel* m) override; ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -298,6 +298,18 @@ private: */ bool areCareDisequal(TNode x, TNode y); + /** 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. + * + * Returns false if a conflict is discovered while doing this assignment. + */ + bool collectModelInfoType( + TypeNode tn, + const std::unordered_set& repSet, + TheoryModel* m); + /** assert pending fact * * This asserts atom with polarity to the equality engine of this class, diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 0171effaf..16bfc75a6 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -83,21 +83,16 @@ class StringEnumerator : public TypeEnumeratorBase { bool isFinished() override { return d_curr.isNull(); } };/* class StringEnumerator */ - +/** + * Enumerates string values for a given length. + */ class StringEnumeratorLength { - private: - uint32_t d_cardinality; - std::vector< unsigned > d_data; - Node d_curr; - void mkCurr() { - //make constant from d_data - d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) ); - } - public: - StringEnumeratorLength(uint32_t length, uint32_t card = 256) - : d_cardinality(card) + StringEnumeratorLength(TypeNode tn, uint32_t length, uint32_t card = 256) + : d_type(tn), d_cardinality(card) { + // TODO (cvc4-projects #23): sequence here + Assert(tn.isString()); for( unsigned i=0; i d_data; + /** The current term */ + Node d_curr; + /** Make the current term from d_data */ + void mkCurr() + { + d_curr = NodeManager::currentNM()->mkConst(::CVC4::String(d_data)); + } }; }/* CVC4::theory::strings namespace */