projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 19054b3) | patch
Add internal support for integer and operator (#4668)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 30 Jun 2020 02:55:51 +0000 (21:55 -0500)
committerGitHub <noreply@github.com>
Tue, 30 Jun 2020 02:55:51 +0000 (19:55 -0700)
commit8c794ae1009bf8515b965c1023de188f50b35d60
tree7dcf7bed2aa581fb806c8b23efe77c33f6632754tree
parent19054b3b1d427e662d30d4322df2b2f2361353dacommit | diff
Add internal support for integer and operator (#4668)

Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
14 files changed:
src/CMakeLists.txt diff | blob | history
src/bindings/java/CMakeLists.txt diff | blob | history
src/cvc4.i diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history
src/util/CMakeLists.txt diff | blob | history
src/util/iand.h [new file with mode: 0644] blob
src/util/iand.i [new file with mode: 0644] blob