summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/ite_simp.cpp3
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp14
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp21
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp45
4 files changed, 50 insertions, 33 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 9a6a8ec61..388c5742d 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -16,7 +16,6 @@
#include <vector>
-#include "options/proof_options.h"
#include "smt/smt_statistics_registry.h"
#include "smt_util/nary_builder.h"
#include "theory/arith/arith_ite_utils.h"
@@ -118,7 +117,7 @@ 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() || options::fewerPreprocessingHoles())
+ if (options::unsatCores())
{
return true;
}
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index f64fce118..3a8bbdb70 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -522,8 +522,10 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Node n = Rewriter::rewrite(geq.andNode(leq));
assertionsToPreprocess->push_back(n);
- PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
-
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(n, Node::null());
+ }
SubstitutionMap nullMap(&fakeContext);
Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
status = te->solve(geq, nullMap);
@@ -591,9 +593,11 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Debug("miplib") << " " << newAssertion << endl;
assertionsToPreprocess->push_back(newAssertion);
- PROOF(ProofManager::currentPM()->addDependence(newAssertion,
- Node::null()));
-
+ 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 6d2482a0e..24c1ac67b 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -19,7 +19,6 @@
#include <vector>
#include "context/cdo.h"
-#include "options/proof_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/theory_model.h"
@@ -54,7 +53,7 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
PreprocessingPassResult NonClausalSimp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
+ Assert(!options::unsatCores());
d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
@@ -98,11 +97,14 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If in conflict, just return false
Trace("non-clausal-simplify")
<< "conflict in non-clausal propagation" << std::endl;
- Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
+ Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n);
- PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(n, Node::null());
+ }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -164,7 +166,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n);
- PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(n, Node::null());
+ }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -207,7 +212,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n);
- PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(n, Node::null());
+ }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -241,7 +249,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// equations[0].second); assertionsToPreprocess->clear();
// Node n = NodeManager::currentNM()->mkConst<bool>(false);
// assertionsToPreprocess->push_back(n);
- // PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
// false); return;
// }
// top_level_substs.simplifyRHS(constantPropagations);
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index a4d8454a0..f4bc43542 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -19,7 +19,6 @@
#include <vector>
#include "options/quantifiers_options.h"
-#include "proof/proof_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/arith/arith_msum.h"
@@ -79,11 +78,14 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
for( int i=0; i<(int)assertions.size(); i++ ){
Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
if( processAssertion( assertions[i] ) ){
- PROOF(
- if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
- macro_assertions.push_back( assertions[i] );
- }
- );
+ if (options::unsatCores()
+ && std::find(macro_assertions.begin(),
+ macro_assertions.end(),
+ assertions[i])
+ == macro_assertions.end())
+ {
+ macro_assertions.push_back(assertions[i]);
+ }
//process this assertion again
i--;
}
@@ -98,17 +100,22 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
if( curr!=assertions[i] ){
curr = Rewriter::rewrite( curr );
Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
- //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
- //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula,
- // which is expensive.
- PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]);
- for (unsigned j = 0; j < macro_assertions.size(); j++) {
- if (macro_assertions[j] != assertions[i])
- {
- ProofManager::currentPM()->addDependence(
- curr, macro_assertions[j]);
- }
- });
+ // for now, it is dependent upon all assertions involving macros, this
+ // 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())
+ {
+ ProofManager::currentPM()->addDependence(curr, assertions[i]);
+ for (unsigned j = 0; j < macro_assertions.size(); j++)
+ {
+ if (macro_assertions[j] != assertions[i])
+ {
+ ProofManager::currentPM()->addDependence(curr,
+ macro_assertions[j]);
+ }
+ }
+ }
assertions[i] = curr;
retVal = true;
}
@@ -432,9 +439,9 @@ Node QuantifierMacros::simplify( Node n ){
for( unsigned i=0; i<children.size(); i++ ){
Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
if( etc.isNull() ){
- //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op,
+ // if this does fail, we are incomplete, since we are eliminating
+ // quantified formula corresponding to op,
// and not ensuring it applies to n when its types are correct.
- //Assert( false );
success = false;
break;
}else if( !etc.isConst() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback