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