From 226244a0bdb68655c06d6d1b55b31be013bf7fa6 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 9 Jun 2021 13:44:13 -0700
Subject: 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.
---
 examples/api/cpp/sets.cpp          |  2 +-
 examples/api/smtlib/relations.smt2 | 41 ++++++++++++++++++++++++++++++++++++++
 examples/api/smtlib/sets.smt2      | 34 +++++++++++++++++++++++++++++++
 3 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 examples/api/smtlib/relations.smt2
 create mode 100644 examples/api/smtlib/sets.smt2

(limited to 'examples')

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))))
+  )
+)
-- 
cgit v1.2.3