diff options
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 14 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 21 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 45 |
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() ){ |