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
|
/********************* */
/*! \file trigger.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
** Minor contributors (to current version): bobot, mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 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__QUANTIFIERS__TRIGGER_H
#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
#include "theory/quantifiers/inst_match.h"
namespace CVC4 {
namespace theory {
namespace inst {
//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 */
IMGenerator* 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 );
IMGenerator* getGenerator() { return d_mg; }
public:
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound();
/** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
void reset( Node eqc );
/** get next match. must call reset( eqc ) once before this function. */
bool getNextMatch( InstMatch& m );
/** get the match against ground term or formula t.
the trigger and t should have the same shape.
Currently the trigger should not be a multi-trigger.
*/
bool getMatch( Node t, InstMatch& m);
/** add ground term t, called when t is added to the TermDb */
int addTerm( Node t );
/** return true if whatever Node is subsituted for the variables the
given Node can't match the pattern */
bool nonunifiable( TNode t, const std::vector<Node> & vars){
return d_mg->nonunifiable(t,vars);
}
/** 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{
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 bool isUsableTrigger( std::vector< Node >& nodes, Node f );
static bool isUsableTrigger( Node n, Node f );
static bool isAtomicTrigger( Node n );
static bool isSimpleTrigger( Node n );
/** filter all nodes that have instances */
static void filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes );
/** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
static int isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 );
/** 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;
}
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
|
