}
}
-std::set<internal::TypeNode> Sort::sortSetToTypeNodes(
- const std::set<Sort>& sorts)
-{
- std::set<internal::TypeNode> types;
- for (const Sort& s : sorts)
- {
- types.insert(s.getTypeNode());
- }
- return types;
-}
-
std::vector<internal::TypeNode> Sort::sortVectorToTypeNodes(
const std::vector<Sort>& sorts)
{
{
}
-DatatypeDecl::DatatypeDecl(const Solver* slv,
- const std::string& name,
- const Sort& param,
- bool isCoDatatype)
- : d_solver(slv),
- d_dtype(new internal::DType(
- name, std::vector<internal::TypeNode>{*param.d_type}, isCoDatatype))
-{
-}
-
DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
const std::vector<Sort>& params,
/** @return The internal wrapped TypeNode of this sort. */
const internal::TypeNode& getTypeNode(void) const;
- /** Helper to convert a set of Sorts to internal TypeNodes. */
- std::set<internal::TypeNode> static sortSetToTypeNodes(
- const std::set<Sort>& sorts);
/** Helper to convert a vector of Sorts to internal TypeNodes. */
std::vector<internal::TypeNode> static sortVectorToTypeNodes(
const std::vector<Sort>& sorts);
const std::string& name,
bool isCoDatatype = false);
- /**
- * Constructor for parameterized datatype declaration.
- * Create sorts parameter with Solver::mkParamSort().
- * @param slv The associated solver object.
- * @param name The name of the datatype.
- * @param param The sort parameter.
- * @param isCoDatatype True if a codatatype is to be constructed.
- */
- DatatypeDecl(const Solver* slv,
- const std::string& name,
- const Sort& param,
- bool isCoDatatype = false);
-
/**
* Constructor for parameterized datatype declaration.
* Create sorts parameter with Solver::mkParamSort().