diff options
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 */ |