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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
/********************* */
/*! \file inst_match_generator.h
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** 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 inst match generator class
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#include "theory/quantifiers/inst_match.h"
#include <map>
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
namespace quantifiers{
class TermArgTrie;
}
namespace inst {
/** base class for producing InstMatch objects */
class IMGenerator {
public:
/** reset instantiation round (call this at beginning of instantiation round) */
virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
/** get the next match. must call reset( eqc ) before this function. */
virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;
/** add instantiations directly */
virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
/** add ground term t, called when t is added to term db */
virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
/** set active add */
virtual void setActiveAdd() {}
};/* class IMGenerator */
class CandidateGenerator;
class InstMatchGenerator : public IMGenerator {
private:
/** candidate generator */
CandidateGenerator* d_cg;
/** policy to use for matching */
int d_matchPolicy;
/** children generators */
std::vector< InstMatchGenerator* > d_children;
std::vector< int > d_children_index;
/** the next generator in order */
InstMatchGenerator* d_next;
/** eq class */
Node d_eq_class;
/** for arithmetic matching */
std::map< Node, Node > d_arith_coeffs;
/** initialize pattern */
void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
public:
enum {
//options for producing matches
MATCH_GEN_DEFAULT = 0,
MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers
//others (internally used)
MATCH_GEN_INTERNAL_ARITHMETIC,
MATCH_GEN_INTERNAL_ERROR,
};
private:
/** for arithmetic */
bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
public:
/** get the match against ground term or formula t.
d_match_pattern and t should have the same shape.
only valid for use where !d_match_pattern.isNull().
*/
bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
/** constructors */
InstMatchGenerator( Node pat, int matchOption = 0 );
/** destructor */
~InstMatchGenerator(){}
/** The pattern we are producing matches for.
If null, this is a multi trigger that is merging matches from d_children.
*/
Node d_pattern;
/** match pattern */
Node d_match_pattern;
public:
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. */
bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
/** add instantiations */
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t */
int addTerm( Node f, Node t, QuantifiersEngine* qe );
bool d_active_add;
void setActiveAdd();
static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe );
static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
};/* class InstMatchGenerator */
/** smart multi-trigger implementation */
class InstMatchGeneratorMulti : public IMGenerator {
private:
/** indexed trie */
typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
/** process new match */
void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
/** process new instantiations */
void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
std::vector< IndexedTrie >& unique_var_tries,
int trieIndex, int childIndex, int endChildIndex, bool modEq );
/** process new instantiations 2 */
void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
std::vector< IndexedTrie >& unique_var_tries,
int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
private:
/** var contains (variable indices) for each pattern node */
std::map< Node, std::vector< int > > d_var_contains;
/** variable indices contained to pattern nodes */
std::map< int, std::vector< Node > > d_var_to_node;
/** quantifier to use */
Node d_f;
/** policy to use for matching */
int d_matchPolicy;
/** children generators */
std::vector< InstMatchGenerator* > d_children;
/** inst match tries for each child */
std::vector< InstMatchTrieOrdered > d_children_trie;
/** calculate matches */
void calculateMatches( QuantifiersEngine* qe );
public:
/** constructors */
InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
/** destructor */
~InstMatchGeneratorMulti(){}
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t */
int addTerm( Node f, Node t, QuantifiersEngine* qe );
};/* class InstMatchGeneratorMulti */
/** smart (single)-trigger implementation */
class InstMatchGeneratorSimple : public IMGenerator {
private:
/** quantifier for match term */
Node d_f;
/** match term */
Node d_match_pattern;
/** add instantiations */
void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
public:
/** constructors */
InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
/** destructor */
~InstMatchGeneratorSimple(){}
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe ) {}
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe ) {}
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t, possibly add instantiations */
int addTerm( Node f, Node t, QuantifiersEngine* qe );
};/* class InstMatchGeneratorSimple */
}
}
}
#endif
|
