diff options
23 files changed, 72 insertions, 115 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 621e3c1c0..e845bf876 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3730,7 +3730,7 @@ Sort Solver::mkParamSort(const std::string& symbol) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort( this, - getNodeManager()->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER)); + getNodeManager()->mkSort(symbol, NodeManager::SORT_FLAG_PLACEHOLDER)); CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 37f0e2527..43161fe04 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -679,18 +679,20 @@ Type ExprManager::getType(Expr expr, bool check) return t; } -Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) { +Expr ExprManager::mkVar(const std::string& name, Type type) +{ NodeManagerScope nms(d_nodeManager); - Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags); + Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); Debug("nm") << "set " << name << " on " << *n << std::endl; INC_STAT_VAR(type, false); return Expr(this, n); } -Expr ExprManager::mkVar(Type type, uint32_t flags) { +Expr ExprManager::mkVar(Type type) +{ NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type, false); - return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags)); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); } Expr ExprManager::mkBoundVar(const std::string& name, Type type) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 1458101ca..f1386b84d 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -352,19 +352,13 @@ class CVC4_PUBLIC ExprManager { /** Make the type of sequence with the given parameterization. */ SequenceType mkSequenceType(Type elementType) const; - /** Bits for use in mkSort() flags. */ - enum { - SORT_FLAG_NONE = 0, - SORT_FLAG_PLACEHOLDER = 1 - };/* enum */ - /** Make a new sort with the given name. */ - SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const; + SortType mkSort(const std::string& name, uint32_t flags) const; /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, size_t arity, - uint32_t flags = SORT_FLAG_NONE) const; + uint32_t flags) const; /** * Get the type of an expression. @@ -374,13 +368,6 @@ class CVC4_PUBLIC ExprManager { */ Type getType(Expr e, bool check = false); - /** Bits for use in mkVar() flags. */ - enum { - VAR_FLAG_NONE = 0, - VAR_FLAG_GLOBAL = 1, - VAR_FLAG_DEFINED = 2 - };/* enum */ - /** * Create a new, fresh variable. This variable is guaranteed to be * distinct from every variable thus far in the ExprManager, even @@ -390,33 +377,16 @@ class CVC4_PUBLIC ExprManager { * * @param name a name to associate to the fresh new variable * @param type the type for the new variable - * @param flags - VAR_FLAG_NONE - no flags; - * VAR_FLAG_GLOBAL - whether this variable is to be - * considered "global" or not. Note that this information isn't - * used by the ExprManager, but is passed on to the ExprManager's - * event subscribers like the model-building service; if isGlobal - * is true, this newly-created variable will still available in - * models generated after an intervening pop. - * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for - * use with SmtEngine::defineFunction(). This keeps a declaration - * from being emitted in API dumps (since a subsequent definition is - * expected to be dumped instead). */ - Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE); + Expr mkVar(const std::string& name, Type type); /** * Create a (nameless) new, fresh variable. This variable is guaranteed * to be distinct from every variable thus far in the ExprManager. * * @param type the type for the new variable - * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global" - * or not. Note that this information isn't used by the ExprManager, - * but is passed on to the ExprManager's event subscribers like the - * model-building service; if isGlobal is true, this newly-created - * variable will still available in models generated after an - * intervening pop. - */ - Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE); + */ + Expr mkVar(Type type); /** * Create a new, fresh variable for use in a binder expression diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f9a743cf6..67ceaf89c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -208,16 +208,11 @@ private: NodeManagerScope to_nms(to_nm); to_e = nn.toExpr(); } else if(n.getKind() == kind::VARIABLE) { - bool isGlobal; - Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal); - // Temporarily set the node manager to nullptr; this gets around // a check that mkVar isn't called internally NodeManagerScope nullScope(nullptr); to_e = d_to->mkVar(name, - type, - isGlobal ? ExprManager::VAR_FLAG_GLOBAL - : d_flags); // FIXME thread safety + type); // FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { // skolems are only available at the Node level (not the Expr level) TypeNode typeNode = TypeNode::fromType(type); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 540e02979..59afec4a6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -904,27 +904,26 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, return type; } -Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) { +Node NodeManager::mkVar(const std::string& name, const TypeNode& type) +{ Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); - setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, flags); + (*i)->nmNotifyNewVar(n); } return n; } -Node* NodeManager::mkVarPtr(const std::string& name, - const TypeNode& type, uint32_t flags) { +Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) +{ Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); - setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, flags); + (*i)->nmNotifyNewVar(*n); } return n; } @@ -1048,24 +1047,24 @@ Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children) return mkNode(kind::AND, cchildren); } -Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) { +Node NodeManager::mkVar(const TypeNode& type) +{ Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); - setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, flags); + (*i)->nmNotifyNewVar(n); } return n; } -Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) { +Node* NodeManager::mkVarPtr(const TypeNode& type) +{ Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); - setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, flags); + (*i)->nmNotifyNewVar(*n); } return n; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1e70dd766..89cd61e09 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -71,7 +71,7 @@ class NodeManagerListener { uint32_t flags) { } - virtual void nmNotifyNewVar(TNode n, uint32_t flags) {} + virtual void nmNotifyNewVar(TNode n) {} virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) {} /** @@ -89,8 +89,8 @@ class NodeManager { friend class expr::TypeChecker; // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags); - friend Expr ExprManager::mkVar(Type, uint32_t flags); + friend Expr ExprManager::mkVar(const std::string&, Type); + friend Expr ExprManager::mkVar(Type); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { @@ -373,12 +373,12 @@ class NodeManager { * version of this is private to avoid internal uses of mkVar() from * within CVC4. Such uses should employ mkSkolem() instead. */ - Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); - Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node mkVar(const std::string& name, const TypeNode& type); + Node* mkVarPtr(const std::string& name, const TypeNode& type); /** Create a variable with the given type. */ - Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); - Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node mkVar(const TypeNode& type); + Node* mkVarPtr(const TypeNode& type); public: @@ -1032,21 +1032,28 @@ class NodeManager { /** Make a type representing a tester with given parameterization */ inline TypeNode mkTesterType(TypeNode domain); + /** Bits for use in mkSort() flags. */ + enum + { + SORT_FLAG_NONE = 0, + SORT_FLAG_PLACEHOLDER = 1 + }; /* enum */ + /** Make a new (anonymous) sort of arity 0. */ - TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE); + TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE); /** Make a new sort with the given name of arity 0. */ - TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE); + TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE); /** Make a new sort by parameterizing the given sort constructor. */ TypeNode mkSort(TypeNode constructor, const std::vector<TypeNode>& children, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + uint32_t flags = SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ TypeNode mkSortConstructor(const std::string& name, size_t arity, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + uint32_t flags = SORT_FLAG_NONE); /** * Get the type for the given node and optionally do type checking. diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index ba8df6fd0..ba19a3bbb 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -26,14 +26,12 @@ namespace expr { // TODO: hide this attribute behind a NodeManager interface. namespace attr { struct VarNameTag { }; - struct GlobalVarTag { }; struct SortArityTag { }; struct TypeTag { }; struct TypeCheckedTag { }; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; -typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr; typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr; diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 0bb386697..23a17c939 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -156,7 +156,7 @@ MipLibTrick::~MipLibTrick() } } -void MipLibTrick::nmNotifyNewVar(TNode n, uint32_t flags) +void MipLibTrick::nmNotifyNewVar(TNode n) { if (n.getType().isBoolean()) { diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index d3cf9da53..f7be87f18 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -32,7 +32,7 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener ~MipLibTrick(); // NodeManagerListener callbacks to collect d_boolVars. - void nmNotifyNewVar(TNode n, uint32_t flags) override; + void nmNotifyNewVar(TNode n) override; void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) override; diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index ecf1e281d..7b54fee61 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -252,7 +252,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::stringstream ss; ss << "T" << i; std::string tname = ss.str(); - TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER); + TypeNode tnu = nm->mkSort(tname, NodeManager::SORT_FLAG_PLACEHOLDER); cterm_to_utype[ct] = tnu; unres.insert(tnu); sdts.push_back(SygusDatatype(tname)); diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index ea0d1b267..ab792f6fe 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -20,7 +20,6 @@ #include <typeinfo> #include <vector> -#include "expr/expr.h" // for ExprSetDepth etc.. #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" #include "options/language.h" // for LANG_AST diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 706c2e886..77f5f7d0d 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -49,12 +49,9 @@ void DumpManager::resetAssertions() // currently, do nothing } -void DumpManager::addToModelCommandAndDump(const NodeCommand& c, - uint32_t flags, - bool userVisible, - const char* dumpTag) +void DumpManager::addToDump(const NodeCommand& c, const char* dumpTag) { - Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl; + Trace("smt") << "SMT addToDump(" << c << ")" << std::endl; if (Dump.isOn(dumpTag)) { if (d_fullyInited) diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 3238d3a8d..192bb2324 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -49,13 +49,10 @@ class DumpManager */ void resetAssertions(); /** - * Add to Model command. This is used for recording a command - * that should be reported during a get-model call. + * Add to dump command. This is used for recording a command + * that should be reported via the dumpTag trace. */ - void addToModelCommandAndDump(const NodeCommand& c, - uint32_t flags = 0, - bool userVisible = true, - const char* dumpTag = "declarations"); + void addToDump(const NodeCommand& c, const char* dumpTag = "declarations"); /** * Set that function f should print in the model if and only if p is true. diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 356cfa8a6..0347a24ef 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -45,9 +45,9 @@ SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm, void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) { DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn); - if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) + if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0) { - d_dm.addToModelCommandAndDump(c, flags); + d_dm.addToDump(c); } } @@ -57,9 +57,9 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn, DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn); - if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) + if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0) { - d_dm.addToModelCommandAndDump(c); + d_dm.addToDump(c); } } @@ -76,18 +76,15 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes( } } DeclareDatatypeNodeCommand c(dtts); - d_dm.addToModelCommandAndDump(c); + d_dm.addToDump(c); } } -void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags) +void SmtNodeManagerListener::nmNotifyNewVar(TNode n) { DeclareFunctionNodeCommand c( n.getAttribute(expr::VarNameAttr()), n, n.getType()); - if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) - { - d_dm.addToModelCommandAndDump(c, flags); - } + d_dm.addToDump(c); } void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, @@ -101,10 +98,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(), id + " is " + comment); } - if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) - { - d_dm.addToModelCommandAndDump(c, flags, false, "skolems"); - } + d_dm.addToDump(c, "skolems"); } } // namespace smt diff --git a/src/smt/listeners.h b/src/smt/listeners.h index ce174e872..d586dfe75 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -59,7 +59,7 @@ class SmtNodeManagerListener : public NodeManagerListener void nmNotifyNewDatatypes(const std::vector<TypeNode>& dtts, uint32_t flags) override; /** Notify when new variable is created */ - void nmNotifyNewVar(TNode n, uint32_t flags) override; + void nmNotifyNewVar(TNode n) override; /** Notify when new skolem is created */ void nmNotifyNewSkolem(TNode n, const std::string& comment, diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d89b6e802..6f775f6b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -675,8 +675,7 @@ void SmtEngine::defineFunction(Node func, } DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula); - d_dumpm->addToModelCommandAndDump( - nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); + d_dumpm->addToDump(nc, "declarations"); // type check body debugCheckFunctionBody(formula, formals, func); diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 1b251f8e0..6bb473f87 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -21,7 +21,6 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "expr/expr.h" #include "theory/rewriter.h" #include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index f99f58969..60bf36139 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -670,7 +670,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, std::stringstream ssutn0; ssutn0 << sdtd.getName() << "_s"; TypeNode abdTNew = - nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER); unres.insert(abdTNew); dtProcessed[sdt] = abdTNew; @@ -712,7 +712,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, std::stringstream ssutn; ssutn << argt.getDType().getName() << "_s"; argtNew = - nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER); Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew << " for " << argt << std::endl; unres.insert(argtNew); 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; diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 9f5ffdf3e..40a8b58dc 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -203,7 +203,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { } void testUndefinedSorts() { - Type foo = d_em->mkSort("foo"); + Type foo = d_em->mkSort("foo", NodeManager::SORT_FLAG_NONE); // We've currently assigned them a specific Beth number, which // isn't really correct, but... TS_ASSERT( !foo.getCardinality().isFinite() ); diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 5fe277520..9909a8a7b 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -243,10 +243,10 @@ class DatatypeBlack : public CxxTest::TestSuite { */ std::set<TypeNode> unresolvedTypes; TypeNode unresList = - d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER); + d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER); unresolvedTypes.insert(unresList); TypeNode unresTree = - d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER); + d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER); unresolvedTypes.insert(unresTree); DType tree("tree"); @@ -309,10 +309,10 @@ class DatatypeBlack : public CxxTest::TestSuite { { std::set<TypeNode> unresolvedTypes; TypeNode unresList = - d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER); + d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER); unresolvedTypes.insert(unresList); TypeNode unresTree = - d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER); + d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER); unresolvedTypes.insert(unresTree); DType tree("tree"); |