Add new idiomatic examples (#7912)

diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst
index bc2c9162e172a22a9612e734f6e841598842150a..8d13129074d9b6a06d7970d97d2269532ae812da 100644 (file)
--- a/docs/api/python/z3compat/z3compat.rst
+++ b/docs/api/python/z3compat/z3compat.rst
@@ -7,6 +7,26 @@ z3py compatibility Python API
 
         This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.
 
+
+This API is missing some features from cvc5 and Z3Py.
+
+It does not (currently) support these cvc5 features:
+
+* The theories of strings and sequences
+* unsatisfiable cores
+* syntax-guided synthesis (SyGuS)
+
+It does not support the following features of Z3Py:
+
+* Patterns for quantifier instantiation
+* Pseudo-boolean counting constraints: AtMost, AtLeast, ...
+* Special relation classes: PartialOrder, LinearOrder, ...
+* HTML integration
+* Hooks for user-defined propagation and probing
+* Fixedpoint API
+* Finite domains
+* SMT2 file parsing
+
 .. toctree::
     :maxdepth: 2
 

diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst
index d703d921160b4e6125a1d626971f80710a69a13d..06cc0143a07da48c734f29caa02865fa45e3b207 100644 (file)
--- a/docs/examples/bitvectors.rst
+++ b/docs/examples/bitvectors.rst
@@ -5,5 +5,6 @@ Theory of Bit-Vectors
 .. api-examples::
     <examples>/api/cpp/bitvectors.cpp
     <examples>/api/java/BitVectors.java
+    <z3pycompat>/test/pgms/example_bitvectors.py
     <examples>/api/python/bitvectors.py
     <examples>/api/smtlib/bitvectors.smt2

diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
index 695ba549332802d0b1ee7fb2b2896c71cab5084f..937b16c4a37681db8bda81e146e22090a8ac8b2a 100644 (file)
--- a/docs/examples/bitvectors_and_arrays.rst
+++ b/docs/examples/bitvectors_and_arrays.rst
@@ -5,5 +5,6 @@ Theory of Bit-Vectors and Arrays
 .. api-examples::
     <examples>/api/cpp/bitvectors_and_arrays.cpp
     <examples>/api/java/BitVectorsAndArrays.java
+    <z3pycompat>/test/pgms/example_bitvectors_and_arrays.py
     <examples>/api/python/bitvectors_and_arrays.py
     <examples>/api/smtlib/bitvectors_and_arrays.smt2

diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
index 80e0e5d1b129047ee5f319984ac32462ca0b78d5..5cf8804e5da5a8ec08b9e153e869b5515968134d 100644 (file)
--- a/docs/examples/combination.rst
+++ b/docs/examples/combination.rst
@@ -4,5 +4,6 @@ Theory Combination
 .. api-examples::
     <examples>/api/cpp/combination.cpp
     <examples>/api/java/Combination.java
+    <z3pycompat>/test/pgms/example_combination.py
     <examples>/api/python/combination.py
     <examples>/api/smtlib/combination.smt2

diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index ce26bc3de261153301824ff01b8d9c27adb95ec5..043af2827ef3d381c40f1ebfcf50a416eabfcc53 100644 (file)
--- a/docs/examples/datatypes.rst
+++ b/docs/examples/datatypes.rst
@@ -5,5 +5,6 @@ Theory of Datatypes
 .. api-examples::
     <examples>/api/cpp/datatypes.cpp
     <examples>/api/java/Datatypes.java
+    <z3pycompat>/test/pgms/example_datatypes.py
     <examples>/api/python/datatypes.py
     <examples>/api/smtlib/datatypes.smt2

diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
index 01b3716df767cfd7a8ad605a5fa8bee557527e38..12c775efb60bc95f8df8c0def51c3ed99edc7b15 100644 (file)
--- a/docs/examples/extract.rst
+++ b/docs/examples/extract.rst
@@ -5,5 +5,6 @@ Theory of Bit-Vectors: :code:`extract`
 .. api-examples::
     <examples>/api/cpp/extract.cpp
     <examples>/api/java/Extract.java
+    <z3pycompat>/test/pgms/example_extract.py
     <examples>/api/python/extract.py
     <examples>/api/smtlib/extract.smt2

diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
index f69c99cf8fdd01cdd3b5fd81147fdb7074b2c31c..5f3dd7855cd5b771bad9ee201c8409309c94c3db 100644 (file)
--- a/docs/examples/floatingpoint.rst
+++ b/docs/examples/floatingpoint.rst
@@ -4,4 +4,5 @@ Theory of Floating-Points
 
 .. api-examples::
     <examples>/api/java/FloatingPointArith.java
+    <z3pycompat>/test/pgms/example_floating_point.py
     <examples>/api/python/floating_point.py

diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
index 046ab07a04bd2ae8c0d2355c3e90125bea7e354a..365cfbdea960d0751aeee73393cf4ebc91f79923 100644 (file)
--- a/docs/examples/helloworld.rst
+++ b/docs/examples/helloworld.rst
@@ -7,5 +7,6 @@ We create a solver, declare a Boolean variable and check whether it is entailed
 .. api-examples::
     <examples>/api/cpp/helloworld.cpp
     <examples>/api/java/HelloWorld.java
+    <z3pycompat>/test/pgms/example_helloworld.py
     <examples>/api/python/helloworld.py
     <examples>/api/smtlib/helloworld.smt2

diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst
index 8a58c89b28ead04758d4c784e97d3e96849a9be0..fedd2a342aedd9e3fa2874fa082662e78fc505a5 100644 (file)
--- a/docs/examples/quickstart.rst
+++ b/docs/examples/quickstart.rst
@@ -5,5 +5,6 @@ Quickstart Example
 .. api-examples::
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst
index 384205c63aacfbe8a0cac4c95daafb0c3f88bf59..5625a6397243f4c71880342c419a7d98166857a5 100644 (file)
--- a/docs/examples/sets.rst
+++ b/docs/examples/sets.rst
@@ -5,5 +5,6 @@ Theory of Sets
 .. api-examples::
     <examples>/api/cpp/sets.cpp
     <examples>/api/java/Sets.java
+    <z3pycompat>/test/pgms/example_sets.py
     <examples>/api/python/sets.py
     <examples>/api/smtlib/sets.smt2