projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 859b55b) | patch
Refactor real2int (#1813)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Mon, 30 Apr 2018 20:33:21 +0000 (15:33 -0500)
committerGitHub <noreply@github.com>
Mon, 30 Apr 2018 20:33:21 +0000 (15:33 -0500)
commitd0e61e49bf51ca7d67188dd71b5f27cd45f6f2ff
tree0c5d181a17768cb1894036fcd16c8eaac8f7a5e4tree
parent859b55b3ba0d6aa43b71e05bdc83480313c107accommit | diff
Refactor real2int (#1813)

This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.
src/Makefile.am diff | blob | history
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/real_to_int.cpp [new file with mode: 0644] blob
src/preprocessing/passes/real_to_int.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress1/arith/real2int-test.smt2 [new file with mode: 0644] blob