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
|
/********************* */
/*! \file inst_strategy_e_matching.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-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief E matching instantiation strategies
**/
#include "cvc4_private.h"
#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
#define __CVC4__INST_STRATEGY_E_MATCHING_H
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/trigger.h"
#include "context/context.h"
#include "context/context_mm.h"
#include "util/statistics_registry.h"
#include "theory/quantifiers/instantiation_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
//instantiation strategies
class InstStrategyUserPatterns : public InstStrategy{
private:
/** explicitly provided patterns */
std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
/** waiting to be generated patterns */
std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait;
/** counter for quantifiers */
std::map< Node, int > d_counter;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
public:
InstStrategyUserPatterns( QuantifiersEngine* ie ) :
InstStrategy( ie ){}
~InstStrategyUserPatterns(){}
public:
/** add pattern */
void addUserPattern( Node f, Node pat );
/** get num patterns */
int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
/** get user pattern */
inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
/** identify */
std::string identify() const { return std::string("UserPatterns"); }
};/* class InstStrategyUserPatterns */
class InstStrategyAutoGenTriggers : public InstStrategy {
public:
enum {
RELEVANCE_NONE,
RELEVANCE_DEFAULT,
};
private:
/** trigger generation strategy */
int d_tr_strategy;
/** regeneration */
bool d_regenerate;
int d_regenerate_frequency;
/** (single,multi) triggers for each quantifier */
std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
std::map< Node, int > d_counter;
/** single, multi triggers for each quantifier */
std::map< Node, std::vector< Node > > d_patTerms[2];
std::map< Node, bool > d_is_single_trigger;
std::map< Node, bool > d_single_trigger_gen;
std::map< Node, bool > d_made_multi_trigger;
//processed trigger this round
std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
//instantiation no patterns
std::map< Node, std::vector< Node > > d_user_no_gen;
private:
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
/** generate triggers */
void generateTriggers( Node f, Theory::Effort effort, int e, int& status );
//bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
/** has user patterns */
bool hasUserPatterns( Node f );
/** has user patterns */
std::map< Node, bool > d_hasUserPatterns;
public:
InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
~InstStrategyAutoGenTriggers(){}
public:
/** get auto-generated trigger */
inst::Trigger* getAutoGenTrigger( Node f );
/** identify */
std::string identify() const { return std::string("AutoGenTriggers"); }
/** add pattern */
void addUserNoPattern( Node f, Node pat );
};/* class InstStrategyAutoGenTriggers */
class FullSaturation : public QuantifiersModule {
private:
/** guessed instantiations */
std::map< Node, bool > d_guessed;
/** process functions */
bool process( Node f, Theory::Effort effort );
public:
FullSaturation( QuantifiersEngine* qe );
~FullSaturation(){}
bool needsCheck( Theory::Effort e );
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node q );
void assertNode( Node n );
/** identify */
std::string identify() const { return std::string("FullSaturation"); }
};/* class FullSaturation */
}
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif
|
