ff: document ff.bitsum (cvc5#10734)

ajreynol · May 8, 2024 · 231c532 · 231c532
1 parent d0a9b54
commit 231c532
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/docs/theories/finite_field.rst b/docs/theories/finite_field.rst
@@ -99,6 +99,16 @@ Examples
   (check-sat)
   ; unsat
 
+
+Experimental Extensions
+^^^^^^^^^^^^^^^^^^^^^^^
+
+These features of the theory are experimental; they may be removed in the
+future:
+
+* ``ff.bitsum``: an n-ary operator for bitsums: ``(ff.bitsum x0 x1 x2)`` is equivalent to :math:`x_0 + 2x_1 + 4x_2`.
+* ``ff.neg``: unary negation
+
 Solvers
 ^^^^^^^