From d8cb3b8695ac70146a0801553afeda6b2c93458f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 3 Jun 2021 17:07:05 -0700 Subject: [PATCH] docs: Migrate datatypes theory reference. (#6662) This migrates https://cvc4.github.io/datatypes. --- docs/_static/custom.css | 11 ++ docs/conf.py.in | 6 + docs/ext/smtliblexer.py | 71 +++++++++++ docs/index.rst | 1 + docs/theories/datatypes.rst | 229 ++++++++++++++++++++++++++++++++++++ docs/theory.rst | 7 ++ 6 files changed, 325 insertions(+) create mode 100644 docs/ext/smtliblexer.py create mode 100644 docs/theories/datatypes.rst create mode 100644 docs/theory.rst diff --git a/docs/_static/custom.css b/docs/_static/custom.css index 23aa6c36d..a5403c295 100644 --- a/docs/_static/custom.css +++ b/docs/_static/custom.css @@ -76,3 +76,14 @@ a:hover, a:focus { color: #ace600; } +.highlight .o { + color: #ac7339; +} + +.highlight .k { + color: #2980b9; +} + +.highlight .m { + color: #ba2121; +} diff --git a/docs/conf.py.in b/docs/conf.py.in index 6a23ff759..65e880bc9 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -12,6 +12,7 @@ # import sys + # add path to enable extensions sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/') @@ -74,3 +75,8 @@ cpp_index_common_prefix = ["cvc5::api::"] # where to look for include-build-file ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}'] + +# -- SMT-LIB syntax highlighting --------------------------------------------- +from smtliblexer import SmtLibLexer +from sphinx.highlighting import lexers +lexers['smtlib'] = SmtLibLexer() diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py new file mode 100644 index 000000000..5dd54d006 --- /dev/null +++ b/docs/ext/smtliblexer.py @@ -0,0 +1,71 @@ +from pygments.lexer import RegexLexer +from pygments import token + +class SmtLibLexer(RegexLexer): + + name = 'smtlib' + + tokens = { + 'root': [ + (r'QF_BV', token.Text), + (r'QF_UFDT', token.Text), + (r'ALL_SUPPORTED', token.Text), + (r'set-logic', token.Keyword), + (r'set-option', token.Keyword), + (r'declare-codatatypes', token.Keyword), + (r'declare-const', token.Keyword), + (r'declare-datatypes', token.Keyword), + (r'declare-fun', token.Keyword), + (r'define-fun', token.Keyword), + (r'assert\b', token.Keyword), + (r'check-sat-assuming', token.Keyword), + (r'check-sat', token.Keyword), + (r'exit', token.Keyword), + (r'get-model', token.Keyword), + (r'get-unsat-assumptions', token.Keyword), + (r'get-unsat-core', token.Keyword), + (r'push', token.Keyword), + (r'pop', token.Keyword), + (r'as', token.Name.Attribute), + (r':incremental', token.Name.Attribute), + (r':named', token.Name.Attribute), + (r':produce-models', token.Name.Attribute), + (r':produce-unsat-cores', token.Name.Attribute), + (r':produce-unsat-assumptions', token.Name.Attribute), + (r'!', token.Name.Attribute), + (r'BitVec', token.Name.Attribute), + (r'RNE', token.Name.Attribute), + (r'Tuple', token.Name.Attribute), + (r'true', token.String), + (r'distinct', token.Operator), + (r'=', token.Operator), + (r'>', token.Operator), + (r'and', token.Operator), + (r'bvadd', token.Operator), + (r'bvashr', token.Operator), + (r'bvmul', token.Operator), + (r'bvugt', token.Operator), + (r'bvult', token.Operator), + (r'bvule', token.Operator), + (r'bvsdiv', token.Operator), + (r'extract', token.Operator), + (r'fp.gt', token.Operator), + (r'ite', token.Operator), + (r'mkTuple', token.Operator), + (r'to_fp_unsigned', token.Operator), + (r'\+zero', token.Operator), + (r'#b[0-1]+', token.Text), + (r'bv[0-9]+', token.Text), + (r'".*?"', token.String), + (r'[a-zA-Z][a-zA-Z0-9]*', token.Name), + (r'[0-9]+', token.Number), + (r'\s', token.Text), + (r'\(_', token.Text), + (r'\(', token.Text), + (r'\)', token.Text), + (r';.*$', token.Comment), + (r'\.\.\.', token.Text) + ] + } + + diff --git a/docs/index.rst b/docs/index.rst index 956ddcc29..5f0ede34f 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -19,5 +19,6 @@ Table of Contents api/api examples/examples languages + theory references genindex diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst new file mode 100644 index 000000000..7dd0e8713 --- /dev/null +++ b/docs/theories/datatypes.rst @@ -0,0 +1,229 @@ +Theory Reference: Datatypes +=========================== + +Logic +----- + +To enable cvc5's decision procedure for datatypes, include ``DT`` in the logic: + +.. code:: smtlib + + (set-logic QF_UFDT) + +Alternatively, use the ``ALL`` logic: + +.. code:: smtlib + + (set-logic ALL) + +Syntax +------ + +cvc5 supports the following syntax for declaring mutually recursive blocks of +datatypes in ``*.smt2`` input files in the smt lib 2.6 format: + +.. code:: smtlib + + (declare-datatypes ((D1 n1) ... (Dk nk)) + (((C1 (S1 T1) ... (Si Ti)) ... (Cj ... )) + ... + ((...) ... (...))) + +where ``D1 ... Dk`` are datatype types, ``C1 ... Cj`` are the constructors for +datatype ``D1``, +``S1 ... Si`` are the selectors (or "destructors") of constructor ``C1``, and +each ``T1 ... Ti`` is a previously declared type or one of ``D1 ... Dk``. +The symbols ``U1 ... Un`` are type parameters (fresh symbols). +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 +``(_ is C)`` for each constructor ``C``, which are unary predicates which +evaluate to true iff their argument has top-symbol ``C``. + +Semantics +--------- + +The decision procedure for inductive datatypes can be found +`here `__. + +Example Declarations +-------------------- + +An enumeration: + +.. code:: smtlib + + (declare-datatypes ((Color 0)) + (((Red) (Black)))) + +A List of ``Int`` with ``cons`` and ``nil`` as constructors: + +.. code:: smtlib + + (declare-datatypes ((list 0)) + (((cons (head Int) (tail list)) (nil)))) + +A parametric List of T's: + +.. code:: smtlib + + (declare-datatypes ((list 1)) + ((par (T) ((cons (head T) (tail (list T))) (nil))))) + +Mutual recursion: + +.. code:: smtlib + + (declare-datatypes ((list 0) (tree 0)) + (((cons (head tree) (tail list)) (nil)) + ((node (data Int) (children list))))) + +A (non-recursive) record type: + +.. code:: smtlib + + (declare-datatypes ((record 0)) + (((rec (fname String) (lname String) (id Int))))) + + +Examples +-------- + +.. code:: smtlib + + (declare-datatypes ((list 0)) + (((cons (head Int) (tail list)) (nil)))) + (declare-const a list) + (declare-const b list) + (assert (and (= (tail a) b) (not ((_ is nil) b)) (> (head b) 0))) + (check-sat) + +.. code:: smtlib + + (declare-datatypes ((record 0)) + (((rec (fname String) (lname String) (id Int))))) + (declare-const x record) + (assert (and (= (fname x) "John") (= (lname x) "Smith"))) + (check-sat) + + +Parametric Datatypes +-------------------- + +Instances of parametric datatypes must have their arguments instantiated with +concrete types. For instance, in the example: + +.. code:: smtlib + + (declare-datatypes ((list 1)) ((par (T) (cons (head T) (tail (list T))) (nil)))) + +To declare a list of ``Int``, use the command: + +.. code:: smtlib + + (declare-const f (list Int)) + +Use of constructors that are ambiguously typed must be cast to a concrete type, +for instance all occurrences of ``nil`` for the above datatype must be cast with +the syntax: + +.. code:: smtlib + + (as nil (list Int)) + +Tuples +------ + +Tuples are a particular instance of an inductive datatype. cvc5 supports +special syntax for tuples as an extension of the SMT-LIB version 2 format. +For example: + +.. code:: smtlib + + (declare-const t (Tuple Int Int)) + (assert (= ((_ tupSel 0) t) 3)) + (assert (not (= t (mkTuple 3 4)))) + + +Codatatypes +----------- + +cvc5 also supports co-inductive datatypes, as described +`here `__. + +The syntax for declaring mutually recursive coinductive datatype blocks is +identical to inductive datatypes, except that ``declare-datatypes`` is replaced +by ``declare-codatatypes``. For example, the following declares the type denote +streams of ``Int``: + +.. code:: smtlib + + (declare-codatatypes ((stream 0)) + (((cons (head Int) (tail stream))))) + + +Syntax/API +---------- + +For the C++ API examples in the table below, we assume that we have created +a `cvc5::api::Solver solver` object. + ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Logic String | ``(set-logic QF_DT)`` | ``solver.setLogic("QF_DT");`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tuple Sort | ``(Tuple , ..., )`` | ``std::vector sorts = { ... };`` | +| | | | +| | | ``Sort s = solver.mkTupleSort(sorts);`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| | ``(declare-const t (tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | +| | | | +| | | ``Sort s = solver.mkTypleSort({s_int, s_int});`` | +| | | | +| | | ``Term t = solver.mkConst(s, "t");`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tuple Constructor | ``(mkTuple , ..., )`` | ``Sort s = solver.mkTypleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getConstructor();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tuple Selector | ``((_ tupSel i) t)`` | ``Sort s = solver.mkTypleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getSelector();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Record Sort | n/a | ``Sort s = mkRecordSort(const std::vector>& fields);`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| | n/a | ``std::vector> fields;`` | +| | | | +| | | ``fields.push_back(std::pair("fst", solver.getIntegerSort()));`` | +| | | | +| | | ``fields.push_back(std::pair("snd", solver.getIntegerSort()));`` | +| | | | +| | | ``Sort s = mkRecordSort(fields);`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Record Constructor | n/a | ``Sort s = mkRecordSort(fields);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getConstructor();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Record Selector | n/a | ``Sort s = mkRecordSort(fields);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getSelector();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {s, , ..., });`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ diff --git a/docs/theory.rst b/docs/theory.rst new file mode 100644 index 000000000..45be41b2e --- /dev/null +++ b/docs/theory.rst @@ -0,0 +1,7 @@ +Theory References +================= + +.. toctree:: + :maxdepth: 1 + + theories/datatypes -- 2.30.2