summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/context/cdqueue.h2
-rw-r--r--src/theory/arith/kinds2
-rw-r--r--src/theory/arrays/kinds2
-rw-r--r--src/theory/arrays/theory_arrays.cpp16
-rw-r--r--src/theory/arrays/theory_arrays.h5
-rw-r--r--src/theory/builtin/kinds5
-rwxr-xr-xsrc/theory/mktheorytraits41
-rw-r--r--src/theory/output_channel.h18
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp2
-rw-r--r--src/theory/theory.h6
-rw-r--r--src/theory/theory_engine.cpp47
-rw-r--r--src/theory/theory_engine.h38
-rw-r--r--src/theory/uf/kinds2
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp4
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<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;
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
@@ -108,24 +108,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
@@ -560,6 +560,12 @@ public:
}
/**
+ * 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
* ::operator<< or ::append()) to the "learned" builder---it should
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<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; \
} \
@@ -392,7 +390,7 @@ void TheoryEngine::combineTheories() {
#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
@@ -456,7 +454,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
#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
@@ -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<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) {
@@ -573,7 +590,7 @@ bool TheoryEngine::presolve() {
#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; \
} \
@@ -597,7 +614,7 @@ void TheoryEngine::postsolve() {
#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()"); \
}
@@ -616,7 +633,7 @@ void TheoryEngine::notifyRestart() {
#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
@@ -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<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
@@ -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;
@@ -352,19 +342,6 @@ class TheoryEngine {
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
*/
@@ -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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback