summaryrefslogtreecommitdiff
path: root/src/theory/fp/fp_converter.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/fp_converter.h')
-rw-r--r--src/theory/fp/fp_converter.h5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 9900c2987..d589eff60 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -300,7 +300,10 @@ class FpConverter
/** Adds a node to the conversion, returns the converted node */
Node convert(TNode);
- /** Gives the node representing the value of a given variable */
+ /**
+ * Gives the node representing the value of a word-blasted variable.
+ * Returns a null node if it has not been word-blasted.
+ */
Node getValue(Valuation&, TNode);
context::CDList<Node> d_additionalAssertions;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback