src/theory/quantifiers/ematching/trigger_term_info.h

   1 /*********************                                                        */
   2 /*! \file trigger_term_info.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief trigger term info class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
  18 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
  19
  20 #include <map>
  21
  22 #include "expr/node.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace inst {
  27
  28 /** Information about a node used in a trigger.
  29  *
  30  * This information includes:
  31  * 1. the free variables of the node, and
  32  * 2. information about which terms are useful for matching.
  33  *
  34  * As an example, consider the trigger
  35  *   { f( x ), g( y ), P( y, z ) }
  36  * for quantified formula
  37  *   forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
  38  *
  39  * Notice that it is only useful to match f( x ) to f-applications not in the
  40  * equivalence class of b, and P( y, z ) to P-applications not in the
  41  * equivalence class of true, as such instances will always be entailed by the
  42  * ground equalities and disequalities the current context. Entailed instances
  43  * are typically not helpful, and are discarded in
  44  * Instantiate::addInstantiation(...) unless the option --no-inst-no-entail is
  45  * enabled. For more details, see page 10 of "Congruence Closure with Free
  46  * Variables", Barbosa et al., TACAS 2017.
  47  *
  48  * This example is referenced for each of the functions below.
  49  */
  50 class TriggerTermInfo
  51 {
  52  public:
  53   TriggerTermInfo() : d_reqPol(0), d_weight(0) {}
  54   ~TriggerTermInfo() {}
  55   /** The free variables in the node
  56    *
  57    * In the trigger term info for f( x ) in the above example, d_fv = { x }
  58    * In the trigger term info for g( y ) in the above example, d_fv = { y }
  59    * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z
  60    * }
  61    */
  62   std::vector<Node> d_fv;
  63   /** Required polarity:  1 for equality, -1 for disequality, 0 for none
  64    *
  65    * In the trigger term info for f( x ) in the above example, d_reqPol = -1
  66    * In the trigger term info for g( y ) in the above example, d_reqPol = 0
  67    * In the trigger term info for P( y, z ) in the above example,  d_reqPol = 1
  68    */
  69   int d_reqPol;
  70   /** Required polarity equal term
  71    *
  72    * If d_reqPolEq is not null,
  73    *   if d_reqPol = 1, then this trigger term must be matched to terms in the
  74    *                    equivalence class of d_reqPolEq,
  75    *   if d_reqPol = -1, then this trigger term must be matched to terms *not*
  76    * in the equivalence class of d_reqPolEq.
  77    *
  78    * This information is typically chosen by analyzing the entailed equalities
  79    * and disequalities of quantified formulas.
  80    * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
  81    * In the trigger term info for g( y ) in the above example,
  82    *   d_reqPolEq = Node::null()
  83    * In the trigger term info for P( y, z ) in the above example,
  84    *   d_reqPolEq = false
  85    */
  86   Node d_reqPolEq;
  87   /** the weight of the trigger (see getTriggerWeight). */
  88   int32_t d_weight;
  89   /** Initialize this information class (can be called more than once).
  90    * q is the quantified formula that n is a trigger term for
  91    * n is the trigger term
  92    * reqPol/reqPolEq are described above
  93    */
  94   void init(Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null());
  95   /** is n an atomic trigger?
  96    *
  97    * An atomic trigger is one whose kind is an atomic trigger kind.
  98    */
  99   static bool isAtomicTrigger(Node n);
 100   /** Is k an atomic trigger kind?
 101    *
 102    * An atomic trigger kind is one for which term indexing/matching is possible.
 103    */
 104   static bool isAtomicTriggerKind(Kind k);
 105   /** is n a relational trigger, e.g. like x >= a ? */
 106   static bool isRelationalTrigger(Node n);
 107   /** Is k a relational trigger kind? */
 108   static bool isRelationalTriggerKind(Kind k);
 109   /** is n a simple trigger (see inst_match_generator.h)? */
 110   static bool isSimpleTrigger(Node n);
 111   /** get trigger weight
 112    *
 113    * Intutively, this function classifies how difficult it is to handle the
 114    * trigger term n, where the smaller the value, the easier.
 115    *
 116    * Returns 0 for triggers that are APPLY_UF terms.
 117    * Returns 1 for other triggers whose kind is atomic.
 118    * Returns 2 otherwise.
 119    */
 120   static int32_t getTriggerWeight(Node n);
 121 };
 122
 123 }  // namespace inst
 124 }  // namespace theory
 125 }  // namespace CVC4
 126
 127 #endif