diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
| commit | 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 (patch) | |
| tree | c30f7f17ae963e3f51cef111b2d549eacff1a852 /src/theory/sep | |
| parent | e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 (diff) | |
Add nullary operator metakind.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/kinds | 3 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 2 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep_type_rules.h | 11 |
3 files changed, 14 insertions, 2 deletions
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 358c63f55..b83515d38 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -12,7 +12,7 @@ properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" -variable SEP_NIL "separation nil" +nullaryoperator SEP_NIL "separation nil" operator SEP_EMP 2 "separation empty heap" operator SEP_PTO 2 "points to relation" @@ -25,5 +25,6 @@ typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule typerule SEP_LABEL ::CVC4::theory::sep::SepLabelTypeRule +typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule endtheory diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index ce5c02179..9d064d74d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1226,7 +1226,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ - Node nil = NodeManager::currentNM()->mkUniqueVar( tn, kind::SEP_NIL ); + Node nil = NodeManager::currentNM()->mkNullaryOperator( tn, kind::SEP_NIL ); setNilRef( tn, nil ); return nil; }else{ diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 23e725a25..25166ca8e 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -99,6 +99,17 @@ struct SepLabelTypeRule { } };/* struct SepLabelTypeRule */ +struct SepNilTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::SEP_NIL); + Assert(check); + TypeNode type = n.getType(false); + return type; + } +};/* struct SepLabelTypeRule */ + + }/* CVC4::theory::sep namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |