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/theory/quantifiers/conjecture_generator.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/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 41d881f2c..ba716254a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/conjecture_generator.h" +#include "expr/skolem_manager.h" #include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" @@ -1089,8 +1090,11 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn ); if( it==d_typ_pred.end() ){ - TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." ); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType()); + Node op = sm->mkDummySkolem( + "PE", op_tn, "was created by conjecture ground term enumerator."); d_typ_pred[tn] = op; return op; }else{ |