summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-07-12 08:35:03 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-07-12 08:50:58 -0500
commit360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch)
tree9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/theory/uf
parentd6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff)
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/theory_uf_type_rules.h3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index a3c775a2a..c31de403c 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -45,8 +45,7 @@ class UfTypeRule {
++argument_it, ++argument_type_it) {
TypeNode currentArgument = (*argument_it).getType();
TypeNode currentArgumentType = *argument_type_it;
- if (!currentArgument.isComparableTo(currentArgumentType)) {
- //if (!currentArgument.isSubtypeOf(currentArgumentType)) { //FIXME:typing
+ if (!currentArgument.isSubtypeOf(currentArgumentType)) {
std::stringstream ss;
ss << "argument type is not a subtype of the function's argument "
<< "type:\n"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback