${CMAKE_CURRENT_BINARY_DIR}/DeclarationDefinitionCommand.java
${CMAKE_CURRENT_BINARY_DIR}/DeclarationSequence.java
${CMAKE_CURRENT_BINARY_DIR}/DeclareFunctionCommand.java
+ ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusFunctionCommand.java
+ ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusPrimedVarCommand.java
+ ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusVarCommand.java
${CMAKE_CURRENT_BINARY_DIR}/DeclareTypeCommand.java
${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionCommand.java
${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionRecCommand.java
${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
${CMAKE_CURRENT_BINARY_DIR}/StringType.java
+ ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java
+ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
+ ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java
${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
if (PARSER_STATE->sygus())
{
// it is a higher-order universal variable
- PARSER_STATE->mkSygusVar(name, t);
- cmd->reset(new EmptyCommand());
+ Expr func = PARSER_STATE->mkBoundVar(name, t);
+ cmd->reset(new DeclareSygusFunctionCommand(name, func, t));
}
else
{
std::vector<Expr> terms;
std::vector<Expr> sygus_vars;
std::vector<std::pair<std::string, Type> > sortedVarNames;
- SExpr sexpr;
- std::unique_ptr<CVC4::CommandSequence> seq;
Type sygus_ret;
- int startIndex = -1;
Expr synth_fun;
Type sygus_type;
+ bool isInv;
}
: /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
- { PARSER_STATE->mkSygusVar(name, t);
- cmd->reset(new EmptyCommand());
+ {
+ Expr var = PARSER_STATE->mkBoundVar(name, t);
+ cmd->reset(new DeclareSygusVarCommand(name, var, t));
}
| /* declare-primed-var */
DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
- { PARSER_STATE->mkSygusVar(name, t, true);
- cmd->reset(new EmptyCommand());
+ {
+ // spurious command, we do not need to create a variable. We only keep
+ // track of the command for sanity checking / dumping
+ cmd->reset(new DeclareSygusPrimedVarCommand(name, t));
}
| /* synth-fun */
- ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } )
+ ( SYNTH_FUN_TOK { isInv = false; }
+ | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
+ )
{ PARSER_STATE->checkThatLogicIsSet(); }
symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- ( sortSymbol[range,CHECK_DECLARED] )? {
- if( range.isNull() ){
+ ( sortSymbol[range,CHECK_DECLARED] )?
+ {
+ if (range.isNull())
+ {
PARSER_STATE->parseError("Must supply return type for synth-fun.");
}
- if( range.isFunction() ){
- PARSER_STATE->parseError("Cannot use synth-fun with function return type.");
+ if (range.isFunction())
+ {
+ PARSER_STATE->parseError(
+ "Cannot use synth-fun with function return type.");
}
- seq.reset(new CommandSequence());
std::vector<Type> var_sorts;
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
- ++i) {
- var_sorts.push_back( (*i).second );
+ for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+ {
+ var_sorts.push_back(p.second);
}
Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
- Type synth_fun_type;
- if( var_sorts.size()>0 ){
- synth_fun_type = EXPR_MANAGER->mkFunctionType(var_sorts, range);
- }else{
- synth_fun_type = range;
- }
+ Type synth_fun_type = var_sorts.size() > 0
+ ? EXPR_MANAGER->mkFunctionType(var_sorts, range)
+ : range;
// we do not allow overloading for synth fun
synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
- // we add a declare function command here
- // this is the single unmuted command in the sequence generated by this smt2 command
- // TODO (as part of #1170) : make this a standard command.
- seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
- PARSER_STATE->pushScope(true);
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
- ++i) {
- Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
- sygus_vars.push_back( v );
- }
- Expr bvl;
- if (!sygus_vars.empty())
- {
- bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars);
- }
- // associate this variable list with the synth fun
- std::vector< Expr > attr_val_bvl;
- attr_val_bvl.push_back( bvl );
- Command* cattr_bvl = new SetUserAttributeCommand("sygus-synth-fun-var-list", synth_fun, attr_val_bvl);
- cattr_bvl->setMuted(true);
- PARSER_STATE->preemptCommand(cattr_bvl);
// set the sygus type to be range by default, which is overwritten below
// if a grammar is provided
sygus_type = range;
+ // create new scope for parsing the grammar, if any
+ PARSER_STATE->pushScope(true);
+ for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+ {
+ sygus_vars.push_back(PARSER_STATE->mkBoundVar(p.first, p.second));
+ }
}
(
// optionally, read the sygus grammar
+ //
+ // the sygus type specifies the required grammar for synth_fun, expressed
+ // as a type
sygusGrammar[sygus_type, sygus_vars, fun]
)?
- { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type
+ {
PARSER_STATE->popScope();
- // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute
- PARSER_STATE->addSygusFunSymbol(sygus_type, synth_fun);
- cmd->reset(seq.release());
+ Debug("parser-sygus") << "...read synth fun " << fun << std::endl;
+ cmd->reset(
+ new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars));
}
| /* constraint */
- CONSTRAINT_TOK {
+ CONSTRAINT_TOK {
PARSER_STATE->checkThatLogicIsSet();
Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
}
term[expr, expr2]
{ Debug("parser-sygus") << "...read constraint " << expr << std::endl;
- PARSER_STATE->addSygusConstraint(expr);
- cmd->reset(new EmptyCommand());
+ cmd->reset(new SygusConstraintCommand(expr));
}
- | INV_CONSTRAINT_TOK {
+ | INV_CONSTRAINT_TOK {
PARSER_STATE->checkThatLogicIsSet();
Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
}
- ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
+ ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
if( !terms.empty() ){
if( !PARSER_STATE->isDefinedFunction(name) ){
std::stringstream ss;
PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
"arguments.");
}
- // get variables (regular and their respective primed versions)
- std::vector<Expr> vars, primed_vars;
- PARSER_STATE->getSygusInvVars(terms[0].getType(), vars, primed_vars);
- // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
- for (unsigned i = 0; i < 4; ++i)
- {
- Expr op = terms[i];
- Debug("parser-sygus")
- << "Make inv-constraint term #" << i << " : " << op << " with type "
- << op.getType() << "..." << std::endl;
- std::vector<Expr> children;
- children.push_back(op);
- // transition relation applied over both variable lists
- if (i == 2)
- {
- children.insert(children.end(), vars.begin(), vars.end());
- children.insert(
- children.end(), primed_vars.begin(), primed_vars.end());
- }
- else
- {
- children.insert(children.end(), vars.begin(), vars.end());
- }
- terms[i] = EXPR_MANAGER->mkExpr(i == 0 ? kind::APPLY_UF : kind::APPLY,
- children);
- // make application of Inv on primed variables
- if (i == 0)
- {
- children.clear();
- children.push_back(op);
- children.insert(
- children.end(), primed_vars.begin(), primed_vars.end());
- terms.push_back(EXPR_MANAGER->mkExpr(kind::APPLY_UF, children));
- }
- }
- //make constraints
- std::vector< Expr > conj;
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1],
- terms[0] ) );
- const Expr term0_and_2 = EXPR_MANAGER->mkExpr(kind::AND, terms[0],
- terms[2] );
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, term0_and_2,
- terms[4] ) );
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3]) );
- Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj );
- Debug("parser-sygus") << "...read invariant constraint " << ic
- << std::endl;
- PARSER_STATE->addSygusConstraint(ic);
- cmd->reset(new EmptyCommand());
+
+ cmd->reset(new SygusInvConstraintCommand(terms));
}
| /* check-synth */
CHECK_SYNTH_TOK
{ PARSER_STATE->checkThatLogicIsSet(); }
- { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
- Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar);
- Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr);
- std::vector<Expr> bodyv;
- Debug("parser-sygus") << "Sygus : Constructing sygus constraint..."
- << std::endl;
- Expr body = EXPR_MANAGER->mkExpr(kind::NOT,
- PARSER_STATE->getSygusConstraints());
- Debug("parser-sygus") << "...constructed sygus constraint " << body
- << std::endl;
- if( !PARSER_STATE->getSygusVars().empty() ){
- Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST,
- PARSER_STATE->getSygusVars());
- body = EXPR_MANAGER->mkExpr(kind::EXISTS, boundVars, body);
- Debug("parser-sygus") << "...constructed exists " << body << std::endl;
- }
- if( !PARSER_STATE->getSygusFunSymbols().empty() ){
- Expr boundVars = EXPR_MANAGER->mkExpr(
- kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols());
- body = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, body, sygusAttr);
- }
- Debug("parser-sygus") << "...constructed forall " << body << std::endl;
- Command* c = new SetUserAttributeCommand("sygus", sygusVar);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
- cmd->reset(new CheckSynthCommand(body));
+ {
+ cmd->reset(new CheckSynthCommand());
}
| command[cmd]
;
*/
sygusGrammar[CVC4::Type & ret,
std::vector<CVC4::Expr>& sygus_vars,
- std::string& fun] @declarations
+ std::string& fun]
+@declarations
{
Type t;
std::string name;
}
}
-void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
-{
- if (!isPrimed)
- {
- d_sygusVars.push_back(mkBoundVar(name, type));
- }
-#ifdef CVC4_ASSERTIONS
- else
- {
- d_sygusVarPrimed.push_back(mkBoundVar(name, type));
- }
-#endif
-}
-
void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
if( type.isInteger() ){
ops.push_back(getExprManager()->mkConst(Rational(0)));
return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
}
-const void Smt2::getSygusInvVars(FunctionType t,
- std::vector<Expr>& vars,
- std::vector<Expr>& primed_vars)
-{
- std::vector<Type> argTypes = t.getArgTypes();
- ExprManager* em = getExprManager();
- for (const Type& ti : argTypes)
- {
- vars.push_back(em->mkBoundVar(ti));
- d_sygusVars.push_back(vars.back());
- std::stringstream ss;
- ss << vars.back() << "'";
- primed_vars.push_back(em->mkBoundVar(ss.str(), ti));
- d_sygusVars.push_back(primed_vars.back());
-#ifdef CVC4_ASSERTIONS
- bool find_new_declared_var = false;
- for (const Expr& e : d_sygusVarPrimed)
- {
- if (e.getType() == ti)
- {
- d_sygusVarPrimed.erase(
- std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e));
- find_new_declared_var = true;
- break;
- }
- }
- if (!find_new_declared_var)
- {
- ss.str("");
- ss << "warning: decleared primed variables do not match invariant's "
- "type\n";
- warning(ss.str());
- }
-#endif
- }
-}
-
-const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
- // When constructing the synthesis conjecture, we quantify on the
- // (higher-order) bound variable synth_fun.
- d_sygusFunSymbols.push_back(synth_fun);
-
- // Variable "sfproxy" carries the type, which may be a SyGuS datatype
- // that corresponds to syntactic restrictions.
- Expr sym = mkBoundVar("sfproxy", t);
- std::vector< Expr > attr_value;
- attr_value.push_back(sym);
- Command* cattr =
- new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
- cattr->setMuted(true);
- preemptCommand(cattr);
-}
-
InputLanguage Smt2::getLanguage() const
{
ExprManager* em = getExprManager();
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
- void addSygusConstraint(Expr constraint) {
- d_sygusConstraints.push_back(constraint);
- }
-
- Expr getSygusConstraints() {
- switch(d_sygusConstraints.size()) {
- case 0: return getExprManager()->mkConst(bool(true));
- case 1: return d_sygusConstraints[0];
- default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints);
- }
- }
-
- const std::vector<Expr>& getSygusVars() {
- return d_sygusVars;
- }
- /** retrieves the invariant variables (both regular and primed)
- *
- * To ensure that the variable list represent the correct argument type order
- * the type of the invariant predicate is used during the variable retrieval
- */
- const void getSygusInvVars(FunctionType t,
- std::vector<Expr>& vars,
- std::vector<Expr>& primed_vars);
-
- const void addSygusFunSymbol( Type t, Expr synth_fun );
- const std::vector<Expr>& getSygusFunSymbols() {
- return d_sygusFunSymbols;
- }
-
/**
* Smt2 parser provides its own checkDeclaration, which does the
* same as the base, but with some more helpful errors.
std::string QueryCommand::getCommandName() const { return "query"; }
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusVarCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
+ Expr var,
+ Type t)
+ : DeclarationDefinitionCommand(id), d_var(var), d_type(t)
+{
+}
+
+Expr DeclareSygusVarCommand::getVar() const { return d_var; }
+Type DeclareSygusVarCommand::getType() const { return d_type; }
+
+void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->declareSygusVar(d_symbol, d_var, d_type);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* DeclareSygusVarCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ return new DeclareSygusVarCommand(d_symbol,
+ d_var.exportTo(exprManager, variableMap),
+ d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusVarCommand::clone() const
+{
+ return new DeclareSygusVarCommand(d_symbol, d_var, d_type);
+}
+
+std::string DeclareSygusVarCommand::getCommandName() const
+{
+ return "declare-var";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusPrimedVarCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand(
+ const std::string& id, Type t)
+ : DeclarationDefinitionCommand(id), d_type(t)
+{
+}
+
+Type DeclareSygusPrimedVarCommand::getType() const { return d_type; }
+
+void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->declareSygusPrimedVar(d_symbol, d_type);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* DeclareSygusPrimedVarCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ return new DeclareSygusPrimedVarCommand(
+ d_symbol, d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusPrimedVarCommand::clone() const
+{
+ return new DeclareSygusPrimedVarCommand(d_symbol, d_type);
+}
+
+std::string DeclareSygusPrimedVarCommand::getCommandName() const
+{
+ return "declare-primed-var";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusFunctionCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusFunctionCommand::DeclareSygusFunctionCommand(const std::string& id,
+ Expr func,
+ Type t)
+ : DeclarationDefinitionCommand(id), d_func(func), d_type(t)
+{
+}
+
+Expr DeclareSygusFunctionCommand::getFunction() const { return d_func; }
+Type DeclareSygusFunctionCommand::getType() const { return d_type; }
+
+void DeclareSygusFunctionCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->declareSygusFunctionVar(d_symbol, d_func, d_type);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* DeclareSygusFunctionCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ return new DeclareSygusFunctionCommand(
+ d_symbol,
+ d_func.exportTo(exprManager, variableMap),
+ d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusFunctionCommand::clone() const
+{
+ return new DeclareSygusFunctionCommand(d_symbol, d_func, d_type);
+}
+
+std::string DeclareSygusFunctionCommand::getCommandName() const
+{
+ return "declare-fun";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SynthFunCommand */
+/* -------------------------------------------------------------------------- */
+
+SynthFunCommand::SynthFunCommand(const std::string& id,
+ Expr func,
+ Type sygusType,
+ bool isInv,
+ const std::vector<Expr>& vars)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_sygusType(sygusType),
+ d_isInv(isInv),
+ d_vars(vars)
+{
+}
+
+SynthFunCommand::SynthFunCommand(const std::string& id,
+ Expr func,
+ Type sygusType,
+ bool isInv)
+ : SynthFunCommand(id, func, sygusType, isInv, {})
+{
+}
+
+Expr SynthFunCommand::getFunction() const { return d_func; }
+const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; }
+Type SynthFunCommand::getSygusType() const { return d_sygusType; }
+bool SynthFunCommand::isInv() const { return d_isInv; }
+
+void SynthFunCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Command* SynthFunCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ return new SynthFunCommand(d_symbol,
+ d_func.exportTo(exprManager, variableMap),
+ d_sygusType.exportTo(exprManager, variableMap),
+ d_isInv);
+}
+
+Command* SynthFunCommand::clone() const
+{
+ return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+}
+
+std::string SynthFunCommand::getCommandName() const
+{
+ return d_isInv ? "synth-inv" : "synth-fun";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SygusConstraintCommand */
+/* -------------------------------------------------------------------------- */
+
+SygusConstraintCommand::SygusConstraintCommand(const Expr& e) : d_expr(e) {}
+
+void SygusConstraintCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->assertSygusConstraint(d_expr);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+Expr SygusConstraintCommand::getExpr() const { return d_expr; }
+
+Command* SygusConstraintCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ return new SygusConstraintCommand(d_expr.exportTo(exprManager, variableMap));
+}
+
+Command* SygusConstraintCommand::clone() const
+{
+ return new SygusConstraintCommand(d_expr);
+}
+
+std::string SygusConstraintCommand::getCommandName() const
+{
+ return "constraint";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SygusInvConstraintCommand */
+/* -------------------------------------------------------------------------- */
+
+SygusInvConstraintCommand::SygusInvConstraintCommand(
+ const std::vector<Expr>& predicates)
+ : d_predicates(predicates)
+{
+}
+
+SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv,
+ const Expr& pre,
+ const Expr& trans,
+ const Expr& post)
+ : SygusInvConstraintCommand(std::vector<Expr>{inv, pre, trans, post})
+{
+}
+
+void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->assertSygusInvConstraint(
+ d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+const std::vector<Expr>& SygusInvConstraintCommand::getPredicates() const
+{
+ return d_predicates;
+}
+
+Command* SygusInvConstraintCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ return new SygusInvConstraintCommand(d_predicates);
+}
+
+Command* SygusInvConstraintCommand::clone() const
+{
+ return new SygusInvConstraintCommand(d_predicates);
+}
+
+std::string SygusInvConstraintCommand::getCommandName() const
+{
+ return "inv-constraint";
+}
+
/* -------------------------------------------------------------------------- */
/* class CheckSynthCommand */
/* -------------------------------------------------------------------------- */
-CheckSynthCommand::CheckSynthCommand() : d_expr() {}
-CheckSynthCommand::CheckSynthCommand(const Expr& expr) : d_expr(expr) {}
-Expr CheckSynthCommand::getExpr() const { return d_expr; }
void CheckSynthCommand::invoke(SmtEngine* smtEngine)
{
try
{
- d_result = smtEngine->checkSynth(d_expr);
+ d_result = smtEngine->checkSynth();
d_commandStatus = CommandSuccess::instance();
smt::SmtScope scope(smtEngine);
d_solution.clear();
Command* CheckSynthCommand::exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap)
{
- CheckSynthCommand* c =
- new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
- c->d_result = d_result;
- return c;
+ return new CheckSynthCommand();
}
-Command* CheckSynthCommand::clone() const
-{
- CheckSynthCommand* c = new CheckSynthCommand(d_expr);
- c->d_result = d_result;
- return c;
-}
+Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
std::string getCommandName() const override;
}; /* class QueryCommand */
-class CVC4_PUBLIC CheckSynthCommand : public Command
+/* ------------------- sygus commands ------------------ */
+
+/** Declares a sygus universal variable */
+class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
+{
+ public:
+ DeclareSygusVarCommand(const std::string& id, Expr var, Type type);
+ /** returns the declared variable */
+ Expr getVar() const;
+ /** returns the declared variable's type */
+ Type getType() const;
+ /** invokes this command
+ *
+ * The declared sygus variable is communicated to the SMT engine in case a
+ * synthesis conjecture is built later on.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ protected:
+ /** the declared variable */
+ Expr d_var;
+ /** the declared variable's type */
+ Type d_type;
+};
+
+/** Declares a sygus primed variable, for invariant problems
+ *
+ * We do not actually build expressions for the declared variables because they
+ * are unnecessary for building SyGuS problems.
+ */
+class CVC4_PUBLIC DeclareSygusPrimedVarCommand
+ : public DeclarationDefinitionCommand
+{
+ public:
+ DeclareSygusPrimedVarCommand(const std::string& id, Type type);
+ /** returns the declared primed variable's type */
+ Type getType() const;
+
+ /** invokes this command
+ *
+ * The type of the primed variable is communicated to the SMT engine for
+ * debugging purposes when a synthesis conjecture is built later on.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ protected:
+ /** the type of the declared primed variable */
+ Type d_type;
+};
+
+/** Declares a sygus universal function variable */
+class CVC4_PUBLIC DeclareSygusFunctionCommand
+ : public DeclarationDefinitionCommand
+{
+ public:
+ DeclareSygusFunctionCommand(const std::string& id, Expr func, Type type);
+ /** returns the declared function variable */
+ Expr getFunction() const;
+ /** returns the declared function variable's type */
+ Type getType() const;
+ /** invokes this command
+ *
+ * The declared sygus function variable is communicated to the SMT engine in
+ * case a synthesis conjecture is built later on.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ protected:
+ /** the declared function variable */
+ Expr d_func;
+ /** the declared function variable's type */
+ Type d_type;
+};
+
+/** Declares a sygus function-to-synthesize
+ *
+ * This command is also used for the special case in which we are declaring an
+ * invariant-to-synthesize
+ */
+class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
{
public:
- CheckSynthCommand();
- CheckSynthCommand(const Expr& expr);
+ SynthFunCommand(const std::string& id,
+ Expr func,
+ Type sygusType,
+ bool isInv,
+ const std::vector<Expr>& vars);
+ SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv);
+ /** returns the function-to-synthesize */
+ Expr 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;
+ /** returns whether the function-to-synthesize should be an invariant */
+ bool isInv() const;
+
+ /** invokes this command
+ *
+ * The declared function-to-synthesize is communicated to the SMT engine in
+ * case a synthesis conjecture is built later on.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ 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;
+ /** 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;
+};
+/** Declares a sygus constraint */
+class CVC4_PUBLIC SygusConstraintCommand : public Command
+{
+ public:
+ SygusConstraintCommand(const Expr& e);
+ /** returns the declared constraint */
Expr getExpr() const;
- Result getResult() const;
+ /** invokes this command
+ *
+ * The declared constraint is communicated to the SMT engine in case a
+ * synthesis conjecture is built later on.
+ */
void invoke(SmtEngine* smtEngine) override;
- void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ /** exports command to given expression manager */
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
Command* clone() const override;
+ /** returns this command's name */
std::string getCommandName() const override;
protected:
- /** the assertion of check-synth */
+ /** the declared constraint */
Expr d_expr;
+};
+
+/** Declares a sygus invariant constraint
+ *
+ * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
+ * language: they are declared in terms of the previously declared
+ * invariant-to-synthesize, precondition, transition relation and condition.
+ *
+ * The actual constraint must be built such that the invariant is not stronger
+ * than the precondition, not weaker than the postcondition and inductive
+ * w.r.t. the transition relation.
+ */
+class CVC4_PUBLIC SygusInvConstraintCommand : public Command
+{
+ public:
+ SygusInvConstraintCommand(const std::vector<Expr>& predicates);
+ SygusInvConstraintCommand(const Expr& inv,
+ const Expr& pre,
+ const Expr& trans,
+ const Expr& post);
+ /** returns the place holder predicates */
+ const std::vector<Expr>& getPredicates() const;
+ /** invokes this command
+ *
+ * The place holders are communicated to the SMT engine and the actual
+ * invariant constraint is built, in case an actual synthesis conjecture is
+ * built later on.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ protected:
+ /** the place holder predicates with which to build the actual constraint
+ * (i.e. the invariant, precondition, transition relation and postcondition)
+ */
+ std::vector<Expr> d_predicates;
+};
+
+/** Declares a synthesis conjecture */
+class CVC4_PUBLIC CheckSynthCommand : public Command
+{
+ public:
+ CheckSynthCommand(){};
+ /** returns the result of the check-synth call */
+ Result getResult() const;
+ /** prints the result of the check-synth-call */
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ /** invokes this command
+ *
+ * This invocation makes the SMT engine build a synthesis conjecture based on
+ * previously declared information (such as universal variables,
+ * functions-to-synthesize and so on), set up attributes to guide the solving,
+ * and then perform a satisfiability check, whose result is stored in
+ * d_result.
+ */
+ void invoke(SmtEngine* smtEngine) override;
+ /** exports command to given expression manager */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ /** creates a copy of this command */
+ Command* clone() const override;
+ /** returns this command's name */
+ std::string getCommandName() const override;
+
+ protected:
/** result of the check-synth call */
Result d_result;
/** string stream that stores the output of the solution */
std::stringstream d_solution;
-}; /* class CheckSynthCommand */
+};
+
+/* ------------------- sygus commands ------------------ */
// this is TRANSFORM in the CVC presentation language
class CVC4_PUBLIC SimplifyCommand : public Command
/* Finishes the initialization of the private portion of SMTEngine. */
void finishInit();
+ /*------------------- sygus utils ------------------*/
+ /**
+ * sygus variables declared (from "declare-var" and "declare-fun" commands)
+ *
+ * The SyGuS semantics for declared variables is that they are implicitly
+ * universally quantified in the constraints.
+ */
+ std::vector<Node> d_sygusVars;
+ /** types of sygus primed variables (for debugging) */
+ std::vector<Type> d_sygusPrimedVarTypes;
+ /** sygus constraints */
+ std::vector<Node> d_sygusConstraints;
+ /** functions-to-synthesize */
+ std::vector<Node> d_sygusFunSymbols;
+ /** maps functions-to-synthesize to their respective input variables lists */
+ std::map<Node, std::vector<Node>> d_sygusFunVars;
+ /** maps functions-to-synthesize to their respective syntactic restrictions
+ *
+ * If function has syntactic restrictions, these are encoded as a SyGuS
+ * datatype type
+ */
+ std::map<Node, TypeNode> d_sygusFunSyntax;
+
+ /*------------------- end of sygus utils ------------------*/
+
private:
std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
return res;
}
-Result SmtEngine::checkSynth(const Expr& e)
-{
- SmtScope smts(this);
- Trace("smt") << "Check synth: " << e << std::endl;
- Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
- return checkSatisfiability(e, true, false);
-}
-
Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
{
Assert(ex.getExprManager() == d_exprManager);
return quickCheck().asValidityResult();
}/* SmtEngine::assertFormula() */
+/*
+ --------------------------------------------------------------------------
+ Handling SyGuS commands
+ --------------------------------------------------------------------------
+*/
+
+void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
+{
+ d_private->d_sygusVars.push_back(Node::fromExpr(var));
+ Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
+}
+
+void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
+{
+#ifdef CVC4_ASSERTIONS
+ d_private->d_sygusPrimedVarTypes.push_back(type);
+#endif
+ Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
+}
+
+void SmtEngine::declareSygusFunctionVar(const std::string& id,
+ Expr var,
+ Type type)
+{
+ d_private->d_sygusVars.push_back(Node::fromExpr(var));
+ Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
+}
+
+void SmtEngine::declareSynthFun(const std::string& id,
+ Expr func,
+ Type sygusType,
+ bool isInv,
+ const std::vector<Expr>& vars)
+{
+ Node fn = Node::fromExpr(func);
+ d_private->d_sygusFunSymbols.push_back(fn);
+ std::vector<Node> var_nodes;
+ for (const Expr& v : vars)
+ {
+ var_nodes.push_back(Node::fromExpr(v));
+ }
+ d_private->d_sygusFunVars[fn] = var_nodes;
+ // whether sygus type encodes syntax restrictions
+ if (sygusType.isDatatype()
+ && static_cast<DatatypeType>(sygusType).getDatatype().isSygus())
+ {
+ d_private->d_sygusFunSyntax[fn] = TypeNode::fromType(sygusType);
+ }
+ Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
+}
+
+void SmtEngine::assertSygusConstraint(Expr constraint)
+{
+ d_private->d_sygusConstraints.push_back(constraint);
+
+ Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
+}
+
+void SmtEngine::assertSygusInvConstraint(const Expr& inv,
+ const Expr& pre,
+ const Expr& trans,
+ const Expr& post)
+{
+ SmtScope smts(this);
+ // build invariant constraint
+
+ // get variables (regular and their respective primed versions)
+ std::vector<Node> terms, vars, primed_vars;
+ terms.push_back(Node::fromExpr(inv));
+ terms.push_back(Node::fromExpr(pre));
+ terms.push_back(Node::fromExpr(trans));
+ terms.push_back(Node::fromExpr(post));
+ // variables are built based on the invariant type
+ FunctionType t = static_cast<FunctionType>(inv.getType());
+ std::vector<Type> argTypes = t.getArgTypes();
+ for (const Type& ti : argTypes)
+ {
+ TypeNode tn = TypeNode::fromType(ti);
+ vars.push_back(d_nodeManager->mkBoundVar(tn));
+ d_private->d_sygusVars.push_back(vars.back());
+ std::stringstream ss;
+ ss << vars.back() << "'";
+ primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn));
+ d_private->d_sygusVars.push_back(primed_vars.back());
+#ifdef CVC4_ASSERTIONS
+ bool find_new_declared_var = false;
+ for (const Type& t : d_private->d_sygusPrimedVarTypes)
+ {
+ if (t == ti)
+ {
+ d_private->d_sygusPrimedVarTypes.erase(
+ std::find(d_private->d_sygusPrimedVarTypes.begin(),
+ d_private->d_sygusPrimedVarTypes.end(),
+ t));
+ find_new_declared_var = true;
+ break;
+ }
+ }
+ if (!find_new_declared_var)
+ {
+ Warning()
+ << "warning: declared primed variables do not match invariant's "
+ "type\n";
+ }
+#endif
+ }
+
+ // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
+ for (unsigned i = 0; i < 4; ++i)
+ {
+ Node op = terms[i];
+ Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
+ << " with type " << op.getType() << "...\n";
+ std::vector<Node> children;
+ children.push_back(op);
+ // transition relation applied over both variable lists
+ if (i == 2)
+ {
+ children.insert(children.end(), vars.begin(), vars.end());
+ children.insert(children.end(), primed_vars.begin(), primed_vars.end());
+ }
+ else
+ {
+ children.insert(children.end(), vars.begin(), vars.end());
+ }
+ terms[i] =
+ d_nodeManager->mkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children);
+ // make application of Inv on primed variables
+ if (i == 0)
+ {
+ children.clear();
+ children.push_back(op);
+ children.insert(children.end(), primed_vars.begin(), primed_vars.end());
+ terms.push_back(d_nodeManager->mkNode(kind::APPLY_UF, children));
+ }
+ }
+ // make constraints
+ std::vector<Node> conj;
+ conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[1], terms[0]));
+ Node term0_and_2 = d_nodeManager->mkNode(kind::AND, terms[0], terms[2]);
+ conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, term0_and_2, terms[4]));
+ conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[0], terms[3]));
+ Node constraint = d_nodeManager->mkNode(kind::AND, conj);
+
+ d_private->d_sygusConstraints.push_back(constraint);
+
+ Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n";
+}
+
+Result SmtEngine::checkSynth()
+{
+ SmtScope smts(this);
+ // build synthesis conjecture from asserted constraints and declared
+ // variables/functions
+ Node sygusVar =
+ d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType());
+ Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar);
+ Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr);
+ std::vector<Node> bodyv;
+ Trace("smt") << "Sygus : Constructing sygus constraint...\n";
+ unsigned n_constraints = d_private->d_sygusConstraints.size();
+ Node body = n_constraints == 0
+ ? d_nodeManager->mkConst(true)
+ : (n_constraints == 1
+ ? d_private->d_sygusConstraints[0]
+ : d_nodeManager->mkNode(
+ kind::AND, d_private->d_sygusConstraints));
+ body = body.notNode();
+ Trace("smt") << "...constructed sygus constraint " << body << std::endl;
+ if (!d_private->d_sygusVars.empty())
+ {
+ Node boundVars =
+ d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars);
+ body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body);
+ Trace("smt") << "...constructed exists " << body << std::endl;
+ }
+ if (!d_private->d_sygusFunSymbols.empty())
+ {
+ Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
+ d_private->d_sygusFunSymbols);
+ body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr);
+ }
+ Trace("smt") << "...constructed forall " << body << std::endl;
+
+ // set attribute for synthesis conjecture
+ setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
+
+ // set attributes for functions-to-synthesize
+ for (const Node& synth_fun : d_private->d_sygusFunSymbols)
+ {
+ // associate var list with function-to-synthesize
+ Assert(d_private->d_sygusFunVars.find(synth_fun)
+ != d_private->d_sygusFunVars.end());
+ const std::vector<Node>& vars = d_private->d_sygusFunVars[synth_fun];
+ Node bvl;
+ if (!vars.empty())
+ {
+ bvl = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, vars);
+ }
+ std::vector<Expr> attr_val_bvl;
+ attr_val_bvl.push_back(bvl.toExpr());
+ setUserAttribute(
+ "sygus-synth-fun-var-list", synth_fun.toExpr(), attr_val_bvl, "");
+ // If the function has syntax restrition, bulid a variable "sfproxy" which
+ // carries the type, a SyGuS datatype that corresponding to the syntactic
+ // restrictions.
+ std::map<Node, TypeNode>::const_iterator it =
+ d_private->d_sygusFunSyntax.find(synth_fun);
+ if (it != d_private->d_sygusFunSyntax.end())
+ {
+ Node sym = d_nodeManager->mkBoundVar("sfproxy", it->second);
+ std::vector<Expr> attr_value;
+ attr_value.push_back(sym.toExpr());
+ setUserAttribute(
+ "sygus-synth-grammar", synth_fun.toExpr(), attr_value, "");
+ }
+ }
+
+ Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
+
+ return checkSatisfiability(body.toExpr(), true, false);
+}
+
+/*
+ --------------------------------------------------------------------------
+ End of Handling SyGuS commands
+ --------------------------------------------------------------------------
+*/
+
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
return node;
}
*/
std::vector<Expr> getUnsatAssumptions(void);
+ /*------------------- sygus commands ------------------*/
+
+ /** adds a variable declaration
+ *
+ * Declared SyGuS variables may be used in SyGuS constraints, in which they
+ * are assumed to be universally quantified.
+ */
+ void declareSygusVar(const std::string& id, Expr var, Type type);
+ /** stores information for debugging sygus invariants setup
+ *
+ * Since in SyGuS the commands "declare-primed-var" are not necessary for
+ * building invariant constraints, we only use them to check that the number
+ * of variables declared corresponds to the number of arguments of the
+ * invariant-to-synthesize.
+ */
+ void declareSygusPrimedVar(const std::string& id, Type type);
+ /** adds a function variable declaration
+ *
+ * Is SyGuS semantics declared functions are treated in the same manner as
+ * declared variables, i.e. as universally quantified (function) variables
+ * which can occur in the SyGuS constraints that compose the conjecture to
+ * which a function is being synthesized.
+ */
+ void declareSygusFunctionVar(const std::string& id, Expr var, Type type);
+ /** adds a function-to-synthesize declaration
+ *
+ * The given type may not correspond to the actual function type but to a
+ * datatype encoding the syntax restrictions for the
+ * function-to-synthesize. In this case this information is stored to be used
+ * during solving.
+ *
+ * vars contains the arguments of the function-to-synthesize. These variables
+ * are also stored to be used during solving.
+ *
+ * isInv determines whether the function-to-synthesize is actually an
+ * invariant. This information is necessary if we are dumping a command
+ * corresponding to this declaration, so that it can be properly printed.
+ */
+ void declareSynthFun(const std::string& id,
+ Expr func,
+ Type type,
+ bool isInv,
+ const std::vector<Expr>& vars);
+ /** adds a regular sygus constraint */
+ void assertSygusConstraint(Expr constraint);
+ /** adds an invariant constraint
+ *
+ * Invariant constraints are not explicitly declared: they are given in terms
+ * of the invariant-to-synthesize, the pre condition, transition relation and
+ * post condition. The actual constraint is built based on the inputs of these
+ * place holder predicates :
+ *
+ * PRE(x) -> INV(x)
+ * INV() ^ TRANS(x, x') -> INV(x')
+ * INV(x) -> POST(x)
+ *
+ * The regular and primed variables are retrieved from the declaration of the
+ * invariant-to-synthesize.
+ */
+ void assertSygusInvConstraint(const Expr& inv,
+ const Expr& pre,
+ const Expr& trans,
+ const Expr& post);
/**
* Assert a synthesis conjecture to the current context and call
* check(). Returns sat, unsat, or unknown result.
+ *
+ * The actual synthesis conjecture is built based on the previously
+ * communicated information to this module (universal variables, defined
+ * functions, functions-to-synthesize, and which constraints compose it). The
+ * built conjecture is a higher-order formula of the form
+ *
+ * exists f1...fn . forall v1...vm . F
+ *
+ * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
+ * universal variables and F is the set of declared constraints.
*/
- Result checkSynth(const Expr& e) /* throw(Exception) */;
+ Result checkSynth() /* throw(Exception) */;
+
+ /*------------------- end of sygus commands-------------*/
/**
* Simplify a formula without doing "much" work. Does not involve
projects / cvc5.git / commitdiff