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.

2 files changed, 10 insertions, 5 deletions

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<CVC4::Command>* 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<std::pair<std::string, CVC4::Type> >::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<Expr>& 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);
 }