summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp2
-rw-r--r--src/expr/expr_manager_template.cpp10
-rw-r--r--src/expr/expr_manager_template.h40
-rw-r--r--src/expr/expr_template.cpp7
-rw-r--r--src/expr/node_manager.cpp25
-rw-r--r--src/expr/node_manager.h29
-rw-r--r--src/expr/node_manager_attributes.h2
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp2
-rw-r--r--src/preprocessing/passes/miplib_trick.h2
-rw-r--r--src/preprocessing/passes/synth_rew_rules.cpp2
-rw-r--r--src/printer/ast/ast_printer.cpp1
-rw-r--r--src/smt/dump_manager.cpp7
-rw-r--r--src/smt/dump_manager.h9
-rw-r--r--src/smt/listeners.cpp22
-rw-r--r--src/smt/listeners.h2
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h1
-rw-r--r--src/theory/datatypes/sygus_datatype_utils.cpp4
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp3
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.cpp2
21 files changed, 67 insertions, 110 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback