diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
commit | bb59480a36fb0f799af53676c07b8fca43c2fff4 (patch) | |
tree | 555fb1210e2e94ba09bb9dd447cac30a6ad2ab70 /src/theory/valuation.cpp | |
parent | 5cb65d8beac0f06fcafbef99d109c09ad029b14d (diff) |
Sharing work
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) { |