projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a4c080) | patch
CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
authorAina Niemetz <aina.niemetz@gmail.com>
Wed, 27 Sep 2017 20:45:27 +0000 (13:45 -0700)
committerGitHub <noreply@github.com>
Wed, 27 Sep 2017 20:45:27 +0000 (13:45 -0700)
commitddbf95c937091b95b742502b760767d757c7cf13
treec15a2fc56226a8aa7cd48f6105f6cca7d349f33etree
parent4a4c0806ef75254f0344978bdfba0f077a1e663acommit | diff
CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)

This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history