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
|
/********************* */
/*! \file qinterval_builder.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 qinterval model class
**/
#include "cvc4_private.h"
#ifndef QINTERVAL_BUILDER
#define QINTERVAL_BUILDER
#include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/first_order_model.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class FirstOrderModelQInt;
class QIntVarNumIndex
{
public:
std::map< int, int > d_var_num;
std::map< int, QIntVarNumIndex > d_var_index;
};
class QIntDef
{
private:
Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );
Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );
void construct_compose_r( FirstOrderModelQInt * m, Node q,
std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,
std::vector< Node >& args,
std::map< unsigned, QIntDef >& children,
std::map< unsigned, Node >& bchildren,
QIntVarNumIndex& vindex,
unsigned depth );
void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );
int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );
void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
Node v, unsigned depth = 0 );
Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
unsigned depth );
bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
unsigned depth );
public:
QIntDef(){}
std::map< Node, QIntDef > d_def;
std::vector< Node > d_def_order;
void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );
bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
std::map< unsigned, QIntDef >& children,
std::map< unsigned, Node >& bchildren, int varChCount,
QIntVarNumIndex& vindex );
bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );
Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }
Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }
void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );
QIntDef * getChild( unsigned i );
Node getValue() { return d_def_order[0]; }
Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }
Node getUpper( unsigned i ) { return d_def_order[i]; }
Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }
int getNumChildren() { return d_def_order.size(); }
bool isTotal( FirstOrderModelQInt * m, Node q );
Node simplify( FirstOrderModelQInt * m, Node q );
Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );
static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
};
class QIntDefIter {
private:
FirstOrderModelQInt * d_fm;
Node d_q;
void resetIndex( QIntDef * qid );
public:
QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );
void debugPrint( const char * c, int t = 0 );
std::vector< QIntDef * > d_index_visited;
std::vector< int > d_index;
bool isFinished() { return d_index.empty(); }
bool increment( int index = -1 );
unsigned getSize() { return d_index.size(); }
Node getLower( int index );
Node getUpper( int index );
void getLowers( std::vector< Node >& reps );
void getUppers( std::vector< Node >& reps );
Node getValue();
};
class QuantVarOrder
{
private:
int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );
int d_var_count;
Node d_q;
void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );
public:
QuantVarOrder( Node q );
std::map< int, Node > d_num_to_var;
std::map< int, int > d_num_to_prev_num;
std::map< int, int > d_num_to_next_num;
std::map< Node, std::vector< int > > d_var_to_num;
std::map< int, int > d_var_num_index;
//std::map< Node, std::map< int, int > > d_var_occur;
//int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }
unsigned getNumVars() { return d_var_count; }
Node getVar( int i ) { return d_num_to_var[i]; }
int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; }
int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; }
int getVarNumIndex( int i ) { return d_var_num_index[i]; }
bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
std::vector< Node >& inst );
void debugPrint( const char * c );
QIntVarNumIndex d_var_occur;
};
class QIntervalBuilder : public QModelBuilder
{
private:
Node d_true;
bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
QIntVarNumIndex& vindex );
public:
QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );
//process build model
void processBuildModel(TheoryModel* m, bool fullModel);
//do exhaustive instantiation
bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
};
}
}
}
#endif
|
