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
|
/********************* */
/*! \file full_model_check.h
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 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
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
#define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
#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
{
private:
int d_complete;
public:
EntryTrie() : d_complete(-1), d_data(-1){}
std::map<Node,EntryTrie> d_child;
int d_data;
void reset() { d_data = -1; d_child.clear(); d_complete = -1; }
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 );
void collectIndices(Node c, int index, std::vector< int >& indices );
bool isComplete(FirstOrderModelFmc * m, Node c, int index);
};/* class EntryTrie */
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;
void basic_simplify( FirstOrderModelFmc * m );
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( FullModelChecker * mc, FirstOrderModelFmc * m );
void debugPrint(const char * tr, Node op, FullModelChecker * m);
};/* class Def */
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< TypeNode, Node > d_array_cond;
std::map< Node, Node > d_array_term_cond;
std::map< Node, std::vector< int > > d_star_insts;
std::map< TypeNode, bool > d_preinitialized_types;
void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
protected:
void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
std::map< int, std::map< int, Node > >& changed_vals );
void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
std::map< int, std::map< int, Node > >& changed_vals );
void convertIntervalModel( FirstOrderModelFmc * fm, Node op );
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, Def & d,
Def & df, 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 );
Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true );
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 mkArrayCond( Node a );
Node evaluateInterpreted( Node n, std::vector< Node > & vals );
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
FullModelChecker( context::Context* c, QuantifiersEngine* qe );
~FullModelChecker() throw() {}
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 );
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
/** process build model */
void preProcessBuildModel(TheoryModel* m, bool fullModel);
void processBuildModel(TheoryModel* m, bool fullModel);
/** get current model value */
Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
bool useSimpleModels();
};/* class FullModelChecker */
}/* CVC4::theory::quantifiers::fmcheck namespace */
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
|
