1 /********************* */
2 /*! \file inst_strategy.h
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Theory uf instantiation strategies
17 #include "cvc4_private.h"
19 #ifndef __CVC4__INST_STRATEGY_H
20 #define __CVC4__INST_STRATEGY_H
22 #include "theory/quantifiers_engine.h"
23 #include "theory/quantifiers/trigger.h"
25 #include "context/context.h"
26 #include "context/context_mm.h"
28 #include "util/stats.h"
29 #include "theory/uf/theory_uf.h"
35 class InstantiatorTheoryUf
;
37 //instantiation strategies
39 class InstStrategyCheckCESolved
: public InstStrategy
{
41 /** InstantiatorTheoryUf class */
42 InstantiatorTheoryUf
* d_th
;
44 std::map
< Node
, bool > d_solved
;
45 /** calc if f is solved */
46 void calcSolved( Node f
);
47 /** process functions */
48 void processResetInstantiationRound( Theory::Effort effort
);
49 int process( Node f
, Theory::Effort effort
, int e
);
51 InstStrategyCheckCESolved( InstantiatorTheoryUf
* th
, QuantifiersEngine
* ie
) :
52 InstStrategy( ie
), d_th( th
){}
53 ~InstStrategyCheckCESolved(){}
55 std::string
identify() const { return std::string("CheckCESolved"); }
56 };/* class InstStrategyCheckCESolved */
58 class InstStrategyUserPatterns
: public InstStrategy
{
60 /** InstantiatorTheoryUf class */
61 InstantiatorTheoryUf
* d_th
;
62 /** explicitly provided patterns */
63 std::map
< Node
, std::vector
< inst::Trigger
* > > d_user_gen
;
64 /** counter for quantifiers */
65 std::map
< Node
, int > d_counter
;
66 /** process functions */
67 void processResetInstantiationRound( Theory::Effort effort
);
68 int process( Node f
, Theory::Effort effort
, int e
);
70 InstStrategyUserPatterns( InstantiatorTheoryUf
* th
, QuantifiersEngine
* ie
) :
71 InstStrategy( ie
), d_th( th
){}
72 ~InstStrategyUserPatterns(){}
75 void addUserPattern( Node f
, Node pat
);
76 /** get num patterns */
77 int getNumUserGenerators( Node f
) { return (int)d_user_gen
[f
].size(); }
78 /** get user pattern */
79 inst::Trigger
* getUserGenerator( Node f
, int i
) { return d_user_gen
[f
][ i
]; }
81 std::string
identify() const { return std::string("UserPatterns"); }
82 };/* class InstStrategyUserPatterns */
84 class InstStrategyAutoGenTriggers
: public InstStrategy
{
91 /** InstantiatorTheoryUf class */
92 InstantiatorTheoryUf
* d_th
;
93 /** trigger generation strategy */
95 /** relevance strategy */
99 int d_regenerate_frequency
;
100 /** generate additional triggers */
101 bool d_generate_additional
;
102 /** triggers for each quantifier */
103 std::map
< Node
, std::map
< inst::Trigger
*, bool > > d_auto_gen_trigger
;
104 std::map
< Node
, int > d_counter
;
105 /** single, multi triggers for each quantifier */
106 std::map
< Node
, std::vector
< Node
> > d_patTerms
[2];
107 std::map
< Node
, bool > d_is_single_trigger
;
108 std::map
< Node
, bool > d_single_trigger_gen
;
109 std::map
< Node
, bool > d_made_multi_trigger
;
111 /** process functions */
112 void processResetInstantiationRound( Theory::Effort effort
);
113 int process( Node f
, Theory::Effort effort
, int e
);
114 /** generate triggers */
115 void generateTriggers( Node f
);
117 InstStrategyAutoGenTriggers( InstantiatorTheoryUf
* th
, QuantifiersEngine
* ie
, int tstrt
, int rstrt
, int rgfr
= -1 ) :
118 InstStrategy( ie
), d_th( th
), d_tr_strategy( tstrt
), d_rlv_strategy( rstrt
), d_generate_additional( false ){
119 setRegenerateFrequency( rgfr
);
121 ~InstStrategyAutoGenTriggers(){}
123 /** get auto-generated trigger */
124 inst::Trigger
* getAutoGenTrigger( Node f
);
126 std::string
identify() const { return std::string("AutoGenTriggers"); }
127 /** set regenerate frequency, if fr<0, turn off regenerate */
128 void setRegenerateFrequency( int fr
){
130 d_regenerate
= false;
132 d_regenerate_frequency
= fr
;
136 /** set generate additional */
137 void setGenerateAdditional( bool val
) { d_generate_additional
= val
; }
138 };/* class InstStrategyAutoGenTriggers */
142 class InstStrategyAddFailSplits
: public InstStrategy
{
144 /** InstantiatorTheoryUf class */
145 InstantiatorTheoryUf
* d_th
;
146 /** process functions */
147 void processResetInstantiationRound( Theory::Effort effort
);
148 int process( Node f
, Theory::Effort effort
, int e
);
150 InstStrategyAddFailSplits( InstantiatorTheoryUf
* th
, QuantifiersEngine
* ie
) :
151 InstStrategy( ie
), d_th( th
){}
152 ~InstStrategyAddFailSplits(){}
154 std::string
identify() const { return std::string("AddFailSplits"); }
155 };/* class InstStrategyAddFailSplits */
159 class InstStrategyFreeVariable
: public InstStrategy
{
161 /** InstantiatorTheoryUf class */
162 InstantiatorTheoryUf
* d_th
;
163 /** guessed instantiations */
164 std::map
< Node
, bool > d_guessed
;
165 /** process functions */
166 void processResetInstantiationRound( Theory::Effort effort
);
167 int process( Node f
, Theory::Effort effort
, int e
);
169 InstStrategyFreeVariable( InstantiatorTheoryUf
* th
, QuantifiersEngine
* ie
) :
170 InstStrategy( ie
), d_th( th
){}
171 ~InstStrategyFreeVariable(){}
173 std::string
identify() const { return std::string("FreeVariable"); }
174 };/* class InstStrategyFreeVariable */
176 }/* CVC4::theory::uf namespace */
177 }/* CVC4::theory namespace */
178 }/* CVC4 namespace */