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.

1 files changed, 5 insertions, 3 deletions

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;