summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/apply_substs.cpp42
-rw-r--r--src/preprocessing/passes/ite_removal.cpp4
-rw-r--r--src/preprocessing/passes/ite_simp.cpp8
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp10
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp18
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp4
6 files changed, 27 insertions, 59 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 92f31b0b8..c93895e79 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -33,32 +33,28 @@ ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
PreprocessingPassResult ApplySubsts::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- if (!options::unsatCores())
- {
- Chat() << "applying substitutions..." << std::endl;
- Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
- << "applying substitutions" << std::endl;
- // TODO(#1255): Substitutions in incremental mode should be managed with a
- // proper data structure.
+ Chat() << "applying substitutions..." << std::endl;
+ Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+ << "applying substitutions" << std::endl;
+ // TODO(#1255): Substitutions in incremental mode should be managed with a
+ // proper data structure.
- theory::TrustSubstitutionMap& tlsm =
- d_preprocContext->getTopLevelSubstitutions();
- unsigned size = assertionsToPreprocess->size();
- for (unsigned i = 0; i < size; ++i)
+ theory::TrustSubstitutionMap& tlsm =
+ d_preprocContext->getTopLevelSubstitutions();
+ unsigned size = assertionsToPreprocess->size();
+ for (unsigned i = 0; i < size; ++i)
+ {
+ if (assertionsToPreprocess->isSubstsIndex(i))
{
- if (assertionsToPreprocess->isSubstsIndex(i))
- {
- continue;
- }
- Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
- << std::endl;
- d_preprocContext->spendResource(
- ResourceManager::Resource::PreprocessStep);
- assertionsToPreprocess->replaceTrusted(
- i, tlsm.apply((*assertionsToPreprocess)[i]));
- Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
- << std::endl;
+ continue;
}
+ Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
+ << std::endl;
+ d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+ assertionsToPreprocess->replaceTrusted(
+ i, tlsm.apply((*assertionsToPreprocess)[i]));
+ Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
+ << std::endl;
}
return PreprocessingPassResult::NO_CONFLICT;
}
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index d2f053379..91af2a5b8 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -50,7 +50,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
// process
assertions->replaceTrusted(i, trn);
// rewritten assertion has a dependence on the node (old pf architecture)
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
}
@@ -61,7 +61,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
imap[newSkolems[j]] = assertions->size();
assertions->pushBackTrusted(newAsserts[j]);
// new assertions have a dependence on the node (old pf architecture)
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
assertion);
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 5568dcad0..746bf33bd 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -114,13 +114,7 @@ ITESimp::Statistics::~Statistics()
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
- // This pass does not support dependency tracking yet
- // (learns substitutions from all assertions so just
- // adding addDependence is not enough)
- if (options::unsatCores())
- {
- return true;
- }
+ Assert(!options::unsatCores());
bool result = true;
bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
if (simpDidALotOfWork)
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 4ed2aede9..0bb386697 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -180,6 +180,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Assert(assertionsToPreprocess->getRealAssertionsEnd()
== assertionsToPreprocess->size());
Assert(!options::incrementalSolving());
+ Assert(!options::unsatCores());
context::Context fakeContext;
TheoryEngine* te = d_preprocContext->getTheoryEngine();
@@ -527,10 +528,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Node n = Rewriter::rewrite(geq.andNode(leq));
assertionsToPreprocess->push_back(n);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get();
Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
@@ -599,11 +596,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Debug("miplib") << " " << newAssertion << endl;
assertionsToPreprocess->push_back(newAssertion);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(newAssertion,
- Node::null());
- }
Debug("miplib") << " assertions to remove: " << endl;
for (vector<TNode>::const_iterator k = asserts[pos_var].begin(),
k_end = asserts[pos_var].end();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 7ace55c0a..656822299 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -66,7 +66,8 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
PreprocessingPassResult NonClausalSimp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- Assert(!options::unsatCores());
+ Assert(!options::unsatCores() || isProofEnabled())
+ << "Unsat cores with non-clausal simp only supported with new proofs";
d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
@@ -111,13 +112,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If in conflict, just return false
Trace("non-clausal-simplify")
<< "conflict in non-clausal propagation" << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
assertionsToPreprocess->pushBackTrusted(conf);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(conf.getNode(), Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -177,14 +173,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If the learned literal simplifies to false, we're in conflict
Trace("non-clausal-simplify")
<< "conflict with " << learned_literals[i].getNode() << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -216,14 +207,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If in conflict, we return false
Trace("non-clausal-simplify")
<< "conflict while solving " << learnedLiteral << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 604f8719c..028bfede5 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -80,7 +80,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
for( int i=0; i<(int)assertions.size(); i++ ){
Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
if( processAssertion( assertions[i] ) ){
- if (options::unsatCores()
+ if (options::unsatCores() && !options::proofNew()
&& std::find(macro_assertions.begin(),
macro_assertions.end(),
assertions[i])
@@ -106,7 +106,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
// is an over-approximation. a more fine-grained unsat core
// computation would require caching dependencies for each subterm of
// the formula, which is expensive.
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(curr, assertions[i]);
for (unsigned j = 0; j < macro_assertions.size(); j++)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback