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

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