1 /********************* */
2 /*! \file trigger_term_info.h
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
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"
26 namespace quantifiers
{
29 /** Information about a node used in a trigger.
31 * This information includes:
32 * 1. the free variables of the node, and
33 * 2. information about which terms are useful for matching.
35 * As an example, consider the trigger
36 * { f( x ), g( y ), P( y, z ) }
37 * for quantified formula
38 * forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
40 * Notice that it is only useful to match f( x ) to f-applications not in the
41 * equivalence class of b, and P( y, z ) to P-applications not in the
42 * equivalence class of true, as such instances will always be entailed by the
43 * ground equalities and disequalities the current context. Entailed instances
44 * are typically not helpful, and are discarded in
45 * Instantiate::addInstantiation(...) unless the option --no-inst-no-entail is
46 * enabled. For more details, see page 10 of "Congruence Closure with Free
47 * Variables", Barbosa et al., TACAS 2017.
49 * This example is referenced for each of the functions below.
54 TriggerTermInfo() : d_reqPol(0), d_weight(0) {}
56 /** The free variables in the node
58 * In the trigger term info for f( x ) in the above example, d_fv = { x }
59 * In the trigger term info for g( y ) in the above example, d_fv = { y }
60 * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z
63 std::vector
<Node
> d_fv
;
64 /** Required polarity: 1 for equality, -1 for disequality, 0 for none
66 * In the trigger term info for f( x ) in the above example, d_reqPol = -1
67 * In the trigger term info for g( y ) in the above example, d_reqPol = 0
68 * In the trigger term info for P( y, z ) in the above example, d_reqPol = 1
71 /** Required polarity equal term
73 * If d_reqPolEq is not null,
74 * if d_reqPol = 1, then this trigger term must be matched to terms in the
75 * equivalence class of d_reqPolEq,
76 * if d_reqPol = -1, then this trigger term must be matched to terms *not*
77 * in the equivalence class of d_reqPolEq.
79 * This information is typically chosen by analyzing the entailed equalities
80 * and disequalities of quantified formulas.
81 * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
82 * In the trigger term info for g( y ) in the above example,
83 * d_reqPolEq = Node::null()
84 * In the trigger term info for P( y, z ) in the above example,
88 /** the weight of the trigger (see getTriggerWeight). */
90 /** Initialize this information class (can be called more than once).
91 * q is the quantified formula that n is a trigger term for
92 * n is the trigger term
93 * reqPol/reqPolEq are described above
95 void init(Node q
, Node n
, int reqPol
= 0, Node reqPolEq
= Node::null());
96 /** is n an atomic trigger?
98 * An atomic trigger is one whose kind is an atomic trigger kind.
100 static bool isAtomicTrigger(Node n
);
101 /** Is k an atomic trigger kind?
103 * An atomic trigger kind is one for which term indexing/matching is possible.
105 static bool isAtomicTriggerKind(Kind k
);
106 /** is n a relational trigger, e.g. like x >= a ? */
107 static bool isRelationalTrigger(Node n
);
108 /** Is k a relational trigger kind? */
109 static bool isRelationalTriggerKind(Kind k
);
110 /** is n a simple trigger (see inst_match_generator.h)? */
111 static bool isSimpleTrigger(Node n
);
112 /** get trigger weight
114 * Intutively, this function classifies how difficult it is to handle the
115 * trigger term n, where the smaller the value, the easier.
117 * Returns 0 for triggers that are APPLY_UF terms.
118 * Returns 1 for other triggers whose kind is atomic.
119 * Returns 2 otherwise.
121 static int32_t getTriggerWeight(Node n
);
125 } // namespace quantifiers
126 } // namespace theory