/*! \file combination_care_graph.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Dejan Jovanovic
** 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.
+ ** 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
**
#include "theory/combination_care_graph.h"
#include "expr/node_visitor.h"
+#include "prop/prop_engine.h"
#include "theory/care_graph.h"
#include "theory/theory_engine.h"
namespace theory {
CombinationCareGraph::CombinationCareGraph(
- TheoryEngine& te, const std::vector<Theory*>& paraTheories)
- : CombinationEngine(te, paraTheories)
+ TheoryEngine& te,
+ const std::vector<Theory*>& paraTheories,
+ ProofNodeManager* pnm)
+ : CombinationEngine(te, paraTheories, pnm)
{
}
Debug("combineTheories")
<< "TheoryEngine::combineTheories(): requesting a split " << std::endl;
- Node split = equality.orNode(equality.notNode());
- sendLemma(split, carePair.d_theory);
+ 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);
// 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);
+ Node e = d_valuation.ensureLiteral(equality);
propEngine->requirePhase(e, true);
}
}