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
|
/********************* */
/*! \file inst_strategy_e_matching.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. 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 "context/context.h"
#include "context/context_mm.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers_engine.h"
#include "util/statistics_registry.h"
#include "options/quantifiers_options.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) override;
int process(Node f, Theory::Effort effort, int e) override;
public:
InstStrategyUserPatterns( QuantifiersEngine* ie ) :
InstStrategy( ie ){}
~InstStrategyUserPatterns(){}
public:
/** add pattern */
void addUserPattern( Node q, Node pat );
/** get num patterns */
int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); }
/** get user pattern */
inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
/** identify */
std::string identify() const override { return std::string("UserPatterns"); }
};/* class InstStrategyUserPatterns */
class InstStrategyAutoGenTriggers : public InstStrategy {
public:
enum {
RELEVANCE_NONE,
RELEVANCE_DEFAULT,
};
private:
/** trigger generation strategy */
TriggerSelMode 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, std::map< Node, bool > > d_patReqPol;
/** information about triggers */
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;
// number of trigger variables per quantifier
std::map< Node, unsigned > d_num_trigger_vars;
std::map< Node, Node > d_vc_partition[2];
std::map< Node, Node > d_pat_to_mpat;
private:
/** process functions */
void processResetInstantiationRound(Theory::Effort effort) override;
int process(Node q, Theory::Effort effort, int e) override;
/** generate triggers */
void generateTriggers(Node q);
void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
void addTrigger(inst::Trigger* tr, Node f);
/** has user patterns */
bool hasUserPatterns(Node q);
/** has user patterns */
std::map<Node, bool> d_hasUserPatterns;
public:
InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
~InstStrategyAutoGenTriggers(){}
public:
/** get auto-generated trigger */
inst::Trigger* getAutoGenTrigger( Node q );
/** identify */
std::string identify() const override
{
return std::string("AutoGenTriggers");
}
/** add pattern */
void addUserNoPattern( Node q, Node pat );
};/* class InstStrategyAutoGenTriggers */
}
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif
|
