1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
/********************* */
/*! \file rr_trigger.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Andrew Reynolds, Francois Bobot
** Minor contributors (to current version): Tianyi Liang
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief trigger class
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H
#define __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H
#include "theory/rewriterules/rr_inst_match.h"
namespace CVC4 {
namespace theory {
namespace rrinst {
//a collect of nodes representing a trigger
class Trigger {
private:
/** the quantifiers engine */
QuantifiersEngine* d_quantEngine;
/** the quantifier this trigger is for */
Node d_f;
/** match generators */
PatsMatcher * d_mg;
private:
/** trigger constructor */
Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false );
public:
~Trigger(){}
public:
std::vector< Node > d_nodes;
public:
void debugPrint( const char* c );
PatsMatcher* getGenerator() { return d_mg; }
public:
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound();
/** get next match. must call reset( eqc ) once before this function. */
bool getNextMatch();
const InstMatch & getInstMatch(){return d_mg->getInstMatch();};
/** return whether this is a multi-trigger */
bool isMultiTrigger() { return d_nodes.size()>1; }
public:
/** add all available instantiations exhaustively, in any equivalence class
if limitInst>0, limitInst is the max # of instantiations to try */
int addInstantiations( InstMatch& baseMatch);
/** mkTrigger method
ie : quantifier engine;
f : forall something ....
nodes : (multi-)trigger
matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* )
keepAll: don't remove unneeded patterns;
trOption : policy for dealing with triggers that already existed (see below)
*/
enum {
//options for producing matches
MATCH_GEN_DEFAULT = 0,
MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E
};
enum{
TR_MAKE_NEW, //make new trigger even if it already may exist
TR_GET_OLD, //return a previous trigger if it had already been created
TR_RETURN_NULL //return null if a duplicate is found
};
static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
bool smartTriggers = false );
static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
bool smartTriggers = false );
private:
/** is subterm of trigger usable */
static bool isUsable( Node n, Node f );
/** collect all APPLY_UF pattern terms for f in n */
static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt );
public:
//different strategies for choosing trigger terms
enum {
TS_MAX_TRIGGER = 0,
TS_MIN_TRIGGER,
TS_ALL,
};
static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false );
public:
/** is usable trigger */
static inline bool isUsableTrigger( TNode n, TNode f ){
//return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
}
static inline bool isAtomicTrigger( TNode n ){
return
n.getKind()==kind::APPLY_UF ||
n.getKind() == kind::APPLY_CONSTRUCTOR ||
n.getKind()==kind::SELECT ||
n.getKind()==kind::STORE;
}
static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
static bool isSimpleTrigger( Node n );
/** get pattern arithmetic */
static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
inline void toStream(std::ostream& out) const {
out << "TRIGGER( ";
for( int i=0; i<(int)d_nodes.size(); i++ ){
if( i>0 ){ out << ", "; }
out << d_nodes[i];
}
out << " )";
}
};
inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
tr.toStream(out);
return out;
}
/** a trie of triggers */
class TriggerTrie
{
private:
Trigger* getTrigger2( std::vector< Node >& nodes );
void addTrigger2( std::vector< Node >& nodes, Trigger* t );
public:
TriggerTrie() : d_tr( NULL ){}
Trigger* d_tr;
std::map< Node, TriggerTrie* > d_children;
Trigger* getTrigger( std::vector< Node >& nodes ){
std::vector< Node > temp;
temp.insert( temp.begin(), nodes.begin(), nodes.end() );
std::sort( temp.begin(), temp.end() );
return getTrigger2( temp );
}
void addTrigger( std::vector< Node >& nodes, Trigger* t ){
std::vector< Node > temp;
temp.insert( temp.begin(), nodes.begin(), nodes.end() );
std::sort( temp.begin(), temp.end() );
return addTrigger2( temp, t );
}
};
}/* CVC4::theory::rrinst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H */
|
