GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/combination_care_graph.cpp Lines: 33 33 100.0 %
Date: 2021-03-22 Branches: 48 92 52.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file combination_care_graph.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic
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 Management of a care graph based approach for theory combination.
13
 **/
14
15
#include "theory/combination_care_graph.h"
16
17
#include "expr/node_visitor.h"
18
#include "prop/prop_engine.h"
19
#include "theory/care_graph.h"
20
#include "theory/model_manager.h"
21
#include "theory/theory_engine.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
8995
CombinationCareGraph::CombinationCareGraph(
27
    TheoryEngine& te,
28
    const std::vector<Theory*>& paraTheories,
29
8995
    ProofNodeManager* pnm)
30
8995
    : CombinationEngine(te, paraTheories, pnm)
31
{
32
8995
}
33
34
17984
CombinationCareGraph::~CombinationCareGraph() {}
35
36
29477
void CombinationCareGraph::combineTheories()
37
{
38
29477
  Trace("combineTheories") << "TheoryEngine::combineTheories()" << std::endl;
39
40
  // Care graph we'll be building
41
58954
  CareGraph careGraph;
42
43
  // get the care graph from the parametric theories
44
104125
  for (Theory* t : d_paraTheories)
45
  {
46
74648
    t->getCareGraph(&careGraph);
47
  }
48
49
58954
  Trace("combineTheories")
50
29477
      << "TheoryEngine::combineTheories(): care graph size = "
51
29477
      << careGraph.size() << std::endl;
52
53
  // Now add splitters for the ones we are interested in
54
29477
  prop::PropEngine* propEngine = d_te.getPropEngine();
55
83138
  for (const CarePair& carePair : careGraph)
56
  {
57
107322
    Debug("combineTheories")
58
53661
        << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
59
53661
        << carePair.d_b << " from " << carePair.d_theory << std::endl;
60
61
    // The equality in question (order for no repetition)
62
107322
    Node equality = carePair.d_a.eqNode(carePair.d_b);
63
64
    // We need to split on it
65
107322
    Debug("combineTheories")
66
53661
        << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
67
68
107322
    TrustNode tsplit;
69
53661
    if (isProofEnabled())
70
    {
71
      // make proof of splitting lemma
72
9890
      tsplit = d_cmbsPg->mkTrustNodeSplit(equality);
73
    }
74
    else
75
    {
76
87542
      Node split = equality.orNode(equality.notNode());
77
43771
      tsplit = TrustNode::mkTrustLemma(split, nullptr);
78
    }
79
53661
    sendLemma(tsplit, carePair.d_theory);
80
81
    // Could check the equality status here:
82
    //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
83
    // and only require true phase below if:
84
    //   es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL
85
    // and require false phase below if:
86
    //   es == EQUALITY_FALSE_IN_MODEL
87
    // This is supposed to force preference to follow what the theory models
88
    // already have but it doesn't seem to make a big difference - need to
89
    // explore more -Clark
90
107322
    Node e = d_valuation.ensureLiteral(equality);
91
53661
    propEngine->requirePhase(e, true);
92
  }
93
29477
}
94
95
33022
bool CombinationCareGraph::buildModel()
96
{
97
  // building the model happens as a separate step
98
33022
  return d_mmanager->buildModel();
99
}
100
101
}  // namespace theory
102
26676
}  // namespace CVC4