GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_registry.cpp Lines: 33 39 84.6 %
Date: 2021-03-22 Branches: 51 126 40.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 term registry class
13
 **/
14
15
#include "theory/quantifiers/term_registry.h"
16
17
#include "options/quantifiers_options.h"
18
#include "options/smt_options.h"
19
#include "theory/quantifiers/quantifiers_state.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
8995
TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
26
8995
    : d_presolve(qs.getUserContext(), true),
27
8995
      d_presolveCache(qs.getUserContext()),
28
8995
      d_termEnum(new TermEnumeration),
29
8995
      d_termDb(new TermDb(qs, qr)),
30
44975
      d_sygusTdb(nullptr)
31
{
32
8995
  if (options::sygus() || options::sygusInst())
33
  {
34
    // must be constructed here since it is required for datatypes finistInit
35
2190
    d_sygusTdb.reset(new TermDbSygus(qs));
36
  }
37
8995
}
38
39
8995
void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
40
{
41
8995
  d_termDb->finishInit(qim);
42
8995
  if (d_sygusTdb.get())
43
  {
44
2190
    d_sygusTdb->finishInit(qim);
45
  }
46
8995
}
47
48
6438
void TermRegistry::presolve()
49
{
50
6438
  d_termDb->presolve();
51
6438
  d_presolve = false;
52
  // add all terms to database
53
6438
  if (options::incrementalSolving() && !options::termDbCd())
54
  {
55
    Trace("quant-engine-proc")
56
        << "Add presolve cache " << d_presolveCache.size() << std::endl;
57
    for (const Node& t : d_presolveCache)
58
    {
59
      addTerm(t);
60
    }
61
    Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
62
  }
63
6438
}
64
65
778703
void TermRegistry::addTerm(Node n, bool withinQuant)
66
{
67
  // don't add terms in quantifier bodies
68
813838
  if (withinQuant && !options::registerQuantBodyTerms())
69
  {
70
35135
    return;
71
  }
72
743568
  if (options::incrementalSolving() && !options::termDbCd())
73
  {
74
    d_presolveCache.insert(n);
75
  }
76
  // only wait if we are doing incremental solving
77
743568
  if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
78
  {
79
743568
    d_termDb->addTerm(n);
80
743568
    if (d_sygusTdb.get() && options::sygusEvalUnfold())
81
    {
82
297479
      d_sygusTdb->getEvalUnfold()->registerEvalTerm(n);
83
    }
84
  }
85
}
86
87
18055585
TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
88
89
30467
TermDbSygus* TermRegistry::getTermDatabaseSygus() const
90
{
91
30467
  return d_sygusTdb.get();
92
}
93
94
2153
TermEnumeration* TermRegistry::getTermEnumeration() const
95
{
96
2153
  return d_termEnum.get();
97
}
98
}  // namespace quantifiers
99
}  // namespace theory
100
61811
}  // namespace CVC4