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

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registry.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed
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 state object
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__SETS__TERM_REGISTRY_H
18
#define CVC4__THEORY__SETS__TERM_REGISTRY_H
19
20
#include <map>
21
#include <vector>
22
23
#include "context/cdhashmap.h"
24
#include "theory/sets/inference_manager.h"
25
#include "theory/sets/skolem_cache.h"
26
#include "theory/sets/solver_state.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace sets {
31
32
/**
33
 * Term registry, the purpose of this class is to maintain a database of
34
 * commonly used terms, and mappings from sets to their "proxy variables".
35
 */
36
8992
class TermRegistry
37
{
38
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
39
40
 public:
41
  TermRegistry(SolverState& state, InferenceManager& im, SkolemCache& skc);
42
  /** Get type constraint skolem
43
   *
44
   * The sets theory solver outputs equality lemmas of the form:
45
   *   n = d_tc_skolem[n][tn]
46
   * where the type of d_tc_skolem[n][tn] is tn, and the type
47
   * of n is not a subtype of tn. This is required to handle benchmarks like
48
   *   test/regress/regress0/sets/sets-of-sets-subtypes.smt2
49
   * where for s : (Set Int) and t : (Set Real), we have that
50
   *   ( s = t ^ y in t ) implies ( exists k : Int. y = k )
51
   * The type constraint Skolem for (y, Int) is the skolemization of k above.
52
   */
53
  Node getTypeConstraintSkolem(Node n, TypeNode tn);
54
  /** get the proxy variable for set n
55
   *
56
   * Proxy variables are used to communicate information that otherwise would
57
   * not be possible due to rewriting. For example, the literal
58
   *   card( singleton( 0 ) ) = 1
59
   * is rewritten to true. Instead, to communicate this fact (e.g. to other
60
   * theories), we require introducing a proxy variable x for singleton( 0 ).
61
   * Then:
62
   *   card( x ) = 1 ^ x = singleton( 0 )
63
   * communicates the equivalent of the above literal.
64
   */
65
  Node getProxy(Node n);
66
  /** Get the empty set of type tn */
67
  Node getEmptySet(TypeNode tn);
68
  /** Get the universe set of type tn if it exists or create a new one */
69
  Node getUnivSet(TypeNode tn);
70
  /** debug print set */
71
  void debugPrintSet(Node s, const char* c) const;
72
73
 private:
74
  /** The inference manager */
75
  InferenceManager& d_im;
76
  /** Reference to the skolem cache */
77
  SkolemCache& d_skCache;
78
  /** Map from set terms to their proxy variables */
79
  NodeMap d_proxy;
80
  /** Backwards map of above */
81
  NodeMap d_proxy_to_term;
82
  /** Cache of type constraint skolems (see getTypeConstraintSkolem) */
83
  std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
84
  /** Map from types to empty set of that type */
85
  std::map<TypeNode, Node> d_emptyset;
86
  /** Map from types to universe set of that type */
87
  std::map<TypeNode, Node> d_univset;
88
}; /* class TheorySetsPrivate */
89
90
}  // namespace sets
91
}  // namespace theory
92
}  // namespace CVC4
93
94
#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */