GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator_simple.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator_simple.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 simple inst match generator class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
18
#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node_trie.h"
24
#include "theory/quantifiers/ematching/inst_match_generator.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace inst {
29
30
/** InstMatchGeneratorSimple class
31
 *
32
 * This is the default generator class for simple single triggers.
33
 * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
34
 * triggers. In practice, around 70-90% of triggers are simple single triggers.
35
 *
36
 * Notice that simple triggers also can have an attached polarity.
37
 * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
38
 * simple single triggers.
39
 *
40
 * The implementation traverses the term indices in TermDatabase for adding
41
 * instantiations, which is more efficient than the techniques required for
42
 * handling non-simple single triggers.
43
 *
44
 * In contrast to other instantiation generators, it does not call
45
 * IMGenerator::sendInstantiation and for performance reasons instead calls
46
 * qe->getInstantiate()->addInstantiation(...) directly.
47
 */
48
15320
class InstMatchGeneratorSimple : public IMGenerator
49
{
50
 public:
51
  /** constructors */
52
  InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat);
53
54
  /** Reset instantiation round. */
55
  void resetInstantiationRound() override;
56
  /** Add instantiations. */
57
  uint64_t addInstantiations(Node q) override;
58
  /** Get active score. */
59
  int getActiveScore() override;
60
61
 private:
62
  /** quantified formula for the trigger term */
63
  Node d_quant;
64
  /** the trigger term */
65
  Node d_match_pattern;
66
  /** equivalence class polarity information
67
   *
68
   * This stores the required polarity/equivalence class with this trigger.
69
   * If d_eqc is non-null, we only produce matches { x->t } such that
70
   * our context does not entail
71
   *   ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
72
   *   ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
73
   * where * denotes application of substitution.
74
   */
75
  bool d_pol;
76
  Node d_eqc;
77
  /** Match pattern arg types.
78
   * Cached values of d_match_pattern[i].getType().
79
   */
80
  std::vector<TypeNode> d_match_pattern_arg_types;
81
  /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
82
  Node d_op;
83
  /**
84
   * Map from child number of d_match_pattern to variable index, or -1 if the
85
   * child is not a variable.
86
   */
87
  std::map<size_t, int> d_var_num;
88
  /** add instantiations, helper function.
89
   *
90
   * m is the current match we are building,
91
   * addedLemmas is the number of lemmas we have added via calls to
92
   *                qe->getInstantiate()->aaddInstantiation(...),
93
   * argIndex is the argument index in d_match_pattern we are currently
94
   *              matching,
95
   * tat is the term index we are currently traversing.
96
   */
97
  void addInstantiations(InstMatch& m,
98
                         uint64_t& addedLemmas,
99
                         size_t argIndex,
100
                         TNodeTrie* tat);
101
};
102
103
}  // namespace inst
104
}  // namespace theory
105
}  // namespace CVC4
106
107
#endif