From dd30200795d4b37398c29f0d20998c9bd63a7fe7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 16 Aug 2012 21:30:41 +0000 Subject: [PATCH] Replace propagateAsDecision() with Theory::getNextDecisionRequest(): * arrays now uses the new approach by using a CDQueue<> * uf strong solver has had the feature disabled, pending a merge from Andy * theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property) * the staticLearning property has been renamed ppStaticLearn to match the function name * theory kinds files are now checked again for correctly-declared properties (this had been disabled) * minor documentation and other fixups --- src/context/cdqueue.h | 2 +- src/theory/arith/kinds | 2 +- src/theory/arrays/kinds | 2 +- src/theory/arrays/theory_arrays.cpp | 16 +++++-- src/theory/arrays/theory_arrays.h | 5 ++ src/theory/builtin/kinds | 5 +- src/theory/mktheorytraits | 41 ++++++++-------- src/theory/output_channel.h | 18 ------- .../quantifiers/instantiation_engine.cpp | 2 +- src/theory/theory.h | 6 +++ src/theory/theory_engine.cpp | 47 +++++++++++-------- src/theory/theory_engine.h | 38 +-------------- src/theory/uf/kinds | 2 +- src/theory/uf/theory_uf_strong_solver.cpp | 4 +- 14 files changed, 86 insertions(+), 104 deletions(-) diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index abdcc0493..e1c59615d 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -144,7 +144,7 @@ public: } /** - * Returns the most recent item added to the list. + * Returns the most recent item added to the queue. */ const T& back() const { Assert(!empty(), "CDQueue::back() called on empty list"); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index b9fac6e20..549e9f19b 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -9,7 +9,7 @@ typechecker "theory/arith/theory_arith_type_rules.h" instantiator ::CVC4::theory::arith::InstantiatorTheoryArith "theory/arith/theory_arith_instantiator.h" properties stable-infinite -properties check propagate staticLearning presolve notifyRestart +properties check propagate ppStaticLearn presolve notifyRestart rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index ef237e351..986654cd3 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -9,7 +9,7 @@ typechecker "theory/arrays/theory_arrays_type_rules.h" instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h" properties polite stable-infinite parametric -properties check propagate presolve +properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 47f3e31db..4f2497d2b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -76,6 +76,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_decisionRequests(c), d_permRef(c) { StatisticsRegistry::registerStat(&d_numRow); @@ -1082,7 +1083,6 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } - void TheoryArrays::queueRowLemma(RowLemmaType lem) { if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) { @@ -1148,8 +1148,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // Prefer equality between indexes so as not to introduce new read terms if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { - Node split = d_valuation.ensureLiteral(i.eqNode(j)); - d_out->propagateAsDecision(split); + d_decisionRequests.push(i.eqNode(j)); } // TODO: maybe add triggers here @@ -1215,6 +1214,17 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } +Node TheoryArrays::getNextDecisionRequest() { + if(! d_decisionRequests.empty()) { + Node n = d_valuation.ensureLiteral(d_decisionRequests.front()); + d_decisionRequests.pop(); + return n; + } else { + return Node::null(); + } +} + + void TheoryArrays::dischargeLemmas() { size_t sz = d_RowQueue.size(); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6787f8ad8..f7cbe8b73 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -228,6 +228,8 @@ class TheoryArrays : public Theory { private: public: + Node getNextDecisionRequest(); + void presolve(); void shutdown() { } @@ -333,6 +335,9 @@ class TheoryArrays : public Theory { context::CDList d_reads; std::hash_map d_diseqCache; + // The decision requests we have for the core + context::CDQueue d_decisionRequests; + // List of nodes that need permanent references in this context context::CDList d_permRef; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 6bb175db3..e52196163 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -32,12 +32,15 @@ # finite the theory is finite # stable-infinite the theory is stably infinite # polite the theory is polite +# parametric the theory is parametric # # check the theory supports the check() function # propagate the theory supports propagate() (and explain()) -# staticLearning the theory supports staticLearning() +# ppStaticLearn the theory supports ppStaticLearn() # notifyRestart the theory supports notifyRestart() # presolve the theory supports presolve() +# postsolve the theory supports postsolve() +# getNextDecisionRequest the theory supports getNextDecisionRequest() # # In the case of the "theory-supports-function" properties, you # need to declare these for your theory or the functions will not diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 60ff05d35..c8ef23a78 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -47,10 +47,11 @@ mk_type_enumerator_cases= theory_has_check="false" theory_has_propagate="false" -theory_has_staticLearning="false" +theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" +theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -143,36 +144,37 @@ struct TheoryTraits<${theory_id}> { static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; - static const bool hasStaticLearning = ${theory_has_staticLearning}; + static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn}; static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; static const bool hasPostsolve = ${theory_has_postsolve}; + static const bool hasGetNextDecisionRequest = ${theory_has_getNextDecisionRequest}; };/* struct TheoryTraits<${theory_id}> */ " # warnings about theory content and properties - # TODO: fix, not corresponding to staticLearning anymore - # dir="$(dirname "$kf")/../../" - # if [ -e "$dir/$theory_header" ]; then - # for function in check propagate staticLearning notifyRestart presolve postsolve; do - # if eval "\$theory_has_$function"; then - # grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || - # echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 - # else - # grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && - # echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 - # fi - # done - # else - # echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 - # fi + dir="$(dirname "$kf")/../../" + if [ -e "$dir/$theory_header" ]; then + for function in check propagate ppStaticLearn notifyRestart presolve postsolve getNextDecisionRequest; do + if eval "\$theory_has_$function"; then + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || + echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 + else + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && + echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 + fi + done + else + echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 + fi theory_has_check="false" theory_has_propagate="false" - theory_has_staticLearning="false" + theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" + theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -264,9 +266,10 @@ function properties { polite) theory_polite="true";; check) theory_has_check="true";; propagate) theory_has_propagate="true";; - staticLearning) theory_has_staticLearning="true";; + ppStaticLearn) theory_has_ppStaticLearn="true";; presolve) theory_has_presolve="true";; postsolve) theory_has_postsolve="true";; + getNextDecisionRequest) theory_has_getNextDecisionRequest="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index b1a5fc60c..a86984cca 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -107,24 +107,6 @@ public: */ virtual bool propagate(TNode n) throw(AssertionException) = 0; - /** - * Request that the core make a decision on this atom. The decision - * will be "as soon as possible," but due to other propagation and - * conflict-detection work going on internally, the request is queued - * up and may be behind other such requests. The request will be - * silently dropped if the atom has a definite value at the point the - * request would be serviced. This request is also context-dependent - * on the search context, meaning that it will be dropped completely - * if a conflict is found before it is serviced. Each request will only - * be serviced a single time, even though the atom may become undefined - * due to backtracking. - * - * @param atom the atom to decide upon (or the negation of an - * atom---the decision will be in the phase provided); must be - * associated to a SAT literal. - */ - virtual void propagateAsDecision(TNode n) throw(AssertionException) = 0; - /** * Tell the core that a valid theory lemma at decision level 0 has * been detected. (This requests a split.) diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index fb3e6fb36..0fa4fad12 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -381,7 +381,7 @@ void InstantiationEngine::propagate( Theory::Effort level ){ bool value; if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ //if not already set, propagate as decision - d_quantEngine->getOutputChannel().propagateAsDecision( it->second ); + //d_quantEngine->getOutputChannel().propagateAsDecision( it->second ); Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 397f7cff7..46244aec6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -559,6 +559,12 @@ public: identify().c_str()); } + /** + * Return a decision request, if the theory has one, or the NULL node + * otherwise. + */ + virtual Node getNextDecisionRequest() { return Node(); } + /** * Statically learn from assertion "in," which has been asserted * true at the top level. The theory should only add (via diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6fbd4a417..6dfc9f22d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -69,8 +69,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagationMapTimestamp(context, 0), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), - d_decisionRequests(context), - d_decisionRequestsIndex(context, 0), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_inPreregister(false), d_factsAsserted(context, false), @@ -285,7 +283,7 @@ void TheoryEngine::check(Theory::Effort effort) { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->check(effort); \ + theoryOf(THEORY)->check(effort); \ if (d_inConflict) { \ break; \ } \ @@ -392,7 +390,7 @@ void TheoryEngine::combineTheories() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \ + theoryOf(THEORY)->getCareGraph(careGraph); \ } // Call on each parametric theory to give us its care graph @@ -456,7 +454,7 @@ void TheoryEngine::propagate(Theory::Effort effort) { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->propagate(effort); \ + theoryOf(THEORY)->propagate(effort); \ } // Propagate for each theory using the statement above @@ -478,6 +476,25 @@ void TheoryEngine::propagate(Theory::Effort effort) { } } +Node TheoryEngine::getNextDecisionRequest() { + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \ + Node n = theoryOf(THEORY)->getNextDecisionRequest(); \ + if(! n.isNull()) { \ + return n; \ + } \ + } + + // Request decision from each theory using the statement above + CVC4_FOR_EACH_THEORY; + + return TNode(); +} + bool TheoryEngine::properConflict(TNode conflict) const { bool value; if (conflict.getKind() == kind::AND) { @@ -573,7 +590,7 @@ bool TheoryEngine::presolve() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasPresolve) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->presolve(); \ + theoryOf(THEORY)->presolve(); \ if(d_inConflict) { \ return true; \ } \ @@ -597,7 +614,7 @@ void TheoryEngine::postsolve() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasPostsolve) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->postsolve(); \ + theoryOf(THEORY)->postsolve(); \ Assert(! d_inConflict, "conflict raised during postsolve()"); \ } @@ -616,7 +633,7 @@ void TheoryEngine::notifyRestart() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->notifyRestart(); \ + theoryOf(THEORY)->notifyRestart(); \ } // notify each theory using the statement above @@ -630,8 +647,8 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasStaticLearning) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->ppStaticLearn(in, learned); \ + if (theory::TheoryTraits::hasPpStaticLearn) { \ + theoryOf(THEORY)->ppStaticLearn(in, learned); \ } // static learning for each theory using the statement above @@ -1027,16 +1044,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } -void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) { - Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl; - - d_propEngine->checkTime(); - - Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)"); - - d_decisionRequests.push_back(literal); -} - theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType().isComparableTo(b.getType())); if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 609b5195e..9dedc3292 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -172,20 +172,18 @@ class TheoryEngine { public: - IntStat conflicts, propagations, lemmas, propagationsAsDecisions, requirePhase, flipDecision; + IntStat conflicts, propagations, lemmas, requirePhase, flipDecision; Statistics(theory::TheoryId theory): conflicts(mkName("theory<", theory, ">::conflicts"), 0), propagations(mkName("theory<", theory, ">::propagations"), 0), lemmas(mkName("theory<", theory, ">::lemmas"), 0), - propagationsAsDecisions(mkName("theory<", theory, ">::propagationsAsDecisions"), 0), requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), flipDecision(mkName("theory<", theory, ">::flipDecision"), 0) { StatisticsRegistry::registerStat(&conflicts); StatisticsRegistry::registerStat(&propagations); StatisticsRegistry::registerStat(&lemmas); - StatisticsRegistry::registerStat(&propagationsAsDecisions); StatisticsRegistry::registerStat(&requirePhase); StatisticsRegistry::registerStat(&flipDecision); } @@ -194,7 +192,6 @@ class TheoryEngine { StatisticsRegistry::unregisterStat(&conflicts); StatisticsRegistry::unregisterStat(&propagations); StatisticsRegistry::unregisterStat(&lemmas); - StatisticsRegistry::unregisterStat(&propagationsAsDecisions); StatisticsRegistry::unregisterStat(&requirePhase); StatisticsRegistry::unregisterStat(&flipDecision); } @@ -247,13 +244,6 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - void propagateAsDecision(TNode literal) throw(AssertionException) { - Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl; - ++ d_statistics.propagationsAsDecisions; - d_engine->d_outputChannelUsed = true; - d_engine->propagateAsDecision(literal, d_theory); - } - theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; @@ -351,19 +341,6 @@ class TheoryEngine { */ context::CDO d_propagatedLiteralsIndex; - /** - * Decisions that are requested via propagateAsDecision(). The theory - * can only request decisions on nodes that have an assigned litearl in - * the SAT solver and are hence referenced in the SAT solver (making the - * use of TNode safe). - */ - context::CDList d_decisionRequests; - - /** - * The index of the next decision requested by a theory. - */ - context::CDO d_decisionRequestsIndex; - /** * Called by the output channel to propagate literals and facts * @return false if immediate conflict @@ -625,18 +602,7 @@ public: } } - TNode getNextDecisionRequest() { - if(d_decisionRequestsIndex < d_decisionRequests.size()) { - TNode req = d_decisionRequests[d_decisionRequestsIndex]; - Debug("propagateAsDecision") << "TheoryEngine requesting decision[" - << d_decisionRequestsIndex << "]: " - << req << std::endl; - d_decisionRequestsIndex = d_decisionRequestsIndex + 1; - return req; - } else { - return TNode::null(); - } - } + Node getNextDecisionRequest(); bool properConflict(TNode conflict) const; bool properPropagation(TNode lit) const; diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index ce8785f86..efad8beb9 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -9,7 +9,7 @@ typechecker "theory/uf/theory_uf_type_rules.h" instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric -properties check propagate staticLearning presolve +properties check propagate ppStaticLearn presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 70b07daa6..2ee8b6c93 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -941,7 +941,7 @@ void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, Output Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_type << ", cardinality = " << d_cardinality << std::endl; Assert( !cn.isNull() ); if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){ - out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] ); + //out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] ); Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_cardinality_literal[ d_cardinality ]; Debug("uf-ss-prop-as-dec") << " " << d_cardinality_literal[ d_cardinality ][0].getType() << std::endl; } @@ -990,7 +990,7 @@ void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* o //add the appropriate lemma Debug("uf-ss-fmf") << "Set cardinality " << d_type << " = " << c << std::endl; Debug("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << std::endl; - out->propagateAsDecision( lem[0] ); + //out->propagateAsDecision( lem[0] ); d_is_cardinality_requested = true; d_is_cardinality_requested_c = true; //now, require old literal to be decided false -- 2.30.2