diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 6e51b55f3..1bd5dc8b7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -130,22 +130,22 @@ bool PropEngine::flipDecision() { } bool PropEngine::isDecision(Node lit) const { - Assert(isTranslatedSatLiteral(lit)); + Assert(isSatLiteral(lit)); return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); } void PropEngine::printSatisfyingAssignment(){ - const CnfStream::TranslationCache& transCache = + const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); Debug("prop-value") << "Literal | Value | Expr" << endl << "----------------------------------------" << "-----------------" << endl; - for(CnfStream::TranslationCache::const_iterator i = transCache.begin(), + for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(), end = transCache.end(); i != end; ++i) { - pair<Node, CnfStream::TranslationInfo> curr = *i; - SatLiteral l = curr.second.literal; + pair<Node, SatLiteral> curr = *i; + SatLiteral l = curr.second; if(!l.isNegated()) { Node n = curr.first; SatValue value = d_satSolver->modelValue(l); @@ -220,10 +220,6 @@ bool PropEngine::isSatLiteral(TNode node) const { return d_cnfStream->hasLiteral(node); } -bool PropEngine::isTranslatedSatLiteral(TNode node) const { - return d_cnfStream->isTranslated(node); -} - bool PropEngine::hasValue(TNode node, bool& value) const { Assert(node.getType().isBoolean()); Assert(d_cnfStream->hasLiteral(node)); |