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.

1 files changed, 459 insertions, 15 deletions

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;
@@ -2228,6 +2233,222 @@ bool Datatype::const_iterator::operator!=(
 }
 
 /* -------------------------------------------------------------------------- */
+/* 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                                          */
 /* -------------------------------------------------------------------------- */
 
@@ -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>(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<Expr> 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<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. !!!
@@ -4238,7 +4683,6 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
  */
 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
 
-
 /* -------------------------------------------------------------------------- */
 /* Conversions                                                                */
 /* -------------------------------------------------------------------------- */