diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 20 | ||||
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 16 | ||||
-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 |
6 files changed, 70 insertions, 49 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index a6b9531b6..a9e2d4d36 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -16,7 +16,7 @@ #include "preprocessing/assertion_pipeline.h" #include "expr/node_manager.h" -#include "proof/proof.h" +#include "options/smt_options.h" #include "proof/proof_manager.h" #include "theory/rewriter.h" @@ -77,7 +77,10 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) { - PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(n, d_nodes[i]); + } if (isProofEnabled()) { d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); @@ -96,11 +99,14 @@ void AssertionPipeline::replace(size_t i, const std::vector<Node>& addnDeps, ProofGenerator* pgen) { - PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]); - for (const auto& addnDep - : addnDeps) { - ProofManager::currentPM()->addDependence(n, addnDep); - }); + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(n, d_nodes[i]); + for (const auto& addnDep : addnDeps) + { + ProofManager::currentPM()->addDependence(n, addnDep); + } + } if (isProofEnabled()) { d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 31c92a09f..ab9c2482b 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -70,11 +70,14 @@ void addLemmaForPair(TNode args1, } else { - Assert(args1.getKind() == kind::SELECT && args1[0] == func); - Assert(args2.getKind() == kind::SELECT && args2[0] == func); + Assert(args1.getKind() == kind::SELECT && args1.getOperator() == func); + Assert(args2.getKind() == kind::SELECT && args2.getOperator() == func); Assert(args1.getNumChildren() == 2); Assert(args2.getNumChildren() == 2); - args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]); + args_eq = nm->mkNode(Kind::AND, + nm->mkNode(kind::EQUAL, args1[0], args2[0]), + nm->mkNode(kind::EQUAL, args1[1], args2[1]) + ); } Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); @@ -153,7 +156,7 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, if (seen.find(term) == seen.end()) { TNode func; - if (term.getKind() == kind::APPLY_UF) + if (term.getKind() == kind::APPLY_UF || term.getKind() == kind::SELECT) { storeFunctionAndAddLemmas(term.getOperator(), term, @@ -163,11 +166,6 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, nm, vec); } - else if (term.getKind() == kind::SELECT) - { - storeFunctionAndAddLemmas( - term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec); - } else { AlwaysAssert(term.getKind() != kind::STORE) 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() ){ |