summaryrefslogtreecommitdiff
path: root/src/theory/booleans
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/booleans')
-rw-r--r--src/theory/booleans/kinds14
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback