diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-29 09:31:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-29 14:31:20 +0000 |
commit | 0e08fa4ff925b201d42544dd4b28c74d1b245bd7 (patch) | |
tree | 60e6e3acb961cda82540903b834e27358f20bd99 /src/theory/quantifiers/fmf/bounded_integers.h | |
parent | ba91b0ea10021ad299f30d23de4864940bb78100 (diff) |
Move decision manager into theory inference manager (#6231)
This makes it so that the decision manager is accessible from TheoryInferenceManager.
This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.h')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index cb64978bb..f3684ab88 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -168,8 +168,7 @@ private: QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - TermRegistry& tr, - DecisionManager* dm); + TermRegistry& tr); virtual ~BoundedIntegers(); void presolve() override; @@ -236,8 +235,6 @@ private: Node matchBoundVar( Node v, Node t, Node e ); bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); - /** Pointer to the decision manager */ - DecisionManager* d_dm; }; } |