diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-20 20:00:22 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 18:11:56 -0400 |
| commit | 1a41e26473ff12108eb6700da3d386ffa9e731bd (patch) | |
| tree | 0bd5e31740d2c3a7c89a0a7e663b734b98982e79 /src/theory/booleans | |
| parent | 75ec455661ecc88a8b9f77f7b913c227b7f3e728 (diff) | |
Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.
Diffstat (limited to 'src/theory/booleans')
| -rw-r--r-- | src/theory/booleans/kinds | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 4d748ca59..ad45e3cbb 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -22,19 +22,19 @@ constant CONST_BOOLEAN \ bool \ ::CVC4::BoolHashFunction \ "util/bool.h" \ - "truth and falsity" + "truth and falsity; payload is a (C++) bool" enumerator BOOLEAN_TYPE \ "::CVC4::theory::booleans::BooleanEnumerator" \ "theory/booleans/type_enumerator.h" operator NOT 1 "logical not" -operator AND 2: "logical and" -operator IFF 2 "logical equivalence" -operator IMPLIES 2 "logical implication" -operator OR 2: "logical or" -operator XOR 2 "exclusive or" -operator ITE 3 "if-then-else" +operator AND 2: "logical and (N-ary)" +operator IFF 2 "logical equivalence (exactly two parameters)" +operator IMPLIES 2 "logical implication (exactly two parameters)" +operator OR 2: "logical or (N-ary)" +operator XOR 2 "exclusive or (exactly two parameters)" +operator ITE 3 "if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort" typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule |