diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:03 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:20 -0600 |
| commit | d73fdfe7e1fe071670a7e5f843c7609db290b63e (patch) | |
| tree | ff8ad52565f6a149689668f74957292486b2eeab /src/theory/sep | |
| parent | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (diff) | |
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/kinds | 8 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep_type_rules.h | 8 |
2 files changed, 0 insertions, 16 deletions
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 5cd9093f4..358c63f55 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -12,13 +12,6 @@ properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" -# constants -constant SEP_NIL_REF \ - ::CVC4::NilRef \ - ::CVC4::NilRefHashFunction \ - "expr/sepconst.h" \ - "the nil reference constant; payload is an instance of the CVC4::NilRef class" - variable SEP_NIL "separation nil" operator SEP_EMP 2 "separation empty heap" @@ -27,7 +20,6 @@ operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" operator SEP_LABEL 2 "separation label (internal use only)" -typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 7d4eb303e..23e725a25 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -25,14 +25,6 @@ namespace CVC4 { namespace theory { namespace sep { -class SepNilRefTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - return TypeNode::fromType( n.getConst<NilRef>().getType() ); - } -}; - class SepEmpTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |