projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3153e2d) | patch
Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remov...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Oct 2017 13:51:05 +0000 (08:51 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Oct 2017 13:51:05 +0000 (08:51 -0500)
commit0f34a6307e4bb7ec01574a8f9e813bd5fc92a30a
tree22d38d5b811334ffab5a7c182864e8018d6e3f26tree
parent3153e2d94d1b12562557d60305bcac52d3128b83commit | diff
Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remove non-invertible operators. Add regression. (#1222)
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 [new file with mode: 0644] blob