blob: 490c8f1003950b41fded712b2670158fc3d13e5d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_REWRITERULES ::CVC4::theory::rewriterules::TheoryRewriteRules "theory/rewriterules/theory_rewriterules.h"
typechecker "theory/rewriterules/theory_rewriterules_type_rules.h"
rewriter ::CVC4::theory::rewriterules::TheoryRewriterulesRewriter "theory/rewriterules/theory_rewriterules_rewriter.h"
properties check
# Theory content goes here.
# constants...
# types...
sort RRHB_TYPE \
Cardinality::INTEGERS \
not-well-founded \
"head and body of the rule type"
# operators...
# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
operator REWRITE_RULE 3 "general rewrite rule"
#HEAD/BODY/TRIGGER
operator RR_REWRITE 2:3 "actual rewrite rule"
operator RR_REDUCTION 2:3 "actual reduction rule"
operator RR_DEDUCTION 2:3 "actual deduction rule"
typerule REWRITE_RULE ::CVC4::theory::rewriterules::RewriteRuleTypeRule
typerule RR_REWRITE ::CVC4::theory::rewriterules::RRRewriteTypeRule
typerule RR_REDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
typerule RR_DEDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
endtheory
|
