1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Model for Theory UF. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY_UF_MODEL_H |
19 |
|
#define CVC5__THEORY_UF_MODEL_H |
20 |
|
|
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "expr/node.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
|
28 |
|
class TheoryModel; |
29 |
|
|
30 |
|
namespace uf { |
31 |
|
|
32 |
110208 |
class UfModelTreeNode |
33 |
|
{ |
34 |
|
public: |
35 |
110208 |
UfModelTreeNode(){} |
36 |
|
/** the data */ |
37 |
|
std::map< Node, UfModelTreeNode > d_data; |
38 |
|
/** the value of this tree node (if all paths lead to same value) */ |
39 |
|
Node d_value; |
40 |
|
public: |
41 |
|
//is this model tree empty? |
42 |
13023 |
bool isEmpty() { return d_data.empty() && d_value.isNull(); } |
43 |
|
//clear |
44 |
|
void clear(); |
45 |
|
/** setValue function */ |
46 |
|
void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); |
47 |
|
/** getFunctionValue */ |
48 |
|
Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true ); |
49 |
|
/** update function */ |
50 |
|
void update( TheoryModel* m ); |
51 |
|
/** simplify function */ |
52 |
|
void simplify( Node op, Node defaultVal, int argIndex ); |
53 |
|
/** is total ? */ |
54 |
|
bool isTotal( Node op, int argIndex ); |
55 |
|
public: |
56 |
|
void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 ); |
57 |
|
}; |
58 |
|
|
59 |
5015 |
class UfModelTree |
60 |
|
{ |
61 |
|
private: |
62 |
|
//the op this model is for |
63 |
|
Node d_op; |
64 |
|
//the order we will treat the arguments |
65 |
|
std::vector< int > d_index_order; |
66 |
|
//the data |
67 |
|
UfModelTreeNode d_tree; |
68 |
|
public: |
69 |
|
//constructors |
70 |
|
UfModelTree(){} |
71 |
5015 |
UfModelTree( Node op ) : d_op( op ){ |
72 |
10030 |
TypeNode tn = d_op.getType(); |
73 |
44055 |
for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){ |
74 |
39040 |
d_index_order.push_back( i ); |
75 |
|
} |
76 |
5015 |
} |
77 |
|
UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){ |
78 |
|
d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); |
79 |
|
} |
80 |
|
/** clear/reset the function */ |
81 |
|
void clear() { d_tree.clear(); } |
82 |
|
/** setValue function |
83 |
|
* |
84 |
|
* For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false |
85 |
|
* |
86 |
|
*/ |
87 |
24582 |
void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){ |
88 |
24582 |
d_tree.setValue( m, n, v, d_index_order, ground, 0 ); |
89 |
24582 |
} |
90 |
|
/** setDefaultValue function */ |
91 |
5015 |
void setDefaultValue( TheoryModel* m, Node v ){ |
92 |
5015 |
d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); |
93 |
5015 |
} |
94 |
|
/** getFunctionValue |
95 |
|
* Returns a representation of this function. |
96 |
|
*/ |
97 |
|
Node getFunctionValue( std::vector< Node >& args, bool simplify = true ); |
98 |
|
/** getFunctionValue for args with set prefix */ |
99 |
|
Node getFunctionValue( const char* argPrefix, bool simplify = true ); |
100 |
|
/** update |
101 |
|
* This will update all values in the tree to be representatives in m. |
102 |
|
*/ |
103 |
|
void update( TheoryModel* m ){ d_tree.update( m ); } |
104 |
|
/** simplify the tree */ |
105 |
5015 |
void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } |
106 |
|
/** is this tree total? */ |
107 |
|
bool isTotal() { return d_tree.isTotal( d_op, 0 ); } |
108 |
|
/** is this tree empty? */ |
109 |
|
bool isEmpty() { return d_tree.isEmpty(); } |
110 |
|
public: |
111 |
|
void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){ |
112 |
|
d_tree.debugPrint( out, m, d_index_order, ind ); |
113 |
|
} |
114 |
|
}; |
115 |
|
|
116 |
|
} |
117 |
|
} |
118 |
|
} // namespace cvc5 |
119 |
|
|
120 |
|
#endif |