From 6f8f56513c93eef7be4e55e97e4b08a0eaadea7f Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Mon, 6 Dec 2021 19:31:47 -0600 Subject: [PATCH] Add documentation for QuickStart.java (#7730) Improve java documentation: add QuickStart and a java API overview. --- docs/api/api.rst | 2 +- docs/api/java/java.rst | 83 +++++++++++++ docs/api/java/quickstart.rst | 191 ++++++++++++++++++++++++++++++ examples/api/java/QuickStart.java | 31 ++++- 4 files changed, 301 insertions(+), 6 deletions(-) create mode 100644 docs/api/java/java.rst create mode 100644 docs/api/java/quickstart.rst diff --git a/docs/api/api.rst b/docs/api/api.rst index 727caea4d..a5dbdf421 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -10,5 +10,5 @@ Additionally, a more pythonic Python API is availble at https://github.com/cvc5/ :maxdepth: 1 C++ API - Java API + Java API Python API diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst new file mode 100644 index 000000000..b15148ff3 --- /dev/null +++ b/docs/api/java/java.rst @@ -0,0 +1,83 @@ +Java API Documentation +====================== + +The Java API for cvc5 mostly mirrors the :doc:`C++ API <../cpp/cpp>` and supports operator +overloading, iterators, and exceptions. +There are a few differences from the C++ API, such as using arbitrary-precision integer pairs, +specifically, pairs of Java `BigInteger` objects, to represent rational numbers. +The :doc:`quickstart guide ` gives a short introduction, +and more examples can be found `here <../../examples/examples.html>`_. + + +For most applications, the `Solver `_ class is the main entry point to cvc5. +The class hierarchy of `cvc5 package `_ +provides more details on the individual classes. + +.. toctree:: + :hidden: + + quickstart + API documentation + +Building cvc5 Java API +^^^^^^^^^^^^^^^^^^^^^^ + +.. code-block:: bash + + $ git clone https://github.com/cvc5/cvc5 + $ cd cvc5 + $ ./configure.sh production --java-bindings --auto-download --prefix=build/install + $ cd build + $ make + $ make install + + $ ls install/lib + cmake libcvc5jni.so libcvc5parser.so libcvc5parser.so.1 libcvc5.so + libpicpoly.a libpicpolyxx.a libpoly.so libpoly.so.0 libpoly.so.0.1.9 + libpolyxx.so libpolyxx.so.0 libpolyxx.so.0.1.9 objects-Production + $ ls install/share/java/ + cvc5-0.0.5-dev.jar cvc5.jar + + # compile example QuickStart.java with cvc5 jar file + $ javac -cp "install/share/java/cvc5.jar" ../examples/api/java/QuickStart.java -d . + + # run example QuickStart with cvc5 jar file and cvc5 shared libraries + $ java -cp "install/share/java/cvc5.jar:." "-Djava.library.path=install/lib" QuickStart + expected: sat + result: sat + value for x: 1/6 + value for y: 1/6 + expected: unsat + result: unsat + unsat core size: 3 + unsat core: + (< 0 a) + (< 0 b) + (< (+ a b) 1) + +`Package io.github.cvc5.api `_ +^^^^^^^^^^^^^^^ + + * class `Datatype `_ + * class `DatatypeConstructor `_ + * class `DatatypeConstructorDecl `_ + * class `DatatypeDecl `_ + * class `DatatypeSelector `_ + * class `Grammar `_ + * class `Op `_ + * class `OptionInfo `_ + * class `Pair `_ + * class `Result `_ + * class `Solver `_ + * class `Sort `_ + * class `Stat `_ + * class `Statistics `_ + * class `Term `_ + * class `Triplet `_ + * class `Utils `_ + * enum `Kind `_ + * enum `Result.UnknownExplanation `_ + * enum `RoundingMode `_ + * exception `CVC5ApiException `_ + * exception `CVC5ApiOptionException `_ + * exception `CVC5ApiRecoverableException `_ diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst new file mode 100644 index 000000000..2c986ab55 --- /dev/null +++ b/docs/api/java/quickstart.rst @@ -0,0 +1,191 @@ +Quickstart Guide +================ + +First, create a cvc5 `Solver `_ +instance using try with resources: + +.. code-block:: java + + try (Solver solver = new Solver()) + { + /** write your code here */ + } + +To produce models and unsat cores, we have to enable the following options. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 32-33 + :dedent: 6 + +Next we set the logic. +The simplest way to set a logic for the solver is to choose ``"ALL"``. +This enables all logics in the solver. +Alternatively, ``"QF_ALL"`` enables all logics without quantifiers. +To optimize the solver's behavior for a more specific logic, +use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 42 + :dedent: 6 + +In the following, we will define real and integer constraints. +For this, we first query the solver for the corresponding sorts. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 46-47 + :dedent: 6 + +Now, we create two constants ``x`` and ``y`` of sort ``Real``, +and two constants ``a`` and ``b`` of sort ``Integer``. +Notice that these are *symbolic* constants, not actual values. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 52-55 + :dedent: 6 + +We define the following constraints regarding ``x`` and ``y``: + +.. math:: + + (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y) + +We construct the required terms and assert them as follows: + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 65-89 + :dedent: 6 + +Now we check if the asserted formula is satisfiable, that is, we check if +there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all +the constraints. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 93 + :dedent: 6 + +The result we get from this satisfiability check is either ``sat``, ``unsat`` +or ``unknown``. +It's status can be queried via +`Result.isSat `_, +`Result.isUnsat `_ and +`Result.isSatUnknown `_. +Alternatively, it can also be printed. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 97-98 + :dedent: 6 + +This will print: + +.. code:: text + + expected: sat + result: sat + +Now, we query the solver for the values for ``x`` and ``y`` that satisfy +the constraints. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 101-102 + :dedent: 6 + +It is also possible to get values for terms that do not appear in the original +formula. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 106-107 + :dedent: 6 + +We can convert these values to Java types. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 109-116 + :dedent: 6 + +Another way to independently compute the value of ``x - y`` would be to +perform the (rational) arithmetic manually. +However, for more complex terms, it is easier to let the solver do the +evaluation. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 122-134 + :dedent: 6 + +This will print: + +.. code:: text + + computed correctly + +Next, we will check satisfiability of the same formula, +only this time over integer variables ``a`` and ``b``. +For this, we first reset the assertions added to the solver. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 140 + :dedent: 6 + +Next, we assert the same assertions as above, but with integers. +This time, we inline the construction of terms +in the assertion command. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 145-149 + :dedent: 6 + +Now, we check whether the revised assertion is satisfiable. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 152-156 + :dedent: 6 + +This time the asserted formula is unsatisfiable: + +.. code:: text + + expected: unsat + result: unsat + +We can query the solver for an unsatisfiable core, that is, a subset +of the assertions that is already unsatisfiable. + +.. literalinclude:: ../../../examples/api/java/QuickStart.java + :language: java + :lines: 160-166 + :dedent: 6 + +This will print: + +.. code:: text + + unsat core size: 3 + unsat core: + (< 0 a) + (< 0 b) + (< (+ a b) 1) + +Example +------- + +| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. +| The source code for this example can be found at `examples/api/java/QuickStart.java `_. + +.. api-examples:: + /api/java/QuickStart.java + /api/cpp/quickstart.cpp + /api/python/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java index a79263cbf..c815278cc 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -106,11 +106,32 @@ public class QuickStart Term xMinusY = solver.mkTerm(Kind.MINUS, x, y); Term xMinusYVal = solver.getValue(xMinusY); - // Further, we can convert the values to java types, - Pair xRational = xVal.getRealValue(); - Pair yRational = yVal.getRealValue(); - System.out.println("value for x: " + xRational.first + "/" + xRational.second); - System.out.println("value for y: " + yRational.first + "/" + yRational.second); + // Further, we can convert the values to java types + Pair xPair = xVal.getRealValue(); + Pair yPair = yVal.getRealValue(); + Pair xMinusYPair = xMinusYVal.getRealValue(); + + System.out.println("value for x: " + xPair.first + "/" + xPair.second); + System.out.println("value for y: " + yPair.first + "/" + yPair.second); + System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second); + + // Another way to independently compute the value of x - y would be + // to perform the (rational) arithmetic manually. + // However, for more complex terms, + // it is easier to let the solver do the evaluation. + Pair xMinusYComputed = + new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)), + xPair.second.multiply(yPair.second)); + BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second); + xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g)); + if (xMinusYComputed.equals(xMinusYPair)) + { + System.out.println("computed correctly"); + } + else + { + System.out.println("computed incorrectly"); + } // Next, we will check satisfiability of the same formula, // only this time over integer variables a and b. -- 2.30.2