1 /********************* */
2 /*! \file combination_care_graph.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Management of a care graph based approach for theory combination.
15 #include "theory/combination_care_graph.h"
17 #include "expr/node_visitor.h"
18 #include "theory/care_graph.h"
19 #include "theory/theory_engine.h"
24 CombinationCareGraph::CombinationCareGraph(
26 const std::vector
<Theory
*>& paraTheories
,
27 ProofNodeManager
* pnm
)
28 : CombinationEngine(te
, paraTheories
, pnm
)
32 CombinationCareGraph::~CombinationCareGraph() {}
34 void CombinationCareGraph::combineTheories()
36 Trace("combineTheories") << "TheoryEngine::combineTheories()" << std::endl
;
38 // Care graph we'll be building
41 // get the care graph from the parametric theories
42 for (Theory
* t
: d_paraTheories
)
44 t
->getCareGraph(&careGraph
);
47 Trace("combineTheories")
48 << "TheoryEngine::combineTheories(): care graph size = "
49 << careGraph
.size() << std::endl
;
51 // Now add splitters for the ones we are interested in
52 prop::PropEngine
* propEngine
= d_te
.getPropEngine();
53 for (const CarePair
& carePair
: careGraph
)
55 Debug("combineTheories")
56 << "TheoryEngine::combineTheories(): checking " << carePair
.d_a
<< " = "
57 << carePair
.d_b
<< " from " << carePair
.d_theory
<< std::endl
;
59 // The equality in question (order for no repetition)
60 Node equality
= carePair
.d_a
.eqNode(carePair
.d_b
);
62 // We need to split on it
63 Debug("combineTheories")
64 << "TheoryEngine::combineTheories(): requesting a split " << std::endl
;
69 // make proof of splitting lemma
70 tsplit
= d_cmbsPg
->mkTrustNodeSplit(equality
);
74 Node split
= equality
.orNode(equality
.notNode());
75 tsplit
= TrustNode::mkTrustLemma(split
, nullptr);
77 sendLemma(tsplit
, carePair
.d_theory
);
79 // Could check the equality status here:
80 // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
81 // and only require true phase below if:
82 // es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL
83 // and require false phase below if:
84 // es == EQUALITY_FALSE_IN_MODEL
85 // This is supposed to force preference to follow what the theory models
86 // already have but it doesn't seem to make a big difference - need to
87 // explore more -Clark
88 Node e
= d_te
.ensureLiteral(equality
);
89 propEngine
->requirePhase(e
, true);
93 bool CombinationCareGraph::buildModel()
95 // building the model happens as a separate step
96 return d_mmanager
->buildModel();