diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/bindings/java/CMakeLists.txt | 6 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 182 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 67 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 29 | ||||
| -rw-r--r-- | src/smt/command.cpp | 302 | ||||
| -rw-r--r-- | src/smt/command.h | 240 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 262 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 77 |
8 files changed, 907 insertions, 258 deletions
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index c3fee67a5..3423a3e1b 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -77,6 +77,9 @@ set(gen_java_files ${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 @@ -200,7 +203,10 @@ set(gen_java_files ${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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ebf50283d..b8b05f7dd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -356,8 +356,8 @@ command [std::unique_ptr<CVC4::Command>* cmd] 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 { @@ -605,111 +605,99 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] 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; @@ -724,85 +712,14 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] 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] ; @@ -818,7 +735,8 @@ sygusCommand [std::unique_ptr<CVC4::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; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4046b7c2..2fd61aabc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -630,20 +630,6 @@ void Smt2::includeFile(const std::string& filename) { } } -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))); @@ -1234,59 +1220,6 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt, 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(); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 80bd8df83..2d57332af 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -273,35 +273,6 @@ private: 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. diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3d838d21c..51cb6663f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -562,17 +562,299 @@ Command* QueryCommand::clone() const 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(); @@ -624,18 +906,10 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const 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"; } diff --git a/src/smt/command.h b/src/smt/command.h index be6d84305..f7824c1aa 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -613,29 +613,255 @@ class CVC4_PUBLIC QueryCommand : public Command 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 196da6b9c..a2dd8276b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -497,6 +497,31 @@ class SmtEnginePrivate : public NodeManagerListener { /* 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; @@ -3692,14 +3717,6 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) 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); @@ -3724,6 +3741,235 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) 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; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 08bb773d6..5aa59fad7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -608,11 +608,86 @@ class CVC4_PUBLIC SmtEngine { */ 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 |