src/theory/quantifiers/trigger.h

   1 /*********************                                                        */
   2 /*! \file trigger.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief trigger class
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
  20 #define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
  21
  22 #include "theory/quantifiers/inst_match.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace inst {
  27
  28 //a collect of nodes representing a trigger
  29 class Trigger {
  30 private:
  31   /** computation of variable contains */
  32   static std::map< TNode, std::vector< TNode > > d_var_contains;
  33   static void computeVarContains( Node n );
  34   static void computeVarContains2( Node n, Node parent );
  35 private:
  36   /** the quantifiers engine */
  37   QuantifiersEngine* d_quantEngine;
  38   /** the quantifier this trigger is for */
  39   Node d_f;
  40   /** match generators */
  41   IMGenerator* d_mg;
  42 private:
  43   /** a trie of triggers */
  44   class TrTrie {
  45   private:
  46     Trigger* getTrigger2( std::vector< Node >& nodes );
  47     void addTrigger2( std::vector< Node >& nodes, Trigger* t );
  48   public:
  49     TrTrie() : d_tr( NULL ){}
  50     Trigger* d_tr;
  51     std::map< TNode, TrTrie* > d_children;
  52     Trigger* getTrigger( std::vector< Node >& nodes ){
  53       std::vector< Node > temp;
  54       temp.insert( temp.begin(), nodes.begin(), nodes.end() );
  55       std::sort( temp.begin(), temp.end() );
  56       return getTrigger2( temp );
  57     }
  58     void addTrigger( std::vector< Node >& nodes, Trigger* t ){
  59       std::vector< Node > temp;
  60       temp.insert( temp.begin(), nodes.begin(), nodes.end() );
  61       std::sort( temp.begin(), temp.end() );
  62       return addTrigger2( temp, t );
  63     }
  64   };/* class Trigger::TrTrie */
  65   /** all triggers will be stored in this trie */
  66   static TrTrie d_tr_trie;
  67 private:
  68   /** trigger constructor */
  69   Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false );
  70 public:
  71   ~Trigger(){}
  72 public:
  73   std::vector< Node > d_nodes;
  74 public:
  75   void debugPrint( const char* c );
  76   IMGenerator* getGenerator() { return d_mg; }
  77 public:
  78   /** reset instantiation round (call this whenever equivalence classes have changed) */
  79   void resetInstantiationRound();
  80   /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
  81   void reset( Node eqc );
  82   /** get next match.  must call reset( eqc ) once before this function. */
  83   bool getNextMatch( InstMatch& m );
  84   /** get the match against ground term or formula t.
  85       the trigger and t should have the same shape.
  86       Currently the trigger should not be a multi-trigger.
  87   */
  88   bool getMatch( Node t, InstMatch& m);
  89   /** add ground term t, called when t is added to the TermDb */
  90   int addTerm( Node t );
  91   /** return true if whatever Node is subsituted for the variables the
  92       given Node can't match the pattern */
  93   bool nonunifiable( TNode t, const std::vector<Node> & vars){
  94     return d_mg->nonunifiable(t,vars);
  95   }
  96   /** return whether this is a multi-trigger */
  97   bool isMultiTrigger() { return d_nodes.size()>1; }
  98 public:
  99   /** add all available instantiations exhaustively, in any equivalence class
 100       if limitInst>0, limitInst is the max # of instantiations to try */
 101   int addInstantiations( InstMatch& baseMatch );
 102   /** mkTrigger method
 103      ie     : quantifier engine;
 104      f      : forall something ....
 105      nodes  : (multi-)trigger
 106      matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* )
 107      keepAll: don't remove unneeded patterns;
 108      trOption : policy for dealing with triggers that already existed (see below)
 109   */
 110   enum{
 111     TR_MAKE_NEW,    //make new trigger even if it already may exist
 112     TR_GET_OLD,     //return a previous trigger if it had already been created
 113     TR_RETURN_NULL  //return null if a duplicate is found
 114   };
 115   static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
 116                              int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
 117                              bool smartTriggers = false );
 118   static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
 119                              int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
 120                              bool smartTriggers = false );
 121 private:
 122   /** is subterm of trigger usable */
 123   static bool isUsable( Node n, Node f );
 124   /** collect all APPLY_UF pattern terms for f in n */
 125   static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt );
 126 public:
 127   //different strategies for choosing trigger terms
 128   enum {
 129     TS_MAX_TRIGGER = 0,
 130     TS_MIN_TRIGGER,
 131     TS_ALL,
 132   };
 133   static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false );
 134 public:
 135   /** is usable trigger */
 136   static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
 137   static bool isUsableTrigger( Node n, Node f );
 138   static bool isAtomicTrigger( Node n );
 139   static bool isSimpleTrigger( Node n );
 140   /** filter all nodes that have instances */
 141   static void filterInstances( std::vector< Node >& nodes );
 142   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
 143   static int isInstanceOf( Node n1, Node n2 );
 144   /** variables subsume, return true if n1 contains all free variables in n2 */
 145   static bool isVariableSubsume( Node n1, Node n2 );
 146   /** get var contains */
 147   static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
 148   static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
 149   /** get pattern arithmetic */
 150   static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
 151
 152   inline void toStream(std::ostream& out) const {
 153     out << "TRIGGER( ";
 154     for( int i=0; i<(int)d_nodes.size(); i++ ){
 155       if( i>0 ){ out << ", "; }
 156       out << d_nodes[i];
 157     }
 158     out << " )";
 159   }
 160 };
 161
 162 inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
 163   tr.toStream(out);
 164   return out;
 165 }
 166
 167 }/* CVC4::theory::inst namespace */
 168 }/* CVC4::theory namespace */
 169 }/* CVC4 namespace */
 170
 171 #endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */