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/kinds | |
| parent | e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 (diff) | |
Add nullary operator metakind.
Diffstat (limited to 'src/theory/sep/kinds')
| -rw-r--r-- | src/theory/sep/kinds | 3 |
1 files changed, 2 insertions, 1 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 |