Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
-Term::Term(const Solver* slv, const CVC4::Expr& e)
- : d_solver(slv)
+Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv)
{
// Ensure that we create the node in the correct node manager.
NodeManagerScope scope(d_solver->getNodeManager());
d_node.reset(new CVC4::Node(e));
}
-Term::Term(const Solver* slv, const CVC4::Node& n)
- : d_solver(slv)
+Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
{
// Ensure that we create the node in the correct node manager.
NodeManagerScope scope(d_solver->getNodeManager());
d_allowVars.insert(ntSymbol);
}
+/**
+ * this function concatinates the outputs of calling f on each element between
+ * first and last, seperated by sep.
+ * @param first the beginning of the range
+ * @param last the end of the range
+ * @param f the function to call on each element in the range, its output must
+ * be overloaded for operator<<
+ * @param sep the string to add between successive calls to f
+ */
+template <typename Iterator, typename Function>
+std::string join(Iterator first, Iterator last, Function f, std::string sep)
+{
+ std::stringstream ss;
+ Iterator i = first;
+
+ if (i != last)
+ {
+ ss << f(*i);
+ ++i;
+ }
+
+ while (i != last)
+ {
+ ss << sep << f(*i);
+ ++i;
+ }
+
+ return ss.str();
+}
+
+std::string Grammar::toString() const
+{
+ std::stringstream ss;
+ ss << " (" // pre-declaration
+ << join(
+ d_ntSyms.cbegin(),
+ d_ntSyms.cend(),
+ [](const Term& t) {
+ std::stringstream s;
+ s << '(' << t << ' ' << t.getSort() << ')';
+ return s.str();
+ },
+ " ")
+ << ")\n (" // grouped rule listing
+ << join(
+ d_ntSyms.cbegin(),
+ d_ntSyms.cend(),
+ [this](const Term& t) {
+ bool allowConst = d_allowConst.find(t) != d_allowConst.cend(),
+ allowVars = d_allowVars.find(t) != d_allowVars.cend();
+ const std::vector<Term>& rules = d_ntsToTerms.at(t);
+ std::stringstream s;
+ s << '(' << t << ' ' << t.getSort() << " ("
+ << (allowConst ? "(Constant " + t.getSort().toString() + ")"
+ : "")
+ << (allowConst && allowVars ? " " : "")
+ << (allowVars ? "(Var " + t.getSort().toString() + ")" : "")
+ << ((allowConst || allowVars) && !rules.empty() ? " " : "")
+ << join(
+ rules.cbegin(),
+ rules.cend(),
+ [](const Term& rule) { return rule.toString(); },
+ " ")
+ << "))";
+ return s.str();
+ },
+ "\n ")
+ << ')';
+
+ return ss.str();
+}
+
Sort Grammar::resolve()
{
d_isResolved = true;
}
}
+std::ostream& operator<<(std::ostream& out, const Grammar& g)
+{
+ return out << g.toString();
+}
+
/* -------------------------------------------------------------------------- */
/* Rounding Mode for Floating Points */
/* -------------------------------------------------------------------------- */
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
Expr result;
bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result);
- if (success) {
+ if (success)
+ {
output = Term(output.d_solver, result);
}
return success;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const
+bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
Expr result;
- bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), gtype, result);
+ bool success = d_smtEngine->getInterpol(
+ conj.d_node->toExpr(), *g.resolve().d_type, result);
+ if (success)
+ {
+ output = Term(output.d_solver, result);
+ }
+ return success;
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getAbduct(Term conj, Term& output) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ Node result;
+ bool success = d_smtEngine->getAbduct(*conj.d_node, result);
+ if (success)
+ {
+ output = Term(output.d_solver, result);
+ }
+ return success;
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ Node result;
+ bool success = d_smtEngine->getAbduct(
+ *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
if (success)
{
output = Term(output.d_solver, result);
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)
- << "non-empty vector";
+ << "a non-empty vector";
for (size_t i = 0, n = boundVars.size(); i < n; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
<< "bound variable associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+ << "a non-null term";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
"bound variable",
boundVars[i],
i)
<< "a bound variable";
- 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(
- this == ntSymbols[i].d_solver, "term", ntSymbols[i], i)
+ this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i)
<< "term associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i)
+ << "a non-null term";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
- "bound variable",
+ "non-terminal",
ntSymbols[i],
i)
<< "a bound variable";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i)
- << "non-null term";
}
return Grammar(this, boundVars, ntSymbols);
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";
+ << "first-class codomain sort for function";
std::vector<Type> varTypes;
for (size_t i = 0, n = boundVars.size(); i < n; ++i)
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
<< "bound variable associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+ << "a non-null term";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
"bound variable",
boundVars[i],
i)
<< "a bound variable";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- !boundVars[i].isNull(), "parameter term", boundVars[i], i)
- << "non-null term";
varTypes.push_back(boundVars[i].d_node->getType().toType());
}
CVC4_API_SOLVER_CHECK_SORT(sort);
class ExprManager;
class NodeManager;
class SmtEngine;
+class SynthFunCommand;
class Type;
class Options;
class Random;
class CVC4_PUBLIC Grammar
{
friend class Solver;
+ friend class CVC4::SynthFunCommand;
public:
/**
*/
void addRule(Term ntSymbol, Term rule);
+ /**
+ * 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);
+
/**
* Allow <ntSymbol> to be an arbitrary constant.
* @param ntSymbol the non-terminal allowed to be any 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
+ * @return a string representation of this grammar.
*/
- void addRules(Term ntSymbol, std::vector<Term> rules);
+ std::string toString() const;
/**
* Nullary constructor. Needed for the Cython API.
bool d_isResolved;
};
+/**
+ * Serialize a grammar to given stream.
+ * @param out the output stream
+ * @param g the grammar to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC;
+
/* -------------------------------------------------------------------------- */
/* Rounding Mode for Floating Points */
/* -------------------------------------------------------------------------- */
/**
* Get an interpolant
- * SMT-LIB: ( get-interpol <term> )
+ * SMT-LIB: ( get-interpol <conj> )
* Requires to enable option 'produce-interpols'.
* @param conj the conjecture term
* @param output a Term I such that A->I and I->B are valid, where A is the
/**
* Get an interpolant
- * SMT-LIB: ( get-interpol <term> )
+ * SMT-LIB: ( get-interpol <conj> <g> )
* Requires to enable option 'produce-interpols'.
* @param conj the conjecture term
- * @param gtype the grammar for the interpolant I
+ * @param g the grammar for the interpolant I
* @param output a Term I such that A->I and I->B are valid, where A is the
* current set of assertions and B is given in the input by conj.
* @return true if it gets I successfully, false otherwise.
*/
- bool getInterpolant(Term conj, const Type& gtype, Term& output) const;
+ bool getInterpolant(Term conj, Grammar& g, Term& output) const;
+
+ /**
+ * Get an abduct.
+ * SMT-LIB: ( get-abduct <conj> )
+ * Requires enabling option 'produce-abducts'
+ * @param conj the conjecture term
+ * @param output a term C such that A^C is satisfiable, and A^~B^C is
+ * unsatisfiable, where A is the current set of assertions and B is
+ * given in the input by conj
+ * @return true if it gets C successfully, false otherwise
+ */
+ bool getAbduct(Term conj, Term& output) const;
+
+ /**
+ * Get an abduct.
+ * SMT-LIB: ( get-abduct <conj> <g> )
+ * Requires enabling option 'produce-abducts'
+ * @param conj the conjecture term
+ * @param g the grammar for the abduct C
+ * @param output a term C such that A^C is satisfiable, and A^~B^C is
+ * unsatisfiable, where A is the current set of assertions and B is
+ * given in the input by conj
+ * @return true if it gets C successfully, false otherwise
+ */
+ bool getAbduct(Term conj, Grammar& g, Term& output) const;
/**
* Print the model of a satisfiable query to the given output stream.
std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
std::string name, fun;
bool isInv;
- CVC4::api::Sort grammar;
+ CVC4::api::Grammar* grammar = nullptr;
}
: /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
api::Term var = PARSER_STATE->bindBoundVar(name, t);
cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
}
-
| /* synth-fun */
( SYNTH_FUN_TOK { isInv = false; }
| SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
* The argument fun is a unique identifier to avoid naming clashes for the
* datatypes constructed by this call.
*/
-sygusGrammar[CVC4::api::Sort & ret,
+sygusGrammar[CVC4::api::Grammar*& ret,
const std::vector<CVC4::api::Term>& sygusVars,
const std::string& fun]
@declarations
{
// the pre-declaration
- std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+ std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
// non-terminal symbols of the grammar
std::vector<CVC4::api::Term> ntSyms;
CVC4::api::Sort t;
std::string name;
CVC4::api::Term e, e2;
- std::vector<api::DatatypeDecl> datatypes;
- std::set<api::Sort> unresTypes;
- std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
unsigned dtProcessed = 0;
- std::unordered_set<unsigned> allowConst;
}
:
// predeclaration
PARSER_STATE->pushScope(true);
for (std::pair<std::string, api::Sort>& i : sortedVarNames)
{
- Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
- // make the datatype, which encodes terms generated by this non-terminal
- std::string dname = i.first;
- datatypes.push_back(SOLVER->mkDatatypeDecl(dname));
- // make its unresolved type, used for referencing the final version of
- // the datatype
- PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
- api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
- unresTypes.insert(urt);
+ PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
// make the non-terminal symbol, which will be parsed as an ordinary
// free variable.
api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
ntSyms.push_back(nts);
- ntsToUnres[nts] = urt;
}
+ ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
}
// the grouped rule listing
LPAREN_TOK
(
term[e,e2] {
// add term as constructor to datatype
- PARSER_STATE->addSygusConstructorTerm(
- datatypes[dtProcessed], e, ntsToUnres);
+ ret->addRule(ntSyms[dtProcessed], e);
}
| LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
- // allow constants in datatypes[dtProcessed]
- allowConst.insert(dtProcessed);
+ // allow constants in datatype for ntSyms[dtProcessed]
+ ret->addAnyConstant(ntSyms[dtProcessed]);
}
| LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
// add variable constructors to datatype
- PARSER_STATE->addSygusConstructorVariables(
- datatypes[dtProcessed], sygusVars, t);
+ ret->addAnyVariable(ntSyms[dtProcessed]);
}
)+
RPAREN_TOK
)+
RPAREN_TOK
{
- if (dtProcessed != sortedVarNames.size())
- {
- PARSER_STATE->parseError(
- "Number of grouped rule listings does not match "
- "number of symbols in predeclaration.");
- }
- api::Term bvl;
- if (!sygusVars.empty())
- {
- bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars);
- }
- Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl;
- for (unsigned i = 0; i < dtProcessed; i++)
- {
- bool aci = allowConst.find(i)!=allowConst.end();
- api::Sort btt = sortedVarNames[i].second;
- datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false);
- Trace("parser-sygus2") << "- " << datatypes[i].getName()
- << ", #cons= " << datatypes[i].getNumConstructors()
- << ", aci= " << aci << std::endl;
- // 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.
- if (datatypes[i].getNumConstructors() == 0)
- {
- std::stringstream se;
- se << "Grouped rule listing for " << datatypes[i].getName()
- << " produced an empty rule list.";
- PARSER_STATE->parseError(se.str());
- }
- }
// pop scope from the pre-declaration
PARSER_STATE->popScope();
- // now, make the sygus datatype
- Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
- std::vector<api::Sort> datatypeTypes =
- SOLVER->mkDatatypeSorts(datatypes, unresTypes);
- // return is the first datatype
- ret = api::Sort(datatypeTypes[0]);
}
;
std::vector<api::Sort> sorts;
std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
std::unique_ptr<CVC4::CommandSequence> seq;
+ api::Grammar* g = nullptr;
}
/* Extended SMT-LIB set of commands syntax, not permitted in
* --smtlib2 compliance mode. */
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
term[e,e2]
(
- sygusGrammar[t, terms, name]
+ sygusGrammar[g, terms, name]
)?
{
- cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
+ cmd->reset(new GetAbductCommand(SOLVER, name, e, g));
}
| GET_INTERPOL_TOK {
PARSER_STATE->checkThatLogicIsSet();
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
term[e,e2]
(
- sygusGrammar[t, terms, name]
+ sygusGrammar[g, terms, name]
)?
{
- cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType()));
+ cmd->reset(new GetInterpolCommand(SOLVER, name, e, g));
}
| DECLARE_HEAP LPAREN_TOK
sortSymbol[t, CHECK_DECLARED]
Smt2::SynthFunFactory::SynthFunFactory(
Smt2* smt2,
- const std::string& fun,
+ const std::string& id,
bool isInv,
api::Sort range,
std::vector<std::pair<std::string, api::Sort>>& sortedVarNames)
- : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
+ : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv)
{
if (range.isNull())
{
{
smt2->parseError("Cannot use synth-fun with function return type.");
}
+
std::vector<api::Sort> varSorts;
for (const std::pair<std::string, api::Sort>& p : sortedVarNames)
{
varSorts.push_back(p.second);
}
- Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
- api::Sort synthFunType =
- varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range)
- : range;
+
+ api::Sort funSort = varSorts.empty()
+ ? range
+ : d_smt2->d_solver->mkFunctionSort(varSorts, range);
// we do not allow overloading for synth fun
- d_synthFun = d_smt2->bindBoundVar(fun, synthFunType);
- // set the sygus type to be range by default, which is overwritten below
- // if a grammar is provided
- d_sygusType = range;
+ d_fun = d_smt2->bindBoundVar(id, funSort);
+
+ Debug("parser-sygus") << "Define synth fun : " << id << std::endl;
d_smt2->pushScope(true);
d_sygusVars = d_smt2->bindBoundVars(sortedVarNames);
}
-Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
-
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar)
+std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
{
- Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
+ Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
+ d_smt2->popScope();
return std::unique_ptr<Command>(new SynthFunCommand(
- d_fun,
- d_synthFun.getExpr(),
- grammar.isNull() ? d_sygusType.getType() : grammar.getType(),
- d_isInv,
- api::termVectorToExprs(d_sygusVars)));
+ d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
}
std::unique_ptr<Command> Smt2::invConstraint(
return cmd;
} /* Smt2::setLogic() */
+api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
+ const std::vector<api::Term>& ntSymbols)
+{
+ d_allocGrammars.emplace_back(new api::Grammar(
+ std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols))));
+ return d_allocGrammars.back().get();
+}
+
bool Smt2::sygus() const
{
InputLanguage ilang = getLanguage();
return d_solver->mkAbstractValue(name.substr(1));
}
-
-void Smt2::addSygusConstructorTerm(
- api::DatatypeDecl& dt,
- api::Term term,
- std::map<api::Term, api::Sort>& ntsToUnres) const
-{
- Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
- // 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<api::Term> args;
- std::vector<api::Sort> cargs;
- api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs);
- std::stringstream ssCName;
- ssCName << op.getKind();
- Trace("parser-sygus2") << "Purified operator " << op
- << ", #args/cargs=" << args.size() << "/"
- << cargs.size() << std::endl;
- if (!args.empty())
- {
- api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
- // its operator is a lambda
- op = d_solver->mkTerm(api::LAMBDA, lbvl, op);
- }
- Trace("parser-sygus2") << "addSygusConstructor: operator " << op
- << std::endl;
- dt.getDatatype().addSygusConstructor(
- op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs));
-}
-
-api::Term Smt2::purifySygusGTerm(api::Term term,
- std::map<api::Term, api::Sort>& ntsToUnres,
- std::vector<api::Term>& args,
- std::vector<api::Sort>& cargs) const
-{
- Trace("parser-sygus2-debug")
- << "purifySygusGTerm: " << term
- << " #nchild=" << term.getExpr().getNumChildren() << std::endl;
- std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term);
- if (itn != ntsToUnres.end())
- {
- api::Term ret = d_solver->mkVar(term.getSort());
- Trace("parser-sygus2-debug")
- << "...unresolved non-terminal, intro " << ret << std::endl;
- args.push_back(api::Term(d_solver, ret.getExpr()));
- cargs.push_back(itn->second);
- return ret;
- }
- std::vector<api::Term> pchildren;
- bool childChanged = false;
- for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
- {
- Trace("parser-sygus2-debug")
- << "......purify child " << i << " : " << term[i] << std::endl;
- api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
- pchildren.push_back(ptermc);
- childChanged = childChanged || ptermc != term[i];
- }
- if (!childChanged)
- {
- Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
- return term;
- }
- api::Term nret = d_solver->mkTerm(term.getOp(), pchildren);
- Trace("parser-sygus2-debug")
- << "...child changed, return " << nret << std::endl;
- return nret;
-}
-
-void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
- const std::vector<api::Term>& sygusVars,
- api::Sort type) const
-{
- // each variable of appropriate type becomes a sygus constructor in dt.
- for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
- {
- api::Term v = sygusVars[i];
- if (v.getSort() == type)
- {
- std::stringstream ss;
- ss << v;
- std::vector<api::Sort> cargs;
- dt.getDatatype().addSygusConstructor(
- v.getExpr(), ss.str(), api::sortVectorToTypes(cargs));
- }
- }
-}
-
InputLanguage Smt2::getLanguage() const
{
return d_solver->getOptions().getInputLanguage();
*/
std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
std::pair<api::Term, std::string> d_lastNamedTerm;
+ /**
+ * A list of sygus grammar objects. We keep track of them here to ensure that
+ * they don't get deleted before the commands using them get invoked.
+ */
+ std::vector<std::unique_ptr<api::Grammar>> d_allocGrammars;
protected:
Smt2(api::Solver* solver,
* Creates an instance of `SynthFunFactory`.
*
* @param smt2 Pointer to the parser state
- * @param fun Name of the function to synthesize
+ * @param id Name of the function to synthesize
* @param isInv True if the goal is to synthesize an invariant, false
* otherwise
* @param range The return type of the function-to-synthesize
*/
SynthFunFactory(
Smt2* smt2,
- const std::string& fun,
+ const std::string& id,
bool isInv,
api::Sort range,
std::vector<std::pair<std::string, api::Sort>>& sortedVarNames);
- ~SynthFunFactory();
const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; }
* @param grammar Optional grammar associated with the synth-fun command
* @return The instance of `SynthFunCommand`
*/
- std::unique_ptr<Command> mkCommand(api::Sort grammar);
+ std::unique_ptr<Command> mkCommand(api::Grammar* grammar);
private:
Smt2* d_smt2;
- std::string d_fun;
- api::Term d_synthFun;
- api::Sort d_sygusType;
+ std::string d_id;
+ api::Term d_fun;
+ api::Sort d_sort;
bool d_isInv;
std::vector<api::Term> d_sygusVars;
};
*/
const LogicInfo& getLogic() const { return d_logic; }
+ /**
+ * 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 a pointer to the grammar
+ */
+ api::Grammar* mkGrammar(const std::vector<api::Term>& boundVars,
+ const std::vector<api::Term>& ntSymbols);
+
bool v2_0() const
{
return getLanguage() == language::input::LANG_SMTLIB_V2_0;
*/
void checkLogicAllowsFunctions();
- void checkUserSymbol(const std::string& name) {
- if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) {
+ void checkUserSymbol(const std::string& name)
+ {
+ if (name.length() > 0 && (name[0] == '.' || name[0] == '@'))
+ {
std::stringstream ss;
- ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB";
+ ss << "cannot declare or define symbol `" << name
+ << "'; symbols starting with . and @ are reserved in SMT-LIB";
parseError(ss.str());
}
else if (isOperatorEnabled(name))
d_lastNamedTerm = std::make_pair(e, name);
}
- void clearLastNamedTerm() {
+ void clearLastNamedTerm()
+ {
d_lastNamedTerm = std::make_pair(api::Term(), "");
}
*/
api::Term mkAbstractValue(const std::string& name);
- /**
- * Adds a constructor to sygus datatype dt whose sygus operator is term.
- *
- * ntsToUnres contains a mapping from non-terminal symbols to the unresolved
- * types they correspond to. This map indicates how the argument term should
- * be interpreted (instances of symbols from the domain of 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 ntsToUnres
- * with bound variables via purifySygusGTerm, and binding these variables
- * via a lambda.
- */
- void addSygusConstructorTerm(
- api::DatatypeDecl& dt,
- api::Term term,
- std::map<api::Term, api::Sort>& ntsToUnres) const;
- /**
- * This adds constructors to dt for sygus variables in sygusVars whose
- * type is argument type. This method should be called when the sygus grammar
- * term (Variable type) is encountered.
- */
- void addSygusConstructorVariables(api::DatatypeDecl& dt,
- const std::vector<api::Term>& sygusVars,
- api::Sort type) const;
/**
* Smt2 parser provides its own checkDeclaration, which does the
* same as the base, but with some more helpful errors.
//------------------------- end processing parse operators
private:
- /** Purify sygus grammar term
- *
- * This returns a term where all occurrences of non-terminal symbols (those
- * 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 type 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 types of the arguments of the
- * sygus constructor.
- */
- api::Term purifySygusGTerm(api::Term term,
- std::map<api::Term, api::Sort>& ntsToUnres,
- std::vector<api::Term>& args,
- std::vector<api::Sort>& cargs) const;
-
void addArithmeticOperators();
void addTranscendentalOperators();
api::Term mkAnd(const std::vector<api::Term>& es);
}; /* class Smt2 */
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // namespace CVC4
#endif /* CVC4__PARSER__SMT2_H */
{
out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
<< ' ';
- Type type = c->getFunction().getType();
- const std::vector<Expr>& vars = c->getVars();
- Assert(!type.isFunction() || !vars.empty());
+ const std::vector<api::Term>& vars = c->getVars();
out << '(';
- if (type.isFunction())
+ if (!vars.empty())
{
// print variable list
- std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end();
- Assert(i != i_end);
- out << '(' << *i << ' ' << i->getType() << ')';
+ std::vector<api::Term>::const_iterator i = vars.begin(), i_end = vars.end();
+ out << '(' << *i << ' ' << i->getSort() << ')';
++i;
while (i != i_end)
{
- out << " (" << *i << ' ' << i->getType() << ')';
+ out << " (" << *i << ' ' << i->getSort() << ')';
++i;
}
- FunctionType ft = type;
- type = ft.getRangeType();
}
out << ')';
// if not invariant-to-synthesize, print return type
if (!c->isInv())
{
- out << ' ' << type;
+ out << ' ' << c->getSort();
}
+ out << '\n';
// print grammar, if any
- toStreamSygusGrammar(out, c->getSygusType());
+ if (c->getGrammar() != nullptr)
+ {
+ out << *c->getGrammar();
+ }
out << ')';
}
out << c->getConjecture();
// print grammar, if any
- toStreamSygusGrammar(out, c->getGrammarType());
+ if (c->getGrammar() != nullptr)
+ {
+ out << *c->getGrammar();
+ }
out << ')';
}
return out;
}
-
/* output stream insertion operator for benchmark statuses */
std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
{
Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
-Command::Command(api::Solver* solver)
+Command::Command(const api::Solver* solver)
: d_solver(solver), d_commandStatus(nullptr), d_muted(false)
{
}
}
/* -------------------------------------------------------------------------- */
-/* class SynthFunCommand */
+/* class SynthFunCommand */
/* -------------------------------------------------------------------------- */
-SynthFunCommand::SynthFunCommand(const std::string& id,
- Expr func,
- Type sygusType,
+SynthFunCommand::SynthFunCommand(const api::Solver* solver,
+ const std::string& id,
+ api::Term fun,
+ const std::vector<api::Term>& vars,
+ api::Sort sort,
bool isInv,
- const std::vector<Expr>& vars)
+ api::Grammar* g)
: DeclarationDefinitionCommand(id),
- d_func(func),
- d_sygusType(sygusType),
+ d_fun(fun),
+ d_vars(vars),
+ d_sort(sort),
d_isInv(isInv),
- d_vars(vars)
+ d_grammar(g)
{
+ d_solver = solver;
}
-SynthFunCommand::SynthFunCommand(const std::string& id,
- Expr func,
- Type sygusType,
- bool isInv)
- : SynthFunCommand(id, func, sygusType, isInv, {})
+api::Term SynthFunCommand::getFunction() const { return d_fun; }
+
+const std::vector<api::Term>& SynthFunCommand::getVars() const
{
+ return d_vars;
}
-Expr SynthFunCommand::getFunction() const { return d_func; }
-const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; }
-Type SynthFunCommand::getSygusType() const { return d_sygusType; }
+api::Sort SynthFunCommand::getSort() const { return d_sort; }
bool SynthFunCommand::isInv() const { return d_isInv; }
+const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
+
void SynthFunCommand::invoke(SmtEngine* smtEngine)
{
try
{
- smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+ smtEngine->declareSynthFun(d_symbol,
+ d_fun.getExpr(),
+ d_grammar == nullptr
+ ? d_sort.getType()
+ : d_grammar->resolve().getType(),
+ d_isInv,
+ api::termVectorToExprs(d_vars));
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
Command* SynthFunCommand::exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap)
{
- return new SynthFunCommand(d_symbol,
- d_func.exportTo(exprManager, variableMap),
- d_sygusType.exportTo(exprManager, variableMap),
- d_isInv);
+ Unimplemented();
}
Command* SynthFunCommand::clone() const
{
- return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+ return new SynthFunCommand(
+ d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
}
std::string SynthFunCommand::getCommandName() const
/* -------------------------------------------------------------------------- */
DefineFunctionRecCommand::DefineFunctionRecCommand(
- api::Solver* solver,
+ const api::Solver* solver,
api::Term func,
const std::vector<api::Term>& formals,
api::Term formula,
}
DefineFunctionRecCommand::DefineFunctionRecCommand(
- api::Solver* solver,
+ const api::Solver* solver,
const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term>>& formals,
const std::vector<api::Term>& formulas,
return "get-instantiations";
}
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+/* -------------------------------------------------------------------------- */
+/* class GetInterpolCommand */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
const std::string& name,
api::Term conj)
: Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
{
}
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
const std::string& name,
api::Term conj,
- const Type& gtype)
+ api::Grammar* g)
: Command(solver),
d_name(name),
d_conj(conj),
- d_sygus_grammar_type(gtype),
+ d_sygus_grammar(g),
d_resultStatus(false)
{
}
api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
-Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; }
+
+const api::Grammar* GetInterpolCommand::getGrammar() const
+{
+ return d_sygus_grammar;
+}
+
api::Term GetInterpolCommand::getResult() const { return d_result; }
void GetInterpolCommand::invoke(SmtEngine* smtEngine)
{
try
{
- if (d_sygus_grammar_type.isNull())
+ if (!d_sygus_grammar)
{
d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
}
else
{
d_resultStatus =
- d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result);
+ d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
}
d_commandStatus = CommandSuccess::instance();
}
Command* GetInterpolCommand::clone() const
{
- GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj);
+ GetInterpolCommand* c =
+ new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
c->d_resultStatus = d_resultStatus;
return c;
return "get-interpol";
}
-GetAbductCommand::GetAbductCommand() {}
-GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
- : d_name(name), d_conj(conj), d_resultStatus(false)
+/* -------------------------------------------------------------------------- */
+/* class GetAbductCommand */
+/* -------------------------------------------------------------------------- */
+
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+ const std::string& name,
+ api::Term conj)
+ : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
{
}
-GetAbductCommand::GetAbductCommand(const std::string& name,
- Expr conj,
- const Type& gtype)
- : d_name(name),
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+ const std::string& name,
+ api::Term conj,
+ api::Grammar* g)
+ : Command(solver),
+ d_name(name),
d_conj(conj),
- d_sygus_grammar_type(gtype),
+ d_sygus_grammar(g),
d_resultStatus(false)
{
}
-Expr GetAbductCommand::getConjecture() const { return d_conj; }
-Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
+api::Term GetAbductCommand::getConjecture() const { return d_conj; }
+
+const api::Grammar* GetAbductCommand::getGrammar() const
+{
+ return d_sygus_grammar;
+}
+
std::string GetAbductCommand::getAbductName() const { return d_name; }
-Expr GetAbductCommand::getResult() const { return d_result; }
+api::Term GetAbductCommand::getResult() const { return d_result; }
void GetAbductCommand::invoke(SmtEngine* smtEngine)
{
try
{
- Node conjNode = Node::fromExpr(d_conj);
- Node resn;
- if (d_sygus_grammar_type.isNull())
+ if (!d_sygus_grammar)
{
- d_resultStatus = smtEngine->getAbduct(conjNode, resn);
+ d_resultStatus = d_solver->getAbduct(d_conj, d_result);
}
else
{
- TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type);
- d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn);
+ d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
}
- d_result = resn.toExpr();
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
Command* GetAbductCommand::exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap)
{
- GetAbductCommand* c =
- new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
- c->d_sygus_grammar_type =
- d_sygus_grammar_type.exportTo(exprManager, variableMap);
- c->d_result = d_result.exportTo(exprManager, variableMap);
- c->d_resultStatus = d_resultStatus;
- return c;
+ Unimplemented();
}
Command* GetAbductCommand::clone() const
{
- GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
- c->d_sygus_grammar_type = d_sygus_grammar_type;
+ GetAbductCommand* c =
+ new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
c->d_resultStatus = d_resultStatus;
return c;
protected:
// shouldn't construct a CommandStatus (use a derived class)
CommandStatus() {}
+
public:
virtual ~CommandStatus() {}
void toStream(std::ostream& out,
typedef CommandPrintSuccess printsuccess;
Command();
- Command(api::Solver* solver);
+ Command(const api::Solver* solver);
Command(const Command& cmd);
virtual ~Command();
}; /* class Command::ExportTransformer */
/** The solver instance that this command is associated with. */
- api::Solver* d_solver;
+ const api::Solver* d_solver;
/**
* This field contains a command status if the command has been
* successful execution.
*/
bool d_muted;
-}; /* class Command */
+}; /* class Command */
/**
* EmptyCommands are the residue of a command after the parser handles
class CVC4_PUBLIC DefineFunctionRecCommand : public Command
{
public:
- DefineFunctionRecCommand(api::Solver* solver,
+ DefineFunctionRecCommand(const api::Solver* solver,
api::Term func,
const std::vector<api::Term>& formals,
api::Term formula,
bool global);
- DefineFunctionRecCommand(api::Solver* solver,
+ DefineFunctionRecCommand(const api::Solver* solver,
const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term> >& formals,
const std::vector<api::Term>& formula,
class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
{
public:
- SynthFunCommand(const std::string& id,
- Expr func,
- Type sygusType,
+ SynthFunCommand(const api::Solver* solver,
+ const std::string& id,
+ api::Term fun,
+ const std::vector<api::Term>& vars,
+ api::Sort sort,
bool isInv,
- const std::vector<Expr>& vars);
- SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv);
+ api::Grammar* g);
/** returns the function-to-synthesize */
- Expr getFunction() const;
+ api::Term getFunction() const;
/** returns the input variables of the function-to-synthesize */
- const std::vector<Expr>& getVars() const;
- /** returns the sygus type of the function-to-synthesize */
- Type getSygusType() const;
+ const std::vector<api::Term>& getVars() const;
+ /** returns the sygus sort of the function-to-synthesize */
+ api::Sort getSort() const;
/** returns whether the function-to-synthesize should be an invariant */
bool isInv() const;
+ /** Get the sygus grammar given for the synth fun command */
+ const api::Grammar* getGrammar() const;
/** invokes this command
*
protected:
/** the function-to-synthesize */
- Expr d_func;
- /** sygus type of the function-to-synthesize
- *
- * If this type is a "sygus datatype" then it encodes a grammar for the
- * possible varlues of the function-to-sytnhesize
- */
- Type d_sygusType;
+ api::Term d_fun;
+ /** the input variables of the function-to-synthesize */
+ std::vector<api::Term> d_vars;
+ /** sort of the function-to-synthesize */
+ api::Sort d_sort;
/** whether the function-to-synthesize should be an invariant */
bool d_isInv;
- /** the input variables of the function-to-synthesize */
- std::vector<Expr> d_vars;
+ /** optional grammar for the possible values of the function-to-sytnhesize */
+ api::Grammar* d_grammar;
};
/** Declares a sygus constraint */
SmtEngine* d_smtEngine;
}; /* class GetSynthSolutionCommand */
-/** The command (get-interpol s B)
+/** The command (get-interpol s B (G)?)
*
* This command asks for an interpolant from the current set of assertions and
* conjecture (goal) B.
class CVC4_PUBLIC GetInterpolCommand : public Command
{
public:
- GetInterpolCommand(api::Solver* solver,
+ GetInterpolCommand(const api::Solver* solver,
const std::string& name,
api::Term conj);
- /** The argument gtype is the grammar of the interpolation query */
- GetInterpolCommand(api::Solver* solver,
+ /** The argument g is the grammar of the interpolation query */
+ GetInterpolCommand(const api::Solver* solver,
const std::string& name,
api::Term conj,
- const Type& gtype);
+ api::Grammar* g);
/** Get the conjecture of the interpolation query */
api::Term getConjecture() const;
- /** Get the grammar sygus datatype type given for the interpolation query */
- Type getGrammarType() const;
+ /** Get the sygus grammar given for the interpolation query */
+ const api::Grammar* getGrammar() const;
/** Get the result of the query, which is the solution to the interpolation
* query. */
api::Term getResult() const;
std::string d_name;
/** The conjecture of the interpolation query */
api::Term d_conj;
- /**
- * The (optional) grammar of the interpolation query, expressed as a sygus
- * datatype type.
- */
- Type d_sygus_grammar_type;
+ /** The (optional) grammar of the interpolation query */
+ api::Grammar* d_sygus_grammar;
/** the return status of the command */
bool d_resultStatus;
/** the return expression of the command */
* find a predicate P, then the output response of this command is:
* (define-fun s () Bool P)
*
- * A grammar type G can be optionally provided to indicate the syntactic
- * restrictions on the possible solutions returned.
+ * A grammar G can be optionally provided to indicate the syntactic restrictions
+ * on the possible solutions returned.
*/
class CVC4_PUBLIC GetAbductCommand : public Command
{
public:
- GetAbductCommand();
- GetAbductCommand(const std::string& name, Expr conj);
- GetAbductCommand(const std::string& name, Expr conj, const Type& gtype);
+ GetAbductCommand(const api::Solver* solver,
+ const std::string& name,
+ api::Term conj);
+ GetAbductCommand(const api::Solver* solver,
+ const std::string& name,
+ api::Term conj,
+ api::Grammar* g);
/** Get the conjecture of the abduction query */
- Expr getConjecture() const;
- /** Get the grammar type given for the abduction query */
- Type getGrammarType() const;
+ api::Term getConjecture() const;
+ /** Get the grammar given for the abduction query */
+ const api::Grammar* getGrammar() const;
/** Get the name of the abduction predicate for the abduction query */
std::string getAbductName() const;
/** Get the result of the query, which is the solution to the abduction query.
*/
- Expr getResult() const;
+ api::Term getResult() const;
void invoke(SmtEngine* smtEngine) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
/** The name of the abduction predicate */
std::string d_name;
/** The conjecture of the abduction query */
- Expr d_conj;
- /**
- * The (optional) grammar of the abduction query, expressed as a sygus
- * datatype type.
- */
- Type d_sygus_grammar_type;
+ api::Term d_conj;
+ /** The (optional) grammar of the abduction query */
+ api::Grammar* d_sygus_grammar;
/** the return status of the command */
bool d_resultStatus;
/** the return expression of the command */
- Expr d_result;
+ api::Term d_result;
}; /* class GetAbductCommand */
class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+
protected:
std::vector<Expr> d_result;
}; /* class GetUnsatAssumptionsCommand */
{
};
-} /* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__COMMAND_H */
setUserAttribute("sygus-synth-grammar", func, attr_value, "");
}
Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
- Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
+ // dumping SynthFunCommand from smt-engine is currently broken (please take at
+ // CVC4/cvc4-projects#211)
+ // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
// sygus conjecture is now stale
setSygusConjectureStale();
}
projects / cvc5.git / commitdiff