diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 13:36:15 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-07 18:36:15 +0000 |
| commit | 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch) | |
| tree | 03b1a5792f2f6ca5537353b86682f427090668da /test/unit/test_node.h | |
| parent | 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff) | |
Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
Diffstat (limited to 'test/unit/test_node.h')
| -rw-r--r-- | test/unit/test_node.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 359cc0b6f..dacc1f543 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -16,6 +16,7 @@ #define CVC4__TEST__UNIT__TEST_NODE_H #include "expr/node_manager.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -29,6 +30,7 @@ class TestNode : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); @@ -38,6 +40,7 @@ class TestNode : public TestInternal std::unique_ptr<NodeManagerScope> d_scope; std::unique_ptr<NodeManager> d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr<TypeNode> d_boolTypeNode; std::unique_ptr<TypeNode> d_bvTypeNode; std::unique_ptr<TypeNode> d_intTypeNode; |