diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-16 12:25:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-16 12:25:20 -0500 |
commit | ca6f1b0350b18ce3e134701f68f7e02813c3fb5f (patch) | |
tree | 0f58df1f9dbad64027b1f45d7e588655817b037d /src/theory/strings/theory_strings.h | |
parent | 55c7c653812e8d9ee68739b38e1bacb67a44d64d (diff) |
Improve strings reductions including skolem caching for contains (#2641)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 236c3906c..ec250288b 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -163,7 +163,18 @@ class TheoryStrings : public Theory { std::vector<Node>& vars, std::vector<Node>& subs, std::map<Node, std::vector<Node> >& exp) override; - int getReduction(int effort, Node n, Node& nr) override; + //--------------------------for checkExtfReductions + /** do reduction + * + * This is called when an extended function application n is not able to be + * simplified by context-depdendent simplification, and we are resorting to + * expanding n to its full semantics via a reduction. This method returns + * true if it successfully reduced n by some reduction and sets isCd to + * true if the reduction was (SAT)-context-dependent, and false otherwise. + * The argument effort has the same meaning as in checkExtfReductions. + */ + bool doReduction(int effort, Node n, bool& isCd); + //--------------------------end for checkExtfReductions // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -278,9 +289,8 @@ private: NodeSet d_pregistered_terms_cache; NodeSet d_registered_terms_cache; NodeSet d_length_lemma_terms_cache; - // preprocess cache + /** preprocessing utility, for performing strings reductions */ StringsPreprocess d_preproc; - NodeBoolMap d_preproc_cache; // extended functions inferences cache NodeSet d_extf_infer_cache; NodeSet d_extf_infer_cache_u; |