From e8a14a4051212860cfc2cec195e9a297984fde0f Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Jan 2022 16:49:02 -0800 Subject: [PATCH] Add new idiomatic examples (#7912) --- docs/api/python/z3compat/z3compat.rst | 20 ++++++++++++++++++++ docs/examples/bitvectors.rst | 1 + docs/examples/bitvectors_and_arrays.rst | 1 + docs/examples/combination.rst | 1 + docs/examples/datatypes.rst | 1 + docs/examples/extract.rst | 1 + docs/examples/floatingpoint.rst | 1 + docs/examples/helloworld.rst | 1 + docs/examples/quickstart.rst | 1 + docs/examples/sets.rst | 1 + 10 files changed, 29 insertions(+) diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst index bc2c9162e..8d1312907 100644 --- 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 d703d9211..06cc0143a 100644 --- a/docs/examples/bitvectors.rst +++ b/docs/examples/bitvectors.rst @@ -5,5 +5,6 @@ Theory of Bit-Vectors .. api-examples:: /api/cpp/bitvectors.cpp /api/java/BitVectors.java + /test/pgms/example_bitvectors.py /api/python/bitvectors.py /api/smtlib/bitvectors.smt2 diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst index 695ba5493..937b16c4a 100644 --- 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:: /api/cpp/bitvectors_and_arrays.cpp /api/java/BitVectorsAndArrays.java + /test/pgms/example_bitvectors_and_arrays.py /api/python/bitvectors_and_arrays.py /api/smtlib/bitvectors_and_arrays.smt2 diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst index 80e0e5d1b..5cf8804e5 100644 --- a/docs/examples/combination.rst +++ b/docs/examples/combination.rst @@ -4,5 +4,6 @@ Theory Combination .. api-examples:: /api/cpp/combination.cpp /api/java/Combination.java + /test/pgms/example_combination.py /api/python/combination.py /api/smtlib/combination.smt2 diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index ce26bc3de..043af2827 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -5,5 +5,6 @@ Theory of Datatypes .. api-examples:: /api/cpp/datatypes.cpp /api/java/Datatypes.java + /test/pgms/example_datatypes.py /api/python/datatypes.py /api/smtlib/datatypes.smt2 diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst index 01b3716df..12c775efb 100644 --- a/docs/examples/extract.rst +++ b/docs/examples/extract.rst @@ -5,5 +5,6 @@ Theory of Bit-Vectors: :code:`extract` .. api-examples:: /api/cpp/extract.cpp /api/java/Extract.java + /test/pgms/example_extract.py /api/python/extract.py /api/smtlib/extract.smt2 diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst index f69c99cf8..5f3dd7855 100644 --- a/docs/examples/floatingpoint.rst +++ b/docs/examples/floatingpoint.rst @@ -4,4 +4,5 @@ Theory of Floating-Points .. api-examples:: /api/java/FloatingPointArith.java + /test/pgms/example_floating_point.py /api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 046ab07a0..365cfbdea 100644 --- 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:: /api/cpp/helloworld.cpp /api/java/HelloWorld.java + /test/pgms/example_helloworld.py /api/python/helloworld.py /api/smtlib/helloworld.smt2 diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst index 8a58c89b2..fedd2a342 100644 --- a/docs/examples/quickstart.rst +++ b/docs/examples/quickstart.rst @@ -5,5 +5,6 @@ Quickstart Example .. api-examples:: /api/cpp/quickstart.cpp /api/java/QuickStart.java + /test/pgms/example_quickstart.py /api/python/quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index 384205c63..5625a6397 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -5,5 +5,6 @@ Theory of Sets .. api-examples:: /api/cpp/sets.cpp /api/java/Sets.java + /test/pgms/example_sets.py /api/python/sets.py /api/smtlib/sets.smt2 -- 2.30.2