merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

1 files changed, 5 insertions, 45 deletions

diff --git a/src/theory/inst_match.h b/src/theory/inst_match.h
index 31a59b261..2b402779d 100644
--- a/src/theory/inst_match.h
+++ b/src/theory/inst_match.h
@@ -19,16 +19,14 @@
 #ifndef __CVC4__INST_MATCH_H
 #define __CVC4__INST_MATCH_H
 
-#include "theory/theory.h"
 #include "util/hash.h"
 
 #include <ext/hash_set>
 #include <iostream>
 #include <map>
 
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
 #include "context/cdlist.h"
+#include "theory/candidate_generator.h"
 
 //#define USE_EFFICIENT_E_MATCHING
 
@@ -76,48 +74,6 @@ namespace uf{
 
 namespace inst {
 
-class CandidateGenerator
-{
-public:
-  CandidateGenerator(){}
-  ~CandidateGenerator(){}
-
-  /** Get candidates functions.  These set up a context to get all match candidates.
-      cg->reset( eqc );
-      do{
-        Node cand = cg->getNextCandidate();
-        //.......
-      }while( !cand.isNull() );
-
-      eqc is the equivalence class you are searching in
-  */
-  virtual void reset( Node eqc ) = 0;
-  virtual Node getNextCandidate() = 0;
-  /** add candidate to list of nodes returned by this generator */
-  virtual void addCandidate( Node n ) {}
-  /** call this at the beginning of each instantiation round */
-  virtual void resetInstantiationRound() = 0;
-public:
-  /** legal candidate */
-  static bool isLegalCandidate( Node n );
-};/* class CandidateGenerator */
-
-/** candidate generator queue (for manual candidate generation) */
-class CandidateGeneratorQueue : public CandidateGenerator {
-private:
-  std::vector< Node > d_candidates;
-  int d_candidate_index;
-public:
-  CandidateGeneratorQueue() : d_candidate_index( 0 ){}
-  ~CandidateGeneratorQueue(){}
-
-  void addCandidate( Node n );
-
-  void resetInstantiationRound(){}
-  void reset( Node eqc );
-  Node getNextCandidate();
-};/* class CandidateGeneratorQueue */
-
 class EqualityQuery {
 public:
   EqualityQuery(){}
@@ -135,6 +91,10 @@ public:
       not contain instantiation constants, if such a term exists.
    */
   virtual Node getInternalRepresentative( Node a ) = 0;
+  /** get the equality engine associated with this query */
+  virtual eq::EqualityEngine* getEngine() = 0;
+  /** get the equivalence class of a */
+  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
 };/* class EqualityQuery */
 
 /** basic class defining an instantiation */