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

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