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.
sets-new
strings
strings-new
+ sygus-fun
+ sygus-inv
)
foreach(example ${CVC4_EXAMPLES_API})
--- /dev/null
+/********************* */
+/*! \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 <cvc4/api/cvc4cpp.h>
+
+#include <iostream>
+
+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;
+}
--- /dev/null
+/********************* */
+/*! \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 <cvc4/api/cvc4cpp.h>
+
+#include <iostream>
+
+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;
+}
#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"
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 << "'";
/* 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(); }
return ExprHashFunction()(*t.d_expr);
}
-
/* -------------------------------------------------------------------------- */
/* Datatypes */
/* -------------------------------------------------------------------------- */
// 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;
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;
return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
}
+/* -------------------------------------------------------------------------- */
+/* Grammar */
+/* -------------------------------------------------------------------------- */
+Grammar::Grammar(const Solver* s,
+ const std::vector<Term>& sygusVars,
+ const std::vector<Term>& 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<Term> 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<CVC4::Datatype> datatypes;
+ std::set<Type> 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<DatatypeType> 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<Term> args;
+ std::vector<Sort> cargs;
+ Term op = purifySygusGTerm(term, args, cargs);
+ std::stringstream ssCName;
+ ssCName << op.getKind();
+ std::shared_ptr<SygusPrintCallback> spc;
+ // callback prints as the expression
+ spc = std::make_shared<printer::SygusExprPrintCallback>(
+ *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<Term>& args,
+ std::vector<Sort>& cargs) const
+{
+ std::unordered_map<Term, Sort, TermHashFunction>::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<Term> 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<Sort> cargs;
+ dt.d_dtype->addSygusConstructor(
+ *v.d_expr, ss.str(), sortVectorToTypes(cargs));
+ }
+ }
+}
+
/* -------------------------------------------------------------------------- */
/* Rounding Mode for Floating Points */
/* -------------------------------------------------------------------------- */
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>(CVC4::BitVector(s, base));
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);
return res;
}
-/* Helpers for mkTerm checks. */
+/* Helpers for mkTerm checks. */
/* .......................................................................... */
void Solver::checkMkTerm(Kind kind, uint32_t nchildren) 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<Term>& boundVars,
+ const std::vector<Term>& 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<Term>& boundVars,
+ Sort sort) const
+{
+ return synthFunHelper(symbol, boundVars, sort);
+}
+
+Term Solver::synthFun(const std::string& symbol,
+ const std::vector<Term>& boundVars,
+ Sort sort,
+ Grammar g) const
+{
+ return synthFunHelper(symbol, boundVars, sort, false, &g);
+}
+
+Term Solver::synthInv(const std::string& symbol,
+ const std::vector<Term>& boundVars) const
+{
+ return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true);
+}
+
+Term Solver::synthInv(const std::string& symbol,
+ const std::vector<Term>& boundVars,
+ Grammar g) const
+{
+ return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g);
+}
+
+Term Solver::synthFunHelper(const std::string& symbol,
+ const std::vector<Term>& 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<Type> 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<Type>& invArgTypes = invType.getArgTypes();
+
+ std::vector<Type> 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<CVC4::Expr, CVC4::Expr> 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<CVC4::Expr, CVC4::Expr>::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<Term> Solver::getSynthSolutions(
+ const std::vector<Term>& 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<CVC4::Expr, CVC4::Expr> 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<Term> synthSolution;
+ synthSolution.reserve(terms.size());
+
+ for (size_t i = 0, n = terms.size(); i < n; ++i)
+ {
+ std::map<CVC4::Expr, CVC4::Expr>::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. !!!
*/
SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
-
/* -------------------------------------------------------------------------- */
/* Conversions */
/* -------------------------------------------------------------------------- */
friend class DatatypeDecl;
friend class Op;
friend class Solver;
+ friend class Grammar;
friend struct SortHashFunction;
friend class Term;
friend class Datatype;
friend class DatatypeConstructor;
friend class Solver;
+ friend class Grammar;
friend struct TermHashFunction;
public:
{
friend class DatatypeConstructorArg;
friend class Solver;
+ friend class Grammar;
+
public:
/**
* Nullary constructor for Cython
std::ostream& operator<<(std::ostream& out,
const DatatypeSelector& stor) CVC4_PUBLIC;
+/* -------------------------------------------------------------------------- */
+/* Grammar */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * A Sygus Grammar.
+ */
+class CVC4_PUBLIC Grammar
+{
+ friend class Solver;
+
+ public:
+ /**
+ * Add <rule> to the set of rules corresponding to <ntSymbol>.
+ * @param ntSymbol the non-terminal to which the rule is added
+ * @param rule the rule to add
+ */
+ void addRule(Term ntSymbol, Term rule);
+
+ /**
+ * Allow <ntSymbol> to be an arbitrary constant.
+ * @param ntSymbol the non-terminal allowed to be any constant
+ */
+ void addAnyConstant(Term ntSymbol);
+
+ /**
+ * Allow <ntSymbol> to be any input variable to corresponding
+ * synth-fun/synth-inv with the same sort as <ntSymbol>.
+ * @param ntSymbol the non-terminal allowed to be any input constant
+ */
+ void addAnyVariable(Term ntSymbol);
+
+ /**
+ * Add <rules> to the set of rules corresponding to <ntSymbol>.
+ * @param ntSymbol the non-terminal to which the rules are added
+ * @param rule the rules to add
+ */
+ void addRules(Term ntSymbol, std::vector<Term> 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<Term>& sygusVars,
+ const std::vector<Term>& 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 <dt> whose sygus operator is <term>.
+ *
+ * <d_ntsToUnres> contains a mapping from non-terminal symbols to the
+ * unresolved sorts they correspond to. This map indicates how the argument
+ * <term> should be interpreted (instances of symbols from the domain of
+ * <d_ntsToUnres> correspond to constructor arguments).
+ *
+ * The sygus operator that is actually added to <dt> corresponds to replacing
+ * each occurrence of non-terminal symbols from the domain of <d_ntsToUnres>
+ * 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 <d_ntsToUnres>) are replaced by fresh variables. For
+ * each variable replaced in this way, we add the fresh variable it is
+ * replaced with to <args>, and the unresolved sorts corresponding to the
+ * non-terminal symbol to <cargs> (constructor args). In other words, <args>
+ * contains the free variables in the term returned by this method (which
+ * should be bound by a lambda), and <cargs> 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<Term>& args,
+ std::vector<Sort>& cargs) const;
+
+ /**
+ * This adds constructors to <dt> for sygus variables in <d_sygusVars> whose
+ * sort is argument <sort>. 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<Term> d_sygusVars;
+ /** The non-terminal symbols of this grammar. */
+ std::vector<Term> d_ntSyms;
+ /**
+ * The mapping from non-terminal symbols to the unresolved sorts they
+ * correspond to.
+ */
+ std::unordered_map<Term, Sort, TermHashFunction> d_ntsToUnres;
+ /**
+ * The mapping from non-terminal symbols to the datatype declarations they
+ * correspond to.
+ */
+ std::unordered_map<Term, DatatypeDecl, TermHashFunction> d_dtDecls;
+ /** The set of non-terminals that can be arbitrary constants. */
+ std::unordered_set<Term, TermHashFunction> d_allowConst;
+};
+
/* -------------------------------------------------------------------------- */
/* Rounding Mode for Floating Points */
/* -------------------------------------------------------------------------- */
*/
Term ensureTermSort(const Term& t, const Sort& s) const;
+ /**
+ * Append <symbol> to the current list of universal variables.
+ * SyGuS v2: ( declare-var <symbol> <sort> )
+ * @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<Term>& boundVars,
+ const std::vector<Term>& ntSymbols) const;
+
+ /**
+ * Synthesize n-ary function.
+ * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> )
+ * @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<Term>& boundVars,
+ Sort sort) const;
+
+ /**
+ * Synthesize n-ary function following specified syntactic constraints.
+ * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
+ * @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<Term>& boundVars,
+ Sort sort,
+ Grammar g) const;
+
+ /**
+ * Synthesize invariant.
+ * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) )
+ * @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<Term>& boundVars) const;
+
+ /**
+ * Synthesize invariant following specified syntactic constraints.
+ * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) <g> )
+ * @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<Term>& boundVars,
+ Grammar g) const;
+
+ /**
+ * Add a forumla to the set of Sygus constraints.
+ * SyGuS v2: ( constraint <term> )
+ * @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 <inv> <pre> <trans> <post> )
+ * @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<Term> getSynthSolutions(const std::vector<Term>& 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;
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. */
std::vector<DatatypeDecl>& dtypedecls,
std::set<Sort>& unresolvedSorts) const;
+ /**
+ * Synthesize n-ary function following specified syntactic constraints.
+ * SMT-LIB: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
+ * @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<Term>& boundVars,
+ const Sort& sort,
+ bool isInv = false,
+ Grammar* g = nullptr) const;
+
/* The expression manager of this solver. */
std::unique_ptr<ExprManager> d_exprMgr;
/* The SMT engine of this solver. */
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)
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#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<Solver> 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&);
+}
void testResetAssertions();
+ void testMkSygusVar();
+ void testMkSygusGrammar();
+ void testSynthFun();
+ void testSynthInv();
+ void testAddSygusConstraint();
+ void testAddSygusInvConstraint();
+ void testGetSynthSolution();
+ void testGetSynthSolutions();
+
private:
std::unique_ptr<Solver> d_solver;
};
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()
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&);
+}
projects / cvc5.git / commitdiff