projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 854b81c) | patch
Minor simplifications for datatype selector triggers (#8636)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Apr 2022 19:41:34 +0000 (14:41 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Apr 2022 19:41:34 +0000 (19:41 +0000)
commitcdec9ce9b5ea190344f63423ebed93bea5f95571
tree397bc57502c1f7cd6cbb4a7856dda04704e1ae37tree
parent854b81c30cbd189e89ef143f4a6aae6ac0deb915commit | diff
Minor simplifications for datatype selector triggers (#8636)

This is leftover simplification from the fact that (s x) is no longer expanded to (ite (is-C x) (s_total x) (uf x)).
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/candidate_generator.h diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history