This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.
strings
strings-new
sygus-fun
+ sygus-grammar
sygus-inv
)
Term one = slv.mkReal(1);
Term plus = slv.mkTerm(PLUS, start, start);
- Term minus = slv.mkTerm(PLUS, start, start);
+ Term minus = slv.mkTerm(MINUS, start, start);
Term ite = slv.mkTerm(ITE, start_bool, start, start);
Term And = slv.mkTerm(AND, start_bool, start_bool);
--- /dev/null
+/********************* */
+/*! \file sygus-grammar.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 id1 ((x Int)) Int
+ ** ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+ **
+ ** (synth-fun id2 ((x Int)) Int
+ ** ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start)))))
+ **
+ ** (synth-fun id3 ((x Int)) Int
+ ** ((Start Int)) ((Start Int (0 (- x) (+ x Start)))))
+ **
+ ** (synth-fun id4 ((x Int)) Int
+ ** ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+ **
+ ** (declare-var x Int)
+ **
+ ** (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
+ **
+ ** (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");
+
+ // declare the grammar non-terminals
+ Term start = slv.mkVar(integer, "Start");
+
+ // define the rules
+ Term zero = slv.mkReal(0);
+ Term neg_x = slv.mkTerm(UMINUS, x);
+ Term plus = slv.mkTerm(PLUS, x, start);
+
+ // create the grammar object
+ Grammar g1 = slv.mkSygusGrammar({x}, {start});
+
+ // bind each non-terminal to its rules
+ g1.addRules(start, {neg_x, plus});
+
+ // copy the first grammar with all of its non-termainals and their rules
+ Grammar g2 = g1;
+ Grammar g3 = g1;
+
+ // add parameters as rules to the start symbol. Similar to "(Variable Int)"
+ g2.addAnyVariable(start);
+
+ // declare the function-to-synthesizse
+ Term id1 = slv.synthFun("id1", {x}, integer, g1);
+ Term id2 = slv.synthFun("id2", {x}, integer, g2);
+
+ g3.addRule(start, zero);
+
+ Term id3 = slv.synthFun("id3", {x}, integer, g3);
+
+ // g1 is reusable as long as it remains unmodified after first use
+ Term id4 = slv.synthFun("id4", {x}, integer, g1);
+
+ // declare universal variables.
+ Term varX = slv.mkSygusVar(integer, "x");
+
+ Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
+ Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);
+ Term id3_x = slv.mkTerm(APPLY_UF, id3, varX);
+ Term id4_x = slv.mkTerm(APPLY_UF, id4, varX);
+
+ // add logical constraints
+ // (constraint (= (id1 x) (id2 x) x))
+ slv.addSygusConstraint(slv.mkTerm(EQUAL, {id1_x, id2_x, id3_x, id4_x, varX}));
+
+ // print solutions if available
+ if (slv.checkSynth().isUnsat())
+ {
+ // Output should be equivalent to:
+ // (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+ // (define-fun id2 ((x Int)) Int x)
+ // (define-fun id3 ((x Int)) Int (+ x 0))
+ // (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+ slv.printSynthSolution(std::cout);
+ }
+
+ return 0;
+}
: d_s(s),
d_sygusVars(sygusVars),
d_ntSyms(ntSymbols),
- d_ntsToUnres(),
- d_dtDecls(),
- d_allowConst()
+ d_ntsToTerms(ntSymbols.size()),
+ d_allowConst(),
+ d_allowVars(),
+ d_isResolved(false)
{
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());
+ d_ntsToTerms.emplace(ntsymbol, std::vector<Term>());
}
}
void Grammar::addRule(Term ntSymbol, Term rule)
{
+ CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
+ "it as an argument to synthFun/synthInv";
CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
CVC4_API_ARG_CHECK_NOT_NULL(rule);
- CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(),
- ntSymbol)
+ CVC4_API_ARG_CHECK_EXPECTED(
+ d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
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);
+ d_ntsToTerms[ntSymbol].push_back(rule);
}
void Grammar::addRules(Term ntSymbol, std::vector<Term> rules)
{
+ CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
+ "it as an argument to synthFun/synthInv";
CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
- CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(),
- ntSymbol)
+ CVC4_API_ARG_CHECK_EXPECTED(
+ d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
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]);
}
+
+ d_ntsToTerms[ntSymbol].insert(
+ d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend());
}
void Grammar::addAnyConstant(Term ntSymbol)
{
+ CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
+ "it as an argument to synthFun/synthInv";
CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
- CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(),
- ntSymbol)
+ CVC4_API_ARG_CHECK_EXPECTED(
+ d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
void Grammar::addAnyVariable(Term ntSymbol)
{
+ CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
+ "it as an argument to synthFun/synthInv";
CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
- CVC4_API_ARG_CHECK_EXPECTED(d_dtDecls.find(ntSymbol) != d_dtDecls.end(),
- ntSymbol)
+ CVC4_API_ARG_CHECK_EXPECTED(
+ d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
<< "ntSymbol to be one of the non-terminal symbols given in the "
"predeclaration";
- addSygusConstructorVariables(d_dtDecls[ntSymbol], ntSymbol.d_expr->getType());
+ d_allowVars.insert(ntSymbol);
}
Sort Grammar::resolve()
{
+ d_isResolved = true;
+
Term bvl;
if (!d_sygusVars.empty())
termVectorToExprs(d_sygusVars));
}
- for (const Term& i : d_ntSyms)
+ std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
+
+ for (Term ntsymbol : 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";
+ // make the unresolved type, used for referencing the final version of
+ // the ntsymbol's datatype
+ ntsToUnres[ntsymbol] = d_s->getExprManager()->mkSort(ntsymbol.toString());
}
- // 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)
+ for (const Term& ntSym : d_ntSyms)
{
- datatypes.push_back(*d_dtDecls[i].d_dtype);
- unresTypes.insert(*d_ntsToUnres[i].d_type);
+ // make the datatype, which encodes terms generated by this non-terminal
+ DatatypeDecl dtDecl(d_s, ntSym.toString());
+
+ for (const Term& consTerm : d_ntsToTerms[ntSym])
+ {
+ addSygusConstructorTerm(dtDecl, consTerm, ntsToUnres);
+ }
+
+ if (d_allowVars.find(ntSym) != d_allowConst.cend())
+ {
+ addSygusConstructorVariables(dtDecl, ntSym.d_expr->getType());
+ }
+
+ bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
+ Type btt = ntSym.d_expr->getType();
+ dtDecl.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(dtDecl.d_dtype->getNumConstructors() != 0)
+ << "Grouped rule listing for " << *dtDecl.d_dtype
+ << " produced an empty rule list";
+
+ datatypes.push_back(*dtDecl.d_dtype);
+ unresTypes.insert(*ntsToUnres[ntSym].d_type);
}
std::vector<DatatypeType> datatypeTypes =
return datatypeTypes[0];
}
-void Grammar::addSygusConstructorTerm(DatatypeDecl& dt, Term term) const
+void Grammar::addSygusConstructorTerm(
+ DatatypeDecl& dt,
+ Term term,
+ const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
{
// At this point, we should know that dt is well founded, and that its
// builtin sygus operators are well-typed.
// 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);
+ Term op = purifySygusGTerm(term, args, cargs, ntsToUnres);
std::stringstream ssCName;
ssCName << op.getKind();
std::shared_ptr<SygusPrintCallback> spc;
*op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
}
-Term Grammar::purifySygusGTerm(Term term,
- std::vector<Term>& args,
- std::vector<Sort>& cargs) const
+Term Grammar::purifySygusGTerm(
+ Term term,
+ std::vector<Term>& args,
+ std::vector<Sort>& cargs,
+ const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
{
std::unordered_map<Term, Sort, TermHashFunction>::const_iterator itn =
- d_ntsToUnres.find(term);
- if (itn != d_ntsToUnres.cend())
+ ntsToUnres.find(term);
+ if (itn != ntsToUnres.cend())
{
Term ret = d_s->getExprManager()->mkBoundVar(term.d_expr->getType());
args.push_back(ret);
bool childChanged = false;
for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++)
{
- Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs);
+ Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs, ntsToUnres);
pchildren.push_back(ptermc);
childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i];
}
Term Solver::synthFun(const std::string& symbol,
const std::vector<Term>& boundVars,
Sort sort,
- Grammar g) const
+ Grammar& g) const
{
return synthFunHelper(symbol, boundVars, sort, false, &g);
}
Term Solver::synthInv(const std::string& symbol,
const std::vector<Term>& boundVars,
- Grammar g) const
+ Grammar& g) const
{
return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g);
}
/**
* Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
*
- * <d_ntsToUnres> contains a mapping from non-terminal symbols to the
+ * <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).
+ * <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>
+ * each occurrence of non-terminal symbols from the domain of <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
+ * @param ntsToUnres mapping from non-terminals to their unresolved sorts
*/
- void addSygusConstructorTerm(DatatypeDecl& dt, Term term) const;
+ void addSygusConstructorTerm(
+ DatatypeDecl& dt,
+ Term term,
+ const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) 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
+ * in the domain of <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>
* @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
+ * @param ntsToUnres mapping from non-terminals to their unresolved sorts
* @return the purfied term
*/
- Term purifySygusGTerm(Term term,
- std::vector<Term>& args,
- std::vector<Sort>& cargs) const;
+ Term purifySygusGTerm(
+ Term term,
+ std::vector<Term>& args,
+ std::vector<Sort>& cargs,
+ const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const;
/**
* This adds constructors to <dt> for sygus variables in <d_sygusVars> whose
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 mapping from non-terminal symbols to their production terms. */
+ std::unordered_map<Term, std::vector<Term>, TermHashFunction> d_ntsToTerms;
/** The set of non-terminals that can be arbitrary constants. */
std::unordered_set<Term, TermHashFunction> d_allowConst;
+ /** The set of non-terminals that can be sygus variables. */
+ std::unordered_set<Term, TermHashFunction> d_allowVars;
+ /** Did we call resolve() before? */
+ bool d_isResolved;
};
/* -------------------------------------------------------------------------- */
Term synthFun(const std::string& symbol,
const std::vector<Term>& boundVars,
Sort sort,
- Grammar g) const;
+ Grammar& g) const;
/**
* Synthesize invariant.
*/
Term synthInv(const std::string& symbol,
const std::vector<Term>& boundVars,
- Grammar g) const;
+ Grammar& g) const;
/**
* Add a forumla to the set of Sygus constraints.
TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
CVC4ApiException&);
TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+
+ d_solver->synthFun("f", {}, boolean, g);
+
+ TS_ASSERT_THROWS(g.addRule(start, d_solver->mkBoolean(false)),
+ CVC4ApiException&);
}
void GrammarBlack::testAddRules()
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)}),
+ TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&);
+ TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+
+ d_solver->synthFun("f", {}, boolean, g);
+
+ TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkBoolean(false)}),
CVC4ApiException&);
- TS_ASSERT_THROWS(g.addRule(start, {d_solver->mkReal(0)}), CVC4ApiException&);
}
void GrammarBlack::testAddAnyConstant()
TS_ASSERT_THROWS(g.addAnyConstant(nullTerm), CVC4ApiException&);
TS_ASSERT_THROWS(g.addAnyConstant(nts), CVC4ApiException&);
+
+ d_solver->synthFun("f", {}, boolean, g);
+
+ TS_ASSERT_THROWS(g.addAnyConstant(start), CVC4ApiException&);
}
void GrammarBlack::testAddAnyVariable()
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&);
+ TS_ASSERT_THROWS(g1.addAnyVariable(nullTerm), CVC4ApiException&);
+ TS_ASSERT_THROWS(g1.addAnyVariable(nts), CVC4ApiException&);
+
+ d_solver->synthFun("f", {}, boolean, g1);
+
+ TS_ASSERT_THROWS(g1.addAnyVariable(start), CVC4ApiException&);
}
projects / cvc5.git / commitdiff