src/theory/quantifiers/ematching/trigger.h

   1 /*********************                                                        */
   2 /*! \file trigger.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 class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
  18 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
  19
  20 #include <map>
  21
  22 #include "expr/node.h"
  23 #include "options/quantifiers_options.h"
  24 #include "theory/quantifiers/inst_match.h"
  25 #include "theory/valuation.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 class QuantifiersEngine;
  31
  32 namespace quantifiers {
  33 class QuantifiersInferenceManager;
  34 }
  35
  36 namespace inst {
  37
  38 class IMGenerator;
  39 class InstMatchGenerator;
  40 /** A collection of nodes representing a trigger.
  41 *
  42 * This class encapsulates all implementations of E-matching in CVC4.
  43 * Its primary use is as a utility of the quantifiers module InstantiationEngine
  44 * (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make
  45 * appropriate calls to Instantiate::addInstantiation(...)
  46 * (see theory/instantiate.h) for the instantiate utility of the quantifiers
  47 * engine (d_quantEngine) associated with this trigger.  These calls
  48 * queue instantiation lemmas to the output channel of TheoryQuantifiers during
  49 * a full effort check.
  50 *
  51 * Concretely, a Trigger* t is used in the following way during a full effort
  52 * check. Assume that t is associated with quantified formula q (see field d_f).
  53 * We call :
  54 *
  55 * // setup initial information
  56 * t->resetInstantiationRound();
  57 * // will produce instantiations based on matching with all terms
  58 * t->reset( Node::null() );
  59 * // add all instantiations based on E-matching with this trigger and the
  60 * // current context
  61 * t->addInstantiations();
  62 *
  63 * This will result in (a set of) calls to
  64 * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
  65 * where m1...mn are InstMatch objects. These calls add the corresponding
  66 * instantiation lemma for (q,mi) on the output channel associated with
  67 * d_quantEngine.
  68 *
  69 * The Trigger class is wrapper around an underlying IMGenerator class, which
  70 * implements various forms of E-matching for its set of nodes (d_nodes), which
  71 * is refered to in the literature as a "trigger". A trigger is a set of terms
  72 * whose free variables are the bound variables of a quantified formula q,
  73 * and that is used to guide instantiations for q (for example, see "Efficient
  74 * E-Matching for SMT Solvers" by de Moura et al).
  75 *
  76 * For example of an instantiation lemma produced by E-matching :
  77 *
  78 * quantified formula : forall x. P( x )
  79 *            trigger : P( x )
  80 *     ground context : ~P( a )
  81 *
  82 * Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
  83 * which is used to generate the instantiation lemma :
  84 *   (forall x. P( x )) => P( a )
  85 *
  86 * Terms that are provided as input to a Trigger class via mkTrigger
  87 * should be in "instantiation constant form", see TermUtil::getInstConstantNode.
  88 * Say we have quantified formula q whose AST is the Node
  89 *   (FORALL
  90 *     (BOUND_VAR_LIST x)
  91 *     (NOT (P x))
  92 *     (INST_PATTERN_LIST (INST_PATTERN (P x))))
  93 * then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where
  94 * IC = TermUtil::getInstantiationConstant( q, i ).
  95 * Trigger expects as input (P IC) to represent the Trigger (P x). This form
  96 * ensures that references to bound variables are unique to quantified formulas,
  97 * which is required to ensure the correctness of instantiation lemmas we
  98 * generate.
  99 *
 100 */
 101 class Trigger {
 102   friend class IMGenerator;
 103
 104  public:
 105   virtual ~Trigger();
 106   /** get the generator associated with this trigger */
 107   IMGenerator* getGenerator() { return d_mg; }
 108   /** Reset instantiation round.
 109    *
 110   * Called once at beginning of an instantiation round.
 111   */
 112   void resetInstantiationRound();
 113   /** Reset the trigger.
 114    *
 115   * eqc is the equivalence class from which to match ground terms. If eqc is
 116   * Node::null(), then we match ground terms from all equivalence classes.
 117   */
 118   void reset( Node eqc );
 119   /** add all available instantiations, based on the current context
 120   *
 121   * This function makes the appropriate calls to d_qe->addInstantiation(...)
 122   * based on the current ground terms and equalities in the current context,
 123   * via queries to functions in d_qe. This calls the addInstantiations function
 124   * of the underlying match generator. It can be extended to
 125   * produce instantiations beyond what is produced by the match generator
 126   * (for example, see theory/quantifiers/ematching/ho_trigger.h).
 127   */
 128   virtual uint64_t addInstantiations();
 129   /** Return whether this is a multi-trigger. */
 130   bool isMultiTrigger() const;
 131   /** Get instantiation pattern list associated with this trigger.
 132    *
 133   * An instantiation pattern list is the node representation of a trigger, in
 134   * particular, it is the third argument of quantified formulas which have user
 135   * (! ... :pattern) attributes.
 136   */
 137   Node getInstPattern() const;
 138   /* A heuristic value indicating how active this generator is.
 139    *
 140   * This returns the number of ground terms for the match operators in terms
 141   * from d_nodes. This score is only used with the experimental option
 142   *   --trigger-active-sel.
 143   */
 144   int getActiveScore();
 145   /** print debug information for the trigger */
 146   void debugPrint(const char* c) const;
 147   /** mkTrigger method
 148    *
 149    * This makes an instance of a trigger object.
 150    *  qe     : pointer to the quantifier engine;
 151    *  q      : the quantified formula we are making a trigger for
 152    *  nodes  : the nodes comprising the (multi-)trigger
 153    *  keepAll: don't remove unneeded patterns;
 154    *  trOption : policy for dealing with triggers that already exist
 155    *             (see below)
 156    *  useNVars : number of variables that should be bound by the trigger
 157    *             typically, the number of quantified variables in q.
 158    */
 159   enum{
 160     TR_MAKE_NEW,    //make new trigger even if it already may exist
 161     TR_GET_OLD,     //return a previous trigger if it had already been created
 162     TR_RETURN_NULL  //return null if a duplicate is found
 163   };
 164   static Trigger* mkTrigger(QuantifiersEngine* qe,
 165                             quantifiers::QuantifiersInferenceManager& qim,
 166                             Node q,
 167                             std::vector<Node>& nodes,
 168                             bool keepAll = true,
 169                             int trOption = TR_MAKE_NEW,
 170                             size_t useNVars = 0);
 171   /** single trigger version that calls the above function */
 172   static Trigger* mkTrigger(QuantifiersEngine* qe,
 173                             quantifiers::QuantifiersInferenceManager& qim,
 174                             Node q,
 175                             Node n,
 176                             bool keepAll = true,
 177                             int trOption = TR_MAKE_NEW,
 178                             size_t useNVars = 0);
 179   /** make trigger terms
 180    *
 181    * This takes a set of eligible trigger terms and stores a subset of them in
 182    * trNodes, such that :
 183    *   (1) the terms in trNodes contain at least n_vars of the quantified
 184    *       variables in quantified formula q, and
 185    *   (2) the set trNodes is minimal, i.e. removing one term from trNodes
 186    *       always violates (1).
 187    */
 188   static bool mkTriggerTerms(Node q,
 189                              std::vector<Node>& nodes,
 190                              size_t nvars,
 191                              std::vector<Node>& trNodes);
 192
 193  protected:
 194   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
 195   Trigger(QuantifiersEngine* ie,
 196           quantifiers::QuantifiersInferenceManager& qim,
 197           Node q,
 198           std::vector<Node>& nodes);
 199   /** add an instantiation (called by InstMatchGenerator)
 200    *
 201    * This calls Instantiate::addInstantiation(...) for instantiations
 202    * associated with m. Typically, m is associated with a single instantiation,
 203    * but in some cases (e.g. higher-order) we may modify m before calling
 204    * Instantiate::addInstantiation(...).
 205    */
 206   virtual bool sendInstantiation(InstMatch& m);
 207   /**
 208    * Ensure that all ground subterms of n have been preprocessed. This makes
 209    * calls to the provided valuation to obtain the preprocessed form of these
 210    * terms. The preprocessed form of each ground subterm is added to gts.
 211    *
 212    * As an optimization, this method does not preprocess terms with no
 213    * arguments, e.g. variables and constants are not preprocessed (as they
 214    * should not change after preprocessing), nor are they added to gts.
 215    *
 216    * @param val The valuation to use for looking up preprocessed terms.
 217    * @param n The node to process, which is in inst-constant form (free
 218    * variables have been substituted by corresponding INST_CONSTANT).
 219    * @param gts The set of preprocessed ground subterms of n.
 220    * @return The converted form of n where all ground subterms have been
 221    * replaced by their preprocessed form.
 222    */
 223   static Node ensureGroundTermPreprocessed(Valuation& val,
 224                                            Node n,
 225                                            std::vector<Node>& gts);
 226   /** The nodes comprising this trigger. */
 227   std::vector<Node> d_nodes;
 228   /**
 229    * The preprocessed ground terms in the nodes of the trigger, which as an
 230    * optimization omits variables and constant subterms. These terms are
 231    * important since we must ensure that the quantifier-free solvers are
 232    * aware of these terms. In particular, when adding instantiations for
 233    * a trigger P(f(a), x), we first check if f(a) is a term in the master
 234    * equality engine. If it is not, then we add the lemma k = f(a) where k
 235    * is the purification skolem for f(a). This ensures that f(a) will be
 236    * registered as a term in the master equality engine on the next
 237    * instantiation round. This is particularly important for cases where
 238    * P(f(a), x) is matched with P(f(b), c), where a=b in the current context.
 239    * This example would fail to match when f(a) is not registered.
 240    */
 241   std::vector<Node> d_groundTerms;
 242   /** The quantifiers engine associated with this trigger. */
 243   QuantifiersEngine* d_quantEngine;
 244   /** Reference to the quantifiers inference manager */
 245   quantifiers::QuantifiersInferenceManager& d_qim;
 246   /** The quantified formula this trigger is for. */
 247   Node d_quant;
 248   /** match generator
 249    *
 250   * This is the back-end utility that implements the underlying matching
 251   * algorithm associated with this trigger.
 252   */
 253   IMGenerator* d_mg;
 254 }; /* class Trigger */
 255
 256 }/* CVC4::theory::inst namespace */
 257 }/* CVC4::theory namespace */
 258 }/* CVC4 namespace */
 259
 260 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */