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.

2 files changed, 3 insertions, 2 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 29f507238..1b3d7b23f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -624,8 +624,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
       }else{
         synth_fun_type = range;
       }
-      // allow overloading for synth fun
-      synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true);
+      // we do not allow overloading for synth fun
+      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
       seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index acfd886ce..a6830d95d 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1090,6 +1090,7 @@ 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
   Expr sym = mkBoundVar("sfproxy", t);
   d_sygusFunSymbols.push_back(sym);