From ed87e0c1ccb0cb93cdedf5229c6a2b47af77743c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 17 Feb 2014 18:59:39 -0500 Subject: [PATCH] Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548). --- src/prop/prop_engine.cpp | 4 ---- src/theory/arith/theory_arith.cpp | 2 +- src/theory/output_channel.h | 4 +++- src/theory/quantifiers/bounded_integers.cpp | 2 +- src/theory/quantifiers/instantiation_engine.cpp | 2 +- src/theory/quantifiers/options | 2 +- src/theory/quantifiers/symmetry_breaking.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.h | 1 + src/theory/quantifiers_engine.cpp | 4 ++-- src/theory/rewriterules/theory_rewriterules.h | 2 +- src/theory/theory_engine.cpp | 17 ++++++++++------- src/theory/theory_engine.h | 8 ++++---- src/theory/theory_test_utils.h | 2 +- src/util/statistics_registry.h | 11 ++++++++--- test/unit/theory/theory_engine_white.h | 2 +- test/unit/theory/theory_white.h | 4 ++-- 17 files changed, 39 insertions(+), 32 deletions(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 036877b6a..2a2a60391 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -111,10 +111,6 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - if(Dump.isOn("lemmas")) { - Dump("lemmas") << AssertCommand(node.toExpr()); - } - // Assert as removable d_cnfStream->convertAndAssert(node, removable, negated); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 239385bfc..85d9d1f9b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -52,7 +52,7 @@ void TheoryArith::addSharedTerm(TNode n){ } Node TheoryArith::ppRewrite(TNode atom) { - CodeTimer timer(d_ppRewriteTimer); + CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true); return d_internal->ppRewrite(atom); } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 44b89e8cb..51187b7dd 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -113,10 +113,12 @@ public: * * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point + * @param preprocess - whether to apply more aggressive preprocessing * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, bool removable = false) + virtual LemmaStatus lemma(TNode n, bool removable = false, + bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 5ad4cef92..78f989807 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -363,7 +363,7 @@ void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem); + d_quantEngine->getOutputChannel().lemma(lem, false, true); l = Node::null(); u = Node::null(); return; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 9a3c07c5e..99dc29bf8 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ nb << f << ceLit; Node lem = nb; Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); + d_quantEngine->getOutputChannel().lemma( lem, false, true ); addedLemma = true; } } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 06d11f70f..6d333521b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -94,7 +94,7 @@ option flipDecision --flip-decision/ bool :default false option internalReps /--disable-quant-internal-reps bool :default true disables instantiating with representatives chosen by quantifiers engine -option finiteModelFind --finite-model-find bool :default false :read-write +option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write use finite model finding heuristic for quantifier instantiation option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 66a3ac79f..0023b05bc 100644 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -298,7 +298,7 @@ bool SubsortSymmetryBreaker::check( Theory::Effort level ) { //flush pending lemmas if( !d_pending_lemmas.empty() ){ for( unsigned i=0; igetOutputChannel().lemma( d_pending_lemmas[i] ); + getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i], false, true ); ++( getStrongSolver()->d_statistics.d_sym_break_lemmas ); } d_pending_lemmas.clear(); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6a3a6fca1..19a915ae9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -164,7 +164,7 @@ void TheoryQuantifiers::assertExistential( Node n ){ nb << n[0] << body.notNode(); Node lem = nb; Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; - d_out->lemma( lem ); + d_out->lemma( lem, false, true ); d_skolemized[n] = true; } } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 8ace5f181..84b65cacd 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -73,6 +73,7 @@ public: bool flipDecision(); void setUserAttribute( const std::string& attr, Node n ); eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } + bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; } private: void assertUniversal( Node n ); void assertExistential( Node n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 36410bd50..41f53740a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -458,7 +458,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; lem = Rewriter::rewrite(lem); if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ - //d_curr_out->lemma( lem ); + //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; @@ -567,7 +567,7 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){ //take default output channel if none is provided d_hasAddedLemma = true; for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){ - out->lemma( d_lemmas_waiting[i] ); + out->lemma( d_lemmas_waiting[i], false, true ); } d_lemmas_waiting.clear(); } diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 30e6f9709..2cefe7f07 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -211,7 +211,7 @@ private: Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - bool ppDontRewriteSubterm(TNode atom){ return true; } + bool ppDontRewriteSubterm(TNode atom) { return true; } private: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 63024e5d5..c29177b49 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -475,7 +475,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), false, false, carePair.theory); + lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); } } @@ -779,7 +779,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) { Node newTerm; if (theoryOf(term)->ppDontRewriteSubterm(term)) { - newTerm = term; + newTerm = Rewriter::rewrite(term); } else { NodeBuilder<> newNode(term.getKind()); if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -1320,7 +1320,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The } } -theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo) { +theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { @@ -1344,15 +1344,18 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable options::lemmaOutputChannel()->notifyNewLemma(node.toExpr()); } + // Run theory preprocessing, maybe + Node ppNode = preprocess ? this->preprocess(node) : Node(node); + // Remove the ITEs std::vector additionalLemmas; IteSkolemMap iteSkolemMap; - additionalLemmas.push_back(node); + additionalLemmas.push_back(ppNode); d_iteRemover.run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); if(Debug.isOn("lemma-ites")) { - Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl; + Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; Debug("lemma-ites") << " + now have the following " << additionalLemmas.size() << " lemma(s):" << endl; for(std::vector::const_iterator i = additionalLemmas.begin(); @@ -1417,11 +1420,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, true, true, THEORY_LAST); + lemma(fullConflict, true, true, false, THEORY_LAST); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, true, true, THEORY_LAST); + lemma(conflict, true, true, false, THEORY_LAST); } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d5de8e3b2..db31ef9b7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -292,18 +292,18 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, theory::THEORY_LAST); + return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, d_theory); + return d_engine->lemma(lemma, false, removable, false, d_theory); } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) { @@ -451,7 +451,7 @@ class TheoryEngine { * @param removable can the lemma be remove (restrictions apply) * @param needAtoms if not THEORY_LAST, then */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo); + theory::LemmaStatus lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index e4921b163..28a749a41 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -87,7 +87,7 @@ public: push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index bd33557d9..8246bfdd2 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -824,6 +824,7 @@ public: */ class CodeTimer { TimerStat& d_timer; + bool d_reentrant; /** Private copy constructor undefined (no copy permitted). */ CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; @@ -831,11 +832,15 @@ class CodeTimer { CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; public: - CodeTimer(TimerStat& timer) : d_timer(timer) { - d_timer.start(); + CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { + if(!allow_reentrant || !(d_reentrant = d_timer.running())) { + d_timer.start(); + } } ~CodeTimer() { - d_timer.stop(); + if(!d_reentrant) { + d_timer.stop(); + } } };/* class CodeTimer */ diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 803b24527..e32e49801 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -58,7 +58,7 @@ class FakeOutputChannel : public OutputChannel { void propagateAsDecision(TNode n) throw(AssertionException) { Unimplemented(); } - LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { Unimplemented(); } void requirePhase(TNode, bool) throw(AssertionException) { diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index e2dfcc464..3259381ad 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -70,7 +70,7 @@ public: // ignore } - LemmaStatus lemma(TNode n, bool removable) + LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false) throw(AssertionException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); @@ -301,7 +301,7 @@ public: void testOutputChannel() { Node n = atom0.orNode(atom1); - d_outputChannel.lemma(n, false); + d_outputChannel.lemma(n); d_outputChannel.split(atom0); Node s = atom0.orNode(atom0.notNode()); TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u); -- 2.30.2