Monday tasks:
[cvc5.git] / src / theory / booleans / kinds
1 # kinds -*- sh -*-
2 #
3 # For documentation on this file format, please refer to
4 # src/theory/builtin/kinds.
5 #
6
7 theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
8
9 properties finite
10
11 rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
12
13 sort BOOLEAN_TYPE \
14 2 \
15 well-founded \
16 "NodeManager::currentNM()->mkConst(false)" \
17 "expr/node_manager.h" \
18 "Boolean type"
19
20 constant CONST_BOOLEAN \
21 bool \
22 ::CVC4::BoolHashStrategy \
23 "util/bool.h" \
24 "truth and falsity"
25
26 operator NOT 1 "logical not"
27 operator AND 2: "logical and"
28 operator IFF 2 "logical equivalence"
29 operator IMPLIES 2 "logical implication"
30 operator OR 2: "logical or"
31 operator XOR 2 "exclusive or"
32 operator ITE 3 "if-then-else"
33
34 endtheory