From 78373c7f5fe93b7e8bbea10e3924f24d25a618ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Oct 2017 14:52:31 -0500 Subject: Make Sygus conjectures higher-order (#1244) * Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks. * Minor fix * Fix bug in Node::hasBoundVar for non-ground operators. * Add regression. * Address review. * Apply clang format. --- src/parser/smt2/Smt2.g | 1 + src/parser/smt2/smt2.cpp | 14 +++++++++----- 2 files changed, 10 insertions(+), 5 deletions(-) (limited to 'src/parser') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 05faf040e..4d39c7635 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -626,6 +626,7 @@ sygusCommand [std::unique_ptr* cmd] 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 >::const_iterator i = diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bc9f2a06f..0fc3678c7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1081,13 +1081,17 @@ const void Smt2::getSygusPrimedVars( std::vector& vars, bool isPrimed ) { } const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ - //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute + // 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); - d_sygusFunSymbols.push_back(sym); - std::vector< Expr > attr_value; - attr_value.push_back( synth_fun ); - Command* cattr = new SetUserAttributeCommand("sygus-synth-fun", sym, attr_value); + attr_value.push_back(sym); + Command* cattr = + new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value); cattr->setMuted(true); preemptCommand(cattr); } -- cgit v1.2.3