diff options
| -rw-r--r-- | src/preproc/preprocessing_pass.h | 22 | ||||
| -rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 373 | ||||
| -rw-r--r-- | src/preproc/preprocessing_passes_core.h | 77 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 81 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 10 |
5 files changed, 327 insertions, 236 deletions
diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h index 5c9561c0a..d956993aa 100644 --- a/src/preproc/preprocessing_pass.h +++ b/src/preproc/preprocessing_pass.h @@ -14,6 +14,20 @@ namespace CVC4 { namespace preproc { + +/** Useful for counting the number of recursive calls. */ +class ScopeCounter { +private: + unsigned& d_depth; +public: + ScopeCounter(unsigned& d) : d_depth(d) { + ++d_depth; + } + ~ScopeCounter(){ + --d_depth; + } +}; + class AssertionPipeline { std::vector<Node> d_nodes; @@ -37,9 +51,15 @@ public: } };// class AssertionPipeline +struct PreprocessingPassResult { + bool d_noConflict; + PreprocessingPassResult(bool noConflict) : d_noConflict(noConflict){ +} +}; + class PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess) = 0; + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) = 0; void dumpAssertions(const char* key, const AssertionPipeline& assertionList) { if( Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key) ) { diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp index d92d2df18..c43d80979 100644 --- a/src/preproc/preprocessing_passes_core.cpp +++ b/src/preproc/preprocessing_passes_core.cpp @@ -18,11 +18,25 @@ namespace CVC4 { namespace preproc { +ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_definitionExpansionTime(definitionExpansionTime){ +} + +PreprocessingPassResult ExpandingDefinitionsPass::apply(AssertionPipeline* assertionsToPreprocess){ +/* Chat() << "expanding definitions..." << std::endl; + Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; + TimerStat::CodeTimer codeTimer(d_definitionExpansionTime); + hash_map<Node, Node, NodeHashFunction> cache; + for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { + assertionsToPreprocess->replace(i, expandDefinitions((*assertionsToPreprocess)[i], cache)); + }*/ + return PreprocessingPassResult(true); +} + NlExtPurifyPass::NlExtPurifyPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){ } -void NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) { +PreprocessingPassResult NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) { std::hash_map<Node, Node, NodeHashFunction> cache; std::hash_map<Node, Node, NodeHashFunction> bcache; std::vector<Node> var_eq; @@ -34,6 +48,7 @@ void NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) { var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]); assertionsToPreprocess->replace(lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq) ); } + return PreprocessingPassResult(true); } Node NlExtPurifyPass::purifyNlTerms(TNode n, NodeMap& cache, @@ -85,17 +100,18 @@ CEGuidedInstPass::CEGuidedInstPass(ResourceManager* resourceManager, d_theoryEngine(theoryEngine){ } -void CEGuidedInstPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult CEGuidedInstPass::apply(AssertionPipeline* assertionsToPreprocess){ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( (*assertionsToPreprocess)[i] ); } + return PreprocessingPassResult(true); } SolveRealAsIntPass::SolveRealAsIntPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){ } -void SolveRealAsIntPass::apply(AssertionPipeline* assertionsToPreprocess) { +PreprocessingPassResult SolveRealAsIntPass::apply(AssertionPipeline* assertionsToPreprocess) { Chat() << "converting reals to ints..." << std::endl; std::hash_map<Node, Node, NodeHashFunction> cache; std::vector<Node> var_eq; @@ -109,6 +125,7 @@ void SolveRealAsIntPass::apply(AssertionPipeline* assertionsToPreprocess) { d_assertions.replace(last_index, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); } */ + return PreprocessingPassResult(true); } Node SolveRealAsIntPass::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) { @@ -203,13 +220,14 @@ SolveIntAsBVPass::SolveIntAsBVPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){ } -void SolveIntAsBVPass::apply(AssertionPipeline* assertionsToPreprocess) +PreprocessingPassResult SolveIntAsBVPass::apply(AssertionPipeline* assertionsToPreprocess) { Chat() << "converting ints to bit-vectors..." << std::endl; std::hash_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { assertionsToPreprocess->replace(i, intToBV((*assertionsToPreprocess)[i], cache) ); } + return PreprocessingPassResult(true); } struct intToBV_stack_element { @@ -448,8 +466,9 @@ BitBlastModePass::BitBlastModePass(ResourceManager* resourceManager, d_theoryEngine(theoryEngine){ } -void BitBlastModePass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult BitBlastModePass::apply(AssertionPipeline* assertionsToPreprocess){ d_theoryEngine->mkAckermanizationAsssertions(assertionsToPreprocess->ref()); + return PreprocessingPassResult(true); } BVAbstractionPass::BVAbstractionPass(ResourceManager* resourceManager, @@ -475,10 +494,11 @@ void BVAbstractionPass::bvAbstraction(AssertionPipeline* assertionsToPreprocess) } } -void BVAbstractionPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult BVAbstractionPass::apply(AssertionPipeline* assertionsToPreprocess){ dumpAssertions("pre-bv-abstraction", *assertionsToPreprocess); bvAbstraction(assertionsToPreprocess); dumpAssertions("post-bv-abstraction", *assertionsToPreprocess); + return PreprocessingPassResult(true); } UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager, @@ -488,21 +508,23 @@ UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager, d_theoryEngine(theoryEngine){ } -void UnconstrainedSimpPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult UnconstrainedSimpPass::apply(AssertionPipeline* assertionsToPreprocess){ TimerStat::CodeTimer unconstrainedSimpTimer(d_unconstrainedSimpTime); spendResource(options::preprocessStep()); Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << std::endl; d_theoryEngine->ppUnconstrainedSimp(assertionsToPreprocess->ref()); + return PreprocessingPassResult(true); } RewritePass::RewritePass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){ } -void RewritePass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult RewritePass::apply(AssertionPipeline* assertionsToPreprocess){ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { assertionsToPreprocess->replace(i, theory::Rewriter::rewrite((*assertionsToPreprocess)[i])); } + return PreprocessingPassResult(true); } NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager, @@ -511,7 +533,7 @@ NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager, d_topLevelSubstitutions(topLevelSubstitutions){ } -void NotUnsatCoresPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult NotUnsatCoresPass::apply(AssertionPipeline* assertionsToPreprocess){ Chat() << "applying substitutions..." << std::endl; Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "applying substitutions" << std::endl; @@ -521,6 +543,7 @@ void NotUnsatCoresPass::apply(AssertionPipeline* assertionsToPreprocess){ assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(d_topLevelSubstitutions->apply((*assertionsToPreprocess)[i]))); Trace("simplify") << " got " << (*assertionsToPreprocess)[i] << std::endl; } + return PreprocessingPassResult(true); } BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager, @@ -528,13 +551,14 @@ BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager, d_theoryEngine(theoryEngine){ } -void BVToBoolPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult BVToBoolPass::apply(AssertionPipeline* assertionsToPreprocess){ dumpAssertions("pre-bv-to-bool", *assertionsToPreprocess); Chat() << "...doing bvToBool..." << std::endl; bvToBool(assertionsToPreprocess); //A rewrite pass was formerly here that has been moved to after the dump dumpAssertions("post-bv-to-bool", *assertionsToPreprocess); Trace("smt") << "POST bvToBool" << std::endl; + return PreprocessingPassResult(true); } void BVToBoolPass::bvToBool(AssertionPipeline* assertionsToPreprocess) { @@ -564,18 +588,19 @@ void BoolToBVPass::boolToBv(AssertionPipeline* assertionsToPreprocess) { assertionsToPreprocess->ref().swap(new_assertions); } -void BoolToBVPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult BoolToBVPass::apply(AssertionPipeline* assertionsToPreprocess){ dumpAssertions("pre-bool-to-bv", *assertionsToPreprocess); Chat() << "...doing boolToBv..." << std::endl; boolToBv(assertionsToPreprocess); dumpAssertions("post-bool-to-bv", *assertionsToPreprocess); Trace("smt") << "POST boolToBv" << std::endl; + return PreprocessingPassResult(true); } SepPreSkolemEmpPass::SepPreSkolemEmpPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){ } -void SepPreSkolemEmpPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult SepPreSkolemEmpPass::apply(AssertionPipeline* assertionsToPreprocess){ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { Node prev = (*assertionsToPreprocess)[i]; Node next = theory::sep::TheorySepRewriter::preprocess( prev ); @@ -585,19 +610,15 @@ void SepPreSkolemEmpPass::apply(AssertionPipeline* assertionsToPreprocess){ Trace("sep-preprocess") << " ...got " << (*assertionsToPreprocess)[i] << std::endl; } } + return PreprocessingPassResult(true); } QuantifiedPass::QuantifiedPass(ResourceManager* resourceManager, - TheoryEngine* theoryEngine, NodeList* &fmfRecFunctionsDefined, - std::map<Node,TypeNode> &fmfRecFunctionsAbs, - std::map<Node, std::vector<Node> > &fmfRecFunctionsConcrete) : - PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), - d_fmfRecFunctionsDefined(fmfRecFunctionsDefined), - d_fmfRecFunctionsAbs(fmfRecFunctionsAbs), - d_fmfRecFunctionsConcrete(fmfRecFunctionsConcrete){ + TheoryEngine* theoryEngine, SmtEngine* smt) : + PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_smt(smt) { } -void QuantifiedPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult QuantifiedPass::apply(AssertionPipeline* assertionsToPreprocess){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl; dumpAssertions("pre-skolem-quant", *assertionsToPreprocess); @@ -626,16 +647,16 @@ void QuantifiedPass::apply(AssertionPipeline* assertionsToPreprocess){ //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF if( options::fmfFunWellDefined() ){ theory::quantifiers::FunDefFmf fdf; - Assert( d_fmfRecFunctionsDefined!=NULL ); + Assert( d_smt->d_fmfRecFunctionsDefined!=NULL ); //must carry over current definitions (for incremental) - for( context::CDList<Node>::const_iterator fit = d_fmfRecFunctionsDefined->begin(); - fit != d_fmfRecFunctionsDefined->end(); ++fit ) { + for( context::CDList<Node>::const_iterator fit = d_smt->d_fmfRecFunctionsDefined->begin(); + fit != d_smt->d_fmfRecFunctionsDefined->end(); ++fit ) { Node f = (*fit); - Assert( d_fmfRecFunctionsAbs.find( f )!= d_fmfRecFunctionsAbs.end() ); - TypeNode ft = d_fmfRecFunctionsAbs[f]; + Assert( d_smt->d_fmfRecFunctionsAbs.find( f )!= d_smt->d_fmfRecFunctionsAbs.end() ); + TypeNode ft = d_smt->d_fmfRecFunctionsAbs[f]; fdf.d_sorts[f] = ft; - std::map< Node, std::vector< Node > >::iterator fcit = d_fmfRecFunctionsConcrete.find( f ); - Assert( fcit!= d_fmfRecFunctionsConcrete.end() ); + std::map< Node, std::vector< Node > >::iterator fcit = d_smt->d_fmfRecFunctionsConcrete.find( f ); + Assert( fcit!= d_smt->d_fmfRecFunctionsConcrete.end() ); for( unsigned j=0; j<fcit->second.size(); j++ ){ fdf.d_input_arg_inj[f].push_back( fcit->second[j] ); } @@ -644,21 +665,22 @@ void QuantifiedPass::apply(AssertionPipeline* assertionsToPreprocess){ //must store new definitions (for incremental) for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){ Node f = fdf.d_funcs[i]; - d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f]; - d_fmfRecFunctionsConcrete[f].clear(); + d_smt->d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f]; + d_smt->d_fmfRecFunctionsConcrete[f].clear(); for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){ - d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] ); + d_smt->d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] ); } - d_fmfRecFunctionsDefined->push_back( f ); + d_smt->d_fmfRecFunctionsDefined->push_back( f ); } } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl; + return PreprocessingPassResult(true); } InferenceOrFairnessPass::InferenceOrFairnessPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, SmtEngine* smt) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_smt(smt){ } -void InferenceOrFairnessPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult InferenceOrFairnessPass::apply(AssertionPipeline* assertionsToPreprocess){ //sort inference technique SortInference * si = d_theoryEngine->getSortInference(); si->simplify( assertionsToPreprocess->ref(), options::sortInference(), options::ufssFairnessMonotone() ); @@ -666,23 +688,25 @@ void InferenceOrFairnessPass::apply(AssertionPipeline* assertionsToPreprocess){ d_smt->setPrintFuncInModel( it->first.toExpr(), false ); d_smt->setPrintFuncInModel( it->second.toExpr(), true ); } +return PreprocessingPassResult(true); } PBRewritePass::PBRewritePass(ResourceManager* resourceManager, theory::arith::PseudoBooleanProcessor* pbsProcessor) : PreprocessingPass(resourceManager), d_pbsProcessor(pbsProcessor){ } -void PBRewritePass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult PBRewritePass::apply(AssertionPipeline* assertionsToPreprocess){ d_pbsProcessor->learn(assertionsToPreprocess->ref()); if(d_pbsProcessor->likelyToHelp()){ d_pbsProcessor->applyReplacements(assertionsToPreprocess->ref()); } + return PreprocessingPassResult(true); } DoStaticLearningPass::DoStaticLearningPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, SmtEngine* smt, TimerStat staticLearningTime) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_smt(smt), d_staticLearningTime(staticLearningTime){ } void DoStaticLearningPass::staticLearning(AssertionPipeline* assertionsToPreprocess){ -/* d_smt->finalOptionsAreSet(); + d_smt->finalOptionsAreSet(); spendResource(options::preprocessStep()); TimerStat::CodeTimer staticLearningTimer(d_staticLearningTime); @@ -699,17 +723,18 @@ void DoStaticLearningPass::staticLearning(AssertionPipeline* assertionsToPreproc } else { assertionsToPreprocess->replace(i, learned); } - }*/ + } } -void DoStaticLearningPass::apply(AssertionPipeline* assertionsToPreprocess){ - /* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << std::endl; +PreprocessingPassResult DoStaticLearningPass::apply(AssertionPipeline* assertionsToPreprocess){ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << std::endl; // Perform static learning Chat() << "doing static learning..." << std::endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing static learning" << std::endl; staticLearning(assertionsToPreprocess); - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << std::endl;*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << std::endl; + return PreprocessingPassResult(true); } RewriteApplyToConstPass::RewriteApplyToConstPass(ResourceManager* resourceManager, TimerStat rewriteApplyToConstTime) : PreprocessingPass(resourceManager), d_rewriteApplyToConstTime(rewriteApplyToConstTime){ @@ -774,18 +799,19 @@ Node RewriteApplyToConstPass::rewriteApplyToConst(TNode n){ return rewr; } -void RewriteApplyToConstPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult RewriteApplyToConstPass::apply(AssertionPipeline* assertionsToPreprocess){ Chat() << "Rewriting applies to constants..." << std::endl; TimerStat::CodeTimer codeTimer(d_rewriteApplyToConstTime); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { (*assertionsToPreprocess)[i] = theory::Rewriter::rewrite(rewriteApplyToConst((*assertionsToPreprocess)[i])); } + return PreprocessingPassResult(true); } BitBlastModeEagerPass::BitBlastModeEagerPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine){ } -void BitBlastModeEagerPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult BitBlastModeEagerPass::apply(AssertionPipeline* assertionsToPreprocess){ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { TNode atom = (*assertionsToPreprocess)[i]; Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom); @@ -793,32 +819,177 @@ void BitBlastModeEagerPass::apply(AssertionPipeline* assertionsToPreprocess){ theory::TheoryModel* m = d_theoryEngine->getModel(); m->addSubstitution(eager_atom, atom); } + return PreprocessingPassResult(true); } NoConflictPass::NoConflictPass(ResourceManager* resourceManager, DecisionEngine* decisionEngine, unsigned realAssertionsEnd, IteSkolemMap* iteSkolemMap) : PreprocessingPass(resourceManager), d_decisionEngine(decisionEngine), d_realAssertionsEnd(realAssertionsEnd), d_iteSkolemMap(iteSkolemMap){ } -void NoConflictPass::apply(AssertionPipeline* assertionsToPreprocess){ +PreprocessingPassResult NoConflictPass::apply(AssertionPipeline* assertionsToPreprocess){ Chat() << "pushing to decision engine..." << std::endl; Assert(iteRewriteAssertionsEnd == assertionsToPreprocess->size()); d_decisionEngine->addAssertions (assertionsToPreprocess->ref(), d_realAssertionsEnd, *d_iteSkolemMap); + return PreprocessingPassResult(true); +} + +RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, + theory::SubstitutionMap* topLevelSubstitutions, + unsigned simplifyAssertionsDepth, bool* noConflict, + IteSkolemMap iteSkolemMap, unsigned realAssertionsEnd) : + PreprocessingPass(resourceManager), + d_topLevelSubstitutions(topLevelSubstitutions), + d_simplifyAssertionsDepth(simplifyAssertionsDepth), + noConflict(noConflict), d_iteSkolemMap(iteSkolemMap), + d_realAssertionsEnd(realAssertionsEnd){ +} + +bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache) +{ + hash_map<Node, bool, NodeHashFunction>::iterator it; + it = cache.find(n); + if (it != cache.end()) { + return (*it).second; + } + + size_t sz = n.getNumChildren(); + if (sz == 0) { + IteSkolemMap::iterator it = d_iteSkolemMap.find(n); + bool bad = false; + if (it != d_iteSkolemMap.end()) { + if (!((*it).first < n)) { + bad = true; + } + } + cache[n] = bad; + return bad; + } + + size_t k = 0; + for (; k < sz; ++k) { + if (checkForBadSkolems(n[k], skolem, cache)) { + cache[n] = true; + return true; + } + } + + cache[n] = false; + return false; +} + +void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache) +{ + hash_map<Node, bool, NodeHashFunction>::iterator it; + it = cache.find(n); + if (it != cache.end()) { + return; + } + + size_t sz = n.getNumChildren(); + if (sz == 0) { + IteSkolemMap::iterator it = d_iteSkolemMap.find(n); + if (it != d_iteSkolemMap.end()) { + skolemSet.insert(n); + } + cache[n] = true; + return; + } + + size_t k = 0; + for (; k < sz; ++k) { + collectSkolems(n[k], skolemSet, cache); + } + cache[n] = true; +} + + +PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPreprocess){ + /* Chat() << "re-simplifying assertions..." << std::endl; + ScopeCounter depth(d_simplifyAssertionsDepth); + // *noConflict &= simplifyAssertions(); + if (*noConflict) { + // Need to fix up assertion list to maintain invariants: + // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced + // during ite removal. + // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. + + // cache for expression traversal + std::hash_map<Node, bool, NodeHashFunction> cache; + + // First, find all skolems that appear in the substitution map - their associated iteExpr will need + // to be moved to the main assertion set + std::set<TNode> skolemSet; + theory::SubstitutionMap::iterator pos = d_topLevelSubstitutions->begin(); + for (; pos != d_topLevelSubstitutions->end(); ++pos) { + collectSkolems((*pos).first, skolemSet, cache); + collectSkolems((*pos).second, skolemSet, cache); + } + + // We need to ensure: + // 1. iteExpr has the form (ite cond (sk = t) (sk = e)) + // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk + // If either of these is violated, we must add iteExpr as a proper assertion + IteSkolemMap::iterator it = d_iteSkolemMap.begin(); + IteSkolemMap::iterator iend = d_iteSkolemMap.end(); + NodeBuilder<> builder(kind::AND); + builder << (*assertionsToPreprocess)[d_realAssertionsEnd - 1]; + std::vector<TNode> toErase; + for (; it != iend; ++it) { + if (skolemSet.find((*it).first) == skolemSet.end()) { + TNode iteExpr = (*assertionsToPreprocess)[(*it).second]; + if (iteExpr.getKind() == kind::ITE && + iteExpr[1].getKind() == kind::EQUAL && + iteExpr[1][0] == (*it).first && + iteExpr[2].getKind() == kind::EQUAL && + iteExpr[2][0] == (*it).first) { + cache.clear(); + bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache); + bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache); + bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache); + if (!bad) { + continue; + } + } + } + // Move this iteExpr into the main assertions + builder << (*assertionsToPreprocess)[(*it).second]; + (*assertionsToPreprocess)[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true); + toErase.push_back((*it).first); + } + if(builder.getNumChildren() > 1) { + while (!toErase.empty()) { + d_iteSkolemMap.erase(toErase.back()); + toErase.pop_back(); + } + (*assertionsToPreprocess)[d_realAssertionsEnd - 1] = theory::Rewriter::rewrite(Node(builder)); + } + // For some reason this is needed for some benchmarks, such as + // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 + // Figure it out later + removeITEs(); + // Assert(iteRewriteAssertionsEnd == d_assertions.size()); + } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;*/ + return PreprocessingPassResult(true); } -RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict) : PreprocessingPass(resourceManager), d_topLevelSubstitutions(topLevelSubstitutions), d_simplifyAssertionsDepth(simplifyAssertionsDepth), noConflict(noConflict){ +SimplifyAssertionsPass::SimplifyAssertionsPass( + ResourceManager* resourceManager, unsigned simplifyAssertionsDepth) : + PreprocessingPass(resourceManager), + d_simplifyAssertionsDepth(simplifyAssertionsDepth){ } // returns false if simplification led to "false" -bool RepeatSimpPass::simplifyAssertions(){ -/* throw(TypeCheckingException, LogicException, UnsafeInterruptException) { - spendResource(options::preprocessStep()); +PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* assertionsToPreprocess) + throw(TypeCheckingException, LogicException, UnsafeInterruptException) { + /* spendResource(options::preprocessStep()); Assert(d_smt.d_pendingPops == 0); try { ScopeCounter depth(d_simplifyAssertionsDepth); Trace("simplify") << "SmtEnginePrivate::simplify()" << endl; - dumpAssertions("pre-nonclausal", d_assertions); + dumpAssertions("pre-nonclausal", *assertionsToPreprocess); if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { // Perform non-clausal simplification @@ -841,7 +1012,7 @@ bool RepeatSimpPass::simplifyAssertions(){ // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) - d_realAssertionsEnd == d_assertions.size() ) { + d_realAssertionsEnd == assertionsToPreprocess->size() ) { Chat() << "...fixing miplib encodings..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "looking for miplib pseudobooleans..." << endl; @@ -855,14 +1026,14 @@ bool RepeatSimpPass::simplifyAssertions(){ } } - dumpAssertions("post-nonclausal", d_assertions); + dumpAssertions("post-nonclausal", *assertionsToPreprocess); Trace("smt") << "POST nonClausalSimplify" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; // before ppRewrite check if only core theory for BV theory - d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref()); + d_smt.d_theoryEngine->staticInitializeBVOptions(assertionsToPreprocess->ref()); - dumpAssertions("pre-theorypp", d_assertions); + dumpAssertions("pre-theorypp", *assertionsToPreprocess); // Theory preprocessing if (d_smt.d_earlyTheoryPP) { @@ -870,16 +1041,16 @@ bool RepeatSimpPass::simplifyAssertions(){ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); // Call the theory preprocessors d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); - d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); - Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { + Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsTopreprocess)[i]); + assertionsToPreprocess->replace(i, d_smt.d_theoryEngine->preprocess((*assertionsToPreprocess)[i])); + Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]); } } - dumpAssertions("post-theorypp", d_assertions); + dumpAssertions("post-theorypp", *assertionsToPreprocess); Trace("smt") << "POST theoryPP" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; // ITE simplification if(options::doITESimp() && @@ -892,20 +1063,20 @@ bool RepeatSimpPass::simplifyAssertions(){ } } - dumpAssertions("post-itesimp", d_assertions); + dumpAssertions("post-itesimp", *assertionsToPreprocess); Trace("smt") << "POST iteSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; // Unconstrained simplification if(options::unconstrainedSimp()) { Chat() << "...doing unconstrained simplification..." << endl; preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine); - pass.apply(&d_assertions); + pass.apply(assertionsToPreprocess); } - dumpAssertions("post-unconstrained", d_assertions); + dumpAssertions("post-unconstrained", *assertionsToPreprocess); Trace("smt") << "POST unconstrainedSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; @@ -917,9 +1088,9 @@ bool RepeatSimpPass::simplifyAssertions(){ } } - dumpAssertions("post-repeatsimp", d_assertions); + dumpAssertions("post-repeatsimp", *assertionsToPreprocess); Trace("smt") << "POST repeatSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any @@ -931,80 +1102,10 @@ bool RepeatSimpPass::simplifyAssertions(){ ss << "A bad expression was produced. Original exception follows:\n" << tcep; InternalError(ss.str().c_str()); - } - return true;*/ - return true; + }*/ + return PreprocessingPassResult(true); } -void RepeatSimpPass::apply(AssertionPipeline* assertionsToPreprocess){ -/* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << std::endl; - Chat() << "re-simplifying assertions..." << std::endl; - ScopeCounter depth(d_simplifyAssertionsDepth); - *noConflict &= simplifyAssertions(); - if (*noConflict) { - // Need to fix up assertion list to maintain invariants: - // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced - // during ite removal. - // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. - - // cache for expression traversal - std::hash_map<Node, bool, NodeHashFunction> cache; - - // First, find all skolems that appear in the substitution map - their associated iteExpr will need - // to be moved to the main assertion set - std::set<TNode> skolemSet; - theory::SubstitutionMap::iterator pos = d_topLevelSubstitutions->begin(); - for (; pos != d_topLevelSubstitutions->end(); ++pos) { - collectSkolems((*pos).first, skolemSet, cache); - collectSkolems((*pos).second, skolemSet, cache); - } - - // We need to ensure: - // 1. iteExpr has the form (ite cond (sk = t) (sk = e)) - // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk - // If either of these is violated, we must add iteExpr as a proper assertion - IteSkolemMap::iterator it = d_iteSkolemMap.begin(); - IteSkolemMap::iterator iend = d_iteSkolemMap.end(); - NodeBuilder<> builder(kind::AND); - builder << d_assertions[d_realAssertionsEnd - 1]; - std::vector<TNode> toErase; - for (; it != iend; ++it) { - if (skolemSet.find((*it).first) == skolemSet.end()) { - TNode iteExpr = d_assertions[(*it).second]; - if (iteExpr.getKind() == kind::ITE && - iteExpr[1].getKind() == kind::EQUAL && - iteExpr[1][0] == (*it).first && - iteExpr[2].getKind() == kind::EQUAL && - iteExpr[2][0] == (*it).first) { - cache.clear(); - bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache); - bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache); - bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache); - if (!bad) { - continue; - } - } - } - // Move this iteExpr into the main assertions - builder << (*assertionsToPreprocess)[(*it).second]; - d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true); - toErase.push_back((*it).first); - } - if(builder.getNumChildren() > 1) { - while (!toErase.empty()) { - d_iteSkolemMap.erase(toErase.back()); - toErase.pop_back(); - } - (*assertionsToPreprocess)[d_realAssertionsEnd - 1] = theory::Rewriter::rewrite(Node(builder)); - } - // For some reason this is needed for some benchmarks, such as - // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 - // Figure it out later - removeITEs(); - // Assert(iteRewriteAssertionsEnd == d_assertions.size()); - } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;*/ -} } // namespace preproc } // namespace CVC4 diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h index f34f3624b..c27890853 100644 --- a/src/preproc/preprocessing_passes_core.h +++ b/src/preproc/preprocessing_passes_core.h @@ -16,10 +16,19 @@ namespace preproc { typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; typedef std::hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; typedef context::CDList<Node> NodeList; - + +class ExpandingDefinitionsPass : public PreprocessingPass { + public: + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime); + private: + TimerStat d_definitionExpansionTime; + Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly); +}; + class NlExtPurifyPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); NlExtPurifyPass(ResourceManager* resourceManager); private: Node purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, @@ -28,7 +37,7 @@ class NlExtPurifyPass : public PreprocessingPass { class CEGuidedInstPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); private: TheoryEngine* d_theoryEngine; @@ -36,7 +45,7 @@ class CEGuidedInstPass : public PreprocessingPass { class SolveRealAsIntPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); SolveRealAsIntPass(ResourceManager* resourceManager); private: Node realToInt(TNode n, NodeMap& cache, std::vector<Node>& var_eq); @@ -44,7 +53,7 @@ class SolveRealAsIntPass : public PreprocessingPass { class SolveIntAsBVPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); SolveIntAsBVPass(ResourceManager* resourceManager); private: Node intToBV(TNode n, NodeToNodeHashMap& cache); @@ -53,7 +62,7 @@ class SolveIntAsBVPass : public PreprocessingPass { class BitBlastModePass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); BitBlastModePass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); private: @@ -62,7 +71,7 @@ class BitBlastModePass : public PreprocessingPass { class BVAbstractionPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); BVAbstractionPass(ResourceManager* resourceManager, SmtEngine* smt, TheoryEngine* theoryEngine); private: @@ -75,7 +84,7 @@ class BVAbstractionPass : public PreprocessingPass { class UnconstrainedSimpPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); UnconstrainedSimpPass(ResourceManager* resourceManager, TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine); private: @@ -86,13 +95,13 @@ class UnconstrainedSimpPass : public PreprocessingPass { class RewritePass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); RewritePass(ResourceManager* resourceManager); }; class NotUnsatCoresPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); NotUnsatCoresPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions); private: @@ -101,7 +110,7 @@ class NotUnsatCoresPass : public PreprocessingPass { class BVToBoolPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); BVToBoolPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); private: @@ -112,7 +121,7 @@ class BVToBoolPass : public PreprocessingPass { class BoolToBVPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsTopreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsTopreprocess); BoolToBVPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); private: @@ -123,27 +132,23 @@ class BoolToBVPass : public PreprocessingPass { class SepPreSkolemEmpPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); SepPreSkolemEmpPass(ResourceManager* resourceManager); }; class QuantifiedPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); - QuantifiedPass(ResourceManager* resourceManager, - TheoryEngine* theoryEngine, NodeList* &fmfRecFunctionsDefined, - std::map<Node,TypeNode> &fmfRecFunctionsAbs, - std::map<Node, std::vector<Node> > &fmfRecFunctionsConcrete); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + QuantifiedPass(ResourceManager* resourceManager, + TheoryEngine* theoryEngine, SmtEngine* smt); private: TheoryEngine* d_theoryEngine; - NodeList* d_fmfRecFunctionsDefined; - std::map<Node,TypeNode> d_fmfRecFunctionsAbs; - std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete; + SmtEngine* d_smt; }; class InferenceOrFairnessPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); InferenceOrFairnessPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, SmtEngine* smt); private: TheoryEngine* d_theoryEngine; @@ -152,7 +157,7 @@ class InferenceOrFairnessPass : public PreprocessingPass { class PBRewritePass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); PBRewritePass(ResourceManager* resourceManager, theory::arith::PseudoBooleanProcessor* pbsProcessor); private: theory::arith::PseudoBooleanProcessor* d_pbsProcessor; @@ -160,7 +165,7 @@ class PBRewritePass : public PreprocessingPass { class DoStaticLearningPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); DoStaticLearningPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, SmtEngine* smt, TimerStat staticLearningTime); private: TheoryEngine* d_theoryEngine; @@ -172,7 +177,7 @@ class DoStaticLearningPass : public PreprocessingPass { class RewriteApplyToConstPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); RewriteApplyToConstPass(ResourceManager* resourceManager, TimerStat rewriteApplyToConstTime); private: TimerStat d_rewriteApplyToConstTime; @@ -181,7 +186,7 @@ class RewriteApplyToConstPass : public PreprocessingPass { class BitBlastModeEagerPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); BitBlastModeEagerPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); private: TheoryEngine* d_theoryEngine; @@ -189,7 +194,7 @@ class BitBlastModeEagerPass : public PreprocessingPass { class NoConflictPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); NoConflictPass(ResourceManager* resourceManager, DecisionEngine* decisionEngine, unsigned realAssertionsEnd, IteSkolemMap* iteSkolemMap ); private: DecisionEngine* d_decisionEngine; @@ -199,15 +204,29 @@ class NoConflictPass : public PreprocessingPass { class RepeatSimpPass : public PreprocessingPass { public: - virtual void apply(AssertionPipeline* assertionsToPreprocess); - RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict); + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict, IteSkolemMap iteSkolemMap, unsigned realAssertionsEnd); private: theory::SubstitutionMap* d_topLevelSubstitutions; + void collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache); + bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache); bool simplifyAssertions(); unsigned d_simplifyAssertionsDepth; bool* noConflict; + IteSkolemMap d_iteSkolemMap; + unsigned d_realAssertionsEnd; }; +class SimplifyAssertionsPass : public PreprocessingPass { + public: + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) throw(TypeCheckingException, LogicException, + UnsafeInterruptException); + SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth); + private: + unsigned d_simplifyAssertionsDepth; + +}; + } // namespace preproc } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9e116bd71..4819d9674 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -124,7 +124,7 @@ void DeleteAndClearCommandVector(std::vector<Command*>& commands) { } /** Useful for counting the number of recursive calls. */ -class ScopeCounter { +/*class ScopeCounter { private: unsigned& d_depth; public: @@ -134,7 +134,7 @@ public: ~ScopeCounter(){ --d_depth; } -}; +};*/ /** * Representation of a defined function. We keep these around in @@ -3503,7 +3503,6 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N cache[n] = true; } - bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache) { hash_map<Node, bool, NodeHashFunction>::iterator it; @@ -3574,6 +3573,8 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", d_assertions); { +/* preproc::ExpandingDefinitionsPass pass(d_resourceManager, d_smt.d_stats->d_definitionExpansionTime); + pass.apply(&d_assertions);*/ Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); @@ -3722,67 +3723,8 @@ void SmtEnginePrivate::processAssertions() { } if( d_smt.d_logic.isQuantified() ){ - - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl; - - dumpAssertions("pre-skolem-quant", d_assertions); - //remove rewrite rules, apply pre-skolemization to existential quantifiers - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Node prev = (d_assertions)[i]; - Node next = quantifiers::QuantifiersRewriter::preprocess( prev ); - if( next!=prev ){ - d_assertions.replace(i, Rewriter::rewrite( next )); - Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev <<std::endl; - Trace("quantifiers-preprocess") << " ...got " << (d_assertions)[i] << std::endl; - } - } - dumpAssertions("post-skolem-quant", d_assertions); - if( options::macrosQuant() ){ - //quantifiers macro expansion - quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); - bool success; - do{ - success = qm.simplify( d_assertions.ref(), true ); - }while( success ); - //finalize the definitions - qm.finalizeDefinitions(); - } - - - //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF - if( options::fmfFunWellDefined() ){ - quantifiers::FunDefFmf fdf; - Assert( d_smt.d_fmfRecFunctionsDefined!=NULL ); - //must carry over current definitions (for incremental) - for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin(); - fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) { - Node f = (*fit); - Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!= d_fmfRecFunctionsAbs.end() ); - TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f]; - fdf.d_sorts[f] = ft; - std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f ); - Assert( fcit!= d_smt.d_fmfRecFunctionsConcrete.end() ); - for( unsigned j=0; j<fcit->second.size(); j++ ){ - fdf.d_input_arg_inj[f].push_back( fcit->second[j] ); - } - } - fdf.simplify(d_assertions.ref()); - //must store new definitions (for incremental) - for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){ - Node f = fdf.d_funcs[i]; - d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f]; - d_smt.d_fmfRecFunctionsConcrete[f].clear(); - for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){ - d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] ); - } - d_smt.d_fmfRecFunctionsDefined->push_back( f ); - } - } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl; - -/* preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, - d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs, d_smt.d_fmfRecFunctionsConcrete); - pass.apply(&d_assertions);*/ + preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, &d_smt); + pass.apply(&d_assertions); } if( options::sortInference() || options::ufssFairnessMonotone() ){ @@ -3839,9 +3781,12 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-repeat-simplify", d_assertions); if(options::repeatSimp()) { -/* preproc::RepeatSimpPass pass(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict); - pass.apply(&d_assertions);*/ - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; + preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth); + noConflict &= pass.apply(&d_assertions).d_noConflict; + + preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); + pass1.apply(&d_assertions); +/* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); @@ -3907,7 +3852,7 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/ } dumpAssertions("post-repeat-simplify", d_assertions); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2bb0787d4..8de31809e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -105,6 +105,11 @@ namespace theory { class TheoryModel; }/* CVC4::theory namespace */ +namespace preproc{ + class DoStaticLearningPass; + class QuantifiedPass; +}/* CVC4::preproc namespace */ + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -117,7 +122,6 @@ namespace theory { // The CNF conversion can go on in PropEngine. class CVC4_PUBLIC SmtEngine { - friend class PreprocessingPass; /** The type of our internal map of defined functions */ typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> DefinedFunctionMap; @@ -348,7 +352,9 @@ class CVC4_PUBLIC SmtEngine { * be called when d_logic is updated. */ void setLogicInternal() throw(); - + + friend class ::CVC4::preproc::DoStaticLearningPass; + friend class ::CVC4::preproc::QuantifiedPass; friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; |