From 4010df600a43165491fccfc0917a0d9e6f551d49 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 28 Apr 2015 20:13:42 +0200
Subject: [PATCH] doc: Be a little more detailed about smt-cvc4-q
---
doc/options.rst | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/doc/options.rst b/doc/options.rst
index 873bfeef1..f55fa74fe 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -144,8 +144,16 @@ These options are available by all Leon components:
* ``smt-z3-q``
- Z3 through SMT-LIB, but (recursive) functions are encoded with universal
- quantification, and inductive reasoning happens within the solver.
+ Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
+ instead encoded with universal quantification.
+ For example, ``def foo(x:A) = e`` would be encoded by asserting
+
+ .. math::
+
+ \forall (x:A). foo(x) = e
+
+ even if ``e`` contains an invocation to ``foo``.
+
Currently, this solver does not handle higher-order functions.
* ``unrollz3``
--
GitLab