This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.
After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.
d_constructors.push_back(c);
}
+void DType::addSygusConstructor(Node op,
+ const std::string& cname,
+ const std::vector<TypeNode>& cargs,
+ int weight)
+{
+ // avoid name clashes
+ std::stringstream ss;
+ ss << getName() << "_" << getNumConstructors() << "_" << cname;
+ std::string name = ss.str();
+ unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
+ std::shared_ptr<DTypeConstructor> c =
+ std::make_shared<DTypeConstructor>(name, cweight);
+ c->setSygus(op);
+ for (size_t j = 0, nargs = cargs.size(); j < nargs; j++)
+ {
+ std::stringstream sname;
+ sname << name << "_" << j;
+ c->addArg(sname.str(), cargs[j]);
+ }
+ addConstructor(c);
+}
+
void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll)
{
Assert(!d_resolved);
// ----------------------- end datatype attributes
class NodeManager;
-
class Datatype;
/**
* be unique; they are for convenience and pretty-printing only.
*/
void addConstructor(std::shared_ptr<DTypeConstructor> c);
+ /** add sygus constructor
+ *
+ * This adds a sygus constructor to this datatype, where
+ * this datatype should be currently unresolved. Note this method is
+ * syntactic sugar for adding a normal constructor and setting it to be a
+ * sygus constructor, and following a naming convention that avoids
+ * constructors with the same name.
+ *
+ * @param op : the builtin operator, constant, or variable that this
+ * constructor encodes
+ * @param cname the name of the constructor (for printing only)
+ * @param cargs the arguments of the constructor.
+ * It should be the case that cargs are sygus datatypes that
+ * encode the arguments of op. For example, a sygus constructor
+ * with op = PLUS should be such that cargs.size()>=2 and
+ * the sygus type of cargs[i] is Real/Int for each i.
+ * @param weight denotes the value added by the constructor when computing the
+ * size of datatype terms. Passing a value < 0 denotes the default weight for
+ * the constructor, which is 0 for nullary constructors and 1 for non-nullary
+ * constructors.
+ */
+ void addSygusConstructor(Node op,
+ const std::string& cname,
+ const std::vector<TypeNode>& cargs,
+ int weight = -1);
/** set sygus
*
addArg(a);
}
-std::string DTypeConstructor::getName() const { return d_name; }
+const std::string& DTypeConstructor::getName() const { return d_name; }
Node DTypeConstructor::getConstructor() const
{
TypeNode returnType) const
{
Assert(isResolved());
- Assert(returnType.isDatatype());
+ Assert(returnType.isDatatype())
+ << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
+ "got "
+ << returnType;
const DType& dt = DType::datatypeOf(d_constructor);
Assert(dt.isParametric());
TypeNode dtt = dt.getTypeNode();
arg->d_selector.setAttribute(DTypeIndexAttr(), index++);
arg->d_resolved = true;
argTypes.push_back(range);
+ // We use \0 as a distinguished marker for unresolved selectors for doing
+ // name resolutions. We now can remove \0 from name if necessary.
+ const size_t nul = arg->d_name.find('\0');
+ if (nul != std::string::npos)
+ {
+ arg->d_name.resize(nul);
+ }
}
Assert(index == getNumArgs());
void addArgSelf(std::string selectorName);
/** Get the name of this constructor. */
- std::string getName() const;
+ const std::string& getName() const;
/**
* Get the constructor operator of this constructor. The
Assert(name != "");
}
-std::string DTypeSelector::getName() const { return d_name; }
+const std::string& DTypeSelector::getName() const { return d_name; }
Node DTypeSelector::getSelector() const
{
TypeNode t;
if (d_resolved)
{
- t = getRangeType();
+ // don't try to print the range type of null, instead we print null itself.
+ if (!getType().isNull())
+ {
+ t = getRangeType();
+ }
}
else if (d_selector.isNull())
{
DTypeSelector(std::string name, Node selector);
/** Get the name of this constructor argument. */
- std::string getName() const;
+ const std::string& getName() const;
/**
* Get the selector for this constructor argument; this call is
paramTypes,
paramReplacements);
}
+ // Check the datatype has been resolved properly.
+ for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ const DTypeConstructor& c = dt[i];
+ TypeNode testerType CVC4_UNUSED = c.getTester().getType();
+ Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut)
+ << "malformed tester in datatype post-resolution";
+ TypeNode ctorType CVC4_UNUSED = c.getConstructor().getType();
+ Assert(ctorType.isConstructor()
+ && ctorType.getNumChildren() == c.getNumArgs() + 1
+ && ctorType.getRangeType() == ut)
+ << "malformed constructor in datatype post-resolution";
+ // for all selectors...
+ for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+ {
+ const DTypeSelector& a = c[j];
+ TypeNode selectorType = a.getType();
+ Assert(a.isResolved() && selectorType.isSelector()
+ && selectorType[0] == ut)
+ << "malformed selector in datatype post-resolution";
+ // This next one's a "hard" check, performed in non-debug builds
+ // as well; the other ones should all be guaranteed by the
+ // CVC4::DType class, but this actually needs to be checked.
+ AlwaysAssert(!selectorType.getRangeType().isFunctionLike())
+ << "cannot put function-like things in datatypes";
+ }
+ }
}
for (NodeManagerListener* nml : d_listeners)