1 /********************* */
2 /*! \file trigger_term_info.h
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
12 ** \brief trigger term info class
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
18 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
22 #include "expr/node.h"
28 /** Information about a node used in a trigger.
30 * This information includes:
31 * 1. the free variables of the node, and
32 * 2. information about which terms are useful for matching.
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 ) ) )
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.
48 * This example is referenced for each of the functions below.
53 TriggerTermInfo() : d_reqPol(0), d_weight(0) {}
55 /** The free variables in the node
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
62 std::vector
<Node
> d_fv
;
63 /** Required polarity: 1 for equality, -1 for disequality, 0 for none
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
70 /** Required polarity equal term
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.
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,
87 /** the weight of the trigger (see getTriggerWeight). */
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
94 void init(Node q
, Node n
, int reqPol
= 0, Node reqPolEq
= Node::null());
95 /** is n an atomic trigger?
97 * An atomic trigger is one whose kind is an atomic trigger kind.
99 static bool isAtomicTrigger(Node n
);
100 /** Is k an atomic trigger kind?
102 * An atomic trigger kind is one for which term indexing/matching is possible.
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
113 * Intutively, this function classifies how difficult it is to handle the
114 * trigger term n, where the smaller the value, the easier.
116 * Returns 0 for triggers that are APPLY_UF terms.
117 * Returns 1 for other triggers whose kind is atomic.
118 * Returns 2 otherwise.
120 static int32_t getTriggerWeight(Node n
);
124 } // namespace theory