diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-09 14:47:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 07:25:13 -0500 |
commit | 50c26544c83a71e87efa487e4af063b1b5647c0f (patch) | |
tree | 82d4f3b2632a2cf06aff70550f37f80dc80d9543 /src/util | |
parent | 53b8499f48a00dc876d56c76fbc79aafe5803529 (diff) |
add new theory (sets)
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/emptyset.cpp | 12 | ||||
-rw-r--r-- | src/util/emptyset.h | 65 |
3 files changed, 79 insertions, 0 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 1d6ce1a73..0717df907 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -87,6 +87,8 @@ libutil_la_SOURCES = \ abstract_value.cpp \ array_store_all.h \ array_store_all.cpp \ + emptyset.h \ + emptyset.cpp \ model.h \ model.cpp \ sort_inference.h \ diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp new file mode 100644 index 000000000..fa1bb8f10 --- /dev/null +++ b/src/util/emptyset.cpp @@ -0,0 +1,12 @@ +#include "util/emptyset.h" +#include <iostream> + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { + return out << "emptyset(" << asa.getType() << ')'; +} + +}/* CVC4 namespace */ diff --git a/src/util/emptyset.h b/src/util/emptyset.h new file mode 100644 index 000000000..aae08e43b --- /dev/null +++ b/src/util/emptyset.h @@ -0,0 +1,65 @@ + +#include "cvc4_public.h" + +#pragma once + +namespace CVC4 { + // messy; Expr needs ArrayStoreAll (because it's the payload of a + // CONSTANT-kinded expression), and ArrayStoreAll needs Expr. + class CVC4_PUBLIC EmptySet; +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" +#include <iostream> + +namespace CVC4 { + +class CVC4_PUBLIC EmptySet { + + const SetType d_type; + +public: + + EmptySet() { } /* Null typed */ + EmptySet(SetType t):d_type(t) { } + + + ~EmptySet() throw() { + } + + SetType getType() const { return d_type; } + + bool operator==(const EmptySet& asa) const throw() { + return d_type == asa.d_type; + } + bool operator!=(const EmptySet& asa) const throw() { + return !(*this == asa); + } + + bool operator<(const EmptySet& asa) const throw() { + return d_type < asa.d_type; + } + bool operator<=(const EmptySet& asa) const throw() { + return d_type <= asa.d_type; + } + bool operator>(const EmptySet& asa) const throw() { + return !(*this <= asa); + } + bool operator>=(const EmptySet& asa) const throw() { + return !(*this < asa); + } + + +};/* class EmptySet */ + +std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC; + +struct CVC4_PUBLIC EmptySetHashFunction { + inline size_t operator()(const EmptySet& asa) const { + return TypeHashFunction()(asa.getType()); + } +};/* struct EmptysetHashFunction */ + + +} |