Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.

The namespaces weren't changed, only the file locations.

1 files changed, 266 insertions, 0 deletions

diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
new file mode 100644
index 000000000..d2a246769
--- /dev/null
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -0,0 +1,266 @@
+/*********************                                                        */
+/*! \file rr_inst_match.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief inst match class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H
+#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H
+
+#include "theory/theory.h"
+#include "util/hash.h"
+#include "util/ntuple.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/quantifiers/inst_match.h"
+#include "expr/node_manager.h"
+#include "expr/node_builder.h"
+
+#include "theory/quantifiers/options.h"
+#include "theory/rewriterules/options.h"
+
+//#define USE_EFFICIENT_E_MATCHING
+
+namespace CVC4 {
+namespace theory {
+
+namespace rrinst{
+
+class CandidateGenerator
+{
+public:
+  CandidateGenerator(){}
+  virtual ~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( TNode eqc ) = 0;
+  virtual TNode getNextCandidate() = 0;
+  /** call this at the beginning of each instantiation round */
+  virtual void resetInstantiationRound() = 0;
+public:
+  /** legal candidate */
+  static inline bool isLegalCandidate( TNode n ){
+    return !n.getAttribute(NoMatchAttribute()) &&
+      ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) &&
+      ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) );
+}
+
+};
+
+
+inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
+  m.toStream(out);
+  return out;
+}
+
+template<bool modEq = false> class InstMatchTrie2;
+template<bool modEq = false> class InstMatchTrie2Pairs;
+
+template<bool modEq = false>
+class InstMatchTrie2Gen
+{
+  friend class InstMatchTrie2<modEq>;
+  friend class InstMatchTrie2Pairs<modEq>;
+
+private:
+
+  class Tree {
+  public:
+    typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel;
+    MLevel e;
+    const size_t level; //context level of creation
+    Tree() CVC4_UNDEFINED;
+    const Tree & operator =(const Tree & t){
+      Assert(t.e.empty()); Assert(e.empty());
+      Assert(t.level == level);
+      return t;
+    }
+    Tree(size_t l): level(l) {};
+    ~Tree(){
+      for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i)
+        delete(i->second);
+    };
+  };
+
+
+  typedef std::pair<Tree *, TNode> Mod;
+
+  class CleanUp{
+  public:
+    inline void operator()(Mod * m){
+      typename Tree::MLevel::iterator i = m->first->e.find(m->second);
+      Assert (i != m->first->e.end()); //should not have been already removed
+      m->first->e.erase(i);
+    };
+  };
+
+  EqualityQuery* d_eQ;
+  CandidateGenerator * d_cG;
+
+  context::Context* d_context;
+  context::CDList<Mod, CleanUp, std::allocator<Mod> > d_mods;
+
+
+  typedef std::map<Node, Node>::const_iterator mapIter;
+
+  /** add the substitution given by the iterator*/
+  void addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel);
+  /** test if it exists match, modulo uf-equations if modEq is true if
+   *  return false the deepest point of divergence is put in [e] and
+   *  [diverge].
+   */
+  bool existsInstMatch( Tree * root,
+                        mapIter & current, mapIter & end,
+                        Tree * & e, mapIter & diverge) const;
+
+  /** add match m in the trie root
+      return true if it was never seen */
+  bool addInstMatch( InstMatch& m, Tree * root);
+
+public:
+  InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* q);
+  InstMatchTrie2Gen(const InstMatchTrie2Gen &) CVC4_UNDEFINED;
+  const InstMatchTrie2Gen & operator =(const InstMatchTrie2Gen & e) CVC4_UNDEFINED;
+};
+
+template<bool modEq>
+class InstMatchTrie2
+{
+  typename InstMatchTrie2Gen<modEq>::Tree d_data;
+  InstMatchTrie2Gen<modEq> d_backtrack;
+public:
+  InstMatchTrie2(context::Context* c,  QuantifiersEngine* q): d_data(0),
+                                                              d_backtrack(c,q) {};
+  InstMatchTrie2(const InstMatchTrie2 &) CVC4_UNDEFINED;
+  const InstMatchTrie2 & operator =(const InstMatchTrie2 & e) CVC4_UNDEFINED;
+  /** add match m in the trie,
+      return true if it was never seen */
+  inline bool addInstMatch( InstMatch& m){
+    return d_backtrack.addInstMatch(m,&d_data);
+  };
+
+};/* class InstMatchTrie2 */
+
+class Matcher
+{
+public:
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
+  /** reset the term to match, return false if there is no such term */
+  virtual bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ) = 0;
+  /** get the next match. If it return false once you shouldn't call
+      getNextMatch again before doing a reset */
+  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
+  /** If reset, or getNextMatch return false they remove from the
+      InstMatch the binding that they have previously created */
+
+  /** virtual Matcher in order to have definned behavior */
+  virtual ~Matcher(){};
+};
+
+
+class ApplyMatcher: public Matcher{
+private:
+  /** What to check first: constant and variable */
+  std::vector< triple< TNode,size_t,EqualityQuery* > > d_constants;
+  std::vector< triple< TNode,size_t,EqualityQuery* > > d_variables;
+  /** children generators, only the sub-pattern which are
+      neither a variable neither a constant appears */
+  std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens;
+  /** the variable that have been set by this matcher (during its own reset) */
+  std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */
+  /** the representant of the argument of the term given by the last reset */
+  std::vector< Node > d_reps;
+public:
+  /** The pattern we are producing matches for */
+  Node d_pattern;
+public:
+  /** constructors */
+  ApplyMatcher( Node pat, QuantifiersEngine* qe);
+  /** destructor */
+  ~ApplyMatcher(){/*TODO delete dandling pointers? */}
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  void resetInstantiationRound( QuantifiersEngine* qe );
+  /** reset the term to match */
+  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe );
+  /** get the next match. */
+  bool getNextMatch(InstMatch& m, QuantifiersEngine* qe);
+private:
+  bool getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset);
+};
+
+
+/* Match literal so you don't choose the equivalence class( */
+class PatMatcher
+{
+public:
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
+  /** reset the matcher, return false if there is no such term */
+  virtual bool reset( InstMatch& m, QuantifiersEngine* qe ) = 0;
+  /** get the next match. If it return false once you shouldn't call
+      getNextMatch again before doing a reset */
+  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
+  /** If reset, or getNextMatch return false they remove from the
+      InstMatch the binding that they have previously created */
+};
+
+Matcher* mkMatcher( Node pat, QuantifiersEngine* qe );
+PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe );
+
+/* Match literal so you don't choose the equivalence class( */
+class PatsMatcher
+{
+public:
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
+  /** reset the matcher, return false if there is no such term */
+  virtual bool getNextMatch( QuantifiersEngine* qe ) = 0;
+  virtual const InstMatch& getInstMatch() = 0;
+  /** Add directly the instantiation to quantifiers engine */
+  virtual int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe) = 0;
+};
+
+PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe );
+PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe );
+
+/** return true if whatever Node is subsituted for the variables the
+    given Node can't match the pattern */
+bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars);
+
+class InstMatchGenerator;
+
+}/* CVC4::theory rrinst */
+
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */