diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-22 20:32:32 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-23 01:32:32 +0000 |
| commit | 61b9dadc88de3bf7d52538f9e914cfb61cbb7bb6 (patch) | |
| tree | f40523a4d2b095101063975145b578c94da7e941 /src/theory/quantifiers_engine.h | |
| parent | 442bc26b6ce093efed14bfd6764dac30bfdf918f (diff) | |
Moving instantiate and skolemize into quantifiers inference manager (#6188)
After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 4d3029ca9..b6562caa7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -237,10 +237,6 @@ public: std::unique_ptr<inst::TriggerTrie> d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** instantiate utility */ - std::unique_ptr<quantifiers::Instantiate> d_instantiate; - /** skolemize utility */ - std::unique_ptr<quantifiers::Skolemize> d_skolemize; //------------- end quantifiers utilities /** * The modules utility, which contains all of the quantifiers modules. |