summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp56
1 files changed, 33 insertions, 23 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ce9ac3da7..982931d4a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -48,11 +48,11 @@
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
+#include "theory/theory_engine_proof_generator.h"
#include "theory/theory_model.h"
#include "theory/theory_traits.h"
#include "theory/uf/equality_engine.h"
#include "util/resource_manager.h"
-#include "theory/theory_engine_proof_generator.h"
using namespace std;
@@ -202,9 +202,13 @@ TheoryEngine::TheoryEngine(context::Context* context,
options::proofNew()
? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext)
: nullptr),
- d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
- d_sharedTerms(
- this, context, userContext, d_pNodeManager.get(), d_lazyProof!=nullptr),
+ d_tepg(
+ new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
+ d_sharedTerms(this,
+ context,
+ userContext,
+ d_pNodeManager.get(),
+ d_lazyProof != nullptr),
d_masterEqualityEngine(nullptr),
d_masterEENotify(*this),
d_quantEngine(nullptr),
@@ -1797,10 +1801,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
std::shared_ptr<LazyCDProof> lcp;
if (d_lazyProof != nullptr)
{
- Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node << std::endl;
+ Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node
+ << std::endl;
lcp.reset(new LazyCDProof(d_pNodeManager.get()));
}
-
+
AssertionPipeline additionalLemmas;
// Run theory preprocessing, maybe
@@ -1856,7 +1861,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
}
void TheoryEngine::processTrustNode(theory::TrustNode trn,
- theory::TheoryId from)
+ theory::TheoryId from)
{
if (d_lazyProof == nullptr)
{
@@ -1876,7 +1881,7 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn,
else
{
// all BUILTIN should be handled
- Assert (from!=THEORY_BUILTIN);
+ Assert(from != THEORY_BUILTIN);
// untrusted theory lemma
std::vector<Node> children;
std::vector<Node> args;
@@ -1936,11 +1941,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
// FIXME: have ~( F ) and E => F, prove ~( E )
- if (d_lazyProof!=nullptr)
+ if (d_lazyProof != nullptr)
{
-
}
-
Node fullConflict = tnc.getNode();
Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
@@ -2040,7 +2043,8 @@ theory::TrustNode TheoryEngine::getExplanation(
TrustNode simpleTrn;
if (d_lazyProof != nullptr)
{
- Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl;
+ Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion
+ << std::endl;
lcp.reset(new LazyCDProof(d_pNodeManager.get()));
}
unsigned i = 0; // Index of the current literal we are processing
@@ -2073,7 +2077,8 @@ theory::TrustNode TheoryEngine::getExplanation(
++ i;
if (lcp != nullptr)
{
- Trace("te-proof-exp") << "- explain " << toExplain.d_node << " trivially..." << std::endl;
+ Trace("te-proof-exp")
+ << "- explain " << toExplain.d_node << " trivially..." << std::endl;
// ------------------MACRO_SR_PRED_INTRO
// toExplain.d_node
std::vector<Node> children;
@@ -2111,7 +2116,8 @@ theory::TrustNode TheoryEngine::getExplanation(
}
if (lcp != nullptr)
{
- Trace("te-proof-exp") << "- AND expand " << toExplain.d_node << std::endl;
+ Trace("te-proof-exp")
+ << "- AND expand " << toExplain.d_node << std::endl;
// toExplain.d_node[0] ... toExplain.d_node[n]
// --------------------------------------------MACRO_SR_PRED_INTRO
// toExplain.d_node
@@ -2161,11 +2167,13 @@ theory::TrustNode TheoryEngine::getExplanation(
}
}
})
- if (lcp !=nullptr)
+ if (lcp != nullptr)
{
- if (!CDProof::isSame(toExplain.d_node,(*find).second.d_node))
+ if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
{
- Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl;
+ Trace("te-proof-exp")
+ << "- t-explained cached: " << toExplain.d_node << " by "
+ << (*find).second.d_node << std::endl;
// does this ever happen?
Assert(false);
simpleExplain = false;
@@ -2194,7 +2202,9 @@ theory::TrustNode TheoryEngine::getExplanation(
}
if (lcp != nullptr)
{
- Trace("te-proof-exp") << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node << " by " << texplanation.getNode() << std::endl;
+ Trace("te-proof-exp")
+ << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
+ << " by " << texplanation.getNode() << std::endl;
// if not a trivial explanation
if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
{
@@ -2203,7 +2213,7 @@ theory::TrustNode TheoryEngine::getExplanation(
// ---------------------------------MACRO_SR_PRED_TRANSFORM
// lit
Node proven = texplanation.getProven();
- if (texplanation.getGenerator()!=nullptr)
+ if (texplanation.getGenerator() != nullptr)
{
lcp->addLazyStep(proven, texplanation.getGenerator());
}
@@ -2217,7 +2227,7 @@ theory::TrustNode TheoryEngine::getExplanation(
unsigned tid = static_cast<unsigned>(toExplain.d_theory);
Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
args.push_back(tidn);
- lcp->addStep(proven,PfRule::THEORY_LEMMA,children,args);
+ lcp->addStep(proven, PfRule::THEORY_LEMMA, children, args);
}
std::vector<Node> children;
children.push_back(proven);
@@ -2320,12 +2330,12 @@ theory::TrustNode TheoryEngine::getExplanation(
{
// single call to a theory's explain method, skip the proof generator
Assert (!simpleTrn.isNull());
- Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl;
- return simpleTrn;
+ Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() <<
+ std::endl; return simpleTrn;
}
*/
// store in the proof generator
- TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp);
+ TrustNode trn = d_tepg->mkTrustExplain(conclusion, exp, lcp);
// return the trust node
return trn;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback