}
/**
- * 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");
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"
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"
d_sharedOther(c),
d_sharedTerms(c, false),
d_reads(c),
+ d_decisionRequests(c),
d_permRef(c)
{
StatisticsRegistry::registerStat(&d_numRow);
Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
}
-
void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
// 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
}
+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();
private:
public:
+ Node getNextDecisionRequest();
+
void presolve();
void shutdown() { }
context::CDList<TNode> d_reads;
std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
+ // The decision requests we have for the core
+ context::CDQueue<Node> d_decisionRequests;
+
// List of nodes that need permanent references in this context
context::CDList<Node> d_permRef;
# 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
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"
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"
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
*/
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.)
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;
}
}
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
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),
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \
+ theoryOf(THEORY)->check(effort); \
if (d_inConflict) { \
break; \
} \
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
+ theoryOf(THEORY)->getCareGraph(careGraph); \
}
// Call on each parametric theory to give us its care graph
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \
+ theoryOf(THEORY)->propagate(effort); \
}
// Propagate for each theory using the statement above
}
}
+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<THEORY>::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) {
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasPresolve) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->presolve(); \
+ theoryOf(THEORY)->presolve(); \
if(d_inConflict) { \
return true; \
} \
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->postsolve(); \
+ theoryOf(THEORY)->postsolve(); \
Assert(! d_inConflict, "conflict raised during postsolve()"); \
}
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \
+ theoryOf(THEORY)->notifyRestart(); \
}
// notify each theory using the statement above
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->ppStaticLearn(in, learned); \
+ if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
+ theoryOf(THEORY)->ppStaticLearn(in, learned); \
}
// static learning for each theory using the statement above
}
-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)) {
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);
}
StatisticsRegistry::unregisterStat(&conflicts);
StatisticsRegistry::unregisterStat(&propagations);
StatisticsRegistry::unregisterStat(&lemmas);
- StatisticsRegistry::unregisterStat(&propagationsAsDecisions);
StatisticsRegistry::unregisterStat(&requirePhase);
StatisticsRegistry::unregisterStat(&flipDecision);
}
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;
*/
context::CDO<unsigned> 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<TNode> d_decisionRequests;
-
- /**
- * The index of the next decision requested by a theory.
- */
- context::CDO<unsigned> d_decisionRequestsIndex;
-
/**
* Called by the output channel to propagate literals and facts
* @return false if immediate conflict
}
}
- 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;
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"
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;
}
//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
projects / cvc5.git / commitdiff