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)
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
---------
(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
--------------------
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
{
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
{
/* -------------------------------------------------------------------------- */
/**
- * 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
{
import java.util.Iterator;
import java.util.NoSuchElementException;
+/**
+ * A cvc5 datatype.
+ */
public class Datatype extends AbstractPointer implements Iterable<DatatypeConstructor>
{
// region construction and destruction
import java.util.Iterator;
import java.util.NoSuchElementException;
+/**
+ * A cvc5 datatype constructor.
+ */
public class DatatypeConstructor extends AbstractPointer implements Iterable<DatatypeSelector>
{
// region construction and destruction
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
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
package io.github.cvc5;
+/**
+ * A cvc5 datatype selector.
+ */
public class DatatypeSelector extends AbstractPointer
{
// region construction and destruction
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
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
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
import java.io.IOException;
import java.util.*;
+/**
+ * A cvc5 solver.
+ */
public class Solver implements IPointer, AutoCloseable
{
private long pointer;
import java.util.List;
+/**
+ * The sort of a cvc5 term.
+ */
public class Sort extends AbstractPointer implements Comparable<Sort>
{
// region construction and destruction
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
import java.util.NoSuchElementException;
import java.util.Set;
+/**
+ * A cvc5 Term.
+ */
public class Term extends AbstractPointer implements Comparable<Term>, Iterable<Term>
{
// region construction and destruction
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`.
"""
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`.
"""
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`.
"""
projects / cvc5.git / commitdiff