<< (idx) << ", expected "
/* -------------------------------------------------------------------------- */
-/* Solver checks. */
+/* Solver checks. */
/* -------------------------------------------------------------------------- */
/**
#define CVC4_API_ARG_CHECK_SOLVER(what, arg) \
CVC4_API_CHECK(this->d_solver == arg.d_solver) \
<< "Given " << (what) << " is not associated with the solver this " \
- << (what) \
- << " is " \
- "associated with";
+ << "object is associated with";
/* -------------------------------------------------------------------------- */
/* Sort checks. */
/**
* Sort check for member functions of classes other than class Solver.
* Check if given sort is not null and associated with the solver object this
- * Sort object is associated with.
+ * object is associated with.
*/
#define CVC4_API_CHECK_SORT(sort) \
do \
/**
* Sort check for member functions of classes other than class Solver.
* Check if each sort in the given container of sorts is not null and
- * associated with the solver object this Sort object is associated with.
+ * associated with the solver object this object is associated with.
*/
-#define CVC4_API_CHECK_SORTS(sorts) \
+#define CVC4_API_CHECK_SORTS(sorts) \
+ do \
+ { \
+ size_t i = 0; \
+ for (const auto& s : sorts) \
+ { \
+ CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \
+ this->d_solver == s.d_solver, "sort", sorts, i) \
+ << "a sort associated with the solver this object is associated " \
+ "with"; \
+ i += 1; \
+ } \
+ } while (0)
+
+/* -------------------------------------------------------------------------- */
+/* Term checks. */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Term check for member functions of classes other than class Solver.
+ * Check if given term is not null and associated with the solver object this
+ * object is associated with.
+ */
+#define CVC4_API_CHECK_TERM(term) \
+ do \
+ { \
+ CVC4_API_ARG_CHECK_NOT_NULL(term); \
+ CVC4_API_ARG_CHECK_SOLVER("term", term); \
+ } while (0)
+
+/**
+ * Term check for member functions of classes other than class Solver.
+ * Check if each term in the given container of terms is not null and
+ * associated with the solver object this object is associated with.
+ */
+#define CVC4_API_CHECK_TERMS(terms) \
+ do \
+ { \
+ size_t i = 0; \
+ for (const auto& s : terms) \
+ { \
+ CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", s, terms, i); \
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \
+ this->d_solver == s.d_solver, "term", terms, i) \
+ << "a term associated with the solver this object is associated " \
+ "with"; \
+ i += 1; \
+ } \
+ } while (0)
+
+/**
+ * Term check for member functions of classes other than class Solver.
+ * Check if each term and sort in the given map (which maps terms to sorts) is
+ * not null and associated with the solver object this object is associated
+ * with.
+ */
+#define CVC4_API_CHECK_TERMS_MAP(map) \
+ do \
+ { \
+ size_t i = 0; \
+ for (const auto& p : map) \
+ { \
+ CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", p.first, map, i); \
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \
+ this->d_solver == p.first.d_solver, "term", map, i) \
+ << "a term associated with the solver this object is associated " \
+ "with"; \
+ CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", p.second, map, i); \
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \
+ this->d_solver == p.second.d_solver, "sort", map, i) \
+ << "a sort associated with the solver this object is associated " \
+ "with"; \
+ i += 1; \
+ } \
+ } while (0)
+
+/**
+ * Term check for member functions of classes other than class Solver.
+ * Check if each term in the given container is not null, associated with the
+ * solver object this object is associated with, and of the given sort.
+ */
+#define CVC4_API_CHECK_TERMS_WITH_SORT(terms, sort) \
do \
{ \
size_t i = 0; \
- for (const auto& s : sorts) \
+ for (const auto& t : terms) \
{ \
- CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \
+ CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \
- this->d_solver == s.d_solver, "sort", sorts, i) \
- << "a sort associated with the solver this sort is associated with"; \
+ this->d_solver == t.d_solver, "term", terms, i) \
+ << "a term associated with the solver this object is associated " \
+ "with"; \
+ CVC4_API_CHECK(t.getSort() == sort) \
+ << "Expected term with sort " << sort << " at index " << i << " in " \
+ << #terms; \
i += 1; \
} \
} while (0)
+/* -------------------------------------------------------------------------- */
+/* DatatypeDecl checks. */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * DatatypeDecl check for member functions of classes other than class Solver.
+ * Check if given datatype declaration is not null and associated with the
+ * solver object this DatatypeDecl object is associated with.
+ */
+#define CVC4_API_CHECK_DTDECL(decl) \
+ do \
+ { \
+ CVC4_API_ARG_CHECK_NOT_NULL(decl); \
+ CVC4_API_ARG_CHECK_SOLVER("datatype declaration", decl); \
+ } while (0)
+
/* -------------------------------------------------------------------------- */
/* Checks for class Solver. */
/* -------------------------------------------------------------------------- */
void Grammar::addRule(const Term& ntSymbol, const Term& rule)
{
+ CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
"it as an argument to synthFun/synthInv";
- CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
- CVC4_API_ARG_CHECK_NOT_NULL(rule);
+ CVC4_API_CHECK_TERM(ntSymbol);
+ CVC4_API_CHECK_TERM(rule);
CVC4_API_ARG_CHECK_EXPECTED(
d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType())
<< "Expected ntSymbol and rule to have the same sort";
-
+ //////// all checks before this line
d_ntsToTerms[ntSymbol].push_back(rule);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
void Grammar::addRules(const Term& ntSymbol, const std::vector<Term>& rules)
{
+ CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
"it as an argument to synthFun/synthInv";
- CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
+ CVC4_API_CHECK_TERM(ntSymbol);
+ CVC4_API_CHECK_TERMS_WITH_SORT(rules, ntSymbol.getSort());
CVC4_API_ARG_CHECK_EXPECTED(
d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
-
- for (size_t i = 0, n = rules.size(); i < n; ++i)
- {
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- !rules[i].isNull(), "parameter rule", rules[i], i)
- << "non-null term";
- CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType())
- << "Expected ntSymbol and rule at index " << i
- << " to have the same sort";
- }
-
+ //////// all checks before this line
d_ntsToTerms[ntSymbol].insert(
d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend());
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
void Grammar::addAnyConstant(const Term& ntSymbol)
{
+ CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
"it as an argument to synthFun/synthInv";
- CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
+ CVC4_API_CHECK_TERM(ntSymbol);
CVC4_API_ARG_CHECK_EXPECTED(
d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
-
+ //////// all checks before this line
d_allowConst.insert(ntSymbol);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
void Grammar::addAnyVariable(const Term& ntSymbol)
{
+ CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
"it as an argument to synthFun/synthInv";
- CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
+ CVC4_API_CHECK_TERM(ntSymbol);
CVC4_API_ARG_CHECK_EXPECTED(
d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
-
+ //////// all checks before this line
d_allowVars.insert(ntSymbol);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
/**
std::string Grammar::toString() const
{
+ CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
std::stringstream ss;
ss << " (" // pre-declaration
<< join(
<< ')';
return ss.str();
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
Sort Grammar::resolve()
{
+ CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
+
d_isResolved = true;
Term bvl;
// return is the first datatype
return Sort(d_solver, datatypeTypes[0]);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
void Grammar::addSygusConstructorTerm(
const Term& term,
const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
{
+ CVC4_API_TRY_CATCH_BEGIN;
+ CVC4_API_CHECK_DTDECL(dt);
+ CVC4_API_CHECK_TERM(term);
+ CVC4_API_CHECK_TERMS_MAP(ntsToUnres);
+ //////// all checks before this line
+
// At this point, we should know that dt is well founded, and that its
// builtin sygus operators are well-typed.
// Now, purify each occurrence of a non-terminal symbol in term, replace by
}
std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs);
dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
Term Grammar::purifySygusGTerm(
std::vector<Sort>& cargs,
const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
{
+ CVC4_API_TRY_CATCH_BEGIN;
+ CVC4_API_CHECK_TERM(term);
+ CVC4_API_CHECK_TERMS(args);
+ CVC4_API_CHECK_SORTS(cargs);
+ CVC4_API_CHECK_TERMS_MAP(ntsToUnres);
+ //////// all checks before this line
+
std::unordered_map<Term, Sort, TermHashFunction>::const_iterator itn =
ntsToUnres.find(term);
if (itn != ntsToUnres.cend())
}
return Term(d_solver, nret);
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
void Grammar::addSygusConstructorVariables(DatatypeDecl& dt,
const Sort& sort) const
{
- Assert(!sort.isNull());
+ CVC4_API_TRY_CATCH_BEGIN;
+ CVC4_API_CHECK_DTDECL(dt);
+ CVC4_API_CHECK_SORT(sort);
+ //////// all checks before this line
+
// each variable of appropriate type becomes a sygus constructor in dt.
for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++)
{
dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs);
}
}
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
std::ostream& operator<<(std::ostream& out, const Grammar& g)
projects / cvc5.git / commitdiff