src/theory/quantifiers/ematching/trigger_term_info.h

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