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.

10 files changed, 34 insertions, 29 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 75e37151a..126feadd8 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -111,6 +111,9 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
         hasBv = (*i).hasBoundVar();
       }
     }
+    if (!hasBv && hasOperator()) {
+      hasBv = getOperator().hasBoundVar();
+    }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);
     Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl;
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);
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4bcb78867..e32d8913d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4574,12 +4574,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
       Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
       quantifiers::SingleInvocationPartition sip;
       std::vector< Node > funcs;
-      for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){
-        // TODO : revisit this when addressing #1205
-        Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute());
-        Assert( !sf.isNull() );
-        funcs.push_back( sf );
-      }
+      funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
       sip.init( funcs, conj_se );
       Trace("smt-synth") << "...finished, got:" << std::endl;
       sip.debugPrint("smt-synth");
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index a838a6a0c..a380dcbf2 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -72,11 +72,10 @@ void CegConjecture::assign( Node q ) {
     // carry the templates
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
       Node v = q[0][i];
-      Node sf = v.getAttribute(SygusSynthFunAttribute());
-      Node templ = d_ceg_si->getTemplate(sf);
+      Node templ = d_ceg_si->getTemplate(v);
       if( !templ.isNull() ){
-        templates[sf] = templ;
-        templates_arg[sf] = d_ceg_si->getTemplateArg(sf);
+        templates[v] = templ;
+        templates_arg[v] = d_ceg_si->getTemplateArg(v);
       }
     }
   }
@@ -562,7 +561,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         status = 1;
         
         //check if there was a template
-        Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute());
+        Node sf = d_quant[0][i];
         Node templ = d_ceg_si->getTemplate( sf );
         if( !templ.isNull() ){
           Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index bf09c83f7..3349492a2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -126,8 +126,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
   std::vector< Node > progs;
   std::map< Node, std::vector< Node > > prog_vars;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node v = q[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
+    Node sf = q[0][i];
     progs.push_back( sf );
     Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
     for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
@@ -469,7 +468,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   Assert( !d_lemmas_produced.empty() );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
-  Node prog = d_quant[0][sol_index].getAttribute(SygusSynthFunAttribute());
+  Node prog = d_quant[0][sol_index];
   std::vector< Node > vars;
   Node s;
   if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index ac3fb85d1..c9a7f07ab 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -51,11 +51,12 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
     SygusAttribute ca;
     n.setAttribute( ca, true );
-  }else if( attr=="sygus-synth-fun" ){
+  } else if (attr == "sygus-synth-grammar") {
     Assert( node_values.size()==1 );
-    Trace("quant-attr-debug") << "Set sygus synth fun " << n << " to "  << node_values[0] << std::endl;
-    SygusSynthFunAttribute ssfa;
-    n.setAttribute( ssfa, node_values[0] );
+    Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
+                              << node_values[0] << std::endl;
+    SygusSynthGrammarAttribute ssg;
+    n.setAttribute(ssg, node_values[0]);
   }else if( attr=="sygus-synth-fun-var-list" ){
     Assert( node_values.size()==1 );
     Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index 2eb541e66..6152417a5 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -83,9 +83,11 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
   std::vector< Node > ebvl;
   Node qbody_subs = q[1];
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node v = q[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
-    Assert( !sf.isNull() );
+    Node sf = q[0][i];
+    // v encodes the syntactic restrictions (via an inductive datatype) on sf
+    // from the input
+    Node v = sf.getAttribute(SygusSynthGrammarAttribute());
+    Assert(!v.isNull());
     Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
     // sfvl may be null for constant synthesis functions
     Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 2360c5bfb..a0b3b8ec2 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -73,8 +73,9 @@ struct SygusProxyAttributeId {};
 typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
 
 // attribute for associating a synthesis function with a first order variable
-struct SygusSynthFunAttributeId {};
-typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute;
+struct SygusSynthGrammarAttributeId {};
+typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
+    SygusSynthGrammarAttribute;
 
 // attribute for associating a variable list with a synth fun
 struct SygusSynthFunVarListAttributeId {};
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 855cdb911..66e05b1cd 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -44,7 +44,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute( "conjecture", this );
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
-  out.handleUserAttribute( "sygus-synth-fun", this );
+  out.handleUserAttribute("sygus-synth-grammar", this);
   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
   out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );