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