diff options
Diffstat (limited to 'src/theory/valuation.h')
| -rw-r--r-- | src/theory/valuation.h | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 58615f481..f819eff9d 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking, barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -57,7 +57,15 @@ public: Node getSatValue(TNode n) const; /** - * Returns true if the node has a sat value. If yes value is set to it's value. + * Returns true if the node has a current SAT assignment. If yes, the + * argument "value" is set to its value. + * + * This is only permitted if n is a theory atom that has an associated + * SAT literal. + * + * @return true if the literal has a current assignment, and returns the + * value in the "value" argument; otherwise false and the "value" + * argument is unmodified. */ bool hasSatValue(TNode n, bool& value) const; |