src/theory/quantifiers/ematching/inst_match_generator.h

   1 /*********************                                                        */
   2 /*! \file inst_match_generator.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Tim King
   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 inst match generator class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
  18 #define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
  19
  20 #include <map>
  21 #include "expr/node_trie.h"
  22 #include "theory/inference_id.h"
  23 #include "theory/quantifiers/inst_match.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class QuantifiersEngine;
  29
  30 namespace quantifiers {
  31 class QuantifiersState;
  32 class QuantifiersInferenceManager;
  33 }  // namespace quantifiers
  34
  35 namespace inst {
  36
  37 class Trigger;
  38
  39 /** IMGenerator class
  40 *
  41 * Virtual base class for generating InstMatch objects, which correspond to
  42 * quantifier instantiations. The main use of this class is as a backend utility
  43 * to Trigger (see theory/quantifiers/ematching/trigger.h).
  44 *
  45 * Some functions below take as argument a pointer to the current quantifiers
  46 * engine, which is used for making various queries about what terms and
  47 * equalities exist in the current context.
  48 *
  49 * Some functions below take a pointer to a parent Trigger object, which is used
  50 * to post-process and finalize the instantiations through
  51 * sendInstantiation(...), where the parent trigger will make calls to
  52 * qe->getInstantiate()->addInstantiation(...). The latter function is the entry
  53 * point in which instantiate lemmas are enqueued to be sent on the output
  54 * channel.
  55 */
  56 class IMGenerator {
  57 public:
  58  IMGenerator(quantifiers::QuantifiersState& qs,
  59              quantifiers::QuantifiersInferenceManager& qim);
  60  virtual ~IMGenerator() {}
  61  /** Reset instantiation round.
  62   *
  63   * Called once at beginning of an instantiation round.
  64   */
  65  virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
  66  /** Reset.
  67   *
  68   * eqc is the equivalence class to search in (any if eqc=null).
  69   * Returns true if this generator can produce instantiations, and false
  70   * otherwise. An example of when it returns false is if it can be determined
  71   * that no appropriate matchable terms occur based on eqc.
  72   */
  73  virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; }
  74  /** Get the next match.
  75   *
  76   * Must call reset( eqc ) before this function. This constructs an
  77   * instantiation, which it populates in data structure m,
  78   * based on the current context using the implemented matching algorithm.
  79   *
  80   * q is the quantified formula we are adding instantiations for
  81   * m is the InstMatch object we are generating
  82   *
  83   * Returns a value >0 if an instantiation was successfully generated
  84   */
  85  virtual int getNextMatch(Node q,
  86                           InstMatch& m,
  87                           QuantifiersEngine* qe,
  88                           Trigger* tparent)
  89  {
  90    return 0;
  91   }
  92   /** add instantiations
  93   *
  94   * This add all available instantiations for q based on the current context
  95   * using the implemented matching algorithm. It typically is implemented as a
  96   * fixed point of getNextMatch above.
  97   *
  98   * It returns the number of instantiations added using calls to calls to
  99   * Instantiate::addInstantiation(...).
 100   */
 101   virtual uint64_t addInstantiations(Node q,
 102                                      QuantifiersEngine* qe,
 103                                      Trigger* tparent)
 104   {
 105     return 0;
 106   }
 107   /** get active score
 108   *
 109   * A heuristic value indicating how active this generator is.
 110   */
 111   virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
 112  protected:
 113   /** send instantiation
 114    *
 115    * This method sends instantiation, specified by m, to the parent trigger
 116    * object, which will in turn make a call to
 117    * Instantiate::addInstantiation(...). This method returns true if a
 118    * call to Instantiate::addInstantiation(...) was successfully made,
 119    * indicating that an instantiation was enqueued in the quantifier engine's
 120    * lemma cache.
 121    */
 122   bool sendInstantiation(Trigger* tparent, InstMatch& m, InferenceId id);
 123   /** The state of the quantifiers engine */
 124   quantifiers::QuantifiersState& d_qstate;
 125   /** The quantifiers inference manager */
 126   quantifiers::QuantifiersInferenceManager& d_qim;
 127 };/* class IMGenerator */
 128
 129 class CandidateGenerator;
 130
 131 /** InstMatchGenerator class
 132 *
 133 * This is the default generator class for non-simple single triggers, that is,
 134 * triggers composed of a single term with nested term applications.
 135 * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
 136 * triggers.
 137 *
 138 * Handling non-simple triggers is done by constructing a linked list of
 139 * InstMatchGenerator classes (see mkInstMatchGenerator), where each
 140 * InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
 141 * then this is the end of the InstMatchGenerator and the last
 142 * InstMatchGenerator is responsible for finalizing the instantiation.
 143 *
 144 * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
 145 *
 146 * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
 147 *
 148 * In a call to getNextMatch,
 149 * if we match against a ground term f( b, c ), then the first InstMatchGenerator
 150 * in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
 151 * match f-applications in the equivalence class of c.
 152 *
 153 * CVC4 employs techniques that ensure that the number of instantiations
 154 * is worst-case polynomial wrt the number of ground terms.
 155 * Consider the axiom/pattern/context (EX2) :
 156 *
 157 *          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
 158 *
 159 *        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
 160 *
 161 * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
 162 *
 163 * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
 164 * instantiated with all combinations of c_1, ... c_100, giving 100^4
 165 * instantiations.
 166 *
 167 * Instead, we enforce that at most 1 instantiation is produced for a
 168 * ( pattern, ground term ) pair per round. Meaning, only one instantiation is
 169 * generated when matching P( a, a, a, a ) against the generator
 170 * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
 171 * Reynolds, Vampire 2016.
 172 *
 173 * To enforce these policies, we use a flag "d_active_add" which dictates the
 174 * behavior of the last element in the linked list. If d_active_add is
 175 *   true -> a call to getNextMatch(...) returns 1 only if adding the
 176 *           instantiation via a call to IMGenerator::sendInstantiation(...)
 177 *           successfully enqueues a lemma via a call to
 178 *           Instantiate::addInstantiation(...). This call may fail e.g. if we
 179 *           have already added the instantiation, or the instantiation is
 180 *           entailed.
 181 *   false -> a call to getNextMatch(...) returns 1 whenever an m is
 182 *            constructed, where typically the caller would use m.
 183 * This is important since a return value >0 signals that the current matched
 184 * terms should be flushed. Consider the above example (EX1), where
 185 * [ f(y,f(x,a)) ] is being matched against f(b,c),
 186 * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
 187 * A successfully added instantiation { x->d, y->b } here signals we should
 188 * not produce further instantiations that match f(y,f(x,a)) with f(b,c).
 189 *
 190 * A number of special cases of triggers are covered by this generator (see
 191 * implementation of initialize), including :
 192 *   Literal triggers, e.g. x >= a, ~x = y
 193 *   Selector triggers, e.g. head( x )
 194 *   Triggers with invertible subterms, e.g. f( x+1 )
 195 *   Variable triggers, e.g. x
 196 *
 197 * All triggers above can be in the context of an equality, e.g.
 198 * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
 199 * ground terms in the equivalence class of b.
 200 * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
 201 * ground terms not in the equivalence class of b.
 202 */
 203 class InstMatchGenerator : public IMGenerator {
 204  public:
 205   /** destructor */
 206   ~InstMatchGenerator() override;
 207
 208   /** Reset instantiation round. */
 209   void resetInstantiationRound(QuantifiersEngine* qe) override;
 210   /** Reset. */
 211   bool reset(Node eqc, QuantifiersEngine* qe) override;
 212   /** Get the next match. */
 213   int getNextMatch(Node q,
 214                    InstMatch& m,
 215                    QuantifiersEngine* qe,
 216                    Trigger* tparent) override;
 217   /** Add instantiations. */
 218   uint64_t addInstantiations(Node q,
 219                              QuantifiersEngine* qe,
 220                              Trigger* tparent) override;
 221
 222   /** set active add flag (true by default)
 223    *
 224   * If active add is true, we call sendInstantiation in calls to getNextMatch,
 225   * instead of returning the match. This is necessary so that we can ensure
 226   * policies that are dependent upon knowing when instantiations are
 227   * successfully added to the output channel through
 228   * Instantiate::addInstantiation(...).
 229   */
 230   void setActiveAdd(bool val);
 231   /** Get active score for this inst match generator
 232    *
 233    * See Trigger::getActiveScore for details.
 234    */
 235   int getActiveScore(QuantifiersEngine* qe) override;
 236   /** exclude match
 237    *
 238    * Exclude matching d_match_pattern with Node n on subsequent calls to
 239    * getNextMatch.
 240    */
 241   void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
 242   /** Get current match.
 243    * Returns the term we are currently matching.
 244    */
 245   Node getCurrentMatch() { return d_curr_matched; }
 246   /** set that this match generator is independent
 247    *
 248   * A match generator is indepndent when this generator fails to produce a
 249   * match in a call to getNextMatch, the overall matching fails.
 250   */
 251   void setIndependent() { d_independent_gen = true; }
 252   //-------------------------------construction of inst match generators
 253   /** mkInstMatchGenerator for single triggers, calls the method below */
 254   static InstMatchGenerator* mkInstMatchGenerator(
 255       Node q,
 256       Node pat,
 257       quantifiers::QuantifiersState& qs,
 258       quantifiers::QuantifiersInferenceManager& qim,
 259       QuantifiersEngine* qe);
 260   /** mkInstMatchGenerator for the multi trigger case
 261   *
 262   * This linked list of InstMatchGenerator classes with one
 263   * InstMatchGeneratorMultiLinear at the head and a list of trailing
 264   * InstMatchGenerators corresponding to each unique subterm of pats with
 265   * free variables.
 266   */
 267   static InstMatchGenerator* mkInstMatchGeneratorMulti(
 268       Node q,
 269       std::vector<Node>& pats,
 270       quantifiers::QuantifiersState& qs,
 271       quantifiers::QuantifiersInferenceManager& qim,
 272       QuantifiersEngine* qe);
 273   /** mkInstMatchGenerator
 274   *
 275   * This generates a linked list of InstMatchGenerators for each unique
 276   * subterm of pats with free variables.
 277   *
 278   * q is the quantified formula associated with the generator we are making
 279   * pats is a set of terms we are making InstMatchGenerator nodes for
 280   * qe is a pointer to the quantifiers engine (used for querying necessary
 281   * information during initialization) pat_map_init maps from terms to
 282   * generators we have already made for them.
 283   *
 284   * It calls initialize(...) for all InstMatchGenerators generated by this call.
 285   */
 286   static InstMatchGenerator* mkInstMatchGenerator(
 287       Node q,
 288       std::vector<Node>& pats,
 289       quantifiers::QuantifiersState& qs,
 290       quantifiers::QuantifiersInferenceManager& qim,
 291       QuantifiersEngine* qe,
 292       std::map<Node, InstMatchGenerator*>& pat_map_init);
 293   //-------------------------------end construction of inst match generators
 294
 295  protected:
 296   /** constructors
 297    *
 298   * These are intentionally private, and are called during linked list
 299   * construction in mkInstMatchGenerator.
 300   */
 301   InstMatchGenerator(Node pat,
 302                      quantifiers::QuantifiersState& qs,
 303                      quantifiers::QuantifiersInferenceManager& qim);
 304   /** The pattern we are producing matches for.
 305    *
 306   * This term and d_match_pattern can be different since this
 307   * term may involve  information regarding phase and (dis)equality entailment,
 308   * or other special cases of Triggers.
 309   *
 310   * For example, for the trigger for P( x ) = false, which matches P( x ) with
 311   * P( t ) in the equivalence class of false,
 312   *   P( x ) = false is d_pattern
 313   *   P( x ) is d_match_pattern
 314   * Another example, for pure theory triggers like head( x ), we have
 315   *   head( x ) is d_pattern
 316   *   x is d_match_pattern
 317   * since head( x ) can match any (List) datatype term x.
 318   *
 319   * If null, this is a multi trigger that is merging matches from d_children,
 320   * which is used in InstMatchGeneratorMulti.
 321   */
 322   Node d_pattern;
 323   /** The match pattern
 324    * This is the term that is matched against ground terms,
 325    * see examples above.
 326    */
 327   Node d_match_pattern;
 328   /** The current term we are matching. */
 329   Node d_curr_matched;
 330   /** do we need to call reset on this generator? */
 331   bool d_needsReset;
 332   /** candidate generator
 333    * This is the back-end utility for InstMatchGenerator.
 334    * It generates a stream of candidate terms to match against d_match_pattern
 335    * below, dependending upon what kind of term we are matching
 336    * (e.g. a matchable term, a variable, a relation, etc.).
 337    */
 338   CandidateGenerator* d_cg;
 339   /** children generators
 340    * These match generators correspond to the children of the term
 341    * we are matching with this generator.
 342    * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
 343    * in the example (EX1) above.
 344    */
 345   std::vector<InstMatchGenerator*> d_children;
 346   /** for each child, the index in the term
 347    * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
 348    * in the example (EX1) above, indicating it is the 2nd child
 349    * of the term.
 350    */
 351   std::vector<size_t> d_children_index;
 352   /** children types
 353    *
 354    * If d_match_pattern is an instantiation constant, then this is a singleton
 355    * vector containing the variable number of the d_match_pattern itself.
 356    * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
 357    * index i, d_children[i] stores the type of node ti is, where:
 358    *   >= 0 : variable (indicates its number),
 359    *   -1 : ground term,
 360    *   -2 : child term.
 361    */
 362   std::vector<int64_t> d_children_types;
 363   /** The next generator in the linked list
 364    * that this generator is a part of.
 365    */
 366   InstMatchGenerator* d_next;
 367   /** The equivalence class we are currently matching in. */
 368   Node d_eq_class;
 369   /** If non-null, then this is a relational trigger of the form x ~
 370    * d_eq_class_rel. */
 371   Node d_eq_class_rel;
 372   /** Excluded matches
 373   * Stores the terms we are not allowed to match.
 374   * These can for instance be specified by the smt2
 375   * extended syntax (! ... :no-pattern).
 376   */
 377   std::map<Node, bool> d_curr_exclude_match;
 378   /** Current first candidate
 379   * Used in a key fail-quickly optimization which generates
 380   * the first candidate term to match during reset().
 381   */
 382   Node d_curr_first_candidate;
 383   /** Indepdendent generate
 384   * If this flag is true, failures to match should be cached.
 385   */
 386   bool d_independent_gen;
 387   /** active add flag, described above. */
 388   bool d_active_add;
 389   /** cached value of d_match_pattern.getType() */
 390   TypeNode d_match_pattern_type;
 391   /** the match operator for d_match_pattern
 392    *
 393    * See TermDatabase::getMatchOperator for details on match operators.
 394    */
 395   Node d_match_pattern_op;
 396   /** get the match against ground term or formula t.
 397    *
 398    * d_match_pattern and t should have the same shape, that is,
 399    * their match operator (see TermDatabase::getMatchOperator) is the same.
 400    * only valid for use where !d_match_pattern.isNull().
 401    */
 402   int getMatch(
 403       Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
 404   /** Initialize this generator.
 405    *
 406    * q is the quantified formula associated with this generator.
 407    *
 408    * This constructs the appropriate information about what
 409    * patterns we are matching and children generators.
 410    *
 411    * It may construct new (child) generators needed to implement
 412    * the matching algorithm for this term. For each new generator
 413    * constructed in this way, it adds them to gens.
 414    */
 415   void initialize(Node q,
 416                   QuantifiersEngine* qe,
 417                   std::vector<InstMatchGenerator*>& gens);
 418   /** Continue next match
 419    *
 420   * This is called during getNextMatch when the current generator in the linked
 421   * list succesfully satisfies its matching constraint. This function either
 422   * calls getNextMatch of the next element in the linked list, or finalizes the
 423   * match (calling sendInstantiation(...) if active add is true, or returning a
 424   * value >0 if active add is false).  Its return value has the same semantics
 425   * as getNextMatch.
 426   */
 427   int continueNextMatch(Node q,
 428                         InstMatch& m,
 429                         QuantifiersEngine* qe,
 430                         Trigger* tparent,
 431                         InferenceId id);
 432   /** Get inst match generator
 433    *
 434    * Gets the InstMatchGenerator that implements the
 435    * appropriate matching algorithm for n within q
 436    * within a linked list of InstMatchGenerators.
 437    */
 438   static InstMatchGenerator* getInstMatchGenerator(
 439       Node q,
 440       Node n,
 441       quantifiers::QuantifiersState& qs,
 442       quantifiers::QuantifiersInferenceManager& qim);
 443 };/* class InstMatchGenerator */
 444
 445 }
 446 }
 447 }
 448
 449 #endif