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
|
/********************* */
/*! \file rep_set.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, 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 Representative set class and utilities
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__REP_SET_H
#define __CVC4__THEORY__REP_SET_H
#include "expr/node.h"
#include <map>
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
/** this class stores a representative set */
class RepSet {
public:
RepSet(){}
~RepSet(){}
std::map< TypeNode, std::vector< Node > > d_type_reps;
std::map< TypeNode, bool > d_type_complete;
std::map< Node, int > d_tmap;
// map from values to terms they were assigned for
std::map< Node, Node > d_values_to_terms;
/** clear the set */
void clear();
/** has type */
bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
/** has rep */
bool hasRep( TypeNode tn, Node n );
/** get cardinality for type */
int getNumRepresentatives( TypeNode tn ) const;
/** add representative for type */
void add( TypeNode tn, Node n );
/** returns index in d_type_reps for node n */
int getIndexFor( Node n ) const;
/** complete all values */
bool complete( TypeNode t );
/** debug print */
void toStream(std::ostream& out);
};/* class RepSet */
//representative domain
typedef std::vector< int > RepDomain;
class RepBoundExt {
public:
virtual ~RepBoundExt() {}
virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
};
/** this class iterates over a RepSet */
class RepSetIterator {
public:
enum {
ENUM_DEFAULT,
ENUM_BOUND_INT,
};
private:
QuantifiersEngine * d_qe;
//initialize function
bool initialize( RepBoundExt* rext = NULL );
//for int ranges
std::map< int, Node > d_lower_bounds;
//for set ranges
std::map< int, std::vector< Node > > d_setm_bounds;
//domain size
int domainSize( int i );
//node this is rep set iterator is for
Node d_owner;
//reset index, 1:success, 0:empty, -1:fail
int resetIndex( int i, bool initial = false );
/** set index order */
void setIndexOrder( std::vector< int >& indexOrder );
/** do reset increment the iterator at index=counter */
int do_reset_increment( int counter, bool initial = false );
//ordering for variables we are indexing over
// for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
// then we consider instantiations in this order:
// a/x a/y a/z
// a/x b/y a/z
// b/x a/y a/z
// b/x b/y a/z
// ...
std::vector< int > d_index_order;
//variables to index they are considered at
// for example, if d_index_order = { 2, 0, 1 }
// then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
std::map< int, int > d_var_order;
//are we only considering a strict subset of the domain of the quantifier?
bool d_incomplete;
public:
RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
~RepSetIterator(){}
//set that this iterator will be iterating over instantiations for a quantifier
bool setQuantifier( Node f, RepBoundExt* rext = NULL );
//set that this iterator will be iterating over the domain of a function
bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
public:
//pointer to model
RepSet* d_rep_set;
//enumeration type?
std::vector< int > d_enum_type;
//current tuple we are considering
std::vector< int > d_index;
//types we are considering
std::vector< TypeNode > d_types;
//domain we are considering
std::vector< std::vector< Node > > d_domain_elements;
public:
/** increment the iterator at index=counter */
int increment2( int i );
/** increment the iterator */
int increment();
/** is the iterator finished? */
bool isFinished();
/** get the i_th term we are considering */
Node getCurrentTerm( int v );
/** get the number of terms we are considering */
int getNumTerms() { return (int)d_index_order.size(); }
/** debug print */
void debugPrint( const char* c );
void debugPrintSmall( const char* c );
//get index order, returns var #
int getIndexOrder( int v ) { return d_index_order[v]; }
//get variable order, returns index #
int getVariableOrder( int i ) { return d_var_order[i]; }
//is incomplete
bool isIncomplete() { return d_incomplete; }
};/* class RepSetIterator */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__REP_SET_H */
|
