projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ce4c31) | patch
Add solver for integer AND (#4681)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Jul 2020 19:54:41 +0000 (14:54 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Jul 2020 19:54:41 +0000 (14:54 -0500)
commite968ea45fd46ce6837d50b2893568872378171f1
tree1e9f4e720830562e4bbf77186ca90f85405aea9ctree
parent9ce4c3153d42bc079470b7bd73bf131499b3fcbecommit | diff
Add solver for integer AND (#4681)

This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.
src/CMakeLists.txt diff | blob | history
src/options/smt_options.toml diff | blob | history
src/theory/arith/nl/iand_solver.cpp [new file with mode: 0644] blob
src/theory/arith/nl/iand_solver.h [new file with mode: 0644] blob
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history