diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
| commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
| tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/quant_conflict_find.h | |
| parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) | |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index fe9aa411b..5b54f8055 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -131,6 +131,8 @@ public: public: QuantInfo(); ~QuantInfo(); + /** Get quantifiers inference manager */ + QuantifiersInferenceManager& getInferenceManager(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; @@ -143,6 +145,8 @@ public: typedef std::map< int, MatchGen * > VarMgMap; private: + /** The parent who owns this class */ + QuantConflictFind* d_parent; MatchGen * d_mg; VarMgMap d_var_mg; public: |