summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--docs/examples/examples.rst3
-rw-r--r--docs/examples/relations.rst7
-rw-r--r--docs/examples/sets.rst1
-rw-r--r--docs/ext/examples.py2
-rw-r--r--docs/ext/smtliblexer.py30
-rw-r--r--docs/theories/datatypes.rst2
-rw-r--r--docs/theories/sets-and-relations.rst201
-rw-r--r--docs/theory.rst1
-rw-r--r--examples/api/cpp/sets.cpp2
-rw-r--r--examples/api/smtlib/relations.smt241
-rw-r--r--examples/api/smtlib/sets.smt234
11 files changed, 315 insertions, 9 deletions
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 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/sets.smt2>`__
+* `C++ API example <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/sets.cpp>`__
+* `Python API example <https://github.com/cvc5/cvc5/blob/master/examples/api/python/sets.cpp>`__
+
+
+Below is a short summary of the sorts, constants, functions and
+predicates. For more details, see
+`this paper at IJCAR 2016 <https://cvc4.github.io/publications/2016/BRBT16.pdf>`__.
+
+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 <Sort>)`` | ``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 <https://cvc4.github.io/publications/2017/MRT+17.pdf>`__.
+
++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
+| | SMTLIB language | C++ API |
++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
+| Logic String | ``(set-logic QF_ALL)`` | ``solver.setLogic("QF_ALL");`` |
++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
+| Tuple Sort | ``(Tuple <Sort_1>, ..., <Sort_n>)`` | ``std::vector<cvc5::api::Sort> 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 <Term_1>, ..., <Term_n>)`` | ``Sort s = solver.mkTypleSort(sorts);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term c = dt[0].getConstructor();`` |
+| | | |
+| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
+| 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_1>, ..., <Sort_n>))`` | ``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 <cvc5/cvc5.h>
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))))
+ )
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback