diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.h | 12 |
2 files changed, 21 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index bd85ea496..736fdebee 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -25,8 +25,13 @@ namespace theory { namespace quantifiers { SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p) - : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1) + : d_tds(tds), + d_parent(p), + d_tlEnum(nullptr), + d_abortSize(-1), + d_rewriteChecks("sygus-rr-verify-rewrite-checks", 0) { + smtStatisticsRegistry()->registerStat(&d_rewriteChecks); } void SygusEnumerator::initialize(Node e) @@ -152,7 +157,8 @@ SygusEnumerator::TermCache::TermCache() void SygusEnumerator::TermCache::initialize(Node e, TypeNode tn, TermDbSygus* tds, - SygusPbe* pbe) + SygusPbe* pbe, + IntStat* rewriteChecks) { Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl; d_enum = e; @@ -161,6 +167,7 @@ void SygusEnumerator::TermCache::initialize(Node e, d_pbe = pbe; d_sizeStartIndex[0] = 0; d_isSygusType = false; + d_rewriteChecks = rewriteChecks; // compute static information about tn if (!d_tn.isDatatype()) @@ -320,7 +327,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n) { d_sampleRrVInit = true; d_samplerRrV.initializeSygus( - d_tds, d_enum, options::sygusSamples(), false); + d_tds, d_enum, options::sygusSamples(), false, d_rewriteChecks); } d_samplerRrV.checkEquivalent(bn, bnr); } @@ -539,7 +546,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn) pbe = nullptr; } } - d_tcache[tn].initialize(d_enum, tn, d_tds, pbe); + d_tcache[tn].initialize(d_enum, tn, d_tds, pbe, &d_rewriteChecks); } SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index d4c466b03..0f5c581f4 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -45,7 +45,10 @@ class SygusEnumerator : public EnumValGenerator { public: SygusEnumerator(TermDbSygus* tds, SynthConjecture* p); - ~SygusEnumerator() {} + ~SygusEnumerator() + { + smtStatisticsRegistry()->unregisterStat(&d_rewriteChecks); + } /** initialize this class with enumerator e */ void initialize(Node e) override; /** Inform this generator that abstract value v was enumerated. */ @@ -100,7 +103,8 @@ class SygusEnumerator : public EnumValGenerator void initialize(Node e, TypeNode tn, TermDbSygus* tds, - SygusPbe* pbe = nullptr); + SygusPbe* pbe = nullptr, + IntStat* rewriteChecks = nullptr); /** get last constructor class index for weight * * This returns a minimal index n such that all constructor classes at @@ -183,6 +187,8 @@ class SygusEnumerator : public EnumValGenerator quantifiers::SygusSampler d_samplerRrV; /** is the above sampler initialized? */ bool d_sampleRrVInit; + + IntStat* d_rewriteChecks; }; /** above cache for each sygus type */ std::map<TypeNode, TermCache> d_tcache; @@ -448,6 +454,8 @@ class SygusEnumerator : public EnumValGenerator */ std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons; //-------------------------------- end externally specified symmetry breaking + + IntStat d_rewriteChecks; }; } // namespace quantifiers |