GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf_model.h Lines: 16 16 100.0 %
Date: 2021-03-22 Branches: 16 30 53.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf_model.h
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 Model for Theory UF
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY_UF_MODEL_H
18
#define CVC4__THEORY_UF_MODEL_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
class TheoryModel;
28
29
namespace uf {
30
31
98689
class UfModelTreeNode
32
{
33
public:
34
98689
  UfModelTreeNode(){}
35
  /** the data */
36
  std::map< Node, UfModelTreeNode > d_data;
37
  /** the value of this tree node (if all paths lead to same value) */
38
  Node d_value;
39
public:
40
  //is this model tree empty?
41
10181
  bool isEmpty() { return d_data.empty() && d_value.isNull(); }
42
  //clear
43
  void clear();
44
  /** setValue function */
45
  void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
46
  /** getFunctionValue */
47
  Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true );
48
  /** update function */
49
  void update( TheoryModel* m );
50
  /** simplify function */
51
  void simplify( Node op, Node defaultVal, int argIndex );
52
  /** is total ? */
53
  bool isTotal( Node op, int argIndex );
54
public:
55
  void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );
56
};
57
58
4785
class UfModelTree
59
{
60
private:
61
  //the op this model is for
62
  Node d_op;
63
  //the order we will treat the arguments
64
  std::vector< int > d_index_order;
65
  //the data
66
  UfModelTreeNode d_tree;
67
public:
68
  //constructors
69
  UfModelTree(){}
70
4785
  UfModelTree( Node op ) : d_op( op ){
71
9570
    TypeNode tn = d_op.getType();
72
42293
    for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){
73
37508
      d_index_order.push_back( i );
74
    }
75
4785
  }
76
  UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){
77
    d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
78
  }
79
  /** clear/reset the function */
80
  void clear() { d_tree.clear(); }
81
  /** setValue function
82
    *
83
    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false
84
    *
85
    */
86
23178
  void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){
87
23178
    d_tree.setValue( m, n, v, d_index_order, ground, 0 );
88
23178
  }
89
  /** setDefaultValue function */
90
4785
  void setDefaultValue( TheoryModel* m, Node v ){
91
4785
    d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
92
4785
  }
93
  /** getFunctionValue
94
    *   Returns a representation of this function.
95
    */
96
  Node getFunctionValue( std::vector< Node >& args, bool simplify = true );
97
  /** getFunctionValue for args with set prefix */
98
  Node getFunctionValue( const char* argPrefix, bool simplify = true );
99
  /** update
100
    *   This will update all values in the tree to be representatives in m.
101
    */
102
  void update( TheoryModel* m ){ d_tree.update( m ); }
103
  /** simplify the tree */
104
4785
  void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
105
  /** is this tree total? */
106
  bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
107
  /** is this tree empty? */
108
  bool isEmpty() { return d_tree.isEmpty(); }
109
public:
110
  void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){
111
    d_tree.debugPrint( out, m, d_index_order, ind );
112
  }
113
};
114
115
}
116
}
117
}
118
119
#endif