From f6bd42406897e165f2c9faffd69ab8db0204004f Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 20 Apr 2020 22:07:42 -0500 Subject: [PATCH] Introduce a public interface for Sygus commands. (#4204) This commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API. --- examples/api/CMakeLists.txt | 2 + examples/api/sygus-fun.cpp | 134 ++++++++++ examples/api/sygus-inv.cpp | 89 +++++++ src/api/cvc4cpp.cpp | 474 ++++++++++++++++++++++++++++++++-- src/api/cvc4cpp.h | 265 ++++++++++++++++++- test/unit/api/CMakeLists.txt | 1 + test/unit/api/grammar_black.h | 119 +++++++++ test/unit/api/solver_black.h | 204 ++++++++++++++- 8 files changed, 1271 insertions(+), 17 deletions(-) create mode 100644 examples/api/sygus-fun.cpp create mode 100644 examples/api/sygus-inv.cpp create mode 100644 test/unit/api/grammar_black.h diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index b121c8833..e4ef4ee78 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -17,6 +17,8 @@ set(CVC4_EXAMPLES_API sets-new strings strings-new + sygus-fun + sygus-inv ) foreach(example ${CVC4_EXAMPLES_API}) diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp new file mode 100644 index 000000000..d6437afa3 --- /dev/null +++ b/examples/api/sygus-fun.cpp @@ -0,0 +1,134 @@ +/********************* */ +/*! \file sygus-fun.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the Sygus API. + ** + ** A simple demonstration of how to use the Sygus API to synthesize max and min + ** functions. Here is the same problem written in Sygus V2 format: + ** + ** (set-logic LIA) + ** + ** (synth-fun max ((x Int) (y Int)) Int + ** ((Start Int) (StartBool Bool)) + ** ((Start Int (0 1 x y + ** (+ Start Start) + ** (- Start Start) + ** (ite StartBool Start Start))) + ** (StartBool Bool ((and StartBool StartBool) + ** (not StartBool) + ** (<= Start Start))))) + ** + ** (synth-fun min ((x Int) (y Int)) Int) + ** + ** (declare-var x Int) + ** (declare-var y Int) + ** + ** (constraint (>= (max x y) x)) + ** (constraint (>= (max x y) y)) + ** (constraint (or (= x (max x y)) + ** (= y (max x y)))) + ** (constraint (= (+ (max x y) (min x y)) + ** (+ x y))) + ** + ** (check-synth) + ** + ** The printed output to this example should be equivalent to: + ** (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + ** (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + **/ + +#include + +#include + +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + // declare input variables for the function-to-synthesize + Term x = slv.mkVar(integer, "x"); + Term y = slv.mkVar(integer, "y"); + + // declare the grammar non-terminals + Term start = slv.mkVar(integer, "Start"); + Term start_bool = slv.mkVar(boolean, "StartBool"); + + // define the rules + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); + + Term plus = slv.mkTerm(PLUS, start, start); + Term minus = slv.mkTerm(PLUS, start, start); + Term ite = slv.mkTerm(ITE, start_bool, start, start); + + Term And = slv.mkTerm(AND, start_bool, start_bool); + Term Not = slv.mkTerm(NOT, start_bool); + Term leq = slv.mkTerm(LEQ, start, start); + + // create the grammar object + Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool}); + + // bind each non-terminal to its rules + g.addRules(start, {zero, one, x, y, plus, minus, ite}); + g.addRules(start_bool, {And, Not, leq}); + + // declare the function-to-synthesize. Optionally, provide the grammar + // constraints + Term max = slv.synthFun("max", {x, y}, integer, g); + Term min = slv.synthFun("min", {x, y}, integer); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + Term varY = slv.mkSygusVar(integer, "y"); + + Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY); + Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY); + + // add logical constraints + // (constraint (>= (max x y) x)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX)); + + // (constraint (>= (max x y) y)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); + + // (constraint (or (= x (max x y)) + // (= y (max x y)))) + slv.addSygusConstraint(slv.mkTerm( + OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY))); + + // (constraint (= (+ (max x y) (min x y)) + // (+ x y))) + slv.addSygusConstraint(slv.mkTerm( + EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + slv.printSynthSolution(std::cout); + } + + return 0; +} diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp new file mode 100644 index 000000000..061ad8c1f --- /dev/null +++ b/examples/api/sygus-inv.cpp @@ -0,0 +1,89 @@ +/********************* */ +/*! \file sygus-inv.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the Sygus API. + ** + ** A simple demonstration of how to use the Sygus API to synthesize a simple + ** invariant. Here is the same problem written in Sygus V2 format: + ** + ** (set-logic LIA) + ** + ** (synth-inv inv-f ((x Int))) + ** + ** (define-fun pre-f ((x Int)) Bool + ** (= x 0)) + ** (define-fun trans-f ((x Int) (xp Int)) Bool + ** (ite (< x 10) (= xp (+ x 1)) (= xp x))) + ** (define-fun post-f ((x Int)) Bool + ** (<= x 10)) + ** + ** (inv-constraint inv-f pre-f trans-f post-f) + ** + ** (check-synth) + ** + ** The printed output to this example should be equivalent to: + ** (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + **/ + +#include + +#include + +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); + Term ten = slv.mkReal(10); + + // declare input variables for functions + Term x = slv.mkVar(integer, "x"); + Term xp = slv.mkVar(integer, "xp"); + + // (ite (< x 10) (= xp (+ x 1)) (= xp x)) + Term ite = slv.mkTerm(ITE, + slv.mkTerm(LT, x, ten), + slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, x)); + + // define the pre-conditions, transition relations, and post-conditions + Term pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, x, zero)); + Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite); + Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten)); + + // declare the invariant-to-synthesize. + Term inv_f = slv.synthInv("inv-f", {x}); + + slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + slv.printSynthSolution(std::cout); + } + + return 0; +} diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ea5eca391..24cd762a1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -45,6 +45,7 @@ #include "options/main_options.h" #include "options/options.h" #include "options/smt_options.h" +#include "printer/sygus_print_callback.h" #include "smt/model.h" #include "smt/smt_engine.h" #include "theory/logic_info.h" @@ -685,9 +686,10 @@ class CVC4ApiExceptionStream CVC4_PREDICT_TRUE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() -#define CVC4_API_CHECK_NOT_NULL \ - CVC4_API_CHECK(!isNullHelper()) << "Invalid call to '" << __PRETTY_FUNCTION__ \ - << "', expected non-null object"; +#define CVC4_API_CHECK_NOT_NULL \ + CVC4_API_CHECK(!isNullHelper()) \ + << "Invalid call to '" << __PRETTY_FUNCTION__ \ + << "', expected non-null object"; #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \ CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'"; @@ -1117,7 +1119,10 @@ Op::~Op() {} /* Split out to avoid nested API calls (problematic with API tracing). */ /* .......................................................................... */ -bool Op::isNullHelper() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); } +bool Op::isNullHelper() const +{ + return (d_expr->isNull() && (d_kind == NULL_EXPR)); +} bool Op::isIndexedHelper() const { return !d_expr->isNull(); } @@ -1730,7 +1735,6 @@ size_t TermHashFunction::operator()(const Term& t) const return ExprHashFunction()(*t.d_expr); } - /* -------------------------------------------------------------------------- */ /* Datatypes */ /* -------------------------------------------------------------------------- */ @@ -1994,8 +1998,9 @@ DatatypeConstructor::const_iterator::const_iterator( // Nullary constructor for Cython DatatypeConstructor::const_iterator::const_iterator() {} -DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: -operator=(const DatatypeConstructor::const_iterator& it) +DatatypeConstructor::const_iterator& +DatatypeConstructor::const_iterator::operator=( + const DatatypeConstructor::const_iterator& it) { d_int_stors = it.d_int_stors; d_stors = it.d_stors; @@ -2013,15 +2018,15 @@ const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const return &d_stors[d_idx]; } -DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: -operator++() +DatatypeConstructor::const_iterator& +DatatypeConstructor::const_iterator::operator++() { ++d_idx; return *this; } -DatatypeConstructor::const_iterator DatatypeConstructor::const_iterator:: -operator++(int) +DatatypeConstructor::const_iterator +DatatypeConstructor::const_iterator::operator++(int) { DatatypeConstructor::const_iterator it(*this); ++d_idx; @@ -2227,6 +2232,222 @@ bool Datatype::const_iterator::operator!=( return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx; } +/* -------------------------------------------------------------------------- */ +/* Grammar */ +/* -------------------------------------------------------------------------- */ +Grammar::Grammar(const Solver* s, + const std::vector& sygusVars, + const std::vector& ntSymbols) + : d_s(s), + d_sygusVars(sygusVars), + d_ntSyms(ntSymbols), + d_ntsToUnres(), + d_dtDecls(), + d_allowConst() +{ + for (Term ntsymbol : d_ntSyms) + { + // make the datatype, which encodes terms generated by this non-terminal + d_dtDecls.emplace(ntsymbol, DatatypeDecl(d_s, ntsymbol.toString())); + // make its unresolved type, used for referencing the final version of + // the datatype + d_ntsToUnres[ntsymbol] = d_s->getExprManager()->mkSort(ntsymbol.toString()); + } +} + +void Grammar::addRule(Term ntSymbol, Term rule) +{ + CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_ARG_CHECK_NOT_NULL(rule); + CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(), + ntSymbol) + << "ntSymbol to be one of the non-terminal symbols given in the " + "predeclaration"; + CVC4_API_CHECK(ntSymbol.d_expr->getType() == rule.d_expr->getType()) + << "Expected ntSymbol and rule to have the same sort"; + + addSygusConstructorTerm(d_dtDecls[ntSymbol], rule); +} + +void Grammar::addRules(Term ntSymbol, std::vector rules) +{ + CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(), + 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_expr->getType() == rules[i].d_expr->getType()) + << "Expected ntSymbol and rule at index " << i + << " to have the same sort"; + + addSygusConstructorTerm(d_dtDecls[ntSymbol], rules[i]); + } +} + +void Grammar::addAnyConstant(Term ntSymbol) +{ + CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(), + ntSymbol) + << "ntSymbol to be one of the non-terminal symbols given in the " + "predeclaration"; + + d_allowConst.insert(ntSymbol); +} + +void Grammar::addAnyVariable(Term ntSymbol) +{ + CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(), + ntSymbol) + << "ntSymbol to be one of the non-terminal symbols given in the " + "predeclaration"; + + addSygusConstructorVariables(d_dtDecls[ntSymbol], ntSymbol.d_expr->getType()); +} + +Sort Grammar::resolve() +{ + Term bvl; + + if (!d_sygusVars.empty()) + { + bvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST, + termVectorToExprs(d_sygusVars)); + } + + for (const Term& i : d_ntSyms) + { + bool aci = d_allowConst.find(i) != d_allowConst.end(); + Type btt = i.d_expr->getType(); + d_dtDecls[i].d_dtype->setSygus(btt, *bvl.d_expr, aci, false); + // We can be in a case where the only rule specified was (Variable T) + // and there are no variables of type T, in which case this is a bogus + // grammar. This results in the error below. + CVC4_API_CHECK(d_dtDecls[i].d_dtype->getNumConstructors() != 0) + << "Grouped rule listing for " << d_dtDecls[i] + << " produced an empty rule list"; + } + + // now, make the sygus datatype + std::vector datatypes; + std::set unresTypes; + + datatypes.reserve(d_ntSyms.size()); + + for (const Term& i : d_ntSyms) + { + datatypes.push_back(*d_dtDecls[i].d_dtype); + unresTypes.insert(*d_ntsToUnres[i].d_type); + } + + std::vector datatypeTypes = + d_s->getExprManager()->mkMutualDatatypeTypes( + datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + + // return is the first datatype + return datatypeTypes[0]; +} + +void Grammar::addSygusConstructorTerm(DatatypeDecl& dt, Term term) const +{ + // 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 + // free variables. These become arguments to constructors. Notice we must do + // a tree traversal in this function, since unique paths to the same term + // should be treated as distinct terms. + // Notice that let expressions are forbidden in the input syntax of term, so + // this does not lead to exponential behavior with respect to input size. + std::vector args; + std::vector cargs; + Term op = purifySygusGTerm(term, args, cargs); + std::stringstream ssCName; + ssCName << op.getKind(); + std::shared_ptr spc; + // callback prints as the expression + spc = std::make_shared( + *op.d_expr, termVectorToExprs(args)); + if (!args.empty()) + { + Term lbvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST, + termVectorToExprs(args)); + // its operator is a lambda + op = d_s->getExprManager()->mkExpr(CVC4::kind::LAMBDA, + {*lbvl.d_expr, *op.d_expr}); + } + dt.d_dtype->addSygusConstructor( + *op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc); +} + +Term Grammar::purifySygusGTerm(Term term, + std::vector& args, + std::vector& cargs) const +{ + std::unordered_map::const_iterator itn = + d_ntsToUnres.find(term); + if (itn != d_ntsToUnres.cend()) + { + Term ret = d_s->getExprManager()->mkBoundVar(term.d_expr->getType()); + args.push_back(ret); + cargs.push_back(itn->second); + return ret; + } + std::vector pchildren; + bool childChanged = false; + for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++) + { + Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs); + pchildren.push_back(ptermc); + childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i]; + } + if (!childChanged) + { + return term; + } + + Term nret; + + if (term.d_expr->isParameterized()) + { + // it's an indexed operator so we should provide the op + nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(), + term.d_expr->getOperator(), + termVectorToExprs(pchildren)); + } + else + { + nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(), + termVectorToExprs(pchildren)); + } + + return nret; +} + +void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const +{ + Assert(!sort.isNull()); + // each variable of appropriate type becomes a sygus constructor in dt. + for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++) + { + Term v = d_sygusVars[i]; + if (v.d_expr->getType() == *sort.d_type) + { + std::stringstream ss; + ss << v; + std::vector cargs; + dt.d_dtype->addSygusConstructor( + *v.d_expr, ss.str(), sortVectorToTypes(cargs)); + } + } +} + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -2317,7 +2538,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const { CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; return mkValHelper(CVC4::BitVector(s, base)); @@ -2328,7 +2549,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, uint32_t base) const { CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; Integer val(s, base); @@ -2505,7 +2726,7 @@ std::vector Solver::termVectorToExprs( return res; } -/* Helpers for mkTerm checks. */ +/* Helpers for mkTerm checks. */ /* .......................................................................... */ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const @@ -4226,6 +4447,230 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const return res; } +Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(sort); + + Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type); + (void)res.getType(true); /* kick off type checking */ + + d_smtEngine->declareSygusVar(symbol, res, *sort.d_type); + + return res; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Grammar Solver::mkSygusGrammar(const std::vector& boundVars, + const std::vector& ntSymbols) const +{ + CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) + << "non-empty vector"; + + for (size_t i = 0, n = boundVars.size(); i < n; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !boundVars[i].isNull(), "parameter term", boundVars[i], i) + << "non-null term"; + } + + for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i) + << "non-null term"; + } + + return Grammar(this, boundVars, ntSymbols); +} + +Term Solver::synthFun(const std::string& symbol, + const std::vector& boundVars, + Sort sort) const +{ + return synthFunHelper(symbol, boundVars, sort); +} + +Term Solver::synthFun(const std::string& symbol, + const std::vector& boundVars, + Sort sort, + Grammar g) const +{ + return synthFunHelper(symbol, boundVars, sort, false, &g); +} + +Term Solver::synthInv(const std::string& symbol, + const std::vector& boundVars) const +{ + return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true); +} + +Term Solver::synthInv(const std::string& symbol, + const std::vector& boundVars, + Grammar g) const +{ + return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g); +} + +Term Solver::synthFunHelper(const std::string& symbol, + const std::vector& boundVars, + const Sort& sort, + bool isInv, + Grammar* g) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(sort); + + CVC4_API_ARG_CHECK_EXPECTED(sort.d_type->isFirstClass(), sort) + << "first-class sort as codomain sort for function sort"; + + std::vector varTypes; + for (size_t i = 0, n = boundVars.size(); i < n; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !boundVars[i].isNull(), "parameter term", boundVars[i], i) + << "non-null term"; + varTypes.push_back(boundVars[i].d_expr->getType()); + } + + if (g != nullptr) + { + CVC4_API_CHECK(g->d_ntSyms[0].d_expr->getType() == *sort.d_type) + << "Invalid Start symbol for Grammar g, Expected Start's sort to be " + << *sort.d_type; + } + + Type funType = varTypes.empty() + ? *sort.d_type + : d_exprMgr->mkFunctionType(varTypes, *sort.d_type); + + Expr fun = d_exprMgr->mkBoundVar(symbol, funType); + (void)fun.getType(true); /* kick off type checking */ + + d_smtEngine->declareSynthFun(symbol, + fun, + g == nullptr ? funType : *g->resolve().d_type, + isInv, + termVectorToExprs(boundVars)); + + return fun; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::addSygusConstraint(Term term) const +{ + CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_ARG_CHECK_EXPECTED( + term.d_expr->getType() == d_exprMgr->booleanType(), term) + << "boolean term"; + + d_smtEngine->assertSygusConstraint(*term.d_expr); +} + +void Solver::addSygusInvConstraint(Term inv, + Term pre, + Term trans, + Term post) const +{ + CVC4_API_ARG_CHECK_NOT_NULL(inv); + CVC4_API_ARG_CHECK_NOT_NULL(pre); + CVC4_API_ARG_CHECK_NOT_NULL(trans); + CVC4_API_ARG_CHECK_NOT_NULL(post); + + CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv) + << "a function"; + + FunctionType invType = inv.d_expr->getType(); + + CVC4_API_ARG_CHECK_EXPECTED(invType.getRangeType().isBoolean(), inv) + << "boolean range"; + + CVC4_API_CHECK(pre.d_expr->getType() == invType) + << "Expected inv and pre to have the same sort"; + + CVC4_API_CHECK(post.d_expr->getType() == invType) + << "Expected inv and post to have the same sort"; + + const std::vector& invArgTypes = invType.getArgTypes(); + + std::vector expectedTypes; + expectedTypes.reserve(2 * invType.getArity() + 1); + + for (size_t i = 0, n = invArgTypes.size(); i < 2 * n; i += 2) + { + expectedTypes.push_back(invArgTypes[i % n]); + expectedTypes.push_back(invArgTypes[(i + 1) % n]); + } + + expectedTypes.push_back(invType.getRangeType()); + FunctionType expectedTransType = d_exprMgr->mkFunctionType(expectedTypes); + + CVC4_API_CHECK(trans.d_expr->getType() == expectedTransType) + << "Expected trans's sort to be " << invType; + + d_smtEngine->assertSygusInvConstraint( + *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr); +} + +Result Solver::checkSynth() const { return d_smtEngine->checkSynth(); } + +Term Solver::getSynthSolution(Term term) const +{ + CVC4_API_ARG_CHECK_NOT_NULL(term); + + std::map map; + CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) + << "The solver is not in a state immediately preceeded by a " + "successful call to checkSynth"; + + std::map::const_iterator it = map.find(*term.d_expr); + + CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; + + return it->second; +} + +std::vector Solver::getSynthSolutions( + const std::vector& terms) const +{ + CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector"; + + for (size_t i = 0, n = terms.size(); i < n; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !terms[i].isNull(), "parameter term", terms[i], i) + << "non-null term"; + } + + std::map map; + CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) + << "The solver is not in a state immediately preceeded by a " + "successful call to checkSynth"; + + std::vector synthSolution; + synthSolution.reserve(terms.size()); + + for (size_t i = 0, n = terms.size(); i < n; ++i) + { + std::map::const_iterator it = + map.find(*terms[i].d_expr); + + CVC4_API_CHECK(it != map.cend()) + << "Synth solution not found for term at index " << i; + + synthSolution.push_back(it->second); + } + + return synthSolution; +} + +void Solver::printSynthSolution(std::ostream& out) const +{ + d_smtEngine->printSynthSolution(out); +} + /** * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! @@ -4238,7 +4683,6 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); } */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } - /* -------------------------------------------------------------------------- */ /* Conversions */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5c435d93e..5cfc61bbb 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -190,6 +190,7 @@ class CVC4_PUBLIC Sort friend class DatatypeDecl; friend class Op; friend class Solver; + friend class Grammar; friend struct SortHashFunction; friend class Term; @@ -749,6 +750,7 @@ class CVC4_PUBLIC Term friend class Datatype; friend class DatatypeConstructor; friend class Solver; + friend class Grammar; friend struct TermHashFunction; public: @@ -1184,6 +1186,8 @@ class CVC4_PUBLIC DatatypeDecl { friend class DatatypeConstructorArg; friend class Solver; + friend class Grammar; + public: /** * Nullary constructor for Cython @@ -1747,6 +1751,130 @@ std::ostream& operator<<(std::ostream& out, std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) CVC4_PUBLIC; +/* -------------------------------------------------------------------------- */ +/* Grammar */ +/* -------------------------------------------------------------------------- */ + +/** + * A Sygus Grammar. + */ +class CVC4_PUBLIC Grammar +{ + friend class Solver; + + public: + /** + * Add to the set of rules corresponding to . + * @param ntSymbol the non-terminal to which the rule is added + * @param rule the rule to add + */ + void addRule(Term ntSymbol, Term rule); + + /** + * Allow to be an arbitrary constant. + * @param ntSymbol the non-terminal allowed to be any constant + */ + void addAnyConstant(Term ntSymbol); + + /** + * Allow to be any input variable to corresponding + * synth-fun/synth-inv with the same sort as . + * @param ntSymbol the non-terminal allowed to be any input constant + */ + void addAnyVariable(Term ntSymbol); + + /** + * Add to the set of rules corresponding to . + * @param ntSymbol the non-terminal to which the rules are added + * @param rule the rules to add + */ + void addRules(Term ntSymbol, std::vector rules); + + private: + /** + * Constructor. + * @param s the solver that created this grammar + * @param sygusVars the input variables to synth-fun/synth-var + * @param ntSymbols the non-terminals of this grammar + */ + Grammar(const Solver* s, + const std::vector& sygusVars, + const std::vector& ntSymbols); + + /** + * Returns the resolved datatype of the Start symbol of the grammar. + * @return the resolved datatype of the Start symbol of the grammar + */ + Sort resolve(); + + /** + * Adds a constructor to sygus datatype
whose sygus operator is . + * + * contains a mapping from non-terminal symbols to the + * unresolved sorts they correspond to. This map indicates how the argument + * should be interpreted (instances of symbols from the domain of + * correspond to constructor arguments). + * + * The sygus operator that is actually added to
corresponds to replacing + * each occurrence of non-terminal symbols from the domain of + * with bound variables via purifySygusGTerm, and binding these variables + * via a lambda. + * + * @param dt the non-terminal's datatype to which a constructor is added + * @param term the sygus operator of the constructor + */ + void addSygusConstructorTerm(DatatypeDecl& dt, Term term) const; + + /** Purify sygus grammar term + * + * This returns a term where all occurrences of non-terminal symbols (those + * in the domain of ) are replaced by fresh variables. For + * each variable replaced in this way, we add the fresh variable it is + * replaced with to , and the unresolved sorts corresponding to the + * non-terminal symbol to (constructor args). In other words, + * contains the free variables in the term returned by this method (which + * should be bound by a lambda), and contains the sorts of the + * arguments of the sygus constructor. + * + * @param term the term to purify + * @param args the free variables in the term returned by this method + * @param cargs the sorts of the arguments of the sygus constructor + * @return the purfied term + */ + Term purifySygusGTerm(Term term, + std::vector& args, + std::vector& cargs) const; + + /** + * This adds constructors to
for sygus variables in whose + * sort is argument . This method should be called when the sygus + * grammar term (Variable sort) is encountered. + * + * @param dt the non-terminal's datatype to which the constructors are added + * @param sort the sort of the sygus variables to add + */ + void addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const; + + /** The solver that created this grammar. */ + const Solver* d_s; + /** Input variables to the corresponding function/invariant to synthesize.*/ + std::vector d_sygusVars; + /** The non-terminal symbols of this grammar. */ + std::vector d_ntSyms; + /** + * The mapping from non-terminal symbols to the unresolved sorts they + * correspond to. + */ + std::unordered_map d_ntsToUnres; + /** + * The mapping from non-terminal symbols to the datatype declarations they + * correspond to. + */ + std::unordered_map d_dtDecls; + /** The set of non-terminals that can be arbitrary constants. */ + std::unordered_set d_allowConst; +}; + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -2802,6 +2930,123 @@ class CVC4_PUBLIC Solver */ Term ensureTermSort(const Term& t, const Sort& s) const; + /** + * Append to the current list of universal variables. + * SyGuS v2: ( declare-var ) + * @param sort the sort of the universal variable + * @param symbol the name of the universal variable + * @return the universal variable + */ + Term mkSygusVar(Sort sort, const std::string& symbol = std::string()) const; + + /** + * Create a Sygus grammar. + * @param boundVars the parameters to corresponding synth-fun/synth-inv + * @param ntSymbols the pre-declaration of the non-terminal symbols + * @return the grammar + */ + Grammar mkSygusGrammar(const std::vector& boundVars, + const std::vector& ntSymbols) const; + + /** + * Synthesize n-ary function. + * SyGuS v2: ( synth-fun ( * ) ) + * @param symbol the name of the function + * @param boundVars the parameters to this function + * @param sort the sort of the return value of this function + * @return the function + */ + Term synthFun(const std::string& symbol, + const std::vector& boundVars, + Sort sort) const; + + /** + * Synthesize n-ary function following specified syntactic constraints. + * SyGuS v2: ( synth-fun ( * ) ) + * @param symbol the name of the function + * @param boundVars the parameters to this function + * @param sort the sort of the return value of this function + * @param g the syntactic constraints + * @return the function + */ + Term synthFun(const std::string& symbol, + const std::vector& boundVars, + Sort sort, + Grammar g) const; + + /** + * Synthesize invariant. + * SyGuS v2: ( synth-inv ( * ) ) + * @param symbol the name of the invariant + * @param boundVars the parameters to this invariant + * @param sort the sort of the return value of this invariant + * @return the invariant + */ + Term synthInv(const std::string& symbol, + const std::vector& boundVars) const; + + /** + * Synthesize invariant following specified syntactic constraints. + * SyGuS v2: ( synth-inv ( * ) ) + * @param symbol the name of the invariant + * @param boundVars the parameters to this invariant + * @param sort the sort of the return value of this invariant + * @param g the syntactic constraints + * @return the invariant + */ + Term synthInv(const std::string& symbol, + const std::vector& boundVars, + Grammar g) const; + + /** + * Add a forumla to the set of Sygus constraints. + * SyGuS v2: ( constraint ) + * @param term the formula to add as a constraint + */ + void addSygusConstraint(Term term) const; + + /** + * Add a set of Sygus constraints to the current state that correspond to an + * invariant synthesis problem. + * SyGuS v2: ( inv-constraint 
   )
+   * @param inv the function-to-synthesize
+   * @param pre the pre-condition
+   * @param trans the transition relation
+   * @param post the post-condition
+   */
+  void addSygusInvConstraint(Term inv, Term pre, Term trans, Term post) const;
+
+  /**
+   * Try to find a solution for the synthesis conjecture corresponding to the
+   * current list of functions-to-synthesize, universal variables and
+   * constraints.
+   * SyGuS v2: ( check-synth )
+   * @return the result of the synthesis conjecture.
+   */
+  Result checkSynth() const;
+
+  /**
+   * Get the synthesis solution of the given term. This method should be called
+   * immediately after the solver answers unsat for sygus input.
+   * @param term the term for which the synthesis solution is queried
+   * @return the synthesis solution of the given term
+   */
+  Term getSynthSolution(Term term) const;
+
+  /**
+   * Get the synthesis solutions of the given terms. This method should be
+   * called immediately after the solver answers unsat for sygus input.
+   * @param terms the terms for which the synthesis solutions is queried
+   * @return the synthesis solutions of the given terms
+   */
+  std::vector getSynthSolutions(const std::vector& terms) const;
+
+  /**
+   * Print solution for synthesis conjecture to the given output stream.
+   * @param out the output stream
+   */
+  void printSynthSolution(std::ostream& out) const;
+
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
   ExprManager* getExprManager(void) const;
@@ -2826,7 +3071,9 @@ class CVC4_PUBLIC Solver
   Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
   /* Helper for mkBitVector functions that take a string and a size as
    * arguments. */
-  Term mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const;
+  Term mkBVFromStrHelper(uint32_t size,
+                         const std::string& s,
+                         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 setLogic. */
@@ -2864,6 +3111,22 @@ class CVC4_PUBLIC Solver
       std::vector& dtypedecls,
       std::set& unresolvedSorts) const;
 
+  /**
+   * Synthesize n-ary function following specified syntactic constraints.
+   * SMT-LIB: ( synth-fun  ( * )  ? )
+   * @param symbol the name of the function
+   * @param boundVars the parameters to this function
+   * @param sort the sort of the return value of this function
+   * @param isInv determines whether this is synth-fun or synth-inv
+   * @param g the syntactic constraints
+   * @return the function
+   */
+  Term synthFunHelper(const std::string& symbol,
+                      const std::vector& boundVars,
+                      const Sort& sort,
+                      bool isInv = false,
+                      Grammar* g = nullptr) const;
+
   /* The expression manager of this solver. */
   std::unique_ptr d_exprMgr;
   /* The SMT engine of this solver. */
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index fc1461862..79f469524 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -7,3 +7,4 @@ cvc4_add_unit_test_black(result_black api)
 cvc4_add_unit_test_black(solver_black api)
 cvc4_add_unit_test_black(sort_black api)
 cvc4_add_unit_test_black(term_black api)
+cvc4_add_unit_test_black(grammar_black api)
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
new file mode 100644
index 000000000..abf37f210
--- /dev/null
+++ b/test/unit/api/grammar_black.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file grammar_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include 
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class GrammarBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testAddRule();
+  void testAddRules();
+  void testAddAnyConstant();
+  void testAddAnyVariable();
+
+ private:
+  std::unique_ptr d_solver;
+};
+
+void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
+
+void GrammarBlack::tearDown() {}
+
+void GrammarBlack::testAddRule()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addRule(start, d_solver->mkBoolean(false)));
+
+  TS_ASSERT_THROWS(g.addRule(nullTerm, d_solver->mkBoolean(false)),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddRules()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addRules(start, {d_solver->mkBoolean(false)}));
+
+  TS_ASSERT_THROWS(g.addRules(nullTerm, {d_solver->mkBoolean(false)}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, {nullTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(nts, {d_solver->mkBoolean(false)}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddAnyConstant()
+{
+  Sort boolean = d_solver->getBooleanSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
+  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
+
+  TS_ASSERT_THROWS(g.addAnyConstant(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addAnyConstant(nts), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddAnyVariable()
+{
+  Sort boolean = d_solver->getBooleanSort();
+
+  Term nullTerm;
+  Term x = d_solver->mkVar(boolean);
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g1 = d_solver->mkSygusGrammar({x}, {start});
+  Grammar g2 = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
+  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
+  TS_ASSERT_THROWS_NOTHING(g2.addAnyVariable(start));
+
+  TS_ASSERT_THROWS(g1.addAnyConstant(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g1.addAnyConstant(nts), CVC4ApiException&);
+}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 7c9af1714..4b5480dba 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -106,6 +106,15 @@ class SolverBlack : public CxxTest::TestSuite
 
   void testResetAssertions();
 
+  void testMkSygusVar();
+  void testMkSygusGrammar();
+  void testSynthFun();
+  void testSynthInv();
+  void testAddSygusConstraint();
+  void testAddSygusInvConstraint();
+  void testGetSynthSolution();
+  void testGetSynthSolutions();
+
  private:
   std::unique_ptr d_solver;
 };
@@ -558,7 +567,7 @@ void SolverBlack::testMkString()
   TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf").toString(),
                    "\"asdf\\u{5c}nasdf\"");
   TS_ASSERT_EQUALS(d_solver->mkString("asdf\\u{005c}nasdf", true).toString(),
-                    "\"asdf\\u{5c}nasdf\"");
+                   "\"asdf\\u{5c}nasdf\"");
 }
 
 void SolverBlack::testMkChar()
@@ -1217,3 +1226,196 @@ void SolverBlack::testResetAssertions()
   d_solver->resetAssertions();
   d_solver->checkSatAssuming({slt, ule});
 }
+
+void SolverBlack::testMkSygusVar()
+{
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkSygusVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkSygusVar(d_solver->getNullSort(), "a"),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testMkSygusGrammar()
+{
+  Term nullTerm;
+  Term boolTerm = d_solver->mkBoolean(true);
+  Term intTerm = d_solver->mkReal(1);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intTerm}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolTerm}, {intTerm}));
+  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {nullTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({nullTerm}, {intTerm}),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testSynthFun()
+{
+  Sort null = d_solver->getNullSort();
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+  Sort boolToBool = d_solver->mkFunctionSort({boolean}, boolean);
+
+  Term nullTerm;
+  Term x = d_solver->mkVar(boolean);
+
+  Term start1 = d_solver->mkVar(boolean);
+  Term start2 = d_solver->mkVar(integer);
+
+  Grammar g1 = d_solver->mkSygusGrammar({x}, {start1});
+  g1.addRule(start1, d_solver->mkBoolean(false));
+
+  Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
+  g2.addRule(start2, d_solver->mkReal(0));
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean));
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean));
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f2", {x}, boolean, g1));
+
+  TS_ASSERT_THROWS(d_solver->synthFun("f3", {nullTerm}, boolean),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->synthFun("f4", {}, null), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->synthFun("f5", {}, boolToBool), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->synthFun("f6", {x}, boolean, g2),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testSynthInv()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+
+  Term nullTerm;
+  Term x = d_solver->mkVar(boolean);
+
+  Term start1 = d_solver->mkVar(boolean);
+  Term start2 = d_solver->mkVar(integer);
+
+  Grammar g1 = d_solver->mkSygusGrammar({x}, {start1});
+  g1.addRule(start1, d_solver->mkBoolean(false));
+
+  Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
+  g2.addRule(start2, d_solver->mkReal(0));
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i2", {x}, g1));
+
+  TS_ASSERT_THROWS(d_solver->synthInv("i3", {nullTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->synthInv("i4", {x}, g2), CVC4ApiException&);
+}
+
+void SolverBlack::testAddSygusConstraint()
+{
+  Term nullTerm;
+  Term boolTerm = d_solver->mkBoolean(true);
+  Term intTerm = d_solver->mkReal(1);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
+  TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusConstraint(intTerm), CVC4ApiException&);
+}
+
+void SolverBlack::testAddSygusInvConstraint()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort real = d_solver->getRealSort();
+
+  Term nullTerm;
+  Term intTerm = d_solver->mkReal(1);
+
+  Term inv = d_solver->declareFun("inv", {real}, boolean);
+  Term pre = d_solver->declareFun("pre", {real}, boolean);
+  Term trans = d_solver->declareFun("trans", {real, real}, boolean);
+  Term post = d_solver->declareFun("post", {real}, boolean);
+
+  Term inv1 = d_solver->declareFun("inv1", {real}, real);
+
+  Term trans1 = d_solver->declareFun("trans1", {boolean, real}, boolean);
+  Term trans2 = d_solver->declareFun("trans2", {real, boolean}, boolean);
+  Term trans3 = d_solver->declareFun("trans3", {real, real}, real);
+
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->addSygusInvConstraint(inv, pre, trans, post));
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(nullTerm, pre, trans, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, nullTerm, trans, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, nullTerm, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, nullTerm),
+                   CVC4ApiException&);
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(intTerm, pre, trans, post),
+                   CVC4ApiException&);
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv1, pre, trans, post),
+                   CVC4ApiException&);
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, trans, trans, post),
+                   CVC4ApiException&);
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, intTerm, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, pre, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans1, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans2, post),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans3, post),
+                   CVC4ApiException&);
+
+  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, trans),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testGetSynthSolution()
+{
+  d_solver->setOption("lang", "sygus2");
+  d_solver->setOption("incremental", "false");
+
+  Term nullTerm;
+  Term x = d_solver->mkBoolean(false);
+  Term f = d_solver->synthFun("f", {}, d_solver->getBooleanSort());
+
+  TS_ASSERT_THROWS(d_solver->getSynthSolution(f), CVC4ApiException&);
+
+  d_solver->checkSynth();
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolution(f));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolution(f));
+
+  TS_ASSERT_THROWS(d_solver->getSynthSolution(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->getSynthSolution(x), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSynthSolutions()
+{
+  d_solver->setOption("lang", "sygus2");
+  d_solver->setOption("incremental", "false");
+
+  Term nullTerm;
+  Term x = d_solver->mkBoolean(false);
+  Term f = d_solver->synthFun("f", {}, d_solver->getBooleanSort());
+
+  TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->getSynthSolutions({f}), CVC4ApiException&);
+
+  d_solver->checkSynth();
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolutions({f}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolutions({f, f}));
+
+  TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->getSynthSolutions({nullTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->getSynthSolutions({x}), CVC4ApiException&);
+}
-- 
2.30.2