From 76ccad7995ce5c11bb6fd5143fab850e931ddfd3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 25 Jan 2020 00:46:56 -0800 Subject: Adds stats and option --- src/options/strings_options.toml | 9 +++++++ src/theory/strings/skolem_cache.cpp | 32 +++++++++++++++++++++++- src/theory/strings/skolem_cache.h | 19 ++++++++++++++ src/theory/strings/theory_strings.cpp | 10 +++++++- src/theory/strings/theory_strings.h | 2 ++ src/theory/strings/theory_strings_preprocess.cpp | 8 +++--- 6 files changed, 74 insertions(+), 6 deletions(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3916c68f3..809f48b6d 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -232,6 +232,15 @@ header = "options/strings_options.h" read_only = true help = "do flat form inferences" +[[option]] + name = "skolemSharing" + category = "expert" + long = "skolem-sharing" + type = "bool" + default = "true" + read_only = true + help = "use skolem sharing" + [[option]] name = "stringRegExpInterMode" category = "expert" diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index b4e1c74ea..cd30d178a 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -14,6 +14,8 @@ #include "theory/strings/skolem_cache.h" +#include "options/strings_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "util/rational.h" @@ -47,7 +49,7 @@ Node SkolemCache::mkTypedSkolemCached( a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); - if (tn == d_strType) + if (options::skolemSharing() && tn == d_strType) { std::tie(id, a, b) = normalizeStringSkolem(id, a, b); } @@ -59,6 +61,11 @@ Node SkolemCache::mkTypedSkolemCached( d_skolemCache[a][b][id] = sk; return sk; } + else + { + d_statistics.d_numCachedSkolems += 1; + d_statistics.d_numSkolems += 1; + } return it->second; } Node SkolemCache::mkTypedSkolemCached(TypeNode tn, @@ -78,6 +85,7 @@ Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) { Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem"); d_allSkolems.insert(n); + d_statistics.d_numSkolems += 1; return n; } @@ -94,6 +102,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) NodeManager* nm = NodeManager::currentNM(); + if (id == SK_FIRST_CTN_IOPRE || id == SK_FIRST_CTN_RFCPRE) + { + id = SK_FIRST_CTN_PRE; + } + else if (id == SK_FIRST_CTN_IOPOST || id == SK_FIRST_CTN_RFCPOST) + { + id = SK_FIRST_CTN_POST; + } + if (id == SK_FIRST_CTN_POST) { // SK_FIRST_CTN_POST(x, y) ---> @@ -196,6 +213,19 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) return std::make_tuple(id, a, b); } +SkolemCache::Statistics::Statistics() + : d_numSkolems("theory::strings::NumSkolems", 0), + d_numCachedSkolems("theory::strings::NumCachedSkolems", 0) +{ + smtStatisticsRegistry()->registerStat(&d_numSkolems); + smtStatisticsRegistry()->registerStat(&d_numCachedSkolems); +} + +SkolemCache::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&d_numSkolems); + smtStatisticsRegistry()->unregisterStat(&d_numCachedSkolems); +} + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index c1e3c7214..3612f8503 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -22,6 +22,7 @@ #include #include "expr/node.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -94,6 +95,13 @@ class SkolemCache // of b in a as the witness for contains( a, b ). SK_FIRST_CTN_PRE, SK_FIRST_CTN_POST, + + SK_FIRST_CTN_IOPRE, + SK_FIRST_CTN_IOPOST, + + SK_FIRST_CTN_RFCPRE, + SK_FIRST_CTN_RFCPOST, + // For integer b, // len( a ) > b => // exists k. a = k ++ a' ^ len( k ) = b @@ -162,6 +170,17 @@ class SkolemCache std::map > > d_skolemCache; /** the set of all skolems we have generated */ std::unordered_set d_allSkolems; + + struct Statistics + { + IntStat d_numSkolems; + IntStat d_numCachedSkolems; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; }; } // namespace strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9949bcea4..8b88af3c0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4418,10 +4418,12 @@ Node TheoryStrings::ppRewrite(TNode atom) { Node atomElim; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) { + d_statistics.d_numStrInRe += 1; // aggressive elimination of regular expression membership atomElim = d_regexp_elim.eliminate(atom); if (!atomElim.isNull()) { + d_statistics.d_numStrInReElim += 1; Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim << " via regular expression elimination." << std::endl; @@ -4451,12 +4453,16 @@ TheoryStrings::Statistics::Statistics() : d_splits("theory::strings::NumOfSplitOnDemands", 0), d_eq_splits("theory::strings::NumOfEqSplits", 0), d_deq_splits("theory::strings::NumOfDiseqSplits", 0), - d_loop_lemmas("theory::strings::NumOfLoops", 0) + d_loop_lemmas("theory::strings::NumOfLoops", 0), + d_numStrInRe("theory::strings::NumStrInRe", 0), + d_numStrInReElim("theory::strings::NumStrInReElim", 0) { smtStatisticsRegistry()->registerStat(&d_splits); smtStatisticsRegistry()->registerStat(&d_eq_splits); smtStatisticsRegistry()->registerStat(&d_deq_splits); smtStatisticsRegistry()->registerStat(&d_loop_lemmas); + smtStatisticsRegistry()->registerStat(&d_numStrInRe); + smtStatisticsRegistry()->registerStat(&d_numStrInReElim); } TheoryStrings::Statistics::~Statistics(){ @@ -4464,6 +4470,8 @@ TheoryStrings::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_eq_splits); smtStatisticsRegistry()->unregisterStat(&d_deq_splits); smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_numStrInRe); + smtStatisticsRegistry()->unregisterStat(&d_numStrInReElim); } /** run the given inference step */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8e2af8434..aeba210f9 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -683,6 +683,8 @@ private: IntStat d_eq_splits; IntStat d_deq_splits; IntStat d_loop_lemmas; + IntStat d_numStrInRe; + IntStat d_numStrInReElim; Statistics(); ~Statistics(); };/* class TheoryStrings::Statistics */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 6272ad129..f93c09cd4 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -134,9 +134,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n)); Node io2 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); + d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPRE, "iopre"); Node io4 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); + d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPOST, "iopost"); // ~contains( substr( x, n, len( x ) - n ), y ) Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate(); @@ -355,9 +355,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node z = t[2]; TypeNode tn = t[0].getType(); Node rp1 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); + d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_RFCPRE, "rfcpre"); Node rp2 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost"); + d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_RFCPOST, "rfcpost"); Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw"); // y = "" -- cgit v1.2.3