summaryrefslogtreecommitdiff
path: root/src/theory/booleans/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/booleans/kinds')
-rw-r--r--src/theory/booleans/kinds11
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index d540d57f5..5580418e5 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -5,6 +5,7 @@
#
theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
+typechecker "theory/booleans/theory_bool_type_rules.h"
properties finite
@@ -31,4 +32,14 @@ operator OR 2: "logical or"
operator XOR 2 "exclusive or"
operator ITE 3 "if-then-else"
+typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule
+
+typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
+typerule AND ::CVC4::theory::boolean::BooleanTypeRule
+typerule IFF ::CVC4::theory::boolean::BooleanTypeRule
+typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
+typerule OR ::CVC4::theory::boolean::BooleanTypeRule
+typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
+typerule ITE ::CVC4::theory::boolean::IteTypeRule
+
endtheory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback