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
|
/********************* */
/*! \file full_model_check.h
** \verbatim
** Original author: Andrew Reynolds
** 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 Full model check class
**/
#ifndef FULL_MODEL_CHECK
#define FULL_MODEL_CHECK
#include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/first_order_model.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
namespace fmcheck {
class FirstOrderModelFmc;
class FullModelChecker;
class EntryTrie
{
public:
EntryTrie() : d_data(-1){}
std::map<Node,EntryTrie> d_child;
int d_data;
void reset() { d_data = -1; d_child.clear(); }
void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );
bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
};
class Def
{
public:
EntryTrie d_et;
//cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
std::vector< Node > d_cond;
//value is returned by FullModelChecker::getRepresentative
std::vector< Node > d_value;
private:
enum {
status_unk,
status_redundant,
status_non_redundant
};
std::vector< int > d_status;
bool d_has_simplified;
public:
Def() : d_has_simplified(false){}
void reset() {
d_et.reset();
d_cond.clear();
d_value.clear();
d_status.clear();
d_has_simplified = false;
}
bool addEntry( FirstOrderModelFmc * m, Node c, Node v);
Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );
int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
void simplify( FirstOrderModelFmc * m );
void debugPrint(const char * tr, Node op, FullModelChecker * m);
};
class FirstOrderModelFmc : public FirstOrderModel
{
friend class FullModelChecker;
private:
/** quant engine */
QuantifiersEngine * d_qe;
/** models for UF */
std::map<Node, Def * > d_models;
std::map<TypeNode, Node > d_model_basis_rep;
std::map<TypeNode, Node > d_type_star;
Node getUsedRepresentative(Node n);
/** get current model value */
Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
void processInitializeModelForTerm(Node n);
public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
// initialize the model
void processInitialize();
Node getFunctionValue(Node op, const char* argPrefix );
bool isStar(Node n);
Node getStar(TypeNode tn);
bool isModelBasisTerm(Node n);
Node getModelBasisTerm(TypeNode tn);
Node getSomeDomainElement(TypeNode tn);
};
class FullModelChecker : public QModelBuilder
{
protected:
Node d_true;
Node d_false;
std::map<TypeNode, std::map< Node, int > > d_rep_ids;
std::map<Node, Def > d_quant_models;
std::map<Node, Node > d_quant_cond;
std::map<Node, std::map< Node, int > > d_quant_var_id;
std::map<Node, std::vector< int > > d_star_insts;
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
protected:
void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,
std::vector< Node > & conds,
std::vector< Node > & values,
std::vector< Node > & entry_conds );
private:
void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
void doNegate( Def & dc );
void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );
void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val );
void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
std::map< int, Node > & entries, int index,
std::vector< Node > & cond, std::vector< Node > & val,
EntryTrie & curr);
void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val );
int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
Node mkCond( std::vector< Node > & cond );
Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
void mkCondVec( Node n, std::vector< Node > & cond );
Node evaluateInterpreted( Node n, std::vector< Node > & vals );
public:
FullModelChecker( context::Context* c, QuantifiersEngine* qe );
~FullModelChecker(){}
int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
/** process build model */
void processBuildModel(TheoryModel* m, bool fullModel);
/** get current model value */
Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
bool useSimpleModels();
};
}
}
}
}
#endif
|
