diff --git a/docs/theories/finite_field.rst b/docs/theories/finite_field.rst index bd3aadb893e..08a76bac5ab 100644 --- 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 ^^^^^^^