GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf_model.cpp Lines: 74 128 57.8 %
Date: 2021-03-23 Branches: 142 442 32.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf_model.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of Theory UF Model
13
 **/
14
15
#include "theory/uf/theory_uf_model.h"
16
17
#include <stack>
18
19
#include "expr/attribute.h"
20
#include "theory/quantifiers/first_order_model.h"
21
#include "theory/rewriter.h"
22
#include "theory/theory_model.h"
23
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace uf {
29
30
//clear
31
void UfModelTreeNode::clear(){
32
  d_data.clear();
33
  d_value = Node::null();
34
}
35
36
//set value function
37
138694
void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
38
138694
  if( d_data.empty() ){
39
    //overwrite value if either at leaf or this is a fresh tree
40
107974
    d_value = v;
41
30720
  }else if( !d_value.isNull() && d_value!=v ){
42
    //value is no longer constant
43
2508
    d_value = Node::null();
44
  }
45
138694
  if( argIndex<(int)indexOrder.size() ){
46
    //take r = null when argument is the model basis
47
221462
    Node r;
48
110731
    if (ground
49
183954
        || (!n.isNull()
50
110731
            && !quantifiers::FirstOrderModel::isModelBasis(
51
                   n[indexOrder[argIndex]])))
52
    {
53
73223
      r = m->getRepresentative( n[ indexOrder[argIndex] ] );
54
    }
55
110731
    d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
56
  }
57
138694
}
58
59
52474
Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
60
52474
  if(!d_data.empty()) {
61
83204
    Node defaultValue = argDefaultValue;
62
41602
    if(d_data.find(Node::null()) != d_data.end()) {
63
37508
      defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
64
    }
65
66
83204
    std::vector<Node> caseArgs;
67
83204
    std::map<Node, Node> caseValues;
68
69
89291
    for (std::pair<const Node, UfModelTreeNode>& p : d_data)
70
    {
71
47689
      if (!p.first.isNull())
72
      {
73
        Node val =
74
20362
            p.second.getFunctionValue(args, index + 1, defaultValue, simplify);
75
10181
        caseArgs.push_back(p.first);
76
10181
        caseValues[p.first] = val;
77
      }
78
    }
79
80
41602
    NodeManager* nm = NodeManager::currentNM();
81
83204
    Node retNode = defaultValue;
82
83
41602
    if(!simplify) {
84
      // "non-simplifying" mode - expand function values to things like:
85
      //   IF      (x=0 AND y=0 AND z=0) THEN value1
86
      //   ELSE IF (x=0 AND y=0 AND z=1) THEN value2
87
      //   [...etc...]
88
      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
89
        Node val = caseValues[ caseArgs[ i ] ];
90
        if(val.getKind() == ITE) {
91
          // use a stack to reverse the order, since we're traversing outside-in
92
          std::stack<TNode> stk;
93
          do {
94
            stk.push(val);
95
            val = val[2];
96
          } while(val.getKind() == ITE);
97
          AlwaysAssert(val == defaultValue)
98
              << "default values don't match when constructing function "
99
                 "definition!";
100
          while(!stk.empty()) {
101
            val = stk.top();
102
            stk.pop();
103
            retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
104
          }
105
        } else {
106
          retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
107
        }
108
      }
109
    } else {
110
      // "simplifying" mode - condense function values
111
51783
      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
112
10181
        retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
113
      }
114
    }
115
41602
    return retNode;
116
  } else {
117
10872
    Assert(!d_value.isNull());
118
10872
    return d_value;
119
  }
120
}
121
122
//update function
123
void UfModelTreeNode::update( TheoryModel* m ){
124
  if( !d_value.isNull() ){
125
    d_value = m->getRepresentative( d_value );
126
  }
127
  std::map< Node, UfModelTreeNode > old = d_data;
128
  d_data.clear();
129
  for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){
130
    Node rep = m->getRepresentative( it->first );
131
    d_data[ rep ] = it->second;
132
    d_data[ rep ].update( m );
133
  }
134
}
135
136
//simplify function
137
52474
void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
138
52474
  if( argIndex<(int)op.getType().getNumChildren()-1 ){
139
83204
    std::vector< Node > eraseData;
140
    //first process the default argument
141
83204
    Node r;
142
41602
    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
143
41602
    if( it!=d_data.end() ){
144
37508
      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
145
        eraseData.push_back( r );
146
      }else{
147
37508
        it->second.simplify( op, defaultVal, argIndex+1 );
148
37508
        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
149
37508
          defaultVal = it->second.d_value;
150
        }else{
151
          defaultVal = Node::null();
152
          if( it->second.isEmpty() ){
153
            eraseData.push_back( r );
154
          }
155
        }
156
      }
157
    }
158
    //now see if any children can be removed, and simplify the ones that cannot
159
96296
    for (auto& kv : d_data)
160
    {
161
54694
      if (!kv.first.isNull())
162
      {
163
17186
        if (!defaultVal.isNull() && kv.second.d_value == defaultVal)
164
        {
165
7005
          eraseData.push_back(kv.first);
166
        }
167
        else
168
        {
169
10181
          kv.second.simplify(op, defaultVal, argIndex + 1);
170
10181
          if (kv.second.isEmpty())
171
          {
172
            eraseData.push_back(kv.first);
173
          }
174
        }
175
      }
176
    }
177
48607
    for( int i=0; i<(int)eraseData.size(); i++ ){
178
7005
      d_data.erase( eraseData[i] );
179
    }
180
  }
181
52474
}
182
183
//is total function
184
2884553
bool UfModelTreeNode::isTotal( Node op, int argIndex ){
185
2884553
  if( argIndex==(int)(op.getType().getNumChildren()-1) ){
186
37508
    return !d_value.isNull();
187
  }else{
188
5694090
    Node r;
189
2847045
    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
190
2847045
    if( it!=d_data.end() ){
191
2847045
      return it->second.isTotal( op, argIndex+1 );
192
    }else{
193
      return false;
194
    }
195
  }
196
}
197
198
void indent( std::ostream& out, int ind ){
199
  for( int i=0; i<ind; i++ ){
200
    out << " ";
201
  }
202
}
203
204
void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
205
  if( !d_data.empty() ){
206
    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
207
      if( !it->first.isNull() ){
208
        indent( out, ind );
209
        out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
210
        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
211
      }
212
    }
213
    if( d_data.find( Node::null() )!=d_data.end() ){
214
      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
215
    }
216
  }else{
217
    indent( out, ind );
218
    out << "return ";
219
    out << m->getRepresentative(d_value);
220
    out << std::endl;
221
  }
222
}
223
224
4785
Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
225
9570
  Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
226
4785
  if(simplify) {
227
4785
    body = Rewriter::rewrite( body );
228
  }
229
9570
  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
230
9570
  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
231
}
232
233
4785
Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
234
9570
  TypeNode type = d_op.getType();
235
9570
  std::vector< Node > vars;
236
42293
  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
237
75016
    std::stringstream ss;
238
37508
    ss << argPrefix << (i+1);
239
37508
    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
240
  }
241
9570
  return getFunctionValue( vars, simplify );
242
}
243
244
}  // namespace uf
245
}  // namespace theory
246
26685
}  // namespace CVC4