1 /********************* */
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief trigger class
17 #include "cvc4_private.h"
19 #ifndef __CVC4__TRIGGER_H
20 #define __CVC4__TRIGGER_H
22 #include "theory/inst_match.h"
28 //a collect of nodes representing a trigger
31 /** computation of variable contains */
32 static std::map
< TNode
, std::vector
< TNode
> > d_var_contains
;
33 static void computeVarContains( Node n
);
34 static void computeVarContains2( Node n
, Node parent
);
36 /** the quantifiers engine */
37 QuantifiersEngine
* d_quantEngine
;
38 /** the quantifier this trigger is for */
40 /** match generators */
43 /** a trie of triggers */
46 Trigger
* getTrigger2( std::vector
< Node
>& nodes
);
47 void addTrigger2( std::vector
< Node
>& nodes
, Trigger
* t
);
49 TrTrie() : d_tr( NULL
){}
51 std::map
< TNode
, TrTrie
* > d_children
;
52 Trigger
* getTrigger( std::vector
< Node
>& nodes
){
53 std::vector
< Node
> temp
;
54 temp
.insert( temp
.begin(), nodes
.begin(), nodes
.end() );
55 std::sort( temp
.begin(), temp
.end() );
56 return getTrigger2( temp
);
58 void addTrigger( std::vector
< Node
>& nodes
, Trigger
* t
){
59 std::vector
< Node
> temp
;
60 temp
.insert( temp
.begin(), nodes
.begin(), nodes
.end() );
61 std::sort( temp
.begin(), temp
.end() );
62 return addTrigger2( temp
, t
);
64 };/* class Trigger::TrTrie */
65 /** all triggers will be stored in this trie */
66 static TrTrie d_tr_trie
;
68 /** trigger constructor */
69 Trigger( QuantifiersEngine
* ie
, Node f
, std::vector
< Node
>& nodes
, int matchOption
= 0, bool smartTriggers
= false );
73 std::vector
< Node
> d_nodes
;
75 void debugPrint( const char* c
);
76 IMGenerator
* getGenerator() { return d_mg
; }
78 /** reset instantiation round (call this whenever equivalence classes have changed) */
79 void resetInstantiationRound();
80 /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
81 void reset( Node eqc
);
82 /** get next match. must call reset( eqc ) once before this function. */
83 bool getNextMatch( InstMatch
& m
);
84 /** get the match against ground term or formula t.
85 the trigger and t should have the same shape.
86 Currently the trigger should not be a multi-trigger.
88 bool getMatch( Node t
, InstMatch
& m
);
89 /** add ground term t, called when t is added to the TermDb */
90 int addTerm( Node t
);
91 /** return true if whatever Node is subsituted for the variables the
92 given Node can't match the pattern */
93 bool nonunifiable( TNode t
, const std::vector
<Node
> & vars
){
94 return d_mg
->nonunifiable(t
,vars
);
96 /** return whether this is a multi-trigger */
97 bool isMultiTrigger() { return d_nodes
.size()>1; }
99 /** add all available instantiations exhaustively, in any equivalence class
100 if limitInst>0, limitInst is the max # of instantiations to try */
101 int addInstantiations( InstMatch
& baseMatch
);
103 ie : quantifier engine;
104 f : forall something ....
105 nodes : (multi-)trigger
106 matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* )
107 keepAll: don't remove unneeded patterns;
108 trOption : policy for dealing with triggers that already existed (see below)
111 TR_MAKE_NEW
, //make new trigger even if it already may exist
112 TR_GET_OLD
, //return a previous trigger if it had already been created
113 TR_RETURN_NULL
//return null if a duplicate is found
115 static Trigger
* mkTrigger( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& nodes
,
116 int matchOption
= 0, bool keepAll
= true, int trOption
= TR_MAKE_NEW
,
117 bool smartTriggers
= false );
118 static Trigger
* mkTrigger( QuantifiersEngine
* qe
, Node f
, Node n
,
119 int matchOption
= 0, bool keepAll
= true, int trOption
= TR_MAKE_NEW
,
120 bool smartTriggers
= false );
122 /** is subterm of trigger usable */
123 static bool isUsable( Node n
, Node f
);
124 /** collect all APPLY_UF pattern terms for f in n */
125 static bool collectPatTerms2( QuantifiersEngine
* qe
, Node f
, Node n
, std::map
< Node
, bool >& patMap
, int tstrt
);
127 //different strategies for choosing trigger terms
133 static void collectPatTerms( QuantifiersEngine
* qe
, Node f
, Node n
, std::vector
< Node
>& patTerms
, int tstrt
, bool filterInst
= false );
135 /** is usable trigger */
136 static bool isUsableTrigger( std::vector
< Node
>& nodes
, Node f
);
137 static bool isUsableTrigger( Node n
, Node f
);
138 static bool isAtomicTrigger( Node n
);
139 static bool isSimpleTrigger( Node n
);
140 /** filter all nodes that have instances */
141 static void filterInstances( std::vector
< Node
>& nodes
);
142 /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
143 static int isInstanceOf( Node n1
, Node n2
);
144 /** variables subsume, return true if n1 contains all free variables in n2 */
145 static bool isVariableSubsume( Node n1
, Node n2
);
146 /** get var contains */
147 static void getVarContains( Node f
, std::vector
< Node
>& pats
, std::map
< Node
, std::vector
< Node
> >& varContains
);
148 static void getVarContainsNode( Node f
, Node n
, std::vector
< Node
>& varContains
);
149 /** get pattern arithmetic */
150 static bool getPatternArithmetic( Node f
, Node n
, std::map
< Node
, Node
>& coeffs
);
152 inline void toStream(std::ostream
& out
) const {
154 for( int i
=0; i
<(int)d_nodes
.size(); i
++ ){
155 if( i
>0 ){ out
<< ", "; }
162 inline std::ostream
& operator<<(std::ostream
& out
, const Trigger
& tr
) {
167 }/* CVC4::theory::inst namespace */
169 }/* CVC4::theory namespace */
171 }/* CVC4 namespace */
173 #endif /* __CVC4__TRIGGER_H */