Improve java documentation: add QuickStart and a java API overview.
:maxdepth: 1
C++ API <cpp/cpp>
- Java API <java/index>
+ Java API <java/java>
Python API <python/python>
--- /dev/null
+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 <quickstart>` gives a short introduction,
+and more examples can be found `here <../../examples/examples.html>`_.
+
+
+For most applications, the `Solver <io/github/cvc5/api/Solver.html>`_ class is the main entry point to cvc5.
+The class hierarchy of `cvc5 package <io/github/cvc5/api/package-summary.html>`_
+provides more details on the individual classes.
+
+.. toctree::
+ :hidden:
+
+ quickstart
+ API documentation <index>
+
+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 <io/github/cvc5/api/package-summary.html>`_
+^^^^^^^^^^^^^^^
+
+ * class `Datatype <io/github/cvc5/api/Datatype.html>`_
+ * class `DatatypeConstructor <io/github/cvc5/api/DatatypeConstructor.html>`_
+ * class `DatatypeConstructorDecl <io/github/cvc5/api/DatatypeConstructorDecl.html>`_
+ * class `DatatypeDecl <io/github/cvc5/api/DatatypeDecl.html>`_
+ * class `DatatypeSelector <io/github/cvc5/api/DatatypeSelector.html>`_
+ * class `Grammar <io/github/cvc5/api/Grammar.html>`_
+ * class `Op <io/github/cvc5/api/Op.html>`_
+ * class `OptionInfo <io/github/cvc5/api/OptionInfo.html>`_
+ * class `Pair<K,V> <io/github/cvc5/api/Pair.html>`_
+ * class `Result <io/github/cvc5/api/Result.html>`_
+ * class `Solver <io/github/cvc5/api/Solver.html>`_
+ * class `Sort <io/github/cvc5/api/Sort.html>`_
+ * class `Stat <io/github/cvc5/api/Stat.html>`_
+ * class `Statistics <io/github/cvc5/api/Statistics.html>`_
+ * class `Term <io/github/cvc5/api/Term.html>`_
+ * class `Triplet<A,B,C> <io/github/cvc5/api/Triplet.html>`_
+ * class `Utils <io/github/cvc5/api/Utils.html>`_
+ * enum `Kind <io/github/cvc5/api/Kind.html>`_
+ * enum `Result.UnknownExplanation <io/github/cvc5/api/Result.UnknownExplanation.html>`_
+ * enum `RoundingMode <io/github/cvc5/api/RoundingMode.html>`_
+ * exception `CVC5ApiException <io/github/cvc5/api/CVC5ApiException.html>`_
+ * exception `CVC5ApiOptionException <io/github/cvc5/api/CVC5ApiOptionException.html>`_
+ * exception `CVC5ApiRecoverableException <io/github/cvc5/api/CVC5ApiRecoverableException.html>`_
--- /dev/null
+Quickstart Guide
+================
+
+First, create a cvc5 `Solver <io/github/cvc5/api/Solver.html>`_
+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 <io/github/cvc5/api/Result.html#isSat()>`_,
+`Result.isUnsat <io/github/cvc5/api/Result.html#isUnsat()>`_ and
+`Result.isSatUnknown <io/github/cvc5/api/Result.html#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 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
+| The source code for this example can be found at `examples/api/java/QuickStart.java <https://github.com/cvc5/cvc5/blob/master/examples/api/java/QuickStart.java>`_.
+
+.. api-examples::
+ <examples>/api/java/QuickStart.java
+ <examples>/api/cpp/quickstart.cpp
+ <examples>/api/python/quickstart.py
+ <examples>/api/smtlib/quickstart.smt2
Term xMinusY = solver.mkTerm(Kind.MINUS, x, y);
Term xMinusYVal = solver.getValue(xMinusY);
- // Further, we can convert the values to java types,
- Pair<BigInteger, BigInteger> xRational = xVal.getRealValue();
- Pair<BigInteger, BigInteger> 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<BigInteger, BigInteger> xPair = xVal.getRealValue();
+ Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
+ Pair<BigInteger, BigInteger> 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<BigInteger, BigInteger> 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.
projects / cvc5.git / commitdiff