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 /src/preprocessing/passes/unconstrained_simplifier.cpp | |
| 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 'src/preprocessing/passes/unconstrained_simplifier.cpp')
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 9a9aaa366..2c01bd6d2 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -19,6 +19,7 @@ #include "preprocessing/passes/unconstrained_simplifier.h" #include "expr/dtype.h" +#include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/logic_exception.h" @@ -126,7 +127,8 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem( + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node n = sm->mkDummySkolem( "unconstrained", t, "a new var introduced because of unconstrained variable " |