summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-04-03 14:52:45 -0700
committerGitHub <noreply@github.com>2020-04-03 14:52:45 -0700
commitaeede74491d1db9c5bac771e78b79934ca4ab552 (patch)
treea3c05a53702514520b9625b30995e7d789c39982 /src/theory/arith
parentbadc9cb00c9086b9303fab1b494e9c5eb88265ec (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/arith')
-rw-r--r--src/theory/arith/theory_arith.cpp4
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arith/theory_arith_private.h4
3 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2c748f188..e4aeca980 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -54,9 +54,9 @@ TheoryArith::~TheoryArith(){
delete d_internal;
}
-std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter()
+TheoryRewriter* TheoryArith::getTheoryRewriter()
{
- return std::unique_ptr<TheoryRewriter>(new ArithRewriter());
+ return d_internal->getTheoryRewriter();
}
void TheoryArith::preRegisterTerm(TNode n){
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 92892d2ae..a16f1ed5e 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -51,7 +51,7 @@ public:
Valuation valuation, const LogicInfo& logicInfo);
virtual ~TheoryArith();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override;
/**
* Does non-context dependent setup for a node connected to a theory.
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index f964c4e04..a4469f3b5 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -426,6 +426,8 @@ public:
TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryArithPrivate();
+ TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+
/**
* Does non-context dependent setup for a node connected to a theory.
*/
@@ -882,6 +884,8 @@ private:
NodeMap d_int_div_skolem;
NodeMap d_nlin_inverse_skolem;
+ /** The theory rewriter for this theory. */
+ ArithRewriter d_rewriter;
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback