projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad61299) | patch
Make candidate rewrite match filtering handle polymorphic operators properly (#2236)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Aug 2018 06:31:14 +0000 (01:31 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 1 Aug 2018 06:31:14 +0000 (23:31 -0700)
commitdef4b45fa41ddf128ab0b2e8f6bb3b8454974008
treee39c3ca613d328f09985b2c0d3d25fd6679d2f68tree
parentad61299aa24a83f935daedab32440d25006e18bbcommit | diff
Make candidate rewrite match filtering handle polymorphic operators properly (#2236)

Currently, the discrimination tree index used for candidate rewrite rule filtering based on matching does not properly distinguish polymorphic operators, which leads to type errors. This makes the index handle them correctly.

Fixes #1923.
src/theory/quantifiers/candidate_rewrite_filter.cpp diff | blob | history
src/theory/quantifiers/candidate_rewrite_filter.h diff | blob | history
src/theory/quantifiers/dynamic_rewrite.cpp diff | blob | history
src/theory/quantifiers/dynamic_rewrite.h diff | blob | history