GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_registry.h Lines: 1 1 100.0 %
Date: 2021-03-23 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
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 term registry class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
18
#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
19
20
#include <map>
21
#include <unordered_set>
22
23
#include "context/cdhashset.h"
24
#include "theory/quantifiers/sygus/term_database_sygus.h"
25
#include "theory/quantifiers/term_database.h"
26
#include "theory/quantifiers/term_enumeration.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
/**
33
 * Term Registry, which manages notifying modules within quantifiers about
34
 * (ground) terms that exist in the current context.
35
 */
36
8994
class TermRegistry
37
{
38
  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
39
40
 public:
41
  TermRegistry(QuantifiersState& qs,
42
               QuantifiersRegistry& qr);
43
  /** Finish init, which sets the inference manager on modules of this class */
44
  void finishInit(QuantifiersInferenceManager* qim);
45
  /** Presolve */
46
  void presolve();
47
48
  /**
49
   * Add term n, which notifies the term database that the ground term n
50
   * exists in the current context.
51
   *
52
   * @param n the term to add
53
   * @param withinQuant whether n occurs within a quantified formula body
54
   */
55
  void addTerm(Node n, bool withinQuant = false);
56
57
  /** get term database */
58
  TermDb* getTermDatabase() const;
59
  /** get term database sygus */
60
  TermDbSygus* getTermDatabaseSygus() const;
61
  /** get term enumeration utility */
62
  TermEnumeration* getTermEnumeration() const;
63
64
 private:
65
  /** has presolve been called */
66
  context::CDO<bool> d_presolve;
67
  /** the set of terms we have seen before presolve */
68
  NodeSet d_presolveCache;
69
  /** term enumeration utility */
70
  std::unique_ptr<TermEnumeration> d_termEnum;
71
  /** term database */
72
  std::unique_ptr<TermDb> d_termDb;
73
  /** sygus term database */
74
  std::unique_ptr<TermDbSygus> d_sygusTdb;
75
};
76
77
}  // namespace quantifiers
78
}  // namespace theory
79
}  // namespace CVC4
80
81
#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */