GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/shared_solver.cpp Lines: 29 43 67.4 %
Date: 2021-03-23 Branches: 45 100 45.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file shared_solver.cpp
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 The shared solver base class
13
 **/
14
15
#include "theory/shared_solver.h"
16
17
#include "expr/node_visitor.h"
18
#include "theory/ee_setup_info.h"
19
#include "theory/logic_info.h"
20
#include "theory/theory_engine.h"
21
22
namespace CVC4 {
23
namespace theory {
24
25
// Always creates shared terms database. In all cases, shared terms
26
// database is used as a way of tracking which calls to Theory::addSharedTerm
27
// we need to make in preNotifySharedFact.
28
// In distributed equality engine management, shared terms database also
29
// maintains an equality engine. In central equality engine management,
30
// it does not.
31
8997
SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
32
    : d_te(te),
33
8997
      d_logicInfo(te.getLogicInfo()),
34
26991
      d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
35
8997
      d_preRegistrationVisitor(&te, d_te.getSatContext()),
36
53982
      d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext())
37
{
38
8997
}
39
40
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi)
41
{
42
  return false;
43
}
44
45
839458
void SharedSolver::preRegister(TNode atom)
46
{
47
839458
  Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl;
48
  // This method uses two different implementations for preregistering terms,
49
  // which depends on whether sharing is enabled.
50
  // If sharing is disabled, we use PreRegisterVisitor, which keeps a global
51
  // SAT-context dependent cache of terms visited.
52
  // If sharing is disabled, we use SharedTermsVisitor which does *not* keep a
53
  // global cache. This is because shared terms must be associated with the
54
  // given atom, and thus it must traverse the set of subterms in each atom.
55
  // See term_registration_visitor.h for more details.
56
839458
  if (d_logicInfo.isSharingEnabled())
57
  {
58
    // register it with the shared terms database if sharing is enabled
59
714601
    preRegisterSharedInternal(atom);
60
    // Collect the shared terms in atom, as well as calling preregister on the
61
    // appropriate theories in atom.
62
    // This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly
63
    // multiple times.
64
714604
    NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom);
65
  }
66
  else
67
  {
68
    // just use the normal preregister visitor, which calls
69
    // Theory::preRegisterTerm possibly multiple times.
70
124858
    NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom);
71
  }
72
839454
  Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl;
73
839454
}
74
75
8708781
void SharedSolver::preNotifySharedFact(TNode atom)
76
{
77
8708781
  if (d_sharedTerms.hasSharedTerms(atom))
78
  {
79
    // Always notify the theories of the shared terms, which is independent of
80
    // the architecture currently.
81
6171688
    SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
82
6171688
    SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
83
36531076
    for (; it != it_end; ++it)
84
    {
85
30359388
      TNode term = *it;
86
15179694
      TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term);
87
212515716
      for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
88
      {
89
197336022
        if (TheoryIdSetUtil::setContains(id, theories))
90
        {
91
2161964
          Theory* t = d_te.theoryOf(id);
92
          // call the add shared term method
93
2161964
          t->addSharedTerm(term);
94
        }
95
      }
96
15179694
      d_sharedTerms.markNotified(term, theories);
97
    }
98
  }
99
8708781
}
100
101
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b)
102
{
103
  return EQUALITY_UNKNOWN;
104
}
105
106
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
107
{
108
  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
109
}
110
111
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
112
                                           TNode a,
113
                                           TNode b,
114
                                           bool value)
115
{
116
  // Propagate equality between shared terms to the one who asked for it
117
  Node equality = a.eqNode(b);
118
  if (value)
119
  {
120
    d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN);
121
  }
122
  else
123
  {
124
    d_te.assertToTheory(
125
        equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
126
  }
127
  return true;
128
}
129
130
7095
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
131
132
}  // namespace theory
133
26685
}  // namespace CVC4