sets api example

2 files changed, 110 insertions, 13 deletions

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index 3508f9900..a1455d168 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -6,18 +6,19 @@ AM_CXXFLAGS = -Wall
 AM_CFLAGS = -Wall
 
 noinst_PROGRAMS = \
-	linear_arith \
-	helloworld \
-	combination \
 	bitvectors \
 	bitvectors_and_arrays \
-	datatypes
+	combination \
+	datatypes \
+	helloworld \
+	linear_arith \
+	sets
 
 noinst_DATA =
 
-linear_arith_SOURCES = \
-	linear_arith.cpp
-linear_arith_LDADD = \
+bitvectors_SOURCES = \
+	bitvectors.cpp
+bitvectors_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
 bitvectors_and_arrays_SOURCES = \
@@ -30,6 +31,11 @@ combination_SOURCES = \
 combination_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
+datatypes_SOURCES = \
+	datatypes.cpp
+datatypes_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
 helloworld_SOURCES = \
 	helloworld.cpp
 helloworld_CXXFLAGS = \
@@ -37,14 +43,14 @@ helloworld_CXXFLAGS = \
 helloworld_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
-bitvectors_SOURCES = \
-	bitvectors.cpp
-bitvectors_LDADD = \
+linear_arith_SOURCES = \
+	linear_arith.cpp
+linear_arith_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
-datatypes_SOURCES = \
-	datatypes.cpp
-datatypes_LDADD = \
+sets_SOURCES = \
+	sets.cpp
+sets_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
 # for installation
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
new file mode 100644
index 000000000..79168e06a
--- /dev/null
+++ b/examples/api/sets.cpp
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file sets.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Reasoning about sets with CVC4.
+ **
+ ** A simple demonstration of reasoning about sets with CVC4.
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "smt/smt_engine.h"
+
+using namespace std;
+using namespace CVC4;
+
+int main() {
+  ExprManager em;
+  SmtEngine smt(&em);
+
+  // Produce models
+  smt.setOption("produce-models", true);
+
+  // Set output language to SMTLIB2
+  cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+  
+  Type integer = em.integerType();
+  Type set = em.mkSetType(integer);
+
+  // Verify union distributions over intersection
+  // (A union B) intersection C = (A intersection C) union (B intersection C)
+  {
+    Expr A = em.mkVar("A", set);
+    Expr B = em.mkVar("B", set);
+    Expr C = em.mkVar("C", set);
+
+    Expr unionAB = em.mkExpr(kind::UNION, A, B);
+    Expr lhs = em.mkExpr(kind::INTERSECTION, unionAB, C);
+
+    Expr intersectionAC = em.mkExpr(kind::INTERSECTION, A, C);
+    Expr intersectionBC = em.mkExpr(kind::INTERSECTION, B, C);
+    Expr rhs = em.mkExpr(kind::UNION, intersectionAC, intersectionBC);
+
+    Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs);
+
+    cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+  }
+
+  // Verify emptset is a subset of any set
+  {
+    Expr A = em.mkVar("A", set);
+    Expr emptyset = em.mkConst(EmptySet(set));
+
+    Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A);
+
+    cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+  }
+
+  // Find me an element in {1, 2} intersection {2, 3}, if there is one.
+  {
+    Expr one = em.mkConst(Rational(1));
+    Expr two = em.mkConst(Rational(2));
+    Expr three = em.mkConst(Rational(3));
+
+    Expr singleton_one = em.mkExpr(kind::SINGLETON, one);
+    Expr singleton_two = em.mkExpr(kind::SINGLETON, two);
+    Expr singleton_three = em.mkExpr(kind::SINGLETON, three);
+    Expr one_two = em.mkExpr(kind::UNION, singleton_one, singleton_two);
+    Expr two_three = em.mkExpr(kind::UNION, singleton_two, singleton_three);
+    Expr intersection = em.mkExpr(kind::INTERSECTION, one_two, two_three);
+
+    Expr x = em.mkVar("x", integer);
+
+    Expr e = em.mkExpr(kind::MEMBER, x, intersection);
+
+    Result result = smt.checkSat(e);
+    cout << "CVC4 reports: " << e << " is " << result << "." << endl;
+
+    if(result == Result::SAT) {
+      cout << "For instance, " << smt.getValue(x) << " is a member." << endl;
+    }
+  }
+}