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
|
/********************* */
/*! \file instantiation_engine.h
** \verbatim
** Original author: Morgan Deters <mdeters@cs.nyu.edu>
** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>
** 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 Instantiation Engine classes
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class InstStrategyUserPatterns;
/** instantiation strategy class */
class InstStrategy {
public:
enum Status {
STATUS_UNFINISHED,
STATUS_UNKNOWN,
STATUS_SAT,
};/* enum Status */
protected:
/** reference to the instantiation engine */
QuantifiersEngine* d_quantEngine;
/** should process a quantifier */
std::map< Node, bool > d_quantActive;
/** calculate should process */
virtual bool calculateShouldProcess( Node f ) { return true; }
public:
InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
virtual ~InstStrategy(){}
/** should process quantified formula f? */
bool shouldProcess( Node f ) {
if( d_quantActive.find( f )==d_quantActive.end() ){
d_quantActive[f] = calculateShouldProcess( f );
}
return d_quantActive[f];
}
/** reset instantiation */
virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
/** process method, returns a status */
virtual int process( Node f, Theory::Effort effort, int e ) = 0;
/** update status */
static void updateStatus( int& currStatus, int addStatus ){
if( addStatus==STATUS_UNFINISHED ){
currStatus = STATUS_UNFINISHED;
}else if( addStatus==STATUS_UNKNOWN ){
if( currStatus==STATUS_SAT ){
currStatus = STATUS_UNKNOWN;
}
}
}
/** identify */
virtual std::string identify() const { return std::string("Unknown"); }
};/* class InstStrategy */
class InstantiationEngine : public QuantifiersModule
{
private:
/** instantiation strategies */
std::vector< InstStrategy* > d_instStrategies;
/** instantiation strategies active */
std::map< InstStrategy*, bool > d_instStrategyActive;
/** user-pattern instantiation strategy */
InstStrategyUserPatterns* d_isup;
/** is instantiation strategy active */
bool isActiveStrategy( InstStrategy* is ) {
return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
}
/** add inst strategy */
void addInstStrategy( InstStrategy* is ){
d_instStrategies.push_back( is );
d_instStrategyActive[is] = true;
}
private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
/** status of instantiation round (one of InstStrategy::STATUS_*) */
int d_inst_round_status;
/** whether the instantiation engine should set incomplete if it cannot answer SAT */
bool d_setIncomplete;
/** inst round counter */
int d_ierCounter;
bool d_performCheck;
/** whether each quantifier is active */
std::map< Node, bool > d_quant_active;
/** whether we have added cbqi lemma */
std::map< Node, bool > d_added_cbqi_lemma;
private:
/** has added cbqi lemma */
bool hasAddedCbqiLemma( Node f ) { return d_added_cbqi_lemma.find( f )!=d_added_cbqi_lemma.end(); }
/** helper functions */
bool hasNonArithmeticVariable( Node f );
bool hasApplyUf( Node f );
/** whether to do CBQI for quantifier f */
bool doCbqi( Node f );
private:
/** do instantiation round */
bool doInstantiationRound( Theory::Effort effort );
/** register literals of n, f is the quantifier it belongs to */
//void registerLiterals( Node n, Node f );
private:
enum{
SAT_CBQI,
SAT_INST_STRATEGY,
};
/** debug sat */
void debugSat( int reason );
public:
InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
~InstantiationEngine(){}
/** initialize */
void finishInit();
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e );
void registerQuantifier( Node f );
void assertNode( Node f );
Node explain(TNode n){ return Node::null(); }
Node getNextDecisionRequest();
/** add user pattern */
void addUserPattern( Node f, Node pat );
public:
/** statistics class */
class Statistics {
public:
IntStat d_instantiations_user_patterns;
IntStat d_instantiations_auto_gen;
IntStat d_instantiations_auto_gen_min;
IntStat d_instantiations_guess;
IntStat d_instantiations_cbqi_arith;
IntStat d_instantiations_cbqi_arith_minus;
IntStat d_instantiations_cbqi_datatypes;
Statistics();
~Statistics();
};
Statistics d_statistics;
};/* class InstantiationEngine */
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
|
