diff options
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 43 |
1 files changed, 42 insertions, 1 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 148b95632..627125a27 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -24,6 +24,38 @@ namespace CVC4 { namespace theory { +bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) { + switch (s1) { + case EQUALITY_TRUE: + case EQUALITY_TRUE_IN_MODEL: + case EQUALITY_TRUE_AND_PROPAGATED: + switch (s2) { + case EQUALITY_TRUE: + case EQUALITY_TRUE_IN_MODEL: + case EQUALITY_TRUE_AND_PROPAGATED: + return true; + default: + return false; + } + break; + case EQUALITY_FALSE: + case EQUALITY_FALSE_IN_MODEL: + case EQUALITY_FALSE_AND_PROPAGATED: + switch (s2) { + case EQUALITY_FALSE: + case EQUALITY_FALSE_IN_MODEL: + case EQUALITY_FALSE_AND_PROPAGATED: + return true; + default: + return false; + } + break; + default: + return false; + } +} + + Node Valuation::getValue(TNode n) const { return d_engine->getValue(n); } @@ -47,7 +79,16 @@ Node Valuation::getSatValue(TNode n) const { } bool Valuation::hasSatValue(TNode n, bool& value) const { - return d_engine->getPropEngine()->hasValue(n, value); + Node normalized = Rewriter::rewrite(n); + if (d_engine->getPropEngine()->isSatLiteral(normalized)) { + return d_engine->getPropEngine()->hasValue(normalized, value); + } else { + return false; + } +} + +EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) { + return d_engine->getEqualityStatus(a, b); } Node Valuation::ensureLiteral(TNode n) { |