From 226244a0bdb68655c06d6d1b55b31be013bf7fa6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 9 Jun 2021 13:44:13 -0700 Subject: [PATCH] docs: Migrate sets and relations theory reference. (#6698) This migrates page https://cvc4.github.io/sets-and-relations. It further adds the SMT2 version of examples/api/cpp/sets.cpp and adds test/regress/regress0/rels/relations-ops.smt2 as smtlib example for relations. --- docs/examples/examples.rst | 3 +- docs/examples/relations.rst | 7 + docs/examples/sets.rst | 1 + docs/ext/examples.py | 2 +- docs/ext/smtliblexer.py | 30 +++- docs/theories/datatypes.rst | 2 +- docs/theories/sets-and-relations.rst | 201 +++++++++++++++++++++++++++ docs/theory.rst | 1 + examples/api/cpp/sets.cpp | 2 +- examples/api/smtlib/relations.smt2 | 41 ++++++ examples/api/smtlib/sets.smt2 | 34 +++++ 11 files changed, 315 insertions(+), 9 deletions(-) create mode 100644 docs/examples/relations.rst create mode 100644 docs/theories/sets-and-relations.rst create mode 100644 examples/api/smtlib/relations.smt2 create mode 100644 examples/api/smtlib/sets.smt2 diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index 528566a3e..5e17d524b 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -16,10 +16,11 @@ For every example, the same problem is constructed and solved using different in datatypes floatingpoint lineararith + relations sequences sets strings combination sygus-fun sygus-grammar - sygus-inv \ No newline at end of file + sygus-inv diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst new file mode 100644 index 000000000..d94fa0aa7 --- /dev/null +++ b/docs/examples/relations.rst @@ -0,0 +1,7 @@ +Theory of Relations +=================== + + +.. api-examples:: + ../../examples/api/smtlib/relations.smt2 + diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index 71a6843c3..b0f1fc1da 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -5,3 +5,4 @@ Theory of Sets .. api-examples:: ../../examples/api/cpp/sets.cpp ../../examples/api/python/sets.py + ../../examples/api/smtlib/sets.smt2 diff --git a/docs/ext/examples.py b/docs/ext/examples.py index 003726de4..9f8f7294e 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -22,7 +22,7 @@ class APIExamples(Directive): '.cpp': {'title': 'C++', 'lang': 'c++'}, '.java': {'title': 'Java', 'lang': 'java'}, '.py': {'title': 'Python', 'lang': 'python'}, - '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'}, + '.smt2': {'title': 'SMT-LIBv2', 'lang': 'smtlib'}, } # The "arguments" are actually the content of the directive diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 2ce860e39..e796e2404 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -7,10 +7,11 @@ class SmtLibLexer(RegexLexer): tokens = { 'root': [ - (r'QF_BV', token.Text), - (r'QF_UFDT', token.Text), (r'ALL', token.Text), (r'QF_ALL', token.Text), + (r'QF_BV', token.Text), + (r'QF_UFDT', token.Text), + (r'QF_UFLIAFS', token.Text), (r'set-info', token.Keyword), (r'set-logic', token.Keyword), (r'set-option', token.Keyword), @@ -38,13 +39,19 @@ class SmtLibLexer(RegexLexer): (r':produce-unsat-assumptions', token.Name.Attribute), (r':status', token.Name.Attribute), (r'!', token.Name.Attribute), + (r'Array', token.Name.Attribute), (r'BitVec', token.Name.Attribute), + (r'Int', token.Name.Attribute), (r'RNE', token.Name.Attribute), + (r'Set', token.Name.Attribute), + (r'String', token.Name.Attribute), (r'Tuple', token.Name.Attribute), + (r'tupSel', token.Name.Attribute), (r'true', token.String), (r'distinct', token.Operator), (r'=', token.Operator), (r'>', token.Operator), + (r'\*', token.Operator), (r'and', token.Operator), (r'bvadd', token.Operator), (r'bvashr', token.Operator), @@ -53,14 +60,29 @@ class SmtLibLexer(RegexLexer): (r'bvult', token.Operator), (r'bvule', token.Operator), (r'bvsdiv', token.Operator), + (r'card', token.Operator), (r'emp', token.Operator), + (r'emptyset', token.Operator), + (r'exists', token.Operator), (r'extract', token.Operator), + (r'forall', token.Operator), (r'fp.gt', token.Operator), + (r'insert', token.Operator), + (r'intersection', token.Operator), (r'ite', token.Operator), + (r'member', token.Operator), (r'mkTuple', token.Operator), - (r'to_fp_unsigned', token.Operator), + (r'not', token.Operator), + (r'product', token.Operator), (r'pto', token.Operator), (r'sep', token.Operator), + (r'singleton', token.Operator), + (r'subset', token.Operator), + (r'tclosure', token.Operator), + (r'to_fp_unsigned', token.Operator), + (r'transpose', token.Operator), + (r'union', token.Operator), + (r'univset', token.Operator), (r'wand', token.Operator), (r'\+zero', token.Operator), (r'#b[0-1]+', token.Text), @@ -76,5 +98,3 @@ class SmtLibLexer(RegexLexer): (r'\.\.\.', token.Text) ] } - - diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 7dd0e8713..5f02a8bf8 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -179,7 +179,7 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Sort s = solver.mkTupleSort(sorts);`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ -| | ``(declare-const t (tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | +| | ``(declare-const t (Tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | | | | | | | | ``Sort s = solver.mkTypleSort({s_int, s_int});`` | | | | | diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst new file mode 100644 index 000000000..79838334f --- /dev/null +++ b/docs/theories/sets-and-relations.rst @@ -0,0 +1,201 @@ +Theory Reference: Sets and Relations +==================================== + +Finite Sets +----------- + +cvc5 supports the theory of finite sets. +The simplest way to get a sense of the syntax is to look at an example: + +.. api-examples:: + ../../examples/api/cpp/sets.cpp + ../../examples/api/python/sets.py + ../../examples/api/smtlib/sets.smt2 + +The source code of these examples is available at: + +* `SMT-LIB 2 language example `__ +* `C++ API example `__ +* `Python API example `__ + + +Below is a short summary of the sorts, constants, functions and +predicates. For more details, see +`this paper at IJCAR 2016 `__. + +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 | append `FS` for finite sets | append `FS` for finite sets | +| | | | +| | ``(set-logic QF_UFLIAFS)`` | ``solver.setLogic("QF_UFLIAFS");`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Sort | ``(Set )`` | ``solver.mkSetSort(cvc5::api::Sort elementSort);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Constants | ``(declare-const X (Set Int)`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Union | ``(union X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::UNION, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Intersection | ``(setminus X Y)`` | ``Term t = solver.mkTerm(Kind::SETMINUS, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Membership | ``(member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::MEMBER, x, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Subset | ``(subset X Y)`` | ``Term t = solver.mkTerm(Kind::SUBSET, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Emptyset | ``(as emptyset (Set Int)`` | ``Term t = solver.mkEmptySet(s);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Singleton Set | ``(singleton 1)`` | ``Term t = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(1));`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Cardinality | ``(card X)`` | ``Term t = solver.mkTerm(Kind::CARD, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Insert / Finite Sets | ``(insert 1 2 3 (singleton 4))`` | ``Term one = solver.mkInteger(1);`` | +| | | | +| | | ``Term two = solver.mkInteger(2);`` | +| | | | +| | | ``Term three = solver.mkInteger(3);`` | +| | | | +| | | ``Term sgl = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(4));``| +| | | | +| | | ``Term t = solver.mkTerm(Kind::INSERT, {one, two, three, sgl});`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Complement | ``(complement X)`` | ``Term t = solver.mkTerm(Kind::COMPLEMENT, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Universe Set | ``(as univset (Set Int))`` | ``Term t = solver.mkUniverseSet(s);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ + + +Semantics +^^^^^^^^^ + +The semantics of most of the above operators (e.g., set union, intersection, +difference) are straightforward. +The semantics for the universe set and complement are more subtle and explained +in the following. + +The universe set ``(as univset (Set T))`` is *not* interpreted as the set +containing all elements of sort ``T``. +Instead it may be interpreted as any set such that all sets of sort ``(Set T)`` +are interpreted as subsets of it. +In other words, it is the union of the interpretations of all (finite) sets in +our input. + +For example: + +.. code:: smtlib + + (declare-fun x () (Set Int)) + (declare-fun y () (Set Int)) + (declare-fun z () (Set Int)) + (assert (member 0 x)) + (assert (member 1 y)) + (assert (= z (as univset (Set Int)))) + (check-sat) + +Here, a possible model is: + +.. code:: smtlib + + (define-fun x () (singleton 0)) + (define-fun y () (singleton 1)) + (define-fun z () (union (singleton 1) (singleton 0))) + +Notice that the universe set in this example is interpreted the same as ``z``, +and is such that all sets in this example (``x``, ``y``, and ``z``) are subsets +of it. + +The set complement operator for ``(Set T)`` is interpreted relative to the +interpretation of the universe set for ``(Set T)``, and not relative to the set +of all elements of sort ``T``. +That is, for all sets ``X`` of sort ``(Set T)``, the complement operator is +such that ``(= (complement X) (setminus (as univset (Set T)) X))`` +holds in all models. + +The motivation for these semantics is to ensure that the universe set for sort +``T`` and applications of set complement can always be interpreted as a finite +set in (quantifier-free) inputs, even if the cardinality of ``T`` is infinite. +Above, notice that we were able to find a model for the universe set of sort +``(Set Int)`` that contained two elements only. + +.. note:: + In the presence of quantifiers, cvc5's implementation of the above theory + allows infinite sets. + In particular, the following formula is SAT (even though cvc5 is not able to + say this): + + .. code:: smtlib + + (set-logic ALL) + (declare-fun x () (Set Int)) + (assert (forall ((z Int) (member (* 2 z) x))) + (check-sat) + + The reason for that is that making this formula (and similar ones) `unsat` is + counter-intuitive when quantifiers are present. + +Finite Relations +---------------- + +Example: + +.. api-examples:: + ../../examples/api/smtlib/relations.smt2 + +For reference, below is a short summary of the sorts, constants, functions and +predicates. +For more details, see +`this paper at CADE 2017 `__. + ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Logic String | ``(set-logic QF_ALL)`` | ``solver.setLogic("QF_ALL");`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| 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});`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Reation Sort | ``(Set (Tuple , ..., ))`` | ``Sort s = solver.mkSetSort(cvc5::api::Sort tupleSort);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Constants | ``(declare-const X (Set (Tuple Int Int)`` | ``Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Transpose | ``(transpose X)`` | ``Term t = solver.mkTerm(Kind::TRANSPOSE, X);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Transitive Closure | ``(tclosure X)`` | ``Term t = solver.mkTerm(Kind::TCLOSURE, X);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Join | ``(join X Y)`` | ``Term t = solver.mkTerm(Kind::JOIN, X, Y);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Product | ``(product X Y)`` | ``Term t = solver.mkTerm(Kind::PRODUCT, X, Y);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ diff --git a/docs/theory.rst b/docs/theory.rst index f0b25aea4..2d2a949d5 100644 --- a/docs/theory.rst +++ b/docs/theory.rst @@ -6,3 +6,4 @@ Theory References theories/datatypes theories/separation-logic + theories/sets-and-relations diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index 5c9652707..c1eded4a4 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about sets with CVC4. + * A simple demonstration of reasoning about sets with cvc5. */ #include diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2 new file mode 100644 index 000000000..11801a868 --- /dev/null +++ b/examples/api/smtlib/relations.smt2 @@ -0,0 +1,41 @@ +(set-logic ALL) +(set-info :status sat) + +(declare-fun r1 () (Set (Tuple String Int))) +(declare-fun r2 () (Set (Tuple Int String))) +(declare-fun r () (Set (Tuple String String))) +(declare-fun s () (Set (Tuple String String))) +(declare-fun t () (Set (Tuple String Int Int String))) +(declare-fun lt1 () (Set (Tuple Int Int))) +(declare-fun lt2 () (Set (Tuple Int Int))) +(declare-fun i () Int) + +(assert + (= r1 + (insert + (mkTuple "a" 1) + (mkTuple "b" 2) + (mkTuple "c" 3) + (singleton (mkTuple "d" 4))))) +(assert + (= r2 + (insert + (mkTuple 1 "1") + (mkTuple 2 "2") + (mkTuple 3 "3") + (singleton (mkTuple 17 "17"))))) +(assert (= r (join r1 r2))) +(assert (= s (transpose r))) +(assert (= t (product r1 r2))) +(assert + (= + lt1 + (insert + (mkTuple 1 2) + (mkTuple 2 3) + (mkTuple 3 4) + (singleton (mkTuple 4 5))))) +(assert (= lt2 (tclosure lt1))) +(assert (= i (card t))) + +(check-sat) diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2 new file mode 100644 index 000000000..437c285e2 --- /dev/null +++ b/examples/api/smtlib/sets.smt2 @@ -0,0 +1,34 @@ +(set-logic QF_UFLIAFS) +(set-option :produce-models true) +(set-option :incremental true) +(declare-const A (Set Int)) +(declare-const B (Set Int)) +(declare-const C (Set Int)) +(declare-const x Int) + +; Verify union distributions over intersection +(check-sat-assuming + ( + (distinct + (intersection (union A B) C) + (union (intersection A C) (intersection B C))) + ) +) + +; Verify emptset is a subset of any set +(check-sat-assuming + ( + (not (subset (as emptyset (Set Int)) A)) + ) +) + +; Find an element in {1, 2} intersection {2, 3}, if there is one. +(check-sat-assuming + ( + (member + x + (intersection + (union (singleton 1) (singleton 2)) + (union (singleton 2) (singleton 3)))) + ) +) -- 2.30.2