Split term database (#1206)

* Move equality query to own file, move equality inference to quantifiers engine.

* Move quantifiers attributes out of TermDb and into QuantAttribute.

* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.

* Split term database into term util.

* Partial fix for #1205 that eliminates need for dependency in node.cpp.

* Add more references to github issues.

1 files changed, 0 insertions, 12 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0c844f92d..75e37151a 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -22,9 +22,6 @@
 #include "base/output.h"
 #include "expr/attribute.h"
 
-#include "theory/quantifiers/term_database.h"
-
-
 using namespace std;
 
 namespace CVC4 {
@@ -113,15 +110,6 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
       for(iterator i = begin(); i != end() && !hasBv; ++i) {
         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;
-        }
-      }
     }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);