projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ebd9c95) | patch
Initial support for solving bit-vector inequalities (#1229)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Oct 2017 19:07:05 +0000 (14:07 -0500)
committerGitHub <noreply@github.com>
Thu, 12 Oct 2017 19:07:05 +0000 (14:07 -0500)
commit5031c6d9a08c84a6e8fe5019c6e278b8b2d7a238
tree9a1a61a9ccfcccbf9c977fc53b8a1394286be47ctree
parentebd9c958a0c20e37cc0e1a79be26afd525dd8fb9commit | diff
Initial support for solving bit-vector inequalities (#1229)

* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack.

* Clang format, remove heuristic.

* Update regressions.

* Simplify interface for CegInstantiator
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.h diff | blob | history
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-inequality2.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 [new file with mode: 0644] blob