Introduce template classes for simple type rules (#2835)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sun, 29 Sep 2019 03:18:22 +0000 (20:18 -0700)
committerGitHub <noreply@github.com>
Sun, 29 Sep 2019 03:18:22 +0000 (20:18 -0700)
commitd06cf394473cbe09c2e1acc333526c41a6dd9687
treecec81c5557fdcf0e144da5a275471e92063e4e45
parente25f99329c9905c67a565481dcb0d6a4499a7557
Introduce template classes for simple type rules (#2835)

This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:

- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)
src/expr/type_checker_template.cpp
src/expr/type_checker_util.h [new file with mode: 0644]
src/theory/arith/kinds
src/theory/arith/theory_arith_type_rules.h
src/theory/bv/kinds
src/theory/bv/theory_bv_type_rules.h
src/theory/strings/kinds
src/theory/strings/theory_strings_type_rules.h