From: Aina Niemetz Date: Wed, 10 Mar 2021 23:27:17 +0000 (-0800) Subject: New C++ Api: Add missing argument checks in Solver functions. (#6094) X-Git-Tag: cvc5-1.0.0~2109 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=489209a31c2a2bf2f5ce465c1a79f73aad90c764;p=cvc5.git New C++ Api: Add missing argument checks in Solver functions. (#6094) This adds missing checks to guard that Term and Sort arguments are associated with the solver object that is called. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e27ba3b91..ea8165c4a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3408,6 +3408,7 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const Term Solver::getValueHelper(const Term& term) const { + // Note: Term is checked in the caller to avoid double checks Node value = d_smtEngine->getValue(*term.d_node); Term res = Term(this, value); // May need to wrap in real cast so that user know this is a real. @@ -3419,10 +3420,15 @@ Term Solver::getValueHelper(const Term& term) const return res; } +Sort Solver::mkTupleSortHelper(const std::vector& sorts) const +{ + // Note: Sorts are checked in the caller to avoid double checks + std::vector typeNodes = Sort::sortVectorToTypeNodes(sorts); + return Sort(this, getNodeManager()->mkTupleType(typeNodes)); +} + Term Solver::mkTermFromKind(Kind kind) const { - NodeManagerScope scope(getNodeManager()); - CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK_EXPECTED( kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; @@ -3442,14 +3448,10 @@ Term Solver::mkTermFromKind(Kind kind) const (void)res.getType(true); /* kick off type checking */ increment_term_stats(kind); return Term(this, res); - - CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTermHelper(Kind kind, const std::vector& children) const { - NodeManagerScope scope(getNodeManager()); - CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -3541,16 +3543,44 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const (void)res.getType(true); /* kick off type checking */ increment_term_stats(kind); return Term(this, res); - CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::mkTermHelper(const Op& op, const std::vector& children) const +{ + CVC4_API_SOLVER_CHECK_OP(op); + + if (!op.isIndexedHelper()) + { + return mkTermHelper(op.d_kind, children); + } + + for (size_t i = 0, size = children.size(); i < size; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !children[i].isNull(), "child term", children[i], i) + << "non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == children[i].d_solver, "child term", children[i], i) + << "child term associated to this solver object"; + } + checkMkTerm(op.d_kind, children.size()); + + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + std::vector echildren = Term::termVectorToNodes(children); + + NodeBuilder<> nb(int_kind); + nb << *op.d_node; + nb.append(echildren); + Node res = nb.constructNode(); + + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); } std::vector Solver::mkDatatypeSortsInternal( const std::vector& dtypedecls, const std::set& unresolvedSorts) const { - NodeManagerScope scope(getNodeManager()); - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector datatypes; for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) { @@ -3566,9 +3596,16 @@ std::vector Solver::mkDatatypeSortsInternal( << "a datatype declaration with at least one constructor"; datatypes.push_back(dtypedecls[i].getDatatype()); } + size_t i = 0; for (auto& sort : unresolvedSorts) { - CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !sort.isNull(), "unresolved sort", sort, i) + << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sort.d_solver, "unresolved sort", sort, i) + << "an unresolved sort associated to this solver object"; + i += 1; } std::set utypes = Sort::sortSetToTypeNodes(unresolvedSorts); @@ -3576,8 +3613,6 @@ std::vector Solver::mkDatatypeSortsInternal( getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes); std::vector retTypes = Sort::typeNodeVectorToSorts(this, dtypes); return retTypes; - - CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::synthFunHelper(const std::string& symbol, @@ -3586,7 +3621,6 @@ Term Solver::synthFunHelper(const std::string& symbol, bool isInv, Grammar* g) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(sort); std::vector varTypes; @@ -3628,12 +3662,11 @@ Term Solver::synthFunHelper(const std::string& symbol, fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); return Term(this, fun); - - CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::ensureTermSort(const Term& term, const Sort& sort) const { + // Note: Term and sort are checked in the caller to avoid double checks CVC4_API_CHECK(term.getSort() == sort || (term.getSort().isInteger() && sort.isReal())) << "Expected conversion from Int to Real"; @@ -3662,6 +3695,20 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const return res; } +Term Solver::ensureRealSort(const Term& t) const +{ + Assert(this == t.d_solver); + CVC4_API_ARG_CHECK_EXPECTED( + t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), + " an integer or real term"); + if (t.getSort() == getIntegerSort()) + { + Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node); + return Term(this, n); + } + return t; +} + bool Solver::isValidInteger(const std::string& s) const { if (s.length() == 0) @@ -3851,6 +3898,7 @@ Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const std::vector Solver::mkDatatypeSorts( const std::vector& dtypedecls) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::set unresolvedSorts; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); @@ -3861,6 +3909,7 @@ std::vector Solver::mkDatatypeSorts( const std::vector& dtypedecls, const std::set& unresolvedSorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4053,8 +4102,7 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) << "non-function-like sort as parameter sort for tuple sort"; } - std::vector typeNodes = Sort::sortVectorToTypeNodes(sorts); - return Sort(this, getNodeManager()->mkTupleType(typeNodes)); + return mkTupleSortHelper(sorts); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4128,19 +4176,6 @@ Term Solver::mkReal(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::ensureRealSort(const Term& t) const -{ - CVC4_API_ARG_CHECK_EXPECTED( - t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), - " an integer or real term"); - if (t.getSort() == getIntegerSort()) - { - Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node); - return Term(this, n); - } - return t; -} - Term Solver::mkReal(int64_t val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4236,7 +4271,7 @@ Term Solver::mkString(const unsigned char c) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkString(const std::vector& s) const +Term Solver::mkString(const std::vector& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper(CVC4::String(s)); @@ -4522,7 +4557,9 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return DatatypeDecl(this, name, isCoDatatype); + CVC4_API_SOLVER_TRY_CATCH_END; } DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, @@ -4530,7 +4567,11 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(param); + CVC4_API_SOLVER_CHECK_SORT(param); return DatatypeDecl(this, name, param, isCoDatatype); + CVC4_API_SOLVER_TRY_CATCH_END; } DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, @@ -4538,7 +4579,18 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + for (size_t i = 0, size = params.size(); i < size; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !params[i].isNull(), "parameter sort", params[i], i) + << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == params[i].d_solver, "parameter sort", params[i], i) + << "sort associated to this solver object"; + } return DatatypeDecl(this, name, params, isCoDatatype); + CVC4_API_SOLVER_TRY_CATCH_END; } /* Create terms */ @@ -4546,6 +4598,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, Term Solver::mkTerm(Kind kind) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermFromKind(kind); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4553,12 +4606,18 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, const Term& child) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(kind, std::vector{child}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(kind, std::vector{child1, child2}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, @@ -4566,13 +4625,19 @@ Term Solver::mkTerm(Kind kind, const Term& child2, const Term& child3) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; // need to use internal term call to check e.g. associative construction return mkTermHelper(kind, std::vector{child1, child2, child3}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, const std::vector& children) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(kind, children); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(const Op& op) const @@ -4598,12 +4663,18 @@ Term Solver::mkTerm(const Op& op) const Term Solver::mkTerm(const Op& op, const Term& child) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(op, std::vector{child}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(op, std::vector{child1, child2}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(const Op& op, @@ -4611,46 +4682,17 @@ Term Solver::mkTerm(const Op& op, const Term& child2, const Term& child3) const { + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkTermHelper(op, std::vector{child1, child2, child3}); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(const Op& op, const std::vector& children) const { - return mkTermHelper(op, children); -} - -Term Solver::mkTermHelper(const Op& op, const std::vector& children) const -{ - if (!op.isIndexedHelper()) - { - return mkTermHelper(op.d_kind, children); - } - NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_SOLVER_CHECK_OP(op); - checkMkTerm(op.d_kind, children.size()); - for (size_t i = 0, size = children.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "child term", children[i], i) - << "non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == children[i].d_solver, "child term", children[i], i) - << "child term associated to this solver object"; - } - - const CVC4::Kind int_kind = extToIntKind(op.d_kind); - std::vector echildren = Term::termVectorToNodes(children); - - NodeBuilder<> nb(int_kind); - nb << *op.d_node; - nb.append(echildren); - Node res = nb.constructNode(); - - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - + return mkTermHelper(op, children); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4664,6 +4706,12 @@ Term Solver::mkTuple(const std::vector& sorts, std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !sorts[i].isNull(), "sort", sorts[i], i) + << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !terms[i].isNull(), "term", terms[i], i) + << "non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == terms[i].d_solver, "child term", terms[i], i) << "child term associated to this solver object"; @@ -4673,7 +4721,7 @@ Term Solver::mkTuple(const std::vector& sorts, args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); } - Sort s = mkTupleSort(sorts); + Sort s = mkTupleSortHelper(sorts); Datatype dt = s.getDatatype(); NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR)); nb << *dt[0].getConstructorTerm().d_node; @@ -5144,6 +5192,7 @@ Term Solver::defineFun(const std::string& symbol, domain_types.push_back(t); } CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -5283,6 +5332,7 @@ Term Solver::defineFunRec(const Term& fun, << "recursive function definitions require a logic with uninterpreted " "functions"; + CVC4_API_SOLVER_CHECK_TERM(fun); if (fun.getSort().isFunction()) { std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); @@ -5356,7 +5406,8 @@ void Solver::defineFunsRec(const std::vector& funs, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == fun.d_solver, "function", fun, j) << "function associated to this solver object"; - CVC4_API_SOLVER_CHECK_TERM(term); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == term.d_solver, "term", term, j) + << "term associated to this solver object"; if (fun.getSort().isFunction()) { @@ -5575,6 +5626,8 @@ void Solver::declareSeparationHeap(const Sort& locSort, const Sort& dataSort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_SORT(locSort); + CVC4_API_SOLVER_CHECK_SORT(dataSort); CVC4_API_CHECK( d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " @@ -5585,12 +5638,12 @@ void Solver::declareSeparationHeap(const Sort& locSort, Term Solver::getSeparationHeap() const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK( d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - NodeManagerScope scope(getNodeManager()); CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; @@ -5602,12 +5655,12 @@ Term Solver::getSeparationHeap() const Term Solver::getSeparationNilTerm() const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK( d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - NodeManagerScope scope(getNodeManager()); CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; @@ -5622,8 +5675,8 @@ Term Solver::getSeparationNilTerm() const */ void Solver::pop(uint32_t nscopes) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot pop when not solving incrementally (use --incremental)"; CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) @@ -5639,8 +5692,9 @@ void Solver::pop(uint32_t nscopes) const bool Solver::getInterpolant(const Term& conj, Term& output) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(conj); Node result; bool success = d_smtEngine->getInterpol(*conj.d_node, result); if (success) @@ -5653,8 +5707,9 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const bool Solver::getInterpolant(const Term& conj, Grammar& g, Term& output) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(conj); Node result; bool success = d_smtEngine->getInterpol(*conj.d_node, *g.resolve().d_type, result); @@ -5668,8 +5723,9 @@ bool Solver::getInterpolant(const Term& conj, Grammar& g, Term& output) const bool Solver::getAbduct(const Term& conj, Term& output) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(conj); Node result; bool success = d_smtEngine->getAbduct(*conj.d_node, result); if (success) @@ -5682,8 +5738,9 @@ bool Solver::getAbduct(const Term& conj, Term& output) const bool Solver::getAbduct(const Term& conj, Grammar& g, Term& output) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(conj); Node result; bool success = d_smtEngine->getAbduct(*conj.d_node, *g.resolve().d_type, result); @@ -5885,7 +5942,9 @@ Term Solver::synthFun(const std::string& symbol, const std::vector& boundVars, const Sort& sort) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return synthFunHelper(symbol, boundVars, sort); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::synthFun(const std::string& symbol, @@ -5893,28 +5952,34 @@ Term Solver::synthFun(const std::string& symbol, Sort sort, Grammar& g) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return synthFunHelper(symbol, boundVars, sort, false, &g); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::synthInv(const std::string& symbol, const std::vector& boundVars) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return synthFunHelper( symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::synthInv(const std::string& symbol, const std::vector& boundVars, Grammar& g) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return synthFunHelper( symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true, &g); + CVC4_API_SOLVER_TRY_CATCH_END; } void Solver::addSygusConstraint(const Term& term) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_EXPECTED( diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 938449f3f..77a2378de 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2784,7 +2784,7 @@ class CVC4_PUBLIC Solver * @param s a list of unsigned values this constant represents as string * @return the String constant */ - Term mkString(const std::vector& s) const; + Term mkString(const std::vector& s) const; /** * Create a character constant from a given string. @@ -3573,6 +3573,8 @@ class CVC4_PUBLIC Solver uint32_t base) const; /** Helper for mkBitVector functions that take an integer as argument. */ Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; + /** Helper for functions that create tuple sorts. */ + Sort mkTupleSortHelper(const std::vector& sorts) const; /** Helper for mkTerm functions that create Term from a Kind */ Term mkTermFromKind(Kind kind) const; /** Helper for mkChar functions that take a string as argument. */