summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-01-11 11:23:15 -0600
committerGitHub <noreply@github.com>2021-01-11 11:23:15 -0600
commit8c04f1639607b34b56e3eaa8d3188b27e1454b41 (patch)
treeb4427f298b2fde0686b7fdd98008f2fdc0173321 /src/prop/prop_engine.h
parentb8841e768a37131c492508cd0e12b9acd8bf4c2b (diff)
Merge theory registrar and theory proxy (#5758)
The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine. This merges the helper class TheoryRegistrar into TheoryProxy.
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r--src/prop/prop_engine.h3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ac2b35ad6..453c1c2af 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -298,9 +298,6 @@ class PropEngine
/** List of all of the assertions that need to be made */
std::vector<Node> d_assertionList;
- /** Theory registrar; kept around for destructor cleanup */
- theory::TheoryRegistrar* d_registrar;
-
/** A pointer to the proof node maneger to be used by this engine. */
ProofNodeManager* d_pnm;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback