GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_rels.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_rels.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, Tim King
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 Sets theory implementation.
13
 **
14
 ** Extension to Sets theory.
15
 **/
16
17
#ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_
18
#define SRC_THEORY_SETS_THEORY_SETS_RELS_H_
19
20
#include <unordered_set>
21
22
#include "context/cdhashset.h"
23
#include "context/cdlist.h"
24
#include "theory/sets/inference_manager.h"
25
#include "theory/sets/rels_utils.h"
26
#include "theory/sets/solver_state.h"
27
#include "theory/sets/term_registry.h"
28
#include "theory/theory.h"
29
#include "theory/uf/equality_engine.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace sets {
34
35
class TheorySetsPrivate;
36
37
48164
class TupleTrie {
38
public:
39
  /** the data */
40
  std::map< Node, TupleTrie > d_data;
41
public:
42
  std::vector<Node> findTerms( std::vector< Node >& reps, int argIndex = 0 );
43
  std::vector<Node> findSuccessors( std::vector< Node >& reps, int argIndex = 0 );
44
  Node existsTerm( std::vector< Node >& reps, int argIndex = 0 );
45
  bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 );
46
  void debugPrint( const char * c, Node n, unsigned depth = 0 );
47
8612
  void clear() { d_data.clear(); }
48
};/* class TupleTrie */
49
50
/** The relations extension of the theory of sets
51
 *
52
 * This class implements inference schemes described in Meng et al. CADE 2017
53
 * for handling quantifier-free constraints in the theory of relations.
54
 *
55
 * In CVC4, relations are represented as sets of tuples. The theory of
56
 * relations includes constraints over operators, e.g. TRANSPOSE, JOIN and so
57
 * on, which apply to sets of tuples.
58
 *
59
 * Since relations are a special case of sets, this class is implemented as an
60
 * extension of the theory of sets. That is, it shares many components of the
61
 * TheorySets object which owns it.
62
 */
63
class TheorySetsRels {
64
  typedef context::CDList<Node> NodeList;
65
  typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
66
  typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
67
68
public:
69
 TheorySetsRels(SolverState& s,
70
                InferenceManager& im,
71
                SkolemCache& skc,
72
                TermRegistry& treg);
73
74
 ~TheorySetsRels();
75
 /**
76
  * Invoke the check method with effort level e. At a high level, this class
77
  * will make calls to TheorySetsPrivate::processInference to assert facts,
78
  * lemmas, and conflicts. If this class makes no such call, then the current
79
  * set of assertions is satisfiable with respect to relations.
80
  */
81
 void check(Theory::Effort e);
82
 /** Is kind k a kind that belongs to the relation theory? */
83
 static bool isRelationKind(Kind k);
84
85
private:
86
  /** True and false constant nodes */
87
  Node                          d_trueNode;
88
  Node                          d_falseNode;
89
90
  /** Reference to the state object for the theory of sets */
91
  SolverState& d_state;
92
  /** Reference to the inference manager for the theory of sets */
93
  InferenceManager& d_im;
94
  /** Reference to the skolem cache */
95
  SkolemCache& d_skCache;
96
  /** Reference to the term registry */
97
  TermRegistry& d_treg;
98
  /** A list of pending inferences to process */
99
  std::vector<Node> d_pending;
100
  NodeSet                       d_shared_terms;
101
102
103
  std::unordered_set< Node, NodeHashFunction >       d_rel_nodes;
104
  std::map< Node, std::vector<Node> >           d_tuple_reps;
105
  std::map< Node, TupleTrie >                   d_membership_trie;
106
107
  /** Symbolic tuple variables that has been reduced to concrete ones */
108
  std::unordered_set< Node, NodeHashFunction >       d_symbolic_tuples;
109
110
  /** Mapping between relation and its member representatives */
111
  std::map< Node, std::vector< Node > >           d_rReps_memberReps_cache;
112
113
  /** Mapping between relation and its member representatives explanation */
114
  std::map< Node, std::vector< Node > >           d_rReps_memberReps_exp_cache;
115
116
  /** Mapping between a relation representative and its equivalent relations involving relational operators */
117
  std::map< Node, std::map<kind::Kind_t, std::vector<Node> > >                  d_terms_cache;
118
119
  /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
120
  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
121
  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
122
  std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
123
124
 private:
125
  /** Send infer
126
   *
127
   * Called when we have inferred fact from explanation reason, where the
128
   * latter should be a conjunction of facts that hold in the current context.
129
   *
130
   * This method adds the node (=> reason exp) to the pending vector d_pending.
131
   */
132
  void sendInfer(Node fact, InferenceId id, Node reason);
133
  /**
134
   * This method flushes the inferences in the pending vector d_pending to
135
   * theory of sets, which may process them as lemmas or as facts to assert to
136
   * the equality engine.
137
   */
138
  void doPendingInfers();
139
  /** Process inference
140
   *
141
   * A wrapper around d_im.assertInference that ensures that we do not send
142
   * inferences with explanations that are not entailed.
143
   */
144
  void processInference(Node conc, InferenceId id, Node exp);
145
146
  /** Methods used in full effort */
147
  void check();
148
  void collectRelsInfo();
149
  void applyTransposeRule( std::vector<Node> tp_terms );
150
  void applyTransposeRule( Node rel, Node rel_rep, Node exp );
151
  void applyProductRule( Node rel, Node rel_rep, Node exp );
152
  void applyJoinRule( Node rel, Node rel_rep, Node exp);
153
  void applyJoinImageRule( Node mem_rep, Node rel_rep, Node exp);
154
  void applyIdenRule( Node mem_rep, Node rel_rep, Node exp);
155
  void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
156
  void buildTCGraphForRel( Node tc_rel );
157
  void doTCInference();
158
  void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
159
  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
160
                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
161
162
  void composeMembersForRels( Node );
163
  void computeMembersForBinOpRel( Node );
164
  void computeMembersForIdenTerm( Node );
165
  void computeMembersForUnaryOpRel( Node );
166
  void computeMembersForJoinImageTerm( Node );
167
168
  bool isTCReachable( Node mem_rep, Node tc_rel );
169
  void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
170
                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
171
172
  /** Helper functions */
173
  bool hasTerm( Node a );
174
  void makeSharedTerm(Node, TypeNode t);
175
  void reduceTupleVar( Node );
176
  bool hasMember( Node, Node );
177
  void computeTupleReps( Node );
178
  bool areEqual( Node a, Node b );
179
  Node getRepresentative( Node t );
180
  inline void addToMembershipDB( Node, Node, Node  );
181
  inline Node constructPair(Node tc_rep, Node a, Node b);
182
  bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );
183
  bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
184
};
185
186
187
}/* CVC4::theory::sets namespace */
188
}/* CVC4::theory namespace */
189
}/* CVC4 namespace */
190
191
192
193
#endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */