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, 76 insertions, 0 deletions

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
new file mode 100644
index 000000000..c3e0a8c5b
--- /dev/null
+++ b/src/theory/quantifiers/equality_query.h
@@ -0,0 +1,76 @@
+/*********************                                                        */
+/*! \file equality_query.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Equality query class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+// TODO : (as part of #1171, #1214) further document and clean this class.
+/** equality query object using theory engine */
+class EqualityQueryQuantifiersEngine : public EqualityQuery
+{
+private:
+  /** pointer to theory engine */
+  QuantifiersEngine* d_qe;
+  /** quantifiers equality inference */
+  context::CDO< unsigned > d_eqi_counter;
+  /** internal representatives */
+  std::map< TypeNode, std::map< Node, Node > > d_int_rep;
+  /** rep score */
+  std::map< Node, int > d_rep_score;
+  /** reset count */
+  int d_reset_count;
+
+  /** processInferences : will merge equivalence classes in master equality engine, if possible */
+  bool processInferences( Theory::Effort e );
+  /** node contains */
+  Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
+  /** get score */
+  int getRepScore( Node n, Node f, int index, TypeNode v_tn );
+  /** flatten representatives */
+  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
+public:
+  EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
+  virtual ~EqualityQueryQuantifiersEngine();
+  /** reset */
+  bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "EqualityQueryQE"; }
+  /** general queries about equality */
+  bool hasTerm( Node a );
+  Node getRepresentative( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  eq::EqualityEngine* getEngine();
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
+  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
+      If cbqi is active, this will return a term in the equivalence class of "a" that does
+      not contain instantiation constants, if such a term exists.
+   */
+  Node getInternalRepresentative( Node a, Node f, int index );
+}; /* EqualityQueryQuantifiersEngine */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */