Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 262085a23..e45ca49e0 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -22,6 +22,8 @@
 #include "base/output.h"
 #include "expr/attribute.h"
 
+#include "theory/quantifiers/term_database.h"
+
 
 using namespace std;
 
@@ -111,6 +113,11 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
       for(iterator i = begin(); i != end() && !hasBv; ++i) {
         hasBv = (*i).hasBoundVar();
       }
+      if( !hasBv ){
+        if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
+          hasBv = true;
+        }
+      }
     }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);