diff options
Diffstat (limited to 'src/expr/builtin_kinds')
| -rw-r--r-- | src/expr/builtin_kinds | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index bb224aa91..c4eb3af1c 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -17,10 +17,13 @@ # SKOLEM. # # operator K #children ["comment"] +# nonatomic_operator K #children ["comment"] # # Declares a "built-in" operator kind K. Really this is the same # as "variable" except that it has an operator (automatically -# generated by NodeManager). +# generated by NodeManager). These two commands are identical, +# except that kinds declared with nonatomic_operator answer false +# to Node::isAtomic(). # # You can specify an exact # of children required as the second # argument to the operator command. In debug mode, assertions are @@ -109,12 +112,11 @@ theory builtin # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \ +constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ "expr/kind.h" "The kind of nodes representing built-in operators" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" -operator ITE 3 "if-then-else" variable SKOLEM "skolem var" variable VARIABLE "variable" operator TUPLE 2: "a tuple" |