diff options
Diffstat (limited to 'src/decision/relevancy.cpp')
-rw-r--r-- | src/decision/relevancy.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index d0d44f606..fe5bdcc20 100644 --- a/src/decision/relevancy.cpp +++ b/src/decision/relevancy.cpp @@ -34,7 +34,7 @@ void Relevancy::setJustified(TNode n) { Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; d_justified.insert(n); - if(d_opt.computeRelevancy) { + if(options::decisionComputeRelevancy()) { d_relevancy[n] = d_maxRelevancy[n]; updateRelevancy(n); } @@ -117,7 +117,7 @@ bool Relevancy::findSplitterRec(TNode node, if(d_polarityCache.find(node) == d_polarityCache.end()) { d_polarityCache[node] = desiredVal; } else { - Assert(d_multipleBacktrace || d_opt.computeRelevancy); + Assert(d_multipleBacktrace || options::decisionComputeRelevancy()); return true; } @@ -289,7 +289,7 @@ bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) { bool ret = false; for(int i = 0; i < n; ++i) { if (findSplitterRec(node[i], desiredVal)) { - if(!d_opt.computeRelevancy) + if(!options::decisionComputeRelevancy()) return true; else ret = true; |