/********************* */
-/*! \file bv_abstraction.cpp
+/*! \file theory_preprocess.cpp
** \verbatim
** Top contributors (to current version):
- ** Mathias Preiner
+ ** Mathias Preiner, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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
**
#include "preprocessing/passes/theory_preprocess.h"
-#include "preprocessing/preprocessing_pass_registry.h"
+#include "options/smt_options.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
: PreprocessingPass(preprocContext, "theory-preprocess"){};
PreprocessingPassResult TheoryPreprocess::applyInternal(
- AssertionPipeline* assertionsToPreprocess)
+ AssertionPipeline* assertions)
{
- TheoryEngine* te = d_preprocContext->getTheoryEngine();
- te->preprocessStart();
- for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+
+ IteSkolemMap& imap = assertions->getIteSkolemMap();
+ PropEngine* propEngine = d_preprocContext->getPropEngine();
+ // Remove all of the ITE occurrences and normalize
+ for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
- TNode a = (*assertionsToPreprocess)[i];
- Assert(Rewriter::rewrite(a) == a);
- assertionsToPreprocess->replace(i, te->preprocess(a));
- a = (*assertionsToPreprocess)[i];
- Assert(Rewriter::rewrite(a) == a);
+ Node assertion = (*assertions)[i];
+ std::vector<theory::TrustNode> newAsserts;
+ std::vector<Node> newSkolems;
+ TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
+ if (!trn.isNull())
+ {
+ // process
+ assertions->replaceTrusted(i, trn);
+ }
+ Assert(newSkolems.size() == newAsserts.size());
+ for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+ {
+ imap[newSkolems[j]] = assertions->size();
+ assertions->pushBackTrusted(newAsserts[j]);
+ // new assertions have a dependence on the node (old pf architecture)
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
+ assertion);
+ }
+ }
}
+
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<TheoryPreprocess> X("theory-preprocess");
} // namespace passes
} // namespace preprocessing