diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-02 11:57:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-02 11:57:26 -0600 |
commit | d85eefdf97566c22dddc94a3cf27ae19c24ec4f3 (patch) | |
tree | 614dc0ed8d4cf269ac996bb16fa2cfe5b65a6459 /src/theory/strings/theory_strings.h | |
parent | 1117b3e69b16c992c5f41ff3f2873ac40fce2cff (diff) |
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.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 22 |
1 files changed, 17 insertions, 5 deletions
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<Node>& vars, std::vector<Node>& subs, std::map<Node, std::vector<Node> >& 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<Node, NodeHashFunction>& repSet, + TheoryModel* m); + /** assert pending fact * * This asserts atom with polarity to the equality engine of this class, |