diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-04-03 14:52:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-03 14:52:45 -0700 |
commit | aeede74491d1db9c5bac771e78b79934ca4ab552 (patch) | |
tree | a3c05a53702514520b9625b30995e7d789c39982 /src/theory/quantifiers | |
parent | badc9cb00c9086b9303fab1b494e9c5eb88265ec (diff) |
Update theory rewriter ownership, add stats to strings (#4202)
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 33 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 38 | ||||
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 6 |
5 files changed, 6 insertions, 78 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index e00bc957f..9070ed51d 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -293,39 +293,6 @@ void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) d_ext_rewrite = er; } -CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( - std::vector<Node>& vars, unsigned nsamples) - : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) -{ -} - -bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) -{ - ExtendedRewriter* er = &d_ext_rewrite; - Node nr; - if (er == nullptr) - { - nr = Rewriter::rewrite(n); - } - else - { - nr = er->extendedRewrite(n); - } - TypeNode tn = nr.getType(); - std::map<TypeNode, CandidateRewriteDatabase>::iterator itc = d_cdbs.find(tn); - if (itc == d_cdbs.end()) - { - Trace("synth-rr-dbg") << "Initialize database for " << tn << std::endl; - // initialize with the extended rewriter owned by this class - d_cdbs[tn].initialize(d_vars, &d_sampler[tn]); - d_cdbs[tn].setExtendedRewriter(er); - itc = d_cdbs.find(tn); - Trace("synth-rr-dbg") << "...finish." << std::endl; - } - Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl; - return itc->second.addTerm(nr, false, out); -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index b68b20998..a9ca659e1 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -103,44 +103,6 @@ class CandidateRewriteDatabase : public ExprMiner bool d_silent; }; -/** - * This class generates and stores candidate rewrite databases for multiple - * types as needed. - */ -class CandidateRewriteDatabaseGen -{ - public: - /** constructor - * - * vars : the variables we are testing substitutions for, for all types, - * nsamples : number of sample points this class will test for all types. - */ - CandidateRewriteDatabaseGen(std::vector<Node>& vars, unsigned nsamples); - /** add term - * - * This registers term n with this class. We generate the candidate rewrite - * database of the appropriate type (if not allocated already), and register - * n with this database. This may result in "candidate-rewrite" being - * printed on the output stream out. We return true if the term sol is - * distinct (up to equivalence) with all previous terms added to this class. - */ - bool addTerm(Node n, std::ostream& out); - - private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; - /** the variables */ - std::vector<Node> d_vars; - /** sygus sampler object for each type */ - std::map<TypeNode, SygusSampler> d_sampler; - /** the number of samples */ - unsigned d_nsamples; - /** candidate rewrite databases for each type */ - std::map<TypeNode, CandidateRewriteDatabase> d_cdbs; - /** an extended rewriter object */ - ExtendedRewriter d_ext_rewrite; -}; - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 7920ecbeb..b0a474c56 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1692,7 +1692,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret) if (ret.getKind() == EQUAL) { - new_ret = strings::SequencesRewriter::rewriteEqualityExt(ret); + new_ret = strings::SequencesRewriter(nullptr).rewriteEqualityExt(ret); } return new_ret; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e3e3c3824..5253638a7 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -54,11 +54,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output TheoryQuantifiers::~TheoryQuantifiers() { } -std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter() -{ - return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter()); -} - void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 7efe7419c..991a47ad0 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -23,6 +23,7 @@ #include "context/context.h" #include "expr/node.h" #include "theory/output_channel.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/valuation.h" @@ -39,7 +40,7 @@ class TheoryQuantifiers : public Theory { const LogicInfo& logicInfo); ~TheoryQuantifiers(); - std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } /** finish initialization */ void finishInit() override; @@ -58,6 +59,9 @@ class TheoryQuantifiers : public Theory { std::vector<Node> node_values, std::string str_value) override; + private: + /** The theory rewriter for this theory. */ + QuantifiersRewriter d_rewriter; };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ |