diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/rewriterules/kinds | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/rewriterules/kinds')
-rw-r--r-- | src/theory/rewriterules/kinds | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds new file mode 100644 index 000000000..01fbda51e --- /dev/null +++ b/src/theory/rewriterules/kinds @@ -0,0 +1,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 "generale 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 |