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
|
/********************* */
/*! \file model_builder.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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 Model Builder class
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#include "theory/quantifiers_engine.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class QModelBuilder : public TheoryEngineModelBuilder
{
protected:
//quantifiers engine
QuantifiersEngine* d_qe;
bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
bool preProcessBuildModelStd(TheoryModel* m);
/** number of lemmas generated while building model */
unsigned d_addedLemmas;
unsigned d_triedLemmas;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilder() throw() {}
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
// >0 : success
// <0 : failed
virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
//debug model
virtual void debugModel( TheoryModel* m );
//statistics
unsigned getNumAddedLemmas() { return d_addedLemmas; }
unsigned getNumTriedLemmas() { return d_triedLemmas; }
};
class TermArgBasisTrie {
private:
bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
public:
/** the data */
std::map< Node, TermArgBasisTrie > d_data;
public:
bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
};/* class TermArgBasisTrie */
/** model builder class
* This class is capable of building candidate models based on the current quantified formulas
* that are asserted. Use:
* (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
* (2) if candidate model is determined to be a real model,
then call QModelBuilder::buildModel( m, true );
*/
class QModelBuilderIG : public QModelBuilder
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
protected:
BoolMap d_basisNoMatch;
//map from operators to model preference data
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
//built model uf
std::map< Node, bool > d_uf_model_constructed;
//whether inst gen was done
bool d_didInstGen;
/** process build model */
virtual bool processBuildModel( TheoryModel* m );
protected:
//reset
virtual void reset( FirstOrderModel* fm ) = 0;
//initialize quantifiers, return number of lemmas produced
virtual int initializeQuantifier( Node f, Node fp );
//analyze model
virtual void analyzeModel( FirstOrderModel* fm );
//analyze quantifiers
virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0;
//do InstGen techniques for quantifier, return number of lemmas produced
virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
//theory-specific build models
virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
protected:
//map from quantifiers to if are SAT
//std::map< Node, bool > d_quant_sat;
//which quantifiers have been initialized
std::map< Node, bool > d_quant_basis_match_added;
//map from quantifiers to model basis match
std::map< Node, InstMatch > d_quant_basis_match;
protected: //helper functions
/** term has constant definition */
bool hasConstantDefinition( Node n );
public:
QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilderIG() throw() {}
public:
/** statistics class */
class Statistics {
public:
IntStat d_num_quants_init;
IntStat d_num_partial_quants_init;
IntStat d_init_inst_gen_lemmas;
IntStat d_inst_gen_lemmas;
IntStat d_eval_formulas;
IntStat d_eval_uf_terms;
IntStat d_eval_lits;
IntStat d_eval_lits_unknown;
Statistics();
~Statistics();
};
Statistics d_statistics;
// is term selected
virtual bool isTermSelected( Node n ) { return false; }
/** quantifier has inst-gen definition */
virtual bool hasInstGen( Node f ) = 0;
/** did inst gen this round? */
bool didInstGen() { return d_didInstGen; }
// is quantifier active?
bool isQuantifierActive( Node f );
//do exhaustive instantiation
int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
//temporary stats
int d_numQuantSat;
int d_numQuantInstGen;
int d_numQuantNoInstGen;
int d_numQuantNoSelForm;
//temporary stat
int d_instGenMatches;
};/* class QModelBuilder */
class QModelBuilderDefault : public QModelBuilderIG
{
private: ///information for (old) InstGen
//map from quantifiers to their selection literals
std::map< Node, Node > d_quant_selection_lit;
std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
//map from quantifiers to their selection literal terms
std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
//map from terms to the selection literals they exist in
std::map< Node, Node > d_term_selection_lit;
//map from operators to terms that appear in selection literals
std::map< Node, std::vector< Node > > d_op_selection_terms;
//get selection score
int getSelectionScore( std::vector< Node >& uf_terms );
protected:
//reset
void reset( FirstOrderModel* fm );
//analyze quantifier
void analyzeQuantifier( FirstOrderModel* fm, Node f );
//do InstGen techniques for quantifier, return number of lemmas produced
int doInstGen( FirstOrderModel* fm, Node f );
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
protected:
std::map< Node, QuantPhaseReq > d_phase_reqs;
public:
QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
~QModelBuilderDefault() throw() {}
//options
bool optReconsiderFuncConstants() { return true; }
//has inst gen
bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
};
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
|
