From: Andrew Reynolds Date: Sat, 2 Apr 2022 01:02:47 +0000 (-0500) Subject: Add a few miscellaneous pieces of documentation (#8533) X-Git-Tag: cvc5-1.0.0~45 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=904f7c5524e0a16d29b6c680c5ef4d187cc4cc97;p=cvc5.git Add a few miscellaneous pieces of documentation (#8533) --- diff --git a/docs/api/python/pythonic/pythonic.rst b/docs/api/python/pythonic/pythonic.rst index d5a31a939..db84892a7 100644 --- a/docs/api/python/pythonic/pythonic.rst +++ b/docs/api/python/pythonic/pythonic.rst @@ -12,7 +12,7 @@ This API is missing some features from cvc5 and Z3Py. It does not (currently) support these cvc5 features: -* The theories of strings and sequences +* The theories of strings, sequences and bags * unsatisfiable cores * syntax-guided synthesis (SyGuS) diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 2ba8906e2..d78c13e0a 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -39,9 +39,11 @@ The numbers ``n1 ... nk`` denote the number of type parameters for the datatype, where ``0`` is used for non-parametric datatypes. In addition to declaring symbols for constructors and selectors, the above -command also adds tester (or "discriminator") indexed symbols of the form +command also allows for tester (or "discriminator") indexed symbols of the form ``(_ is C)`` for each constructor ``C``, which are unary predicates which -evaluate to true iff their argument has top-symbol ``C``. +evaluate to true iff their argument has top-symbol ``C``. It also allows for +updater indexed symbols of the form ``(_ update Sij)`` for each selector ``Sij``, +whose semantics are described below. Semantics --------- @@ -109,6 +111,27 @@ Examples (assert (and (= (fname x) "John") (= (lname x) "Smith"))) (check-sat) +Datatype Updaters +-------------------- + +Datatype updaters are a (non-standard) extension available in datatype logics. +The term: + +.. code:: smtlib + ((_ update Sij) t u) + +is equivalent to replacing the field of ``t`` denoted by the selector ``Sij`` +with the value ``u``, or ``t`` itself if that selector does not apply to the +constructor symbol of ``t``. For example, for the list datatype, we have that: + +.. code:: smtlib + ((_ update head) (cons 4 nil) 7) = (cons 7 nil) + ((_ update tail) (cons 4 nil) (cons 5 nil)) = (cons 4 (cons 5 nil)) + ((_ update head) nil 5) = nil + +Note that datatype updaters can be seen as syntax sugar for an if-then-else +term that checks whether the constructor of ``t`` is the same as the one +associated with the given selector. Parametric Datatypes -------------------- diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 6b372b4ce..3470884e1 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1789,7 +1789,8 @@ class DatatypeConstructorIterator; class DatatypeIterator; /** - * A cvc5 datatype constructor declaration. + * A cvc5 datatype constructor declaration. A datatype constructor declaration + * is a specification used for creating a datatype constructor. */ class CVC5_EXPORT DatatypeConstructorDecl { @@ -1877,7 +1878,16 @@ class CVC5_EXPORT DatatypeConstructorDecl class Solver; /** - * A cvc5 datatype declaration. + * A cvc5 datatype declaration. A datatype declaration is not itself a datatype + * (see Datatype), but a specification for creating a datatype sort. + * + * The interface for a datatype declaration coincides with the syntax for the + * SMT-LIB 2.6 command `declare-datatype`, or a single datatype within the + * `declare-datatypes` command. + * + * Datatype sorts can be constructed from DatatypeDecl using the methods: + * - Solver::mkDatatypeSort() + * - Solver::mkDatatypeSorts() */ class CVC5_EXPORT DatatypeDecl { @@ -2629,7 +2639,9 @@ std::ostream& operator<<(std::ostream& out, /* -------------------------------------------------------------------------- */ /** - * A Sygus Grammar. + * A Sygus Grammar. This class can be used to define a context-free grammar + * of terms. Its interface coincides with the definition of grammars + * (``GrammarDef``) in the SyGuS IF 2.1 standard. */ class CVC5_EXPORT Grammar { diff --git a/src/api/java/io/github/cvc5/Datatype.java b/src/api/java/io/github/cvc5/Datatype.java index 06ceaa67f..30d5b8888 100644 --- a/src/api/java/io/github/cvc5/Datatype.java +++ b/src/api/java/io/github/cvc5/Datatype.java @@ -18,6 +18,9 @@ package io.github.cvc5; import java.util.Iterator; import java.util.NoSuchElementException; +/** + * A cvc5 datatype. + */ public class Datatype extends AbstractPointer implements Iterable { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java index c8bff0900..808328946 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java @@ -18,6 +18,9 @@ package io.github.cvc5; import java.util.Iterator; import java.util.NoSuchElementException; +/** + * A cvc5 datatype constructor. + */ public class DatatypeConstructor extends AbstractPointer implements Iterable { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java index b4e755781..6bee8133c 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java @@ -15,6 +15,10 @@ package io.github.cvc5; +/** + * A cvc5 datatype constructor declaration. A datatype constructor declaration + * is a specification used for creating a datatype constructor. + */ public class DatatypeConstructorDecl extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/DatatypeDecl.java b/src/api/java/io/github/cvc5/DatatypeDecl.java index 3c15a049d..aacbed8ab 100644 --- a/src/api/java/io/github/cvc5/DatatypeDecl.java +++ b/src/api/java/io/github/cvc5/DatatypeDecl.java @@ -15,6 +15,18 @@ package io.github.cvc5; +/** + * A cvc5 datatype declaration. A datatype declaration is not itself a datatype + * (see {@link Datatype}), but a specification for creating a datatype sort. + * + * The interface for a datatype declaration coincides with the syntax for the + * SMT-LIB 2.6 command `declare-datatype`, or a single datatype within the + * `declare-datatypes` command. + * + * Datatype sorts can be constructed from DatatypeDecl using the methods: + * - {@link Solver#mkDatatypeSort(DatatypeDecl)} + * - {@link Solver#mkDatatypeSorts(DatatypeDecl[])} + */ public class DatatypeDecl extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/DatatypeSelector.java b/src/api/java/io/github/cvc5/DatatypeSelector.java index 4f64c045c..4978143c9 100644 --- a/src/api/java/io/github/cvc5/DatatypeSelector.java +++ b/src/api/java/io/github/cvc5/DatatypeSelector.java @@ -15,6 +15,9 @@ package io.github.cvc5; +/** + * A cvc5 datatype selector. + */ public class DatatypeSelector extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/Grammar.java b/src/api/java/io/github/cvc5/Grammar.java index 36c6ad789..389fc9177 100644 --- a/src/api/java/io/github/cvc5/Grammar.java +++ b/src/api/java/io/github/cvc5/Grammar.java @@ -15,6 +15,11 @@ package io.github.cvc5; +/** + * A Sygus Grammar. This class can be used to define a context-free grammar + * of terms. Its interface coincides with the definition of grammars + * (``GrammarDef``) in the SyGuS IF 2.1 standard. + */ public class Grammar extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/Op.java b/src/api/java/io/github/cvc5/Op.java index 68a24fb42..30dd50229 100644 --- a/src/api/java/io/github/cvc5/Op.java +++ b/src/api/java/io/github/cvc5/Op.java @@ -15,6 +15,11 @@ package io.github.cvc5; +/** + * A cvc5 operator. + * An operator is a term that represents certain operators, instantiated + * with its required parameters, e.g., a term of kind {@link Kind#BITVECTOR_EXTRACT}. + */ public class Op extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/Result.java b/src/api/java/io/github/cvc5/Result.java index 7607e6276..e66f07d46 100644 --- a/src/api/java/io/github/cvc5/Result.java +++ b/src/api/java/io/github/cvc5/Result.java @@ -18,6 +18,9 @@ package io.github.cvc5; import java.util.HashMap; import java.util.Map; +/** + * Encapsulation of a three-valued solver result, with explanations. + */ public class Result extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 908e90dc5..ccff49870 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -19,6 +19,9 @@ import io.github.cvc5.modes.BlockModelsMode; import java.io.IOException; import java.util.*; +/** + * A cvc5 solver. + */ public class Solver implements IPointer, AutoCloseable { private long pointer; diff --git a/src/api/java/io/github/cvc5/Sort.java b/src/api/java/io/github/cvc5/Sort.java index a5d4a539a..8c00a41e6 100644 --- a/src/api/java/io/github/cvc5/Sort.java +++ b/src/api/java/io/github/cvc5/Sort.java @@ -17,6 +17,9 @@ package io.github.cvc5; import java.util.List; +/** + * The sort of a cvc5 term. + */ public class Sort extends AbstractPointer implements Comparable { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/SynthResult.java b/src/api/java/io/github/cvc5/SynthResult.java index b94951d93..d7e611e67 100644 --- a/src/api/java/io/github/cvc5/SynthResult.java +++ b/src/api/java/io/github/cvc5/SynthResult.java @@ -15,6 +15,16 @@ package io.github.cvc5; +/** + * Encapsulation of a solver synth result. + * + * This is the return value of the API methods: + * - {@link Solver#checkSynth()} + * - {@link Solver#checkSynthNext()} + * + * which we call synthesis queries. This class indicates whether the + * synthesis query has a solution, has no solution, or is unknown. + */ public class SynthResult extends AbstractPointer { // region construction and destruction diff --git a/src/api/java/io/github/cvc5/Term.java b/src/api/java/io/github/cvc5/Term.java index a60b11427..9ab394cd3 100644 --- a/src/api/java/io/github/cvc5/Term.java +++ b/src/api/java/io/github/cvc5/Term.java @@ -23,6 +23,9 @@ import java.util.List; import java.util.NoSuchElementException; import java.util.Set; +/** + * A cvc5 Term. + */ public class Term extends AbstractPointer implements Comparable, Iterable { // region construction and destruction diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 65d699193..f39b9cf04 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -365,7 +365,8 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: """ - A cvc5 datatype constructor declaration. + A cvc5 datatype constructor declaration. A datatype constructor + declaration is a specification used for creating a datatype constructor. Wrapper class for :cpp:class:`cvc5::DatatypeConstructorDecl`. """ @@ -421,7 +422,19 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: """ - A cvc5 datatype declaration. + A cvc5 datatype declaration. A datatype declaration is not itself a + datatype (see :py:class:`cvc5.Datatype`), but a specification for creating a datatype + sort. + + The interface for a datatype declaration coincides with the syntax for + the SMT-LIB 2.6 command `declare-datatype`, or a single datatype within + the `declare-datatypes` command. + + Datatype sorts can be constructed from :py:class:`DatatypeDecl` using + the methods: + + - :py:meth:`Solver.mkDatatypeSort()` + - :py:meth:`Solver.mkDatatypeSorts()` Wrapper class for :cpp:class:`cvc5::DatatypeDecl`. """ @@ -594,7 +607,9 @@ cdef class Op: cdef class Grammar: """ - A Sygus Grammar. + A Sygus Grammar. This class can be used to define a context-free grammar + of terms. Its interface coincides with the definition of grammars + (``GrammarDef``) in the SyGuS IF 2.1 standard. Wrapper class for :cpp:class:`cvc5::Grammar`. """