diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-11 09:46:28 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-11 09:46:28 -0600 |
| commit | b8841e768a37131c492508cd0e12b9acd8bf4c2b (patch) | |
| tree | a4de18a51ac37abcf874265bea431154f18cc2ac /src/theory/quantifiers | |
| parent | ae82eb306143ade54a6f99b2aae0b62b8c77cd35 (diff) | |
Further simplifications in preparation for removing Expr layer (#5756)
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.
These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.
This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9c98d6608..4588e8952 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -464,7 +464,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) Node bvl; std::string veName("_virtual_enum_grammar"); SygusDatatype sdt(veName); - TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER); + TypeNode u = nm->mkSort(veName, NodeManager::SORT_FLAG_PLACEHOLDER); std::set<TypeNode> unresolvedTypes; unresolvedTypes.insert(u); std::vector<TypeNode> cargsEmpty; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 23d924581..00a72cbcb 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -377,7 +377,8 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set<TypeNode>& unres) { - TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); + TypeNode unresolved = NodeManager::currentNM()->mkSort( + name, NodeManager::SORT_FLAG_PLACEHOLDER); unres.insert(unresolved); return unresolved; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index bbb16dfd5..644d50a95 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -58,7 +58,7 @@ bool OpPosTrie::getOrMakeType(TypeNode tn, ss << "_" << std::to_string(op_pos[i]); } d_unres_tn = NodeManager::currentNM()->mkSort( - ss.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + ss.str(), NodeManager::SORT_FLAG_PLACEHOLDER); Trace("sygus-grammar-normalize-trie") << "\tCreating type " << d_unres_tn << "\n"; unres_tn = d_unres_tn; |