src/theory/quantifiers/ematching/inst_match_generator.h

   1 /*********************                                                        */
   2 /*! \file inst_match_generator.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 "theory/quantifiers/inst_match_trie.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 class QuantifiersEngine;
  27 namespace quantifiers{
  28   class TermArgTrie;
  29 }
  30
  31 namespace inst {
  32
  33 class Trigger;
  34
  35 /** IMGenerator class
  36 *
  37 * Virtual base class for generating InstMatch objects, which correspond to
  38 * quantifier instantiations. The main use of this class is as a backend utility
  39 * to Trigger (see theory/quantifiers/ematching/trigger.h).
  40 *
  41 * Some functions below take as argument a pointer to the current quantifiers
  42 * engine, which is used for making various queries about what terms and
  43 * equalities exist in the current context.
  44 *
  45 * Some functions below take a pointer to a parent Trigger object, which is used
  46 * to post-process and finalize the instantiations through
  47 * sendInstantiation(...), where the parent trigger will make calls to
  48 * qe->getInstantiate()->addInstantiation(...). The latter function is the entry
  49 * point in which instantiate lemmas are enqueued to be sent on the output
  50 * channel.
  51 */
  52 class IMGenerator {
  53 public:
  54   virtual ~IMGenerator() {}
  55   /** Reset instantiation round.
  56   *
  57   * Called once at beginning of an instantiation round.
  58   */
  59   virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
  60   /** Reset.
  61   *
  62   * eqc is the equivalence class to search in (any if eqc=null).
  63   * Returns true if this generator can produce instantiations, and false
  64   * otherwise. An example of when it returns false is if it can be determined
  65   * that no appropriate matchable terms occur based on eqc.
  66   */
  67   virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; }
  68   /** Get the next match.
  69   *
  70   * Must call reset( eqc ) before this function. This constructs an
  71   * instantiation, which it populates in data structure m,
  72   * based on the current context using the implemented matching algorithm.
  73   *
  74   * q is the quantified formula we are adding instantiations for
  75   * m is the InstMatch object we are generating
  76   *
  77   * Returns a value >0 if an instantiation was successfully generated
  78   */
  79   virtual int getNextMatch(Node q,
  80                            InstMatch& m,
  81                            QuantifiersEngine* qe,
  82                            Trigger* tparent)
  83   {
  84     return 0;
  85   }
  86   /** add instantiations
  87   *
  88   * This add all available instantiations for q based on the current context
  89   * using the implemented matching algorithm. It typically is implemented as a
  90   * fixed point of getNextMatch above.
  91   *
  92   * It returns the number of instantiations added using calls to calls to
  93   * Instantiate::addInstantiation(...).
  94   */
  95   virtual int addInstantiations(Node q,
  96                                 QuantifiersEngine* qe,
  97                                 Trigger* tparent)
  98   {
  99     return 0;
 100   }
 101   /** get active score
 102   *
 103   * A heuristic value indicating how active this generator is.
 104   */
 105   virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
 106  protected:
 107   /** send instantiation
 108    *
 109    * This method sends instantiation, specified by m, to the parent trigger
 110    * object, which will in turn make a call to
 111    * Instantiate::addInstantiation(...). This method returns true if a
 112    * call to Instantiate::addInstantiation(...) was successfully made,
 113    * indicating that an instantiation was enqueued in the quantifier engine's
 114    * lemma cache.
 115    */
 116   bool sendInstantiation(Trigger* tparent, InstMatch& m);
 117 };/* class IMGenerator */
 118
 119 class CandidateGenerator;
 120
 121 /** InstMatchGenerator class
 122 *
 123 * This is the default generator class for non-simple single triggers, that is,
 124 * triggers composed of a single term with nested term applications.
 125 * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
 126 * triggers.
 127 *
 128 * Handling non-simple triggers is done by constructing a linked list of
 129 * InstMatchGenerator classes (see mkInstMatchGenerator), where each
 130 * InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
 131 * then this is the end of the InstMatchGenerator and the last
 132 * InstMatchGenerator is responsible for finalizing the instantiation.
 133 *
 134 * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
 135 *
 136 * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
 137 *
 138 * In a call to getNextMatch,
 139 * if we match against a ground term f( b, c ), then the first InstMatchGenerator
 140 * in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
 141 * match f-applications in the equivalence class of c.
 142 *
 143 * CVC4 employs techniques that ensure that the number of instantiations
 144 * is worst-case polynomial wrt the number of ground terms.
 145 * Consider the axiom/pattern/context (EX2) :
 146 *
 147 *          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
 148 *
 149 *        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
 150 *
 151 * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
 152 *
 153 * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
 154 * instantiated with all combinations of c_1, ... c_100, giving 100^4
 155 * instantiations.
 156 *
 157 * Instead, we enforce that at most 1 instantiation is produced for a
 158 * ( pattern, ground term ) pair per round. Meaning, only one instantiation is
 159 * generated when matching P( a, a, a, a ) against the generator
 160 * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
 161 * Reynolds, Vampire 2016.
 162 *
 163 * To enforce these policies, we use a flag "d_active_add" which dictates the
 164 * behavior of the last element in the linked list. If d_active_add is
 165 *   true -> a call to getNextMatch(...) returns 1 only if adding the
 166 *           instantiation via a call to IMGenerator::sendInstantiation(...)
 167 *           successfully enqueues a lemma via a call to
 168 *           Instantiate::addInstantiation(...). This call may fail e.g. if we
 169 *           have already added the instantiation, or the instantiation is
 170 *           entailed.
 171 *   false -> a call to getNextMatch(...) returns 1 whenever an m is
 172 *            constructed, where typically the caller would use m.
 173 * This is important since a return value >0 signals that the current matched
 174 * terms should be flushed. Consider the above example (EX1), where
 175 * [ f(y,f(x,a)) ] is being matched against f(b,c),
 176 * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
 177 * A successfully added instantiation { x->d, y->b } here signals we should
 178 * not produce further instantiations that match f(y,f(x,a)) with f(b,c).
 179 *
 180 * A number of special cases of triggers are covered by this generator (see
 181 * implementation of initialize), including :
 182 *   Literal triggers, e.g. x >= a, ~x = y
 183 *   Selector triggers, e.g. head( x )
 184 *   Triggers with invertible subterms, e.g. f( x+1 )
 185 *   Variable triggers, e.g. x
 186 *
 187 * All triggers above can be in the context of an equality, e.g.
 188 * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
 189 * ground terms in the equivalence class of b.
 190 * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
 191 * ground terms not in the equivalence class of b.
 192 */
 193 class InstMatchGenerator : public IMGenerator {
 194  public:
 195   /** destructor */
 196   ~InstMatchGenerator() override;
 197
 198   /** Reset instantiation round. */
 199   void resetInstantiationRound(QuantifiersEngine* qe) override;
 200   /** Reset. */
 201   bool reset(Node eqc, QuantifiersEngine* qe) override;
 202   /** Get the next match. */
 203   int getNextMatch(Node q,
 204                    InstMatch& m,
 205                    QuantifiersEngine* qe,
 206                    Trigger* tparent) override;
 207   /** Add instantiations. */
 208   int addInstantiations(Node q,
 209                         QuantifiersEngine* qe,
 210                         Trigger* tparent) override;
 211
 212   /** set active add flag (true by default)
 213    *
 214   * If active add is true, we call sendInstantiation in calls to getNextMatch,
 215   * instead of returning the match. This is necessary so that we can ensure
 216   * policies that are dependent upon knowing when instantiations are
 217   * successfully added to the output channel through
 218   * Instantiate::addInstantiation(...).
 219   */
 220   void setActiveAdd(bool val);
 221   /** Get active score for this inst match generator
 222    *
 223    * See Trigger::getActiveScore for details.
 224    */
 225   int getActiveScore(QuantifiersEngine* qe) override;
 226   /** exclude match
 227    *
 228    * Exclude matching d_match_pattern with Node n on subsequent calls to
 229    * getNextMatch.
 230    */
 231   void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
 232   /** Get current match.
 233    * Returns the term we are currently matching.
 234    */
 235   Node getCurrentMatch() { return d_curr_matched; }
 236   /** set that this match generator is independent
 237    *
 238   * A match generator is indepndent when this generator fails to produce a
 239   * match in a call to getNextMatch, the overall matching fails.
 240   */
 241   void setIndependent() { d_independent_gen = true; }
 242   //-------------------------------construction of inst match generators
 243   /** mkInstMatchGenerator for single triggers, calls the method below */
 244   static InstMatchGenerator* mkInstMatchGenerator(Node q,
 245                                                   Node pat,
 246                                                   QuantifiersEngine* qe);
 247   /** mkInstMatchGenerator for the multi trigger case
 248   *
 249   * This linked list of InstMatchGenerator classes with one
 250   * InstMatchGeneratorMultiLinear at the head and a list of trailing
 251   * InstMatchGenerators corresponding to each unique subterm of pats with
 252   * free variables.
 253   */
 254   static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
 255                                                        std::vector<Node>& pats,
 256                                                        QuantifiersEngine* qe);
 257   /** mkInstMatchGenerator
 258   *
 259   * This generates a linked list of InstMatchGenerators for each unique
 260   * subterm of pats with free variables.
 261   *
 262   * q is the quantified formula associated with the generator we are making
 263   * pats is a set of terms we are making InstMatchGenerator nodes for
 264   * qe is a pointer to the quantifiers engine (used for querying necessary
 265   * information during initialization) pat_map_init maps from terms to
 266   * generators we have already made for them.
 267   *
 268   * It calls initialize(...) for all InstMatchGenerators generated by this call.
 269   */
 270   static InstMatchGenerator* mkInstMatchGenerator(
 271       Node q,
 272       std::vector<Node>& pats,
 273       QuantifiersEngine* qe,
 274       std::map<Node, InstMatchGenerator*>& pat_map_init);
 275   //-------------------------------end construction of inst match generators
 276
 277  protected:
 278   /** constructors
 279    *
 280   * These are intentionally private, and are called during linked list
 281   * construction in mkInstMatchGenerator.
 282   */
 283   InstMatchGenerator(Node pat);
 284   InstMatchGenerator();
 285   /** The pattern we are producing matches for.
 286    *
 287   * This term and d_match_pattern can be different since this
 288   * term may involve  information regarding phase and (dis)equality entailment,
 289   * or other special cases of Triggers.
 290   *
 291   * For example, for the trigger for P( x ) = false, which matches P( x ) with
 292   * P( t ) in the equivalence class of false,
 293   *   P( x ) = false is d_pattern
 294   *   P( x ) is d_match_pattern
 295   * Another example, for pure theory triggers like head( x ), we have
 296   *   head( x ) is d_pattern
 297   *   x is d_match_pattern
 298   * since head( x ) can match any (List) datatype term x.
 299   *
 300   * If null, this is a multi trigger that is merging matches from d_children,
 301   * which is used in InstMatchGeneratorMulti.
 302   */
 303   Node d_pattern;
 304   /** The match pattern
 305    * This is the term that is matched against ground terms,
 306    * see examples above.
 307    */
 308   Node d_match_pattern;
 309   /** The current term we are matching. */
 310   Node d_curr_matched;
 311   /** do we need to call reset on this generator? */
 312   bool d_needsReset;
 313   /** candidate generator
 314    * This is the back-end utility for InstMatchGenerator.
 315    * It generates a stream of candidate terms to match against d_match_pattern
 316    * below, dependending upon what kind of term we are matching
 317    * (e.g. a matchable term, a variable, a relation, etc.).
 318    */
 319   CandidateGenerator* d_cg;
 320   /** children generators
 321    * These match generators correspond to the children of the term
 322    * we are matching with this generator.
 323    * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
 324    * in the example (EX1) above.
 325    */
 326   std::vector<InstMatchGenerator*> d_children;
 327   /** for each child, the index in the term
 328    * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
 329    * in the example (EX1) above, indicating it is the 2nd child
 330    * of the term.
 331    */
 332   std::vector<int> d_children_index;
 333   /** children types
 334    *
 335    * If d_match_pattern is an instantiation constant, then this is a singleton
 336    * vector containing the variable number of the d_match_pattern itself.
 337    * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
 338    * index i, d_children[i] stores the type of node ti is, where:
 339    *   >= 0 : variable (indicates its number),
 340    *   -1 : ground term,
 341    *   -2 : child term.
 342    */
 343   std::vector<int> d_children_types;
 344   /** The next generator in the linked list
 345    * that this generator is a part of.
 346    */
 347   InstMatchGenerator* d_next;
 348   /** The equivalence class we are currently matching in. */
 349   Node d_eq_class;
 350   /** If non-null, then this is a relational trigger of the form x ~
 351    * d_eq_class_rel. */
 352   Node d_eq_class_rel;
 353   /** Excluded matches
 354   * Stores the terms we are not allowed to match.
 355   * These can for instance be specified by the smt2
 356   * extended syntax (! ... :no-pattern).
 357   */
 358   std::map<Node, bool> d_curr_exclude_match;
 359   /** Current first candidate
 360   * Used in a key fail-quickly optimization which generates
 361   * the first candidate term to match during reset().
 362   */
 363   Node d_curr_first_candidate;
 364   /** Indepdendent generate
 365   * If this flag is true, failures to match should be cached.
 366   */
 367   bool d_independent_gen;
 368   /** active add flag, described above. */
 369   bool d_active_add;
 370   /** cached value of d_match_pattern.getType() */
 371   TypeNode d_match_pattern_type;
 372   /** the match operator for d_match_pattern
 373    *
 374    * See TermDatabase::getMatchOperator for details on match operators.
 375    */
 376   Node d_match_pattern_op;
 377   /** get the match against ground term or formula t.
 378    *
 379    * d_match_pattern and t should have the same shape, that is,
 380    * their match operator (see TermDatabase::getMatchOperator) is the same.
 381    * only valid for use where !d_match_pattern.isNull().
 382    */
 383   int getMatch(
 384       Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
 385   /** Initialize this generator.
 386    *
 387    * q is the quantified formula associated with this generator.
 388    *
 389    * This constructs the appropriate information about what
 390    * patterns we are matching and children generators.
 391    *
 392    * It may construct new (child) generators needed to implement
 393    * the matching algorithm for this term. For each new generator
 394    * constructed in this way, it adds them to gens.
 395    */
 396   void initialize(Node q,
 397                   QuantifiersEngine* qe,
 398                   std::vector<InstMatchGenerator*>& gens);
 399   /** Continue next match
 400    *
 401   * This is called during getNextMatch when the current generator in the linked
 402   * list succesfully satisfies its matching constraint. This function either
 403   * calls getNextMatch of the next element in the linked list, or finalizes the
 404   * match (calling sendInstantiation(...) if active add is true, or returning a
 405   * value >0 if active add is false).  Its return value has the same semantics
 406   * as getNextMatch.
 407   */
 408   int continueNextMatch(Node q,
 409                         InstMatch& m,
 410                         QuantifiersEngine* qe,
 411                         Trigger* tparent);
 412   /** Get inst match generator
 413    *
 414    * Gets the InstMatchGenerator that implements the
 415    * appropriate matching algorithm for n within q
 416    * within a linked list of InstMatchGenerators.
 417    */
 418   static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 419 };/* class InstMatchGenerator */
 420
 421 /** match generator for purified terms
 422 * This handles the special case of invertible terms like x+1 (see
 423 * Trigger::getTermInversionVariable).
 424 */
 425 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 426 public:
 427   VarMatchGeneratorTermSubs( Node var, Node subs );
 428
 429   /** Reset */
 430   bool reset(Node eqc, QuantifiersEngine* qe) override
 431   {
 432     d_eq_class = eqc;
 433     return true;
 434   }
 435   /** Get the next match. */
 436   int getNextMatch(Node q,
 437                    InstMatch& m,
 438                    QuantifiersEngine* qe,
 439                    Trigger* tparent) override;
 440
 441  private:
 442   /** variable we are matching (x in the example x+1). */
 443   TNode d_var;
 444   /** cache of d_var.getType() */
 445   TypeNode d_var_type;
 446   /** The substitution for what we match (x-1 in the example x+1). */
 447   Node d_subs;
 448   /** stores whether we have written a value for d_var in the current match. */
 449   bool d_rm_prev;
 450 };
 451
 452 /** InstMatchGeneratorMultiLinear class
 453 *
 454 * This is the default implementation of multi-triggers.
 455 *
 456 * Handling multi-triggers using this class is done by constructing a linked
 457 * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
 458 * InstMatchGeneratorMultiLinear at the head and a list of trailing
 459 * InstMatchGenerators.
 460 *
 461 * CVC4 employs techniques that ensure that the number of instantiations
 462 * is worst-case polynomial wrt the number of ground terms, where this class
 463 * lifts this policy to multi-triggers. In particular consider
 464 *
 465 *  multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
 466 *
 467 * For this multi-trigger, we insist that for each i=1...4, and each ground term
 468 * t, there is at most 1 instantiation added as a result of matching
 469 *    ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
 470 * against ground terms of the form
 471 *    ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
 472 * Meaning we add instantiations for the multi-trigger
 473 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
 474 *   ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
 475 *   ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
 476 *   ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
 477 * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
 478 *
 479 * For example, we disallow adding instantiations based on matching against both
 480 * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
 481 * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
 482 * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
 483 * against f( x1 ) twice.
 484 *
 485 * This policy can be disabled by --no-multi-trigger-linear.
 486 *
 487 */
 488 class InstMatchGeneratorMultiLinear : public InstMatchGenerator {
 489   friend class InstMatchGenerator;
 490
 491  public:
 492   /** Reset. */
 493   bool reset(Node eqc, QuantifiersEngine* qe) override;
 494   /** Get the next match. */
 495   int getNextMatch(Node q,
 496                    InstMatch& m,
 497                    QuantifiersEngine* qe,
 498                    Trigger* tparent) override;
 499
 500  protected:
 501   /** reset the children of this generator */
 502   int resetChildren(QuantifiersEngine* qe);
 503   /** constructor */
 504   InstMatchGeneratorMultiLinear(Node q,
 505                                 std::vector<Node>& pats,
 506                                 QuantifiersEngine* qe);
 507 };/* class InstMatchGeneratorMulti */
 508
 509 /** InstMatchGeneratorMulti
 510 *
 511 * This is an earlier implementation of multi-triggers
 512 * that is enabled by --multi-trigger-cache.
 513 * This generator takes the product of instantiations
 514 * found by single trigger matching, and does
 515 * not have the guarantee that the number of
 516 * instantiations is polynomial wrt the number of
 517 * ground terms.
 518 */
 519 class InstMatchGeneratorMulti : public IMGenerator {
 520  public:
 521   /** constructors */
 522   InstMatchGeneratorMulti(Node q,
 523                           std::vector<Node>& pats,
 524                           QuantifiersEngine* qe);
 525   /** destructor */
 526   ~InstMatchGeneratorMulti() override;
 527
 528   /** Reset instantiation round. */
 529   void resetInstantiationRound(QuantifiersEngine* qe) override;
 530   /** Reset. */
 531   bool reset(Node eqc, QuantifiersEngine* qe) override;
 532   /** Add instantiations. */
 533   int addInstantiations(Node q,
 534                         QuantifiersEngine* qe,
 535                         Trigger* tparent) override;
 536
 537  private:
 538   /** indexed trie */
 539   typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
 540   /** process new match
 541    *
 542    * Called during addInstantiations(...).
 543    * Indicates we produced a match m for child fromChildIndex
 544    * addedLemmas is how many instantiations we succesfully send
 545    * via IMGenerator::sendInstantiation(...) calls.
 546    */
 547   void processNewMatch(QuantifiersEngine* qe,
 548                        Trigger* tparent,
 549                        InstMatch& m,
 550                        int fromChildIndex,
 551                        int& addedLemmas);
 552   /** helper for process new match
 553    * tr is the inst match trie (term index) we are currently traversing.
 554    * trieIndex is depth we are in trie tr.
 555    * childIndex is the index of the term in the multi trigger we are currently
 556    *               processing.
 557    * endChildIndex is the index of the term in the multi trigger that generated
 558    *                  a new term, and hence we will end when the product
 559    *                  computed by this function returns to.
 560    * modEq is whether we are matching modulo equality.
 561    */
 562   void processNewInstantiations(QuantifiersEngine* qe,
 563                                 Trigger* tparent,
 564                                 InstMatch& m,
 565                                 int& addedLemmas,
 566                                 InstMatchTrie* tr,
 567                                 int trieIndex,
 568                                 int childIndex,
 569                                 int endChildIndex,
 570                                 bool modEq);
 571   /** Map from pattern nodes to indices of variables they contain. */
 572   std::map< Node, std::vector< int > > d_var_contains;
 573   /** Map from variable indices to pattern nodes that contain them. */
 574   std::map< int, std::vector< Node > > d_var_to_node;
 575   /** quantified formula we are producing matches for */
 576   Node d_quant;
 577   /** children generators
 578    * These are inst match generators for each term in the multi trigger.
 579    */
 580   std::vector< InstMatchGenerator* > d_children;
 581   /** variable orderings
 582    * Stores a heuristically determined variable ordering (unique
 583    * variables first) for each term in the multi trigger.
 584    */
 585   std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
 586   /** inst match tries for each child node
 587    * This data structure stores all InstMatch objects generated
 588    * by matching for each term in the multi trigger.
 589    */
 590   std::vector< InstMatchTrieOrdered > d_children_trie;
 591 };/* class InstMatchGeneratorMulti */
 592
 593 /** InstMatchGeneratorSimple class
 594 *
 595 * This is the default generator class for simple single triggers.
 596 * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
 597 * triggers. In practice, around 70-90% of triggers are simple single triggers.
 598 *
 599 * Notice that simple triggers also can have an attached polarity.
 600 * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
 601 * simple single triggers.
 602 *
 603 * The implementation traverses the term indices in TermDatabase for adding
 604 * instantiations, which is more efficient than the techniques required for
 605 * handling non-simple single triggers.
 606 *
 607 * In contrast to other instantiation generators, it does not call
 608 * IMGenerator::sendInstantiation and for performance reasons instead calls
 609 * qe->getInstantiate()->addInstantiation(...) directly.
 610 */
 611 class InstMatchGeneratorSimple : public IMGenerator {
 612  public:
 613   /** constructors */
 614   InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
 615
 616   /** Reset instantiation round. */
 617   void resetInstantiationRound(QuantifiersEngine* qe) override;
 618   /** Add instantiations. */
 619   int addInstantiations(Node q,
 620                         QuantifiersEngine* qe,
 621                         Trigger* tparent) override;
 622   /** Get active score. */
 623   int getActiveScore(QuantifiersEngine* qe) override;
 624
 625  private:
 626   /** quantified formula for the trigger term */
 627   Node d_quant;
 628   /** the trigger term */
 629   Node d_match_pattern;
 630   /** equivalence class polarity information
 631    *
 632   * This stores the required polarity/equivalence class with this trigger.
 633   * If d_eqc is non-null, we only produce matches { x->t } such that
 634   * our context does not entail
 635   *   ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
 636   *   ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
 637   * where * denotes application of substitution.
 638   */
 639   bool d_pol;
 640   Node d_eqc;
 641   /** Match pattern arg types.
 642    * Cached values of d_match_pattern[i].getType().
 643    */
 644   std::vector< TypeNode > d_match_pattern_arg_types;
 645   /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
 646   Node d_op;
 647   /** Map from child number to variable index. */
 648   std::map< int, int > d_var_num;
 649   /** add instantiations, helper function.
 650    *
 651    * m is the current match we are building,
 652    * addedLemmas is the number of lemmas we have added via calls to
 653    *                qe->getInstantiate()->aaddInstantiation(...),
 654    * argIndex is the argument index in d_match_pattern we are currently
 655    *              matching,
 656    * tat is the term index we are currently traversing.
 657    */
 658   void addInstantiations(InstMatch& m,
 659                          QuantifiersEngine* qe,
 660                          int& addedLemmas,
 661                          unsigned argIndex,
 662                          quantifiers::TermArgTrie* tat);
 663 };/* class InstMatchGeneratorSimple */
 664 }
 665 }
 666 }
 667
 668 #endif