Separate sygus term utilities to new file, minor cleanup from last commit.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index e45ca49e0..0c844f92d 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -114,6 +114,10 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
         hasBv = (*i).hasBoundVar();
       }
       if( !hasBv ){
+        //FIXME : this is a hack to handle synthesis conjectures
+        // the issue is that we represent second-order quantification in synthesis conjectures via a Node:
+        //  exists x forall y P[f,y], where x is a dummy variable that maps to f through attribute SygusSynthFunVarListAttributeId
+        //  when asked whether a node has a bound variable, we want to treat f as if it were a bound (second-order) variable. -AJR
         if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
           hasBv = true;
         }