projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f51d3e3) | patch
Incremental support for bv_to_int (#4967)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 28 Aug 2020 21:42:51 +0000 (14:42 -0700)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 21:42:51 +0000 (16:42 -0500)
commit48dfcfd271ff9fa04766e29fb82ba83290da1ad8
treec187227cf376e9202c509a0fc05da500a427ac06tree
parentf51d3e353fe8e50e5e73c37c17229e603a56ecddcommit | diff
Incremental support for bv_to_int (#4967)

This PR adds support for incremental solving in bv_to_int.
This amounts to:

using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/preprocessing/passes/bv_to_int.h diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bvuf_to_intuf.smt2 [deleted file] blob | history
test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 [deleted file] blob | history
test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 [deleted file] blob | history
test/regress/regress2/bv_to_int_inc1.smt2 [new file with mode: 0644] blob