diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-01 08:46:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-01 08:46:30 -0500 |
commit | 12af221551c34a4bffc0282e7b3fa8dea661190c (patch) | |
tree | 40a384f74915e2c009bb2a66bd0295e62edcfc2e /src/theory/strings/theory_strings_preprocess.h | |
parent | c62980dab74b3db795961f90a4c49c463437a8eb (diff) | |
parent | 04154c08c1af81bb751376ae9379c071a95c5a3f (diff) |
Merge branch 'master' into lfscTestslfscTests
Diffstat (limited to 'src/theory/strings/theory_strings_preprocess.h')
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 48 |
1 files changed, 32 insertions, 16 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index fb6404aa6..113d909a8 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -2,9 +2,9 @@ /*! \file theory_strings_preprocess.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang + ** Andrew Reynolds, Tianyi Liang, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -44,21 +44,41 @@ class StringsPreprocess { context::UserContext* u, SequencesStatistics& stats); ~StringsPreprocess(); + /** The reduce routine + * + * This is the main routine for constructing the reduction lemma for + * an extended function t. It returns the simplified form of t, as well + * as assertions for t, interpeted conjunctively. The reduction lemma + * for t is: + * asserts[0] ^ ... ^ asserts[n] ^ t = t' + * where t' is the term returned by this method. + * The argument sc defines the methods for generating new Skolem variables. + * The return value is t itself if it is not reduced by this class. + * + * The reduction lemma for t is a way of specifying the complete semantics + * of t. In other words, any model satisfying the reduction lemma of t + * correctly interprets t. + * + * @param t The node to reduce, + * @param asserts The vector for storing the assertions that correspond to + * the reduction of t, + * @param sc The skolem cache for generating new variables, + * @return The reduced form of t. + */ + static Node reduce(Node t, std::vector<Node>& asserts, SkolemCache* sc); /** - * Returns a node t' such that - * (exists k) new_nodes => t = t' - * is valid, where k are the free skolems introduced when constructing - * new_nodes. + * Calls the above method for the skolem cache owned by this class, and + * records statistics. */ - Node simplify(Node t, std::vector<Node>& new_nodes); + Node simplify(Node t, std::vector<Node>& asserts); /** * Applies simplifyRec on t until a fixed point is reached, and returns * the resulting term t', which is such that - * (exists k) new_nodes => t = t' + * (exists k) asserts => t = t' * is valid, where k are the free skolems introduced when constructing - * new_nodes. + * asserts. */ - Node processAssertion(Node t, std::vector<Node>& new_nodes); + Node processAssertion(Node t, std::vector<Node>& asserts); /** * Replaces all formulas t in vec_node with an equivalent formula t' that * contains no free instances of extended functions (that is, extended @@ -68,21 +88,17 @@ class StringsPreprocess { void processAssertions(std::vector<Node>& vec_node); private: - /** commonly used constants */ - Node d_zero; - Node d_one; - Node d_neg_one; /** pointer to the skolem cache used by this class */ SkolemCache* d_sc; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; /** * Applies simplify to all top-level extended function subterms of t. New - * assertions created in this reduction are added to new_nodes. The argument + * assertions created in this reduction are added to asserts. The argument * visited stores a cache of previous results. */ Node simplifyRec(Node t, - std::vector<Node>& new_nodes, + std::vector<Node>& asserts, std::map<Node, Node>& visited); }; |